src/crypto/blake/blake3/blake3.bend
0x9ee2e9a299991dcc089fe22c7f3ceb5f · 212 lines · 0 definitions
1import Base
2import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/crypto/blake/blake3/types.bend as T
3import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/crypto/blake/blake3/compress.bend as C
4
5# BLAKE3 hash mode, 32-byte output.
6#
7# blake3(words, byte_length): the message is packed little-endian, four bytes
8# per U32 word, and byte_length is its logical length. The result is None when
9# byte_length exceeds 4 * the array's capacity, else the 32-byte digest as
10# eight little-endian U32 words. Bytes past byte_length in the last word do not
11# influence the result.
12#
13# The message is split into 1024-byte chunks (the last one holds the remaining
14# 1..1024 bytes, or 0 for the empty message). Every chunk but the last is
15# compressed to its chaining value as soon as it is read and pushed on a stack
16# of subtree chaining values, merged like a binary counter: a slot holds the
17# chaining value of a complete subtree of 2^i chunks, and pushing into a full
18# slot merges both into a parent node carried to the next slot. The last chunk
19# stays pending; at the end the stack is folded into it from the smallest
20# subtree up, and the resulting root node is compressed with ROOT.
21
22def iv() -> T.CV:
23 T.CV{1779033703,3144134277,1013904242,2773480762,1359893119,2600822924,528734635,1541459225}
24
25# GENERATED BEGIN (tools/generators/blake3/gen.py)
26# Reads the 16 words of a block at word `index`, threading the array.
27def read15(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
28 (a,w15) = pair
29 (a,T.B{w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15})
30
31def read14(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
32 (a,w14) = pair
33 read15(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
34
35def read13(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
36 (a,w13) = pair
37 read14(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
38
39def read12(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
40 (a,w12) = pair
41 read13(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
42
43def read11(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
44 (a,w11) = pair
45 read12(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
46
47def read10(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
48 (a,w10) = pair
49 read11(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
50
51def read9(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
52 (a,w9) = pair
53 read10(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
54
55def read8(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
56 (a,w8) = pair
57 read9(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
58
59def read7(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
60 (a,w7) = pair
61 read8(index,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
62
63def read6(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
64 (a,w6) = pair
65 read7(index,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
66
67def read5(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
68 (a,w5) = pair
69 read6(index,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
70
71def read4(+index: U32, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
72 (a,w4) = pair
73 read5(index,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
74
75def read3(+index: U32, w0: U32, w1: U32, w2: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
76 (a,w3) = pair
77 read4(index,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
78
79def read2(+index: U32, w0: U32, w1: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
80 (a,w2) = pair
81 read3(index,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
82
83def read1(+index: U32, w0: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
84 (a,w1) = pair
85 read2(index,w0,w1,Array.get(U32,a,U32.add(index,2)))
86
87def read0(+index: U32, pair: Array<U32> & U32) -> Array<U32> & T.Block:
88 (a,w0) = pair
89 read1(index,w0,Array.get(U32,a,U32.add(index,1)))
90
91def read_block(a: Array<U32>, +index: U32) -> Array<U32> & T.Block:
92 read0(index,Array.get(U32,a,index))
93# GENERATED END
94
95# The block truncated to its first `len` bytes: the word at byte offset pos
96# keeps its low len - pos bytes (all four when at least four remain).
97def partial(w: U32, delta: Nat) -> U32:
98 match delta:
99 case 0n: 0
100 case 1n: U32.and(w,255)
101 case 2n: U32.and(w,65535)
102 case 3n: U32.and(w,16777215)
103 case 4n+q: w
104
105def mask(w: U32, +pos: Nat, +len: Nat) -> U32:
106 partial(w,Nat.sub(len,pos))
107
108def mask_block(b: T.Block, +len: Nat) -> T.Block:
109 match b:
110 case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}:
111 T.B{mask(m0,0n,len),mask(m1,4n,len),mask(m2,8n,len),mask(m3,12n,len),mask(m4,16n,len),mask(m5,20n,len),mask(m6,24n,len),mask(m7,28n,len),mask(m8,32n,len),mask(m9,36n,len),mask(m10,40n,len),mask(m11,44n,len),mask(m12,48n,len),mask(m13,52n,len),mask(m14,56n,len),mask(m15,60n,len)}
112
113# A chunk that is not the last: n more full blocks after the current one, the
114# current block in `pair`; flags is CHUNK_START on the first block and 0 after.
115# Returns the chunk's chaining value.
116def full_go(n: Nat, +counter: U32, +index: U32, +flags: U32, cv: T.CV, pair: Array<U32> & T.Block) -> Array<U32> & T.CV:
117 match n pair:
118 case 0n Tuple{a,b}: (a,C.compress(cv,b,counter,64,U32.or(flags,2)))
119 case 1n+p Tuple{a,b}: full_go(p,counter,U32.add(index,16),0,C.compress(cv,b,counter,64,flags),read_block(a,U32.add(index,16)))
120
121def full_chunk(a: Array<U32>, +counter: U32, +index: U32) -> Array<U32> & T.CV:
122 full_go(15n,counter,index,1,iv(),read_block(a,index))
123
124# The last chunk: n full blocks before its last block of len bytes (1..64, or
125# 0 for the empty message). Returns the pending output of the last block.
126def last_go(n: Nat, +counter: U32, +index: U32, +flags: U32, +len: Nat, cv: T.CV, pair: Array<U32> & T.Block) -> Array<U32> & T.Out:
127 match n pair:
128 case 0n Tuple{a,b}: (a,T.Out{cv,mask_block(b,len),counter,U32.from_nat(len),U32.or(flags,2)})
129 case 1n+p Tuple{a,b}: last_go(p,counter,U32.add(index,16),0,len,C.compress(cv,b,counter,64,flags),read_block(a,U32.add(index,16)))
130
131def last_chunk(a: Array<U32>, +counter: U32, +index: U32, +len: Nat) -> Array<U32> & T.Out:
132 +n = Nat.div(Nat.sub(len,1n),64n)
133 last_go(n,counter,index,1,Nat.sub(len,Nat.mul(n,64n)),iv(),read_block(a,index))
134
135def out_cv(o: T.Out) -> T.CV:
136 match o:
137 case T.Out{cv,b,t,len,flags}: C.compress(cv,b,t,len,flags)
138
139def root_cv(o: T.Out) -> T.CV:
140 match o:
141 case T.Out{cv,b,t,len,flags}: C.compress(cv,b,t,len,U32.or(flags,8))
142
143def parent_block(l: T.CV, r: T.CV) -> T.Block:
144 match l r:
145 case T.CV{l0,l1,l2,l3,l4,l5,l6,l7} T.CV{r0,r1,r2,r3,r4,r5,r6,r7}:
146 T.B{l0,l1,l2,l3,l4,l5,l6,l7,r0,r1,r2,r3,r4,r5,r6,r7}
147
148def parent_out(l: T.CV, r: T.CV) -> T.Out:
149 T.Out{iv(),parent_block(l,r),0,64,4}
150
151def parent_cv(l: T.CV, r: T.CV) -> T.CV:
152 C.compress(iv(),parent_block(l,r),0,64,4)
153
154# The subtree stack, smallest subtree first: slot i is empty or holds the
155# chaining value of a complete subtree of 2^i chunks.
156type Stack is Data:
157 SNil{}
158 SEmpty{rest: Stack}
159 SFull{cv: T.CV, rest: Stack}
160
161def push(s: Stack, c: T.CV) -> Stack:
162 match s:
163 case SNil{}: SFull{c,SNil{}}
164 case SEmpty{r}: SFull{c,r}
165 case SFull{d,r}: SEmpty{push(r,parent_cv(d,c))}
166
167# Folds the stack into the pending output of the rightmost subtree.
168def finish(s: Stack, o: T.Out) -> T.Out:
169 match s:
170 case SNil{}: o
171 case SEmpty{r}: finish(r,o)
172 case SFull{d,r}: finish(r,parent_out(d,out_cv(o)))
173
174def pushed(s: Stack, pair: Array<U32> & T.CV) -> Array<U32> & Stack:
175 (a,c) = pair
176 (a,push(s,c))
177
178# n chunks before the last; len is the byte length of the last chunk.
179def chunks(n: Nat, +counter: U32, +index: U32, +len: Nat, pair: Array<U32> & Stack) -> T.Out:
180 match n pair:
181 case 0n Tuple{a,s}: finish(s,Pair.snd(Array<U32>,T.Out,last_chunk(a,counter,index,len)))
182 case 1n+p Tuple{a,s}: chunks(p,U32.inc(counter),U32.add(index,256),len,pushed(s,full_chunk(a,counter,index)))
183
184def unchecked(a: Array<U32>, +length: Nat) -> T.CV:
185 +n = Nat.div(Nat.sub(length,1n),1024n)
186 root_cv(chunks(n,0,0,Nat.sub(length,Nat.mul(n,1024n)),(a,SNil{})))
187
188def digest(c: T.CV) -> Array<U32>:
189 match c:
190 case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}:
191 a = Array.new(U32,3n,0)
192 a = Array.set(U32,a,0,h0)
193 a = Array.set(U32,a,1,h1)
194 a = Array.set(U32,a,2,h2)
195 a = Array.set(U32,a,3,h3)
196 a = Array.set(U32,a,4,h4)
197 a = Array.set(U32,a,5,h5)
198 a = Array.set(U32,a,6,h6)
199 a = Array.set(U32,a,7,h7)
200 a
201
202def checked(valid: Bool, a: Array<U32>, +length: Nat) -> Maybe<&1,Array<U32>>:
203 match valid:
204 case False{}: None{}
205 case True{}: Some{digest(unchecked(a,length))}
206
207def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
208 (a,capacity) = pair
209 checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
210
211def blake3(words: Array<U32>, byte_length: Nat) -> Maybe<&1,Array<U32>>:
212 sized(byte_length,Array.size(U32,words))