spec/crypto/blake/blake2b.bend

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

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
3
4# BLAKE2b-512 (RFC 7693), unkeyed, as an executable specification.
5#
6# Written from the RFC; it never calls the implementation. It shares only the
7# record types of src/crypto/blake/blake2b/types.bend: a 64-bit word is a pair
8# of U32 halves T.W{lo, hi} (low half first), the working vector v[0..15] is
9# T.V{..}, the chaining value h[0..7] is T.H{..} and the 128-bit byte counter t
10# is four little-endian U32 limbs T.C{..}. The state is indexed with at/put and
11# the message schedule is read from the SIGMA table, as in the RFC's pseudocode.
12#
13# Input convention (shared with the public API): the message bytes are packed
14# little-endian, four per U32 word, in an Array<U32>; byte_length is the number
15# of message bytes. Bytes of the last block past byte_length are zero.
16
17# ---------------------------------------------------------------- 64-bit words
18
19# (a + b) mod 2^64: the low halves add modulo 2^32; the high halves add the
20# carry out of the low half, which is 1 exactly when the low sum wrapped.
21def add(a: T.Lane, b: T.Lane) -> T.Lane:
22  match a b:
23    case T.W{+al,ah} T.W{bl,bh}:
24      +lo = U32.add(al,bl)
25      T.W{lo,U32.add(U32.add(ah,bh),Bool.to_u32(U32.is_lt(lo,al)))}
26
27def xor(a: T.Lane, b: T.Lane) -> T.Lane:
28  match a b:
29    case T.W{al,ah} T.W{bl,bh}: T.W{U32.xor(al,bl),U32.xor(ah,bh)}
30
31# x >>> n for 0 < n < 32: each half takes its own bits shifted right and the
32# other half's low bits shifted in from the top.
33def rotr_small(+lo: U32, +hi: U32, +n: Nat) -> T.Lane:
34  T.W{U32.or(U32.shrn(lo,n),U32.shln(hi,Nat.sub(32n,n))),U32.or(U32.shrn(hi,n),U32.shln(lo,Nat.sub(32n,n)))}
35
36# n > 32 rotates the swapped halves by n - 32.
37def rotr_split(lo: U32, hi: U32, +n: Nat, small: Bool) -> T.Lane:
38  match small:
39    case True{}: rotr_small(lo,hi,n)
40    case False{}: rotr_small(hi,lo,Nat.sub(n,32n))
41
42# Right rotation of a 64-bit word by n (0 <= n < 64).
43def rotr(a: T.Lane, +n: Nat) -> T.Lane:
44  match a n:
45    case T.W{lo,hi} 0n: T.W{lo,hi}
46    case T.W{lo,hi} 32n: T.W{hi,lo}
47    case T.W{lo,hi} n: rotr_split(lo,hi,n,Nat.is_lt(n,32n))
48
49# ---------------------------------------------------------------- constants
50
51# RFC 7693 section 2.6: IV[i], the SHA-512 initial hash values.
52def iv(i: Nat) -> T.Lane:
53  match i:
54    case 0n: T.W{4089235720,1779033703}
55    case 1n: T.W{2227873595,3144134277}
56    case 2n: T.W{4271175723,1013904242}
57    case 3n: T.W{1595750129,2773480762}
58    case 4n: T.W{2917565137,1359893119}
59    case 5n: T.W{725511199,2600822924}
60    case 6n: T.W{4215389547,528734635}
61    case 7n: T.W{327033209,1541459225}
62    case _: T.W{0,0}
63
64# RFC 7693 section 2.7: the message word schedule SIGMA[r].
65def sigma(r: Nat) -> List<&2,Nat>:
66  match r:
67    case 0n: [0n,1n,2n,3n,4n,5n,6n,7n,8n,9n,10n,11n,12n,13n,14n,15n]
68    case 1n: [14n,10n,4n,8n,9n,15n,13n,6n,1n,12n,0n,2n,11n,7n,5n,3n]
69    case 2n: [11n,8n,12n,0n,5n,2n,15n,13n,10n,14n,3n,6n,7n,1n,9n,4n]
70    case 3n: [7n,9n,3n,1n,13n,12n,11n,14n,2n,6n,5n,10n,4n,0n,15n,8n]
71    case 4n: [9n,0n,5n,7n,2n,4n,10n,15n,14n,1n,11n,12n,6n,8n,3n,13n]
72    case 5n: [2n,12n,6n,10n,0n,11n,8n,3n,4n,13n,7n,5n,15n,14n,1n,9n]
73    case 6n: [12n,5n,1n,15n,14n,13n,4n,10n,0n,7n,6n,3n,9n,2n,8n,11n]
74    case 7n: [13n,11n,7n,14n,12n,1n,3n,9n,5n,0n,15n,4n,8n,6n,2n,10n]
75    case 8n: [6n,15n,14n,9n,11n,3n,0n,8n,12n,2n,13n,7n,1n,4n,10n,5n]
76    case 9n: [10n,2n,8n,4n,7n,6n,1n,5n,15n,11n,9n,14n,3n,12n,13n,0n]
77    case _: []
78
79def nth(-A: Data, xs: List<&2,A>, n: Nat, +zero: A) -> A:
80  match xs n:
81    case Nil{} _: zero
82    case x <> rest 0n: x
83    case x <> rest 1n+p: nth(A,rest,p,zero)
84
85# ---------------------------------------------------------------- the working vector
86
87def at(s: T.State, i: Nat) -> T.Lane:
88  match s i:
89    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 0n: v0
90    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 1n: v1
91    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 2n: v2
92    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 3n: v3
93    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 4n: v4
94    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 5n: v5
95    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 6n: v6
96    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 7n: v7
97    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 8n: v8
98    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 9n: v9
99    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 10n: v10
100    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 11n: v11
101    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 12n: v12
102    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 13n: v13
103    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 14n: v14
104    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 15n: v15
105    case _ _: T.W{0,0}
106
107def put(s: T.State, i: Nat, x: T.Lane) -> T.State:
108  match s i:
109    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 0n: T.V{x,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}
110    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 1n: T.V{v0,x,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}
111    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 2n: T.V{v0,v1,x,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}
112    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 3n: T.V{v0,v1,v2,x,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}
113    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 4n: T.V{v0,v1,v2,v3,x,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}
114    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 5n: T.V{v0,v1,v2,v3,v4,x,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}
115    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 6n: T.V{v0,v1,v2,v3,v4,v5,x,v7,v8,v9,v10,v11,v12,v13,v14,v15}
116    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 7n: T.V{v0,v1,v2,v3,v4,v5,v6,x,v8,v9,v10,v11,v12,v13,v14,v15}
117    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 8n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,x,v9,v10,v11,v12,v13,v14,v15}
118    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 9n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,x,v10,v11,v12,v13,v14,v15}
119    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 10n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,x,v11,v12,v13,v14,v15}
120    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 11n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,x,v12,v13,v14,v15}
121    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 12n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,x,v13,v14,v15}
122    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 13n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,x,v14,v15}
123    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 14n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,x,v15}
124    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 15n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,x}
125    case s _: s
126
127# ---------------------------------------------------------------- G, the round, F
128
129# RFC 7693 section 3.1, the mixing function G with R1..R4 = 32, 24, 16, 63:
130#   v[a] := (v[a] + v[b] + x) mod 2^64;  v[d] := (v[d] ^ v[a]) >>> R1
131#   v[c] := (v[c] + v[d])     mod 2^64;  v[b] := (v[b] ^ v[c]) >>> R2
132#   v[a] := (v[a] + v[b] + y) mod 2^64;  v[d] := (v[d] ^ v[a]) >>> R3
133#   v[c] := (v[c] + v[d])     mod 2^64;  v[b] := (v[b] ^ v[c]) >>> R4
134def mix(+s: T.State, +a: Nat, +b: Nat, +c: Nat, +d: Nat, x: T.Lane, y: T.Lane) -> T.State:
135  +a1 = add(add(at(s,a),at(s,b)),x)
136  +d1 = rotr(xor(at(s,d),a1),32n)
137  +c1 = add(at(s,c),d1)
138  +b1 = rotr(xor(at(s,b),c1),24n)
139  +a2 = add(add(a1,b1),y)
140  +d2 = rotr(xor(d1,a2),16n)
141  +c2 = add(c1,d2)
142  +b2 = rotr(xor(b1,c2),63n)
143  put(put(put(put(s,a,a2),b,b2),c,c2),d,d2)
144
145# G reads the vector's sixteen words and mixes the four at a, b, c, d.
146def G(v: T.State, +a: Nat, +b: Nat, +c: Nat, +d: Nat, x: T.Lane, y: T.Lane) -> T.State:
147  match v:
148    case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}:
149      mix(T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15},a,b,c,d,x,y)
150
151# m[s[j]]: the j-th message word of the round's schedule s.
152def word(+m: List<&2,T.Lane>, +s: List<&2,Nat>, +j: Nat) -> T.Lane:
153  nth(T.Lane,m,nth(Nat,s,j,0n),T.W{0,0})
154
155# RFC 7693 section 3.2, one round of F with schedule s = SIGMA[i mod 10].
156def round(v: T.State, +m: List<&2,T.Lane>, +s: List<&2,Nat>) -> T.State:
157  v = G(v,0n,4n,8n,12n,word(m,s,0n),word(m,s,1n))
158  v = G(v,1n,5n,9n,13n,word(m,s,2n),word(m,s,3n))
159  v = G(v,2n,6n,10n,14n,word(m,s,4n),word(m,s,5n))
160  v = G(v,3n,7n,11n,15n,word(m,s,6n),word(m,s,7n))
161  v = G(v,0n,5n,10n,15n,word(m,s,8n),word(m,s,9n))
162  v = G(v,1n,6n,11n,12n,word(m,s,10n),word(m,s,11n))
163  v = G(v,2n,7n,8n,13n,word(m,s,12n),word(m,s,13n))
164  G(v,3n,4n,9n,14n,word(m,s,14n),word(m,s,15n))
165
166# Rounds i, i+1, .., i+n-1.
167def rounds(n: Nat, +i: Nat, v: T.State, +m: List<&2,T.Lane>) -> T.State:
168  match n:
169    case 0n: v
170    case 1n+p: rounds(p,1n+i,round(v,m,sigma(Nat.mod(i,10n))),m)
171
172def invert_if(last: Bool, x: T.Lane) -> T.Lane:
173  match last:
174    case True{}: xor(x,T.W{4294967295,4294967295})
175    case False{}: x
176
177# v[0..7] := h[0..7]; v[8..15] := IV[0..7]; v[12] ^= t mod 2^64;
178# v[13] ^= t >> 64; if last block, v[14] := ~v[14].
179def start(h: T.Chain, t: T.Counter, last: Bool) -> T.State:
180  match h t:
181    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.C{t0,t1,t2,t3}:
182      T.V{h0,h1,h2,h3,h4,h5,h6,h7,iv(0n),iv(1n),iv(2n),iv(3n),xor(iv(4n),T.W{t0,t1}),xor(iv(5n),T.W{t2,t3}),invert_if(last,iv(6n)),iv(7n)}
183
184# h[i] := h[i] ^ v[i] ^ v[i + 8].
185def finish(h: T.Chain, v: T.State) -> T.Chain:
186  match h v:
187    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}:
188      T.H{xor(xor(h0,v0),v8),xor(xor(h1,v1),v9),xor(xor(h2,v2),v10),xor(xor(h3,v3),v11),xor(xor(h4,v4),v12),xor(xor(h5,v5),v13),xor(xor(h6,v6),v14),xor(xor(h7,v7),v15)}
189
190# RFC 7693 section 3.2: F(h, m, t, f) with twelve rounds.
191def compress(+h: T.Chain, +m: List<&2,T.Lane>, t: T.Counter, last: Bool) -> T.Chain:
192  finish(h,rounds(12n,0n,start(h,t,last),m))
193
194# ---------------------------------------------------------------- message blocks
195
196# t := t + x on the 128-bit counter, carrying from limb to limb.
197def advance(c: T.Counter, +x: U32) -> T.Counter:
198  match c:
199    case T.C{c0,c1,c2,c3}:
200      +s0 = U32.add(c0,x)
201      +k0 = Bool.to_u32(U32.is_lt(s0,x))
202      +s1 = U32.add(c1,k0)
203      +k1 = Bool.to_u32(U32.is_lt(s1,k0))
204      +s2 = U32.add(c2,k1)
205      T.C{s0,s1,s2,U32.add(c3,Bool.to_u32(U32.is_lt(s2,k1)))}
206
207# The low n bytes of a little-endian word (all four when n >= 4).
208def keep(w: U32, n: Nat) -> U32:
209  match n:
210    case 0n: 0
211    case 1n: U32.and(w,255)
212    case 2n: U32.and(w,65535)
213    case 3n: U32.and(w,16777215)
214    case _: w
215
216# The word holding block bytes pos..pos+3 when only `remain` bytes are message:
217# the bytes at or past `remain` are zero padding.
218def mask(w: U32, +pos: Nat, +remain: Nat) -> U32:
219  keep(w,Nat.sub(remain,pos))
220
221def trim(ws: List<&2,U32>, +pos: Nat, +remain: Nat) -> List<&2,U32>:
222  match ws:
223    case Nil{}: Nil{}
224    case w <> rest: mask(w,pos,remain) <> trim(rest,Nat.add(pos,4n),remain)
225
226def prepare(last: Bool, ws: List<&2,U32>, remain: Nat) -> List<&2,U32>:
227  match last:
228    case False{}: ws
229    case True{}: trim(ws,0n,remain)
230
231# m[i] = the little-endian 64-bit word of block bytes 8i..8i+7.
232def lanes(ws: List<&2,U32>) -> List<&2,T.Lane>:
233  match ws:
234    case lo <> hi <> rest: T.W{lo,hi} <> lanes(rest)
235    case _: Nil{}
236
237# Reads the block's 32 words base+0 .. base+31 from the array, then compresses.
238def gather(n: Nat, +base: U32, +next: U32, +last: Bool, +remain: Nat, t: T.Counter, h: T.Chain, acc: List<&2,U32>, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
239  match n pair:
240    case 0n Tuple{a,w}:
241      (a,compress(h,lanes(prepare(last,List.reverse(&2,U32,w <> acc),remain)),t,last))
242    case 1n+p Tuple{a,w}:
243      gather(p,base,U32.inc(next),last,remain,t,h,w <> acc,Array.get(U32,a,U32.add(base,next)))
244
245# A block that is not the last: t already counts its 128 bytes.
246def absorb(a: Array<U32>, +index: U32, t: T.Counter, h: T.Chain) -> Array<U32> & T.Chain:
247  gather(31n,index,1,False{},0n,t,h,Nil{},Array.get(U32,a,index))
248
249# The last block: remain message bytes (1..128; 0 for the empty message), t := t + remain.
250def final(a: Array<U32>, +index: U32, +remain: Nat, t: T.Counter, h: T.Chain) -> T.Chain:
251  Pair.snd(Array<U32>,T.Chain,gather(31n,index,1,True{},remain,advance(t,U32.from_nat(remain)),h,Nil{},Array.get(U32,a,index)))
252
253# n blocks that are not the last, then the last one.
254def blocks(n: Nat, +index: U32, +remain: Nat, t: T.Counter, pair: Array<U32> & T.Chain) -> T.Chain:
255  match n pair:
256    case 0n Tuple{a,h}: final(a,index,remain,t,h)
257    case 1n+p Tuple{a,h}:
258      +t2 = advance(t,128)
259      blocks(p,U32.add(index,32),remain,t2,absorb(a,index,t2,h))
260
261# h[0..7] := IV[0..7]; h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0, nn = 64.
262def initial() -> T.Chain:
263  T.H{xor(iv(0n),T.W{16842816,0}),iv(1n),iv(2n),iv(3n),iv(4n),iv(5n),iv(6n),iv(7n)}
264
265# dd = max(1, ceil(ll / 128)) blocks: dd - 1 = (ll - 1) div 128 full blocks
266# (0 when ll = 0), then the last block with the remaining ll - 128 (dd - 1) bytes.
267def unchecked(a: Array<U32>, +length: Nat) -> T.Chain:
268  +n = Nat.div(Nat.sub(length,1n),128n)
269  blocks(n,0,Nat.sub(length,Nat.mul(n,128n)),T.C{0,0,0,0},(a,initial()))
270
271# The 64-byte digest h[0..7] as sixteen little-endian words.
272def digest(h: T.Chain) -> Array<U32>:
273  match h:
274    case T.H{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7}}:
275      ANode{ANode{ANode{ANode{ALeaf{l0},ALeaf{u0}},ANode{ALeaf{l1},ALeaf{u1}}},ANode{ANode{ALeaf{l2},ALeaf{u2}},ANode{ALeaf{l3},ALeaf{u3}}}},ANode{ANode{ANode{ALeaf{l4},ALeaf{u4}},ANode{ALeaf{l5},ALeaf{u5}}},ANode{ANode{ALeaf{l6},ALeaf{u6}},ANode{ALeaf{l7},ALeaf{u7}}}}}
276
277def checked(valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
278  match valid:
279    case False{}: None{}
280    case True{}: Some{digest(unchecked(a,length))}
281
282def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
283  (a,capacity) = pair
284  checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
285
286# BLAKE2b-512 of the first byte_length bytes of the packed words; None when
287# byte_length exceeds the array's 4 * capacity bytes.
288def blake2b(words: Array<U32>, byte_length: Nat) -> Maybe<&1,Array<U32>>:
289  sized(byte_length,Array.size(U32,words))