spec/crypto/blake/blake2s.bend

bend-collections-laws-crypto@1.0.0.0 · 231 lines · 35 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend as T
3
4# Executable specification of unkeyed BLAKE2s-256, written from RFC 7693.
5# Only the neutral chaining-value record T.State is shared with the
6# implementation; no implementation function is called. The work vector,
7# the message block and SIGMA are lists indexed as in the RFC, and the message
8# is handled byte by byte: the packed input is read as little-endian bytes,
9# the final block is zero-padded byte-wise, and block words are reassembled
10# from bytes (RFC 7693 section 2.4, "little-endian byte order").
11
12# ---------------------------------------------------------------- 2.6 constants
13
14# IV[0..7] = 0x6A09E667 0xBB67AE85 0x3C6EF372 0xA54FF53A
15#            0x510E527F 0x9B05688C 0x1F83D9AB 0x5BE0CD19
16def iv() -> List<&2,U32>:
17  [1779033703, 3144134277, 1013904242, 2773480762, 1359893119, 2600822924, 528734635, 1541459225]
18
19# SIGMA[i mod 10].
20def sigma(r: Nat) -> List<&2,Nat>:
21  match r:
22    case 0n: [0n, 1n, 2n, 3n, 4n, 5n, 6n, 7n, 8n, 9n, 10n, 11n, 12n, 13n, 14n, 15n]
23    case 1n: [14n, 10n, 4n, 8n, 9n, 15n, 13n, 6n, 1n, 12n, 0n, 2n, 11n, 7n, 5n, 3n]
24    case 2n: [11n, 8n, 12n, 0n, 5n, 2n, 15n, 13n, 10n, 14n, 3n, 6n, 7n, 1n, 9n, 4n]
25    case 3n: [7n, 9n, 3n, 1n, 13n, 12n, 11n, 14n, 2n, 6n, 5n, 10n, 4n, 0n, 15n, 8n]
26    case 4n: [9n, 0n, 5n, 7n, 2n, 4n, 10n, 15n, 14n, 1n, 11n, 12n, 6n, 8n, 3n, 13n]
27    case 5n: [2n, 12n, 6n, 10n, 0n, 11n, 8n, 3n, 4n, 13n, 7n, 5n, 15n, 14n, 1n, 9n]
28    case 6n: [12n, 5n, 1n, 15n, 14n, 13n, 4n, 10n, 0n, 7n, 6n, 3n, 9n, 2n, 8n, 11n]
29    case 7n: [13n, 11n, 7n, 14n, 12n, 1n, 3n, 9n, 5n, 0n, 15n, 4n, 8n, 6n, 2n, 10n]
30    case 8n: [6n, 15n, 14n, 9n, 11n, 3n, 0n, 8n, 12n, 2n, 13n, 7n, 1n, 4n, 10n, 5n]
31    case 9n: [10n, 2n, 8n, 4n, 7n, 6n, 1n, 5n, 15n, 11n, 9n, 14n, 3n, 12n, 13n, 0n]
32    case 10n+p: sigma(p)
33
34# ---------------------------------------------------------------- list indexing
35
36def get(xs: List<&2,U32>, i: Nat) -> U32:
37  match xs i:
38    case Nil{} _: 0
39    case x <> rest 0n: x
40    case x <> rest 1n+p: get(rest, p)
41
42def index(xs: List<&2,Nat>, i: Nat) -> Nat:
43  match xs i:
44    case Nil{} _: 0n
45    case x <> rest 0n: x
46    case x <> rest 1n+p: index(rest, p)
47
48def put(xs: List<&2,U32>, i: Nat, y: U32) -> List<&2,U32>:
49  match xs i:
50    case Nil{} _: Nil{}
51    case x <> rest 0n: y <> rest
52    case x <> rest 1n+p: x <> put(rest, p, y)
53
54# ---------------------------------------------------------------- 3.1 G
55
56# x >>> n: rotation of a 32-bit word right by n bits (0 < n < 32).
57def rotr(+x: U32, +n: Nat) -> U32:
58  U32.or(U32.shrn(x, n), U32.shln(x, Nat.sub(32n, n)))
59
60# G(v[0..15], a, b, c, d, x, y) with BLAKE2s rotations R1..R4 = 16, 12, 8, 7.
61def mix(+v: List<&2,U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, x: U32, y: U32) -> List<&2,U32>:
62  +va = U32.add(U32.add(get(v, a), get(v, b)), x)
63  +vd = rotr(U32.xor(get(v, d), va), 16n)
64  +vc = U32.add(get(v, c), vd)
65  +vb = rotr(U32.xor(get(v, b), vc), 12n)
66  +va2 = U32.add(U32.add(va, vb), y)
67  +vd2 = rotr(U32.xor(vd, va2), 8n)
68  +vc2 = U32.add(vc, vd2)
69  +vb2 = rotr(U32.xor(vb, vc2), 7n)
70  put(put(put(put(v, a, va2), b, vb2), c, vc2), d, vd2)
71
72# ---------------------------------------------------------------- 3.2 F
73
74# One round with schedule s: four column steps, then four diagonal steps.
75def round(v: List<&2,U32>, +s: List<&2,Nat>, +m: List<&2,U32>) -> List<&2,U32>:
76  v1 = mix(v, 0n, 4n, 8n, 12n, get(m, index(s, 0n)), get(m, index(s, 1n)))
77  v2 = mix(v1, 1n, 5n, 9n, 13n, get(m, index(s, 2n)), get(m, index(s, 3n)))
78  v3 = mix(v2, 2n, 6n, 10n, 14n, get(m, index(s, 4n)), get(m, index(s, 5n)))
79  v4 = mix(v3, 3n, 7n, 11n, 15n, get(m, index(s, 6n)), get(m, index(s, 7n)))
80  v5 = mix(v4, 0n, 5n, 10n, 15n, get(m, index(s, 8n)), get(m, index(s, 9n)))
81  v6 = mix(v5, 1n, 6n, 11n, 12n, get(m, index(s, 10n)), get(m, index(s, 11n)))
82  v7 = mix(v6, 2n, 7n, 8n, 13n, get(m, index(s, 12n)), get(m, index(s, 13n)))
83  mix(v7, 3n, 4n, 9n, 14n, get(m, index(s, 14n)), get(m, index(s, 15n)))
84
85# Rounds i, i+1, ..., i+n-1.
86def rounds(n: Nat, +i: Nat, v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>:
87  match n:
88    case 0n: v
89    case 1n+p: rounds(p, 1n+i, round(v, sigma(i), m), m)
90
91def invert(last: Bool, +v: List<&2,U32>) -> List<&2,U32>:
92  match last:
93    case True{}: put(v, 14n, U32.xor(get(v, 14n), 4294967295))
94    case False{}: v
95
96# F(h, m, t, f) with r rounds (r = 10 for BLAKE2s): t = t0 + 2^32 * t1 is the
97# byte counter, f the final-block flag.
98def compress(+r: Nat, h: T.State, +m: List<&2,U32>, +t0: U32, +t1: U32, last: Bool) -> T.State:
99  match h:
100    case T.H{+h0, +h1, +h2, +h3, +h4, +h5, +h6, +h7}:
101      +v0 = List.append(&2, U32, [h0, h1, h2, h3, h4, h5, h6, h7], iv())
102      +v1 = put(v0, 12n, U32.xor(get(v0, 12n), t0))
103      +v2 = put(v1, 13n, U32.xor(get(v1, 13n), t1))
104      +v = rounds(r, 0n, invert(last, v2), m)
105      T.H{U32.xor(U32.xor(h0, get(v, 0n)), get(v, 8n)),
106          U32.xor(U32.xor(h1, get(v, 1n)), get(v, 9n)),
107          U32.xor(U32.xor(h2, get(v, 2n)), get(v, 10n)),
108          U32.xor(U32.xor(h3, get(v, 3n)), get(v, 11n)),
109          U32.xor(U32.xor(h4, get(v, 4n)), get(v, 12n)),
110          U32.xor(U32.xor(h5, get(v, 5n)), get(v, 13n)),
111          U32.xor(U32.xor(h6, get(v, 6n)), get(v, 14n)),
112          U32.xor(U32.xor(h7, get(v, 7n)), get(v, 15n))}
113
114# ---------------------------------------------------------------- 2.4 bytes
115
116# Byte k (0 = least significant) of a word: the packed input holds four
117# message bytes per word in little-endian order.
118def byte(+w: U32, k: Nat) -> U32:
119  U32.and(255, U32.shrn(w, Nat.mul(8n, k)))
120
121def octets(+w: U32) -> List<&2,U32>:
122  [byte(w, 0n), byte(w, 1n), byte(w, 2n), byte(w, 3n)]
123
124def serialize(ws: List<&2,U32>) -> List<&2,U32>:
125  match ws:
126    case Nil{}: Nil{}
127    case w <> rest: List.append(&2, U32, octets(w), serialize(rest))
128
129# Zero padding: the byte at message offset i survives only when i < length.
130def keep_if(inside: Bool, b: U32) -> U32:
131  match inside:
132    case True{}: b
133    case False{}: 0
134
135def pad(bytes: List<&2,U32>, +i: Nat, +length: Nat) -> List<&2,U32>:
136  match bytes:
137    case Nil{}: Nil{}
138    case b <> rest: keep_if(Nat.is_lt(i, length), b) <> pad(rest, 1n+i, length)
139
140# A block word from four bytes, least significant first.
141def word(b0: U32, b1: U32, b2: U32, b3: U32) -> U32:
142  U32.or(U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.shln(b2, 16n)), U32.shln(b3, 24n))
143
144def words(bytes: List<&2,U32>) -> List<&2,U32>:
145  match bytes:
146    case b0 <> b1 <> b2 <> b3 <> rest: word(b0, b1, b2, b3) <> words(rest)
147    case _: Nil{}
148
149# ---------------------------------------------------------------- 3.3 BLAKE2s
150
151# The byte counter t as two 32-bit halves: t + n, with the carry into t1.
152def carry(c: Bool, hi: U32) -> U32:
153  match c:
154    case True{}: U32.add(hi, 1)
155    case False{}: hi
156
157def count_hi(+lo: U32, hi: U32, +n: U32) -> U32:
158  carry(U32.is_lt(U32.add(lo, n), n), hi)
159
160# Read the sixteen words of the block at word offset base, in order.
161def gather(n: Nat, +base: U32, +next: U32, acc: List<&2,U32>, pair: Array<U32> & U32) -> Array<U32> & List<&2,U32>:
162  match n pair:
163    case 0n Tuple{a, w}: (a, List.reverse(&2, U32, w <> acc))
164    case 1n+p Tuple{a, w}: gather(p, base, U32.inc(next), w <> acc, Array.get(U32, a, U32.add(base, next)))
165
166def read_block(a: Array<U32>, +base: U32) -> Array<U32> & List<&2,U32>:
167  gather(15n, base, 1, [], Array.get(U32, a, base))
168
169# A block before the last: all 64 bytes are message bytes.
170def full_block(+r: Nat, pair: Array<U32> & List<&2,U32>, h: T.State, +t0: U32, +t1: U32) -> Array<U32> & T.State:
171  (a, ws) = pair
172  (a, compress(r, h, words(serialize(ws)), t0, t1, False{}))
173
174# The last block: the remaining bytes, zero-padded to 64.
175def last_block(+r: Nat, pair: Array<U32> & List<&2,U32>, +remain: Nat, h: T.State, +t0: U32, +t1: U32) -> T.State:
176  (a, ws) = pair
177  compress(r, h, words(pad(serialize(ws), 0n, remain)), t0, t1, True{})
178
179def absorb(+r: Nat, a: Array<U32>, +base: U32, h: T.State, +t0: U32, +t1: U32) -> Array<U32> & T.State:
180  full_block(r, read_block(a, base), h, t0, t1)
181
182def finish(+r: Nat, a: Array<U32>, +base: U32, +t0: U32, t1: U32, +remain: Nat, h: T.State) -> T.State:
183  +n = U32.from_nat(remain)
184  last_block(r, read_block(a, base), remain, h, U32.add(t0, n), count_hi(t0, t1, n))
185
186# n full blocks, then the last one; t counts the bytes compressed so far.
187def blocks(+r: Nat, n: Nat, +base: U32, +t0: U32, t1: U32, +remain: Nat, pair: Array<U32> & T.State) -> T.State:
188  match n pair:
189    case 0n Tuple{a, h}: finish(r, a, base, t0, t1, remain, h)
190    case 1n+p Tuple{a, h}:
191      +c0 = U32.add(t0, 64)
192      +c1 = count_hi(t0, t1, 64)
193      blocks(r, p, U32.add(base, 16), c0, c1, remain, absorb(r, a, base, h, c0, c1))
194
195# h[0..7] := IV[0..7]; h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0, nn = 32.
196def initial() -> T.State:
197  T.H{U32.xor(1779033703, U32.xor(16842752, 32)), 3144134277, 1013904242, 2773480762, 1359893119, 2600822924, 528734635, 1541459225}
198
199# dd = ceil(ll / 64) blocks, and dd = 1 for the empty message.
200def block_count(+ll: Nat) -> Nat:
201  match ll:
202    case 0n: 1n
203    case 1n+p: Nat.div(Nat.add(ll, 63n), 64n)
204
205def hash(+r: Nat, a: Array<U32>, +ll: Nat) -> T.State:
206  +n = Nat.sub(block_count(ll), 1n)
207  blocks(r, n, 0, 0, 0, Nat.sub(ll, Nat.mul(64n, n)), (a, initial()))
208
209# The 32-byte digest as eight little-endian words, in a fresh 8-slot array.
210def digest(h: T.State) -> Array<U32>:
211  match h:
212    case T.H{h0, h1, h2, h3, h4, h5, h6, h7}:
213      ANode{ANode{ANode{ALeaf{h0}, ALeaf{h1}}, ANode{ALeaf{h2}, ALeaf{h3}}}, ANode{ANode{ALeaf{h4}, ALeaf{h5}}, ANode{ALeaf{h6}, ALeaf{h7}}}}
214
215def checked(+r: Nat, valid: Bool, a: Array<U32>, ll: Nat) -> Maybe<&1,Array<U32>>:
216  match valid:
217    case False{}: None{}
218    case True{}: Some{digest(hash(r, a, ll))}
219
220def sized(+r: Nat, +ll: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
221  (a, capacity) = pair
222  checked(r, Nat.is_le(ll, Nat.mul(4n, U32.to_nat(capacity))), a, ll)
223
224# The hash with r rounds per compression, of the first ll bytes of the packed
225# array a; None when ll exceeds the 4 * capacity bytes the array holds.
226def blake2s_rounds(+r: Nat, a: Array<U32>, ll: Nat) -> Maybe<&1,Array<U32>>:
227  sized(r, ll, Array.size(U32, a))
228
229# BLAKE2s-256: r = 10.
230def blake2s(a: Array<U32>, ll: Nat) -> Maybe<&1,Array<U32>>:
231  blake2s_rounds(10n, a, ll)