spec/math/random/chacha8rand.bend

bend-collections-laws-crypto@1.0.0.0 · 243 lines · 32 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
4
5# Executable specification of ChaCha8Rand, transcribed from C2SP
6# chacha8rand (https://c2sp.org/chacha8rand, the generator of Go's
7# math/rand/v2.ChaCha8 and runtime) and, for the ChaCha block function, from
8# RFC 8439 sections 2.1-2.3 with eight rounds (Bernstein's ChaCha8). The
9# state is the RFC's list x[0..15] of 32-bit words, indexed as in the RFC;
10# nothing of the implementation is used except the neutral records W.U64{lo,
11# hi} (the little-endian reading of eight output bytes) and B.K (a key as
12# eight words, key_list).
13#
14#   quarter(x, a, b, c, d)   RFC 8439 2.1-2.2, on state indices
15#   double_round(x)          RFC 8439 2.3 inner_block: columns, then diagonals
16#   chacha8(key, ctr)        the ChaCha8 block: 4 double rounds, then the
17#                            input state added word by word (RFC 8439 2.3)
18#   c2sp_block(key, i)       C2SP: words 0..3 minus the constants, word 12
19#                            minus the block number i
20#   group(key, g)            C2SP's permutation of the four blocks g .. g + 3:
21#                            for each word position, the word of each block
22#   iteration(key)           the 1024 bytes (256 words) of one iteration
23#   output(key), next_key(key)  its first 992 bytes and last 32 bytes
24#   stream(n, key)           the first n 64-bit outputs of the generator
25#                            keyed by key (words read little-endian in pairs)
26#   key_of_seed(seed)        the eight little-endian words of a 32-byte seed
27#                            (Go's byteorder.LEUint32), None unless 32 bytes
28#                            below 256
29
30# the key record as the list of its eight little-endian words
31def key_list(k: B.Key) -> List<&2, U32>:
32  match k:
33    case B.K{k0, k1, k2, k3, k4, k5, k6, k7}:
34      [k0, k1, k2, k3, k4, k5, k6, k7]
35
36def get(xs: List<&2, U32>, i: Nat) -> U32:
37  match xs i:
38    case Nil{} _:
39      0
40    case Con{x, rest} 0n:
41      x
42    case Con{x, rest} 1n+p:
43      get(rest, p)
44
45def put(xs: List<&2, U32>, i: Nat, y: U32) -> List<&2, U32>:
46  match xs i:
47    case Nil{} _:
48      Nil{}
49    case Con{x, rest} 0n:
50      Con{y, rest}
51    case Con{x, rest} 1n+p:
52      Con{x, put(rest, p, y)}
53
54# x <<< n, 0 < n < 32
55def rotl(+x: U32, +n: Nat) -> U32:
56  U32.or(U32.shln(x, n), U32.shrn(x, Nat.sub(32n, n)))
57
58# RFC 8439 2.1: a += b; d ^= a; d <<<= 16; c += d; b ^= c; b <<<= 12;
59# a += b; d ^= a; d <<<= 8; c += d; b ^= c; b <<<= 7 (2.2: on x[a..d])
60def quarter(+x: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat) -> List<&2, U32>:
61  +a1 = U32.add(get(x, a), get(x, b))
62  +d1 = rotl(U32.xor(get(x, d), a1), 16n)
63  +c1 = U32.add(get(x, c), d1)
64  +b1 = rotl(U32.xor(get(x, b), c1), 12n)
65  +a2 = U32.add(a1, b1)
66  +d2 = rotl(U32.xor(d1, a2), 8n)
67  +c2 = U32.add(c1, d2)
68  +b2 = rotl(U32.xor(b1, c2), 7n)
69  put(put(put(put(x, a, a2), b, b2), c, c2), d, d2)
70
71# RFC 8439 2.3 inner_block (on the sixteen words of a state)
72def double_round(x: List<&2, U32>) -> List<&2, U32>:
73  match x:
74    case [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]:
75      y1 = quarter([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15], 0n, 4n, 8n, 12n)
76      y2 = quarter(y1, 1n, 5n, 9n, 13n)
77      y3 = quarter(y2, 2n, 6n, 10n, 14n)
78      y4 = quarter(y3, 3n, 7n, 11n, 15n)
79      y5 = quarter(y4, 0n, 5n, 10n, 15n)
80      y6 = quarter(y5, 1n, 6n, 11n, 12n)
81      y7 = quarter(y6, 2n, 7n, 8n, 13n)
82      quarter(y7, 3n, 4n, 9n, 14n)
83    case _:
84      x
85
86def double_rounds(n: Nat, x: List<&2, U32>) -> List<&2, U32>:
87  match n:
88    case 0n:
89      x
90    case 1n+p:
91      double_rounds(p, double_round(x))
92
93def append(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
94  match xs:
95    case Nil{}:
96      ys
97    case Con{x, rest}:
98      Con{x, append(rest, ys)}
99
100# RFC 8439 2.3: constants, key (eight words), block counter, nonce (here zero)
101def initial(key: List<&2, U32>, +ctr: U32) -> List<&2, U32>:
102  match key:
103    case [k0, k1, k2, k3, k4, k5, k6, k7]:
104      [1634760805, 857760878, 2036477234, 1797285236, k0, k1, k2, k3, k4, k5, k6, k7, ctr, 0, 0, 0]
105    case _:
106      []
107
108def add_words(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
109  match xs ys:
110    case Con{x, xt} Con{y, yt}:
111      Con{U32.add(x, y), add_words(xt, yt)}
112    case _ _:
113      Nil{}
114
115# the ChaCha8 block function: eight rounds, then the input added back
116def chacha8(+key: List<&2, U32>, +ctr: U32) -> List<&2, U32>:
117  add_words(double_rounds(4n, initial(key, ctr)), initial(key, ctr))
118
119def sub_at(+x: List<&2, U32>, +i: Nat, +c: U32) -> List<&2, U32>:
120  put(x, i, U32.sub(get(x, i), c))
121
122# C2SP: for each block, subtract the constants from words 0..3 and the block
123# counter from word 12
124def subtract(+b: List<&2, U32>, +i: U32) -> List<&2, U32>:
125  sub_at(sub_at(sub_at(sub_at(sub_at(b, 0n, 1634760805), 1n, 857760878), 2n, 2036477234), 3n, 1797285236), 12n, i)
126
127def c2sp_block(+key: List<&2, U32>, +i: U32) -> List<&2, U32>:
128  subtract(chacha8(key, i), i)
129
130# C2SP: "for each sequence of four blocks, first we output the first four
131# bytes of each block, then the next four bytes of each block, and so on"
132def interleave(k: Nat, +i: Nat, +b0: List<&2, U32>, +b1: List<&2, U32>, +b2: List<&2, U32>, +b3: List<&2, U32>) -> List<&2, U32>:
133  match k:
134    case 0n:
135      []
136    case 1n+p:
137      Con{get(b0, i), Con{get(b1, i), Con{get(b2, i), Con{get(b3, i), interleave(p, Nat.add(i, 1n), b0, b1, b2, b3)}}}}
138
139# the blocks g, g + 1, g + 2, g + 3, permuted
140def group(+key: List<&2, U32>, +g: U32) -> List<&2, U32>:
141  interleave(16n, 0n, c2sp_block(key, g), c2sp_block(key, U32.add(g, 1)), c2sp_block(key, U32.add(g, 2)), c2sp_block(key, U32.add(g, 3)))
142
143# one iteration: the sixteen blocks 0..15, permuted, as 256 words
144def iteration(+key: List<&2, U32>) -> List<&2, U32>:
145  append(group(key, 0), append(group(key, 4), append(group(key, 8), group(key, 12))))
146
147def take(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
148  match n xs:
149    case 0n _:
150      []
151    case 1n+p Nil{}:
152      []
153    case 1n+p Con{x, rest}:
154      Con{x, take(p, rest)}
155
156def drop(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
157  match n xs:
158    case 0n _:
159      xs
160    case 1n+p Nil{}:
161      []
162    case 1n+p Con{x, rest}:
163      drop(p, rest)
164
165# the first 992 bytes are output, the last 32 bytes key the next iteration
166def output(+key: List<&2, U32>) -> List<&2, U32>:
167  take(248n, iteration(key))
168
169def next_key(+key: List<&2, U32>) -> List<&2, U32>:
170  drop(248n, iteration(key))
171
172# consecutive little-endian word pairs as 64-bit words
173def words64(xs: List<&2, U32>) -> List<&2, W.U64>:
174  match xs:
175    case Con{lo, Con{hi, rest}}:
176      Con{W.U64{lo, hi}, words64(rest)}
177    case _:
178      []
179
180def head(xs: List<&2, W.U64>) -> W.U64:
181  match xs:
182    case Nil{}:
183      W.U64{0, 0}
184    case Con{x, rest}:
185      x
186
187def tail(xs: List<&2, W.U64>) -> List<&2, W.U64>:
188  match xs:
189    case Nil{}:
190      []
191    case Con{x, rest}:
192      rest
193
194# n outputs: the words left of the current iteration, then the next
195# iterations, each keyed by the last 32 bytes of the one before
196def stream_go(n: Nat, buf: List<&2, W.U64>, +key: List<&2, U32>) -> List<&2, W.U64>:
197  match n buf:
198    case 0n _:
199      []
200    case 1n+p Con{x, rest}:
201      Con{x, stream_go(p, rest, key)}
202    case 1n+p Nil{}:
203      Con{head(words64(output(key))), stream_go(p, tail(words64(output(key))), next_key(key))}
204
205# the first n 64-bit outputs of ChaCha8Rand keyed by key (eight words)
206def stream(n: Nat, +key: List<&2, U32>) -> List<&2, W.U64>:
207  stream_go(n, [], key)
208
209# Go's byteorder.LEUint32: b0 | b1 << 8 | b2 << 16 | b3 << 24
210def le32(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> U32:
211  U32.or(U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.shln(b2, 16n)), U32.shln(b3, 24n))
212
213def bytes_ok(bs: List<&2, U32>) -> Bool:
214  match bs:
215    case Nil{}:
216      True{}
217    case Con{+b, rest}:
218      Bool.and(U32.is_lt(b, 256), bytes_ok(rest))
219
220def words_of(bs: List<&2, U32>) -> List<&2, U32>:
221  match bs:
222    case Con{b0, Con{b1, Con{b2, Con{b3, rest}}}}:
223      Con{le32(b0, b1, b2, b3), words_of(rest)}
224    case _:
225      []
226
227def length(bs: List<&2, U32>) -> Nat:
228  match bs:
229    case Nil{}:
230      0n
231    case Con{b, rest}:
232      1n+length(rest)
233
234def key_if(+bs: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
235  match ok:
236    case True{}:
237      Some{words_of(bs)}
238    case False{}:
239      None{}
240
241# the key of a seed: 32 bytes, each below 256
242def key_of_seed(+seed: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
243  key_if(seed, Bool.and(bytes_ok(seed), Nat.is_eq(length(seed), 32n)))