src/crypto/blake/blake2s/blake2s.bend

bend-collections@1.0.0.0 · 210 lines · 46 definitions

1# Generated by tools/generators/blake2s_gen.py; do not edit.
2import Base
3import bend-collections@1.0.0.0/src/crypto/blake/blake2s/types.bend as T
4import bend-collections@1.0.0.0/src/crypto/blake/blake2s/compress.bend as C
5
6# The 64-bit byte counter t is kept as two U32 halves (t0 low, t1 high).
7def carry(c: Bool, hi: U32) -> U32:
8  match c:
9    case True{}: U32.add(hi,1)
10    case False{}: hi
11
12def count_hi(+lo: U32, hi: U32, +n: U32) -> U32:
13  carry(U32.is_lt(U32.add(lo,n),n),hi)
14
15def read15(+index: U32, h: T.State, t0: U32, t1: 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.State:
16  (a,w15) = pair
17  (a,C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}))
18
19def read14(+index: U32, h: T.State, t0: U32, t1: 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.State:
20  (a,w14) = pair
21  read15(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
22
23def read13(+index: U32, h: T.State, t0: U32, t1: 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.State:
24  (a,w13) = pair
25  read14(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
26
27def read12(+index: U32, h: T.State, t0: U32, t1: 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.State:
28  (a,w12) = pair
29  read13(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
30
31def read11(+index: U32, h: T.State, t0: U32, t1: 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.State:
32  (a,w11) = pair
33  read12(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
34
35def read10(+index: U32, h: T.State, t0: U32, t1: 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.State:
36  (a,w10) = pair
37  read11(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
38
39def read9(+index: U32, h: T.State, t0: U32, t1: 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.State:
40  (a,w9) = pair
41  read10(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
42
43def read8(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
44  (a,w8) = pair
45  read9(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
46
47def read7(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
48  (a,w7) = pair
49  read8(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
50
51def read6(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
52  (a,w6) = pair
53  read7(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
54
55def read5(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
56  (a,w5) = pair
57  read6(index,h,t0,t1,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
58
59def read4(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
60  (a,w4) = pair
61  read5(index,h,t0,t1,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
62
63def read3(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
64  (a,w3) = pair
65  read4(index,h,t0,t1,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
66
67def read2(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
68  (a,w2) = pair
69  read3(index,h,t0,t1,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
70
71def read1(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
72  (a,w1) = pair
73  read2(index,h,t0,t1,w0,w1,Array.get(U32,a,U32.add(index,2)))
74
75def read0(+index: U32, h: T.State, t0: U32, t1: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
76  (a,w0) = pair
77  read1(index,h,t0,t1,w0,Array.get(U32,a,U32.add(index,1)))
78
79def absorb(a: Array<U32>, +index: U32, h: T.State, t0: U32, t1: U32) -> Array<U32> & T.State:
80  read0(index,h,t0,t1,Array.get(U32,a,index))
81
82# The final block keeps the bytes before the logical length and zeroes the rest.
83# keep(n, w) keeps the low n bytes of w.
84def keep(n: Nat, +w: U32) -> U32:
85  match n:
86    case 0n: 0
87    case 1n: U32.and(255,w)
88    case 2n: U32.and(65535,w)
89    case 3n: U32.and(16777215,w)
90    case 4n+p: w
91
92def pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32:
93  keep(Nat.sub(remain,pos),w)
94
95def pad15(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: 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) -> T.State:
96  (a,w15) = pair
97  C.compress(h,pad_word(w0,0n,remain),pad_word(w1,4n,remain),pad_word(w2,8n,remain),pad_word(w3,12n,remain),pad_word(w4,16n,remain),pad_word(w5,20n,remain),pad_word(w6,24n,remain),pad_word(w7,28n,remain),pad_word(w8,32n,remain),pad_word(w9,36n,remain),pad_word(w10,40n,remain),pad_word(w11,44n,remain),pad_word(w12,48n,remain),pad_word(w13,52n,remain),pad_word(w14,56n,remain),pad_word(w15,60n,remain),t0,t1,True{})
98
99def pad14(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: 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) -> T.State:
100  (a,w14) = pair
101  pad15(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
102
103def pad13(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: 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) -> T.State:
104  (a,w13) = pair
105  pad14(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
106
107def pad12(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: 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) -> T.State:
108  (a,w12) = pair
109  pad13(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
110
111def pad11(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: 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) -> T.State:
112  (a,w11) = pair
113  pad12(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
114
115def pad10(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: 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) -> T.State:
116  (a,w10) = pair
117  pad11(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
118
119def pad9(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32, pair: Array<U32> & U32) -> T.State:
120  (a,w9) = pair
121  pad10(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
122
123def pad8(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32, pair: Array<U32> & U32) -> T.State:
124  (a,w8) = pair
125  pad9(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
126
127def pad7(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32, pair: Array<U32> & U32) -> T.State:
128  (a,w7) = pair
129  pad8(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
130
131def pad6(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32, pair: Array<U32> & U32) -> T.State:
132  (a,w6) = pair
133  pad7(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
134
135def pad5(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32, pair: Array<U32> & U32) -> T.State:
136  (a,w5) = pair
137  pad6(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
138
139def pad4(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32, pair: Array<U32> & U32) -> T.State:
140  (a,w4) = pair
141  pad5(remain,index,h,t0,t1,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
142
143def pad3(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32, pair: Array<U32> & U32) -> T.State:
144  (a,w3) = pair
145  pad4(remain,index,h,t0,t1,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
146
147def pad2(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32, pair: Array<U32> & U32) -> T.State:
148  (a,w2) = pair
149  pad3(remain,index,h,t0,t1,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
150
151def pad1(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32, pair: Array<U32> & U32) -> T.State:
152  (a,w1) = pair
153  pad2(remain,index,h,t0,t1,w0,w1,Array.get(U32,a,U32.add(index,2)))
154
155def pad0(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, pair: Array<U32> & U32) -> T.State:
156  (a,w0) = pair
157  pad1(remain,index,h,t0,t1,w0,Array.get(U32,a,U32.add(index,1)))
158
159def finish(a: Array<U32>, +index: U32, +t0: U32, t1: U32, +remain: Nat, h: T.State) -> T.State:
160  +n = U32.from_nat(remain)
161  pad0(remain,index,h,U32.add(t0,n),count_hi(t0,t1,n),Array.get(U32,a,index))
162
163def blocks(n: Nat, +index: U32, +t0: U32, t1: U32, +remain: Nat, pair: Array<U32> & T.State) -> T.State:
164  match n pair:
165    case 0n Tuple{a,h}: finish(a,index,t0,t1,remain,h)
166    case 1n+p Tuple{a,h}:
167      +c0 = U32.add(t0,64)
168      +c1 = count_hi(t0,t1,64)
169      blocks(p,U32.add(index,16),c0,c1,remain,absorb(a,index,h,c0,c1))
170
171# Parameter block for an unkeyed 32-byte digest: h0 = IV0 ^ 0x01010020.
172def initial() -> T.State:
173  T.H{1795745351,3144134277,1013904242,2773480762,1359893119,2600822924,528734635,1541459225}
174
175# Blocks before the last one: max(1, ceil(length/64)) - 1.
176def leading(length: Nat) -> Nat:
177  Nat.sub(Nat.div(Nat.add(length,63n),64n),1n)
178
179def unchecked(a: Array<U32>, +length: Nat) -> T.State:
180  +n = leading(length)
181  blocks(n,0,0,0,Nat.sub(length,Nat.mul(64n,n)),(a,initial()))
182
183def digest(h: T.State) -> Array<U32>:
184  match h:
185    case T.H{h0,h1,h2,h3,h4,h5,h6,h7}:
186      a = Array.new(U32,3n,0)
187      a = Array.set(U32,a,0,h0)
188      a = Array.set(U32,a,1,h1)
189      a = Array.set(U32,a,2,h2)
190      a = Array.set(U32,a,3,h3)
191      a = Array.set(U32,a,4,h4)
192      a = Array.set(U32,a,5,h5)
193      a = Array.set(U32,a,6,h6)
194      a = Array.set(U32,a,7,h7)
195      a
196
197def checked(valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
198  match valid:
199    case False{}: None{}
200    case True{}: Some{digest(unchecked(a,length))}
201
202def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
203  (a,capacity) = pair
204  checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
205
206# BLAKE2s-256 of the first `length` bytes of `a` (four little-endian bytes per
207# word): the eight little-endian digest words, or None when length exceeds
208# 4 * the array capacity.
209def blake2s(a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
210  sized(length,Array.size(U32,a))