spec/crypto/blake/blake3.bend

bend-collections-laws-crypto@1.0.0.0 · 288 lines · 45 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
4
5# BLAKE3 in hash mode with a 32-byte output, written from the BLAKE3
6# specification document (O'Connor, Aumasson, Neves, Wilcox-O'Hearn, 2020):
7# section 2.2 (the compression function), 2.3 (modes: hash mode keys with IV),
8# 2.4 (chunks), 2.5 (the tree) and 2.6 (the root and its output).
9#
10# This file is independent of the implementation in src/crypto/blake/blake3/:
11# it shares only the plain record types CV, Block and Out and never calls the
12# implementation. It favours the document's structure over speed: the state
13# and the message are lists indexed by position, the message schedule comes
14# from repeatedly applying the permutation table, and the tree is defined
15# recursively by its shape rather than by the implementation's stack.
16#
17# Input convention: the message is an array of U32 words holding its bytes
18# little-endian, four per word (byte 4i+j is bits 8j..8j+7 of word i);
19# byte_length is the logical length. A 64-byte block is therefore sixteen
20# consecutive words, and a block of len < 64 bytes is zero past its len bytes.
21
22# ---- constants (2.2, 2.3) ----
23
24def iv() -> List<&2,U32>:
25  [1779033703,3144134277,1013904242,2773480762,1359893119,2600822924,528734635,1541459225]
26
27def msg_permutation() -> List<&2,Nat>:
28  [2n,6n,3n,10n,7n,0n,4n,13n,1n,11n,12n,5n,9n,14n,15n,8n]
29
30def chunk_start() -> U32:
31  1
32
33def chunk_end() -> U32:
34  2
35
36def parent_flag() -> U32:
37  4
38
39def root_flag() -> U32:
40  8
41
42# ---- word lists ----
43
44def at(xs: List<&2,U32>, i: Nat) -> U32:
45  match xs i:
46    case Nil{} _: 0
47    case Con{x,r} 0n: x
48    case Con{x,r} 1n+j: at(r,j)
49
50def put(xs: List<&2,U32>, i: Nat, +v: U32) -> List<&2,U32>:
51  match xs i:
52    case Nil{} _: Nil{}
53    case Con{x,r} 0n: Con{v,r}
54    case Con{x,r} 1n+j: Con{x,put(r,j,v)}
55
56def cv_words(c: T.CV) -> List<&2,U32>:
57  match c:
58    case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}: [h0,h1,h2,h3,h4,h5,h6,h7]
59
60# (Each list consumer below starts by matching its list, so that it stays an
61# unevaluated call on a symbolic list; the Nil cases agree with the general
62# formula, since at(Nil, i) = 0 and put(Nil, i, x) = Nil.)
63def cv_of(+ws: List<&2,U32>) -> T.CV:
64  match ws:
65    case Nil{}: T.CV{0,0,0,0,0,0,0,0}
66    case Con{+x,+r}:
67      +l = {Con{x,r} : List<&2,U32>}
68      T.CV{at(l,0n),at(l,1n),at(l,2n),at(l,3n),at(l,4n),at(l,5n),at(l,6n),at(l,7n)}
69
70def block_of(+ws: List<&2,U32>) -> T.Block:
71  match ws:
72    case Nil{}: T.B{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
73    case Con{+x,+r}:
74      +l = {Con{x,r} : List<&2,U32>}
75      T.B{at(l,0n),at(l,1n),at(l,2n),at(l,3n),at(l,4n),at(l,5n),at(l,6n),at(l,7n),at(l,8n),at(l,9n),at(l,10n),at(l,11n),at(l,12n),at(l,13n),at(l,14n),at(l,15n)}
76
77# ---- the compression function (2.2) ----
78
79# Right rotation by n bits, 0 < n < 32.
80def rotr(+x: U32, +n: Nat) -> U32:
81  U32.or(U32.shrn(x,n),U32.shln(x,Nat.sub(32n,n)))
82
83# The quarter-round G on state positions a, b, c, d with message words mx, my.
84def g(+v: List<&2,U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +mx: U32, +my: U32) -> List<&2,U32>:
85  +va = U32.add(U32.add(at(v,a),at(v,b)),mx)
86  +vd = rotr(U32.xor(at(v,d),va),16n)
87  +vc = U32.add(at(v,c),vd)
88  +vb = rotr(U32.xor(at(v,b),vc),12n)
89  +va2 = U32.add(U32.add(va,vb),my)
90  +vd2 = rotr(U32.xor(vd,va2),8n)
91  +vc2 = U32.add(vc,vd2)
92  +vb2 = rotr(U32.xor(vb,vc2),7n)
93  put(put(put(put(v,a,va2),b,vb2),c,vc2),d,vd2)
94
95# A round mixes the columns, then the diagonals, of the 4x4 state.
96def columns(+v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>:
97  +v1 = g(v,0n,4n,8n,12n,at(m,0n),at(m,1n))
98  +v2 = g(v1,1n,5n,9n,13n,at(m,2n),at(m,3n))
99  +v3 = g(v2,2n,6n,10n,14n,at(m,4n),at(m,5n))
100  g(v3,3n,7n,11n,15n,at(m,6n),at(m,7n))
101
102def diagonals(+v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>:
103  +v1 = g(v,0n,5n,10n,15n,at(m,8n),at(m,9n))
104  +v2 = g(v1,1n,6n,11n,12n,at(m,10n),at(m,11n))
105  +v3 = g(v2,2n,7n,8n,13n,at(m,12n),at(m,13n))
106  g(v3,3n,4n,9n,14n,at(m,14n),at(m,15n))
107
108def round(v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>:
109  match v:
110    case Nil{}: Nil{}
111    case Con{+x,+r}: diagonals(columns(Con{x,r},m),m)
112
113# The message words are permuted between rounds: word i of the next round is
114# word msg_permutation[i] of this one.
115def permute_go(ps: List<&2,Nat>, +m: List<&2,U32>) -> List<&2,U32>:
116  match ps:
117    case Nil{}: Nil{}
118    case Con{p,r}: Con{at(m,p),permute_go(r,m)}
119
120def permute(+m: List<&2,U32>) -> List<&2,U32>:
121  permute_go(msg_permutation(),m)
122
123def rounds(n: Nat, +v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>:
124  match n:
125    case 0n: v
126    case 1n+k: rounds(k,round(v,m),permute(m))
127
128# The initial state of compress(h, m, t, len, flags): h[0..7], IV[0..3], the
129# counter t (low word, then the high word, always 0 here: an input has fewer
130# than 2^32 chunks), the block length and the flags.
131def init(c: T.CV, +t: U32, +len: U32, +flags: U32) -> List<&2,U32>:
132  SC.append(U32,cv_words(c),[at(iv(),0n),at(iv(),1n),at(iv(),2n),at(iv(),3n),t,0,len,flags])
133
134# The new chaining value: word i xor word i+8 of the final state (the 64-byte
135# extended output is not needed for a 32-byte digest).
136def output(+v: List<&2,U32>) -> T.CV:
137  T.CV{U32.xor(at(v,0n),at(v,8n)),U32.xor(at(v,1n),at(v,9n)),U32.xor(at(v,2n),at(v,10n)),U32.xor(at(v,3n),at(v,11n)),U32.xor(at(v,4n),at(v,12n)),U32.xor(at(v,5n),at(v,13n)),U32.xor(at(v,6n),at(v,14n)),U32.xor(at(v,7n),at(v,15n))}
138
139# Seven rounds over the block's words.
140def compress(c: T.CV, b: T.Block, +t: U32, +len: U32, +flags: U32) -> T.CV:
141  match b:
142    case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}:
143      output(rounds(7n,init(c,t,len,flags),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]))
144
145# ---- reading blocks ----
146
147# The sixteen words of the block at word `index`, in order.
148def gather(n: Nat, +base: U32, +next: U32, acc: List<&2,U32>, pair: Array<U32> & U32) -> Array<U32> & List<&2,U32>:
149  match n pair:
150    case 0n Tuple{a,w}: (a,List.reverse(&2,U32,Con{w,acc}))
151    case 1n+p Tuple{a,w}: gather(p,base,U32.inc(next),Con{w,acc},Array.get(U32,a,U32.add(base,next)))
152
153def as_block(pair: Array<U32> & List<&2,U32>) -> Array<U32> & T.Block:
154  (a,ws) = pair
155  (a,block_of(ws))
156
157def read_block(a: Array<U32>, +index: U32) -> Array<U32> & T.Block:
158  as_block(gather(15n,index,1,Nil{},Array.get(U32,a,index)))
159
160# A block holding len bytes (len <= 64) is zero past them: the word at byte
161# offset pos keeps its min(4, len - pos) low bytes.
162def low_bytes(w: U32, k: Nat) -> U32:
163  match k:
164    case 0n: 0
165    case 1n: U32.and(w,255)
166    case 2n: U32.and(w,65535)
167    case 3n: U32.and(w,16777215)
168    case 4n+q: w
169
170def keep(w: U32, +pos: Nat, +len: Nat) -> U32:
171  low_bytes(w,Nat.min(4n,Nat.sub(len,pos)))
172
173def zero_tail(b: T.Block, +len: Nat) -> T.Block:
174  match b:
175    case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}:
176      T.B{keep(m0,0n,len),keep(m1,4n,len),keep(m2,8n,len),keep(m3,12n,len),keep(m4,16n,len),keep(m5,20n,len),keep(m6,24n,len),keep(m7,28n,len),keep(m8,32n,len),keep(m9,36n,len),keep(m10,40n,len),keep(m11,44n,len),keep(m12,48n,len),keep(m13,52n,len),keep(m14,56n,len),keep(m15,60n,len)}
177
178# ---- chunks (2.4) ----
179
180# The blocks of a chunk are compressed in order starting from the key (IV in
181# hash mode), all with the chunk counter t; the first block carries
182# CHUNK_START and the last CHUNK_END. The last block is not compressed here:
183# it is the chunk's output node (2.5, 2.6 decide its flags and use).
184# n blocks follow the current block (in pair); the last block has len bytes.
185def chunk_blocks(n: Nat, +t: U32, +index: U32, +flags: U32, +len: Nat, cv: T.CV, pair: Array<U32> & T.Block) -> Array<U32> & T.Out:
186  match n pair:
187    case 0n Tuple{a,b}: (a,T.Out{cv,zero_tail(b,len),t,U32.from_nat(len),U32.or(flags,chunk_end())})
188    case 1n+p Tuple{a,b}: chunk_blocks(p,t,U32.add(index,16),0,len,compress(cv,zero_tail(b,64n),t,64,flags),read_block(a,U32.add(index,16)))
189
190# A chunk of len bytes (1..1024; 0 only for the empty message) at word index
191# has max(1, ceil(len/64)) blocks: n = (len - 1) div 64 full blocks, then a
192# last block of len - 64n bytes.
193def chunk(a: Array<U32>, +t: U32, +index: U32, +len: Nat) -> Array<U32> & T.Out:
194  +n = Nat.div(Nat.sub(len,1n),64n)
195  chunk_blocks(n,t,index,chunk_start(),Nat.sub(len,Nat.mul(n,64n)),cv_of(iv()),read_block(a,index))
196
197# Every chunk but the last holds 1024 bytes; chunk t starts at word 256t.
198def chunk_at(more: Nat, +t: U32, +index: U32, +len: Nat, a: Array<U32>) -> Array<U32> & T.Out:
199  match more:
200    case 0n: chunk(a,t,index,len)
201    case 1n+q: chunk(a,t,index,1024n)
202
203# The outputs of the chunks, in order; `pair` holds the current chunk, n
204# chunks follow it, the last one of len bytes.
205def chunks(+n: Nat, +t: U32, +index: U32, +len: Nat, pair: Array<U32> & T.Out) -> List<&2,T.Out>:
206  match n pair:
207    case 0n Tuple{a,o}: Con{o,Nil{}}
208    case 1n+p Tuple{a,o}: Con{o,chunks(p,U32.inc(t),U32.add(index,256),len,chunk_at(p,U32.inc(t),U32.add(index,256),len,a))}
209
210# A message of `length` bytes has max(1, ceil(length/1024)) chunks: n =
211# (length - 1) div 1024 full ones, then the last of length - 1024n bytes.
212def message_chunks(a: Array<U32>, +length: Nat) -> List<&2,T.Out>:
213  +n = Nat.div(Nat.sub(length,1n),1024n)
214  +last = Nat.sub(length,Nat.mul(n,1024n))
215  chunks(n,0,0,last,chunk_at(n,0,0,last,a))
216
217# ---- the tree (2.5) ----
218
219# A node's chaining value: its compression with its own flags.
220def cv(o: T.Out) -> T.CV:
221  match o:
222    case T.Out{c,b,t,len,flags}: compress(c,b,t,len,flags)
223
224# A parent node: key IV, block = left child CV ++ right child CV, counter 0,
225# length 64, flag PARENT.
226def parent(l: T.CV, r: T.CV) -> T.Out:
227  T.Out{cv_of(iv()),block_of(SC.append(U32,cv_words(l),cv_words(r))),0,64,parent_flag()}
228
229def is_nil(xs: List<&2,T.Out>) -> Bool:
230  match xs:
231    case Nil{}: True{}
232    case Con{x,r}: False{}
233
234def first(xs: List<&2,T.Out>) -> T.Out:
235  match xs:
236    case Nil{}: T.Out{cv_of(iv()),block_of(Nil{}),0,0,0}
237    case Con{x,r}: x
238
239def join(l: T.Out, r: T.Out, alone: Bool) -> T.Out:
240  match alone:
241    case True{}: l
242    case False{}: parent(cv(l),cv(r))
243
244# The tree over the chunk outputs xs, 1 <= |xs| <= 2^h. The chunks are its
245# leaves in order; a left subtree is always complete with a power of two of
246# chunks, the largest one that leaves at least one chunk to its right: with
247# h = g+1 and |xs| > 2^g the left subtree takes the first 2^g chunks and the
248# right one the rest, while |xs| <= 2^g (nothing left for the right) means the
249# tree already fits in height g.
250def tree(+h: Nat, +xs: List<&2,T.Out>) -> T.Out:
251  match h xs:
252    case 0n Nil{}: first(Nil{})
253    case 0n Con{+x,+r}: first(Con{x,r})
254    case 1n+g Nil{}: first(Nil{})
255    case 1n+g Con{+x,+r}:
256      +k = SC.pow2(g)
257      join(tree(g,SC.take(T.Out,Con{x,r},k)),tree(g,SC.drop(T.Out,Con{x,r},k)),is_nil(SC.drop(T.Out,Con{x,r},k)))
258
259# ---- the root and the digest (2.6) ----
260
261# The root node is compressed with ROOT added to its flags; the 32-byte digest
262# is the resulting chaining value, words in little-endian order. A single
263# chunk is itself the root.
264def root(o: T.Out) -> T.CV:
265  match o:
266    case T.Out{c,b,t,len,flags}: compress(c,b,t,len,U32.or(flags,root_flag()))
267
268def hash(a: Array<U32>, +length: Nat) -> T.CV:
269  +cs = message_chunks(a,length)
270  root(tree(SC.length(T.Out,cs),cs))
271
272def digest(c: T.CV) -> Array<U32>:
273  match c:
274    case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}:
275      ANode{ANode{ANode{ALeaf{h0},ALeaf{h1}},ANode{ALeaf{h2},ALeaf{h3}}},ANode{ANode{ALeaf{h4},ALeaf{h5}},ANode{ALeaf{h6},ALeaf{h7}}}}
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(hash(a,length))}
281
282# None when byte_length exceeds the 4 * capacity bytes the array can hold.
283def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
284  (a,capacity) = pair
285  checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
286
287def blake3(words: Array<U32>, byte_length: Nat) -> Maybe<&1,Array<U32>>:
288  sized(byte_length,Array.size(U32,words))