src/crypto/sha/packed/core.bend
bend-collections@1.0.0.0 · 490 lines · 63 definitions
1import Base
2import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S
3
4type ShaWindow is Data:
5 W{a: U32, b: U32, c: U32, d: U32, e: U32, f: U32, g: U32, h: U32,
6 i: U32, j: U32, k: U32, l: U32, m: U32, n: U32, o: U32, p: U32}
7
8
9
10def initial() -> S.State:
11 S.H{1779033703, 3144134277, 1013904242, 2773480762,
12 1359893119, 2600822924, 528734635, 1541459225}
13
14def big0(+x: U32) -> U32:
15 ((U32.shrn(x, 2n) .|. U32.shln(x, 30n))
16 .^. (U32.shrn(x, 13n) .|. U32.shln(x, 19n))
17 .^. (U32.shrn(x, 22n) .|. U32.shln(x, 10n)) : U32)
18
19def big1(+x: U32) -> U32:
20 ((U32.shrn(x, 6n) .|. U32.shln(x, 26n))
21 .^. (U32.shrn(x, 11n) .|. U32.shln(x, 21n))
22 .^. (U32.shrn(x, 25n) .|. U32.shln(x, 7n)) : U32)
23
24def small0(+x: U32) -> U32:
25 ((U32.shrn(x, 7n) .|. U32.shln(x, 25n))
26 .^. (U32.shrn(x, 18n) .|. U32.shln(x, 14n))
27 .^. U32.shrn(x, 3n) : U32)
28
29def small1(+x: U32) -> U32:
30 ((U32.shrn(x, 17n) .|. U32.shln(x, 15n))
31 .^. (U32.shrn(x, 19n) .|. U32.shln(x, 13n))
32 .^. U32.shrn(x, 10n) : U32)
33
34def choose(+x: U32, y: U32, z: U32) -> U32:
35 ((x .&. y) .^. (U32.not(x) .&. z) : U32)
36
37def majority(+x: U32, +y: U32, +z: U32) -> U32:
38 ((x .&. y) .^. (x .&. z) .^. (y .&. z) : U32)
39
40def step(s: S.State, k: U32, w: U32) -> S.State:
41 S.H{+a, +b, +c, d, +e, +f, +g, h} = s
42 +t1 = (h + big1(e) + choose(e, f, g) + k + w : U32)
43 t2 = (big0(a) + majority(a, b, c) : U32)
44 S.H{(t1 + t2 : U32), a, b, c, (d + t1 : U32), e, f, g}
45
46def feedforward(x: S.State, y: S.State) -> S.State:
47 S.H{a, b, c, d, e, f, g, h} = x
48 S.H{i, j, k, l, m, n, o, p} = y
49 S.H{(a + i : U32), (b + j : U32), (c + k : U32), (d + l : U32),
50 (e + m : U32), (f + n : U32), (g + o : U32), (h + p : U32)}
51
52def pack(a: U32, b: U32, c: U32, d: U32) -> U32:
53 (U32.shln((a .&. 255 : U32), 24n)
54 .|. U32.shln((b .&. 255 : U32), 16n)
55 .|. U32.shln((c .&. 255 : U32), 8n) .|. (d .&. 255) : U32)
56
57def kr64(q: Nat, win: ShaWindow, s: S.State) -> S.State:
58 s
59
60def kr63(q: Nat, win: ShaWindow, s: S.State) -> S.State:
61 match q win:
62 case 0n _:
63 s
64 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
65 +w = (small1(b) + g + small0(t) + u : U32)
66 kr64(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3329325298, w))
67
68def kr62(q: Nat, win: ShaWindow, s: S.State) -> S.State:
69 match q win:
70 case 0n _:
71 s
72 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
73 +w = (small1(b) + g + small0(t) + u : U32)
74 kr63(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3204031479, w))
75
76def kr61(q: Nat, win: ShaWindow, s: S.State) -> S.State:
77 match q win:
78 case 0n _:
79 s
80 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
81 +w = (small1(b) + g + small0(t) + u : U32)
82 kr62(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2756734187, w))
83
84def kr60(q: Nat, win: ShaWindow, s: S.State) -> S.State:
85 match q win:
86 case 0n _:
87 s
88 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
89 +w = (small1(b) + g + small0(t) + u : U32)
90 kr61(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2428436474, w))
91
92def kr59(q: Nat, win: ShaWindow, s: S.State) -> S.State:
93 match q win:
94 case 0n _:
95 s
96 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
97 +w = (small1(b) + g + small0(t) + u : U32)
98 kr60(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2361852424, w))
99
100def kr58(q: Nat, win: ShaWindow, s: S.State) -> S.State:
101 match q win:
102 case 0n _:
103 s
104 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
105 +w = (small1(b) + g + small0(t) + u : U32)
106 kr59(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2227730452, w))
107
108def kr57(q: Nat, win: ShaWindow, s: S.State) -> S.State:
109 match q win:
110 case 0n _:
111 s
112 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
113 +w = (small1(b) + g + small0(t) + u : U32)
114 kr58(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2024104815, w))
115
116def kr56(q: Nat, win: ShaWindow, s: S.State) -> S.State:
117 match q win:
118 case 0n _:
119 s
120 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
121 +w = (small1(b) + g + small0(t) + u : U32)
122 kr57(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1955562222, w))
123
124def kr55(q: Nat, win: ShaWindow, s: S.State) -> S.State:
125 match q win:
126 case 0n _:
127 s
128 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
129 +w = (small1(b) + g + small0(t) + u : U32)
130 kr56(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1747873779, w))
131
132def kr54(q: Nat, win: ShaWindow, s: S.State) -> S.State:
133 match q win:
134 case 0n _:
135 s
136 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
137 +w = (small1(b) + g + small0(t) + u : U32)
138 kr55(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1537002063, w))
139
140def kr53(q: Nat, win: ShaWindow, s: S.State) -> S.State:
141 match q win:
142 case 0n _:
143 s
144 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
145 +w = (small1(b) + g + small0(t) + u : U32)
146 kr54(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1322822218, w))
147
148def kr52(q: Nat, win: ShaWindow, s: S.State) -> S.State:
149 match q win:
150 case 0n _:
151 s
152 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
153 +w = (small1(b) + g + small0(t) + u : U32)
154 kr53(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 958139571, w))
155
156def kr51(q: Nat, win: ShaWindow, s: S.State) -> S.State:
157 match q win:
158 case 0n _:
159 s
160 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
161 +w = (small1(b) + g + small0(t) + u : U32)
162 kr52(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 883997877, w))
163
164def kr50(q: Nat, win: ShaWindow, s: S.State) -> S.State:
165 match q win:
166 case 0n _:
167 s
168 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
169 +w = (small1(b) + g + small0(t) + u : U32)
170 kr51(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 659060556, w))
171
172def kr49(q: Nat, win: ShaWindow, s: S.State) -> S.State:
173 match q win:
174 case 0n _:
175 s
176 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
177 +w = (small1(b) + g + small0(t) + u : U32)
178 kr50(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 506948616, w))
179
180def kr48(q: Nat, win: ShaWindow, s: S.State) -> S.State:
181 match q win:
182 case 0n _:
183 s
184 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
185 +w = (small1(b) + g + small0(t) + u : U32)
186 kr49(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 430227734, w))
187
188def kr47(q: Nat, win: ShaWindow, s: S.State) -> S.State:
189 match q win:
190 case 0n _:
191 s
192 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
193 +w = (small1(b) + g + small0(t) + u : U32)
194 kr48(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 275423344, w))
195
196def kr46(q: Nat, win: ShaWindow, s: S.State) -> S.State:
197 match q win:
198 case 0n _:
199 s
200 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
201 +w = (small1(b) + g + small0(t) + u : U32)
202 kr47(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 4094571909, w))
203
204def kr45(q: Nat, win: ShaWindow, s: S.State) -> S.State:
205 match q win:
206 case 0n _:
207 s
208 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
209 +w = (small1(b) + g + small0(t) + u : U32)
210 kr46(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3600352804, w))
211
212def kr44(q: Nat, win: ShaWindow, s: S.State) -> S.State:
213 match q win:
214 case 0n _:
215 s
216 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
217 +w = (small1(b) + g + small0(t) + u : U32)
218 kr45(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3516065817, w))
219
220def kr43(q: Nat, win: ShaWindow, s: S.State) -> S.State:
221 match q win:
222 case 0n _:
223 s
224 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
225 +w = (small1(b) + g + small0(t) + u : U32)
226 kr44(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3345764771, w))
227
228def kr42(q: Nat, win: ShaWindow, s: S.State) -> S.State:
229 match q win:
230 case 0n _:
231 s
232 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
233 +w = (small1(b) + g + small0(t) + u : U32)
234 kr43(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3259730800, w))
235
236def kr41(q: Nat, win: ShaWindow, s: S.State) -> S.State:
237 match q win:
238 case 0n _:
239 s
240 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
241 +w = (small1(b) + g + small0(t) + u : U32)
242 kr42(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2820302411, w))
243
244def kr40(q: Nat, win: ShaWindow, s: S.State) -> S.State:
245 match q win:
246 case 0n _:
247 s
248 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
249 +w = (small1(b) + g + small0(t) + u : U32)
250 kr41(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2730485921, w))
251
252def kr39(q: Nat, win: ShaWindow, s: S.State) -> S.State:
253 match q win:
254 case 0n _:
255 s
256 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
257 +w = (small1(b) + g + small0(t) + u : U32)
258 kr40(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2456956037, w))
259
260def kr38(q: Nat, win: ShaWindow, s: S.State) -> S.State:
261 match q win:
262 case 0n _:
263 s
264 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
265 +w = (small1(b) + g + small0(t) + u : U32)
266 kr39(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2177026350, w))
267
268def kr37(q: Nat, win: ShaWindow, s: S.State) -> S.State:
269 match q win:
270 case 0n _:
271 s
272 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
273 +w = (small1(b) + g + small0(t) + u : U32)
274 kr38(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1986661051, w))
275
276def kr36(q: Nat, win: ShaWindow, s: S.State) -> S.State:
277 match q win:
278 case 0n _:
279 s
280 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
281 +w = (small1(b) + g + small0(t) + u : U32)
282 kr37(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1695183700, w))
283
284def kr35(q: Nat, win: ShaWindow, s: S.State) -> S.State:
285 match q win:
286 case 0n _:
287 s
288 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
289 +w = (small1(b) + g + small0(t) + u : U32)
290 kr36(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1396182291, w))
291
292def kr34(q: Nat, win: ShaWindow, s: S.State) -> S.State:
293 match q win:
294 case 0n _:
295 s
296 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
297 +w = (small1(b) + g + small0(t) + u : U32)
298 kr35(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1294757372, w))
299
300def kr33(q: Nat, win: ShaWindow, s: S.State) -> S.State:
301 match q win:
302 case 0n _:
303 s
304 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
305 +w = (small1(b) + g + small0(t) + u : U32)
306 kr34(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 773529912, w))
307
308def kr32(q: Nat, win: ShaWindow, s: S.State) -> S.State:
309 match q win:
310 case 0n _:
311 s
312 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
313 +w = (small1(b) + g + small0(t) + u : U32)
314 kr33(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 666307205, w))
315
316def kr31(q: Nat, win: ShaWindow, s: S.State) -> S.State:
317 match q win:
318 case 0n _:
319 s
320 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
321 +w = (small1(b) + g + small0(t) + u : U32)
322 kr32(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 338241895, w))
323
324def kr30(q: Nat, win: ShaWindow, s: S.State) -> S.State:
325 match q win:
326 case 0n _:
327 s
328 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
329 +w = (small1(b) + g + small0(t) + u : U32)
330 kr31(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 113926993, w))
331
332def kr29(q: Nat, win: ShaWindow, s: S.State) -> S.State:
333 match q win:
334 case 0n _:
335 s
336 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
337 +w = (small1(b) + g + small0(t) + u : U32)
338 kr30(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3584528711, w))
339
340def kr28(q: Nat, win: ShaWindow, s: S.State) -> S.State:
341 match q win:
342 case 0n _:
343 s
344 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
345 +w = (small1(b) + g + small0(t) + u : U32)
346 kr29(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3336571891, w))
347
348def kr27(q: Nat, win: ShaWindow, s: S.State) -> S.State:
349 match q win:
350 case 0n _:
351 s
352 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
353 +w = (small1(b) + g + small0(t) + u : U32)
354 kr28(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3210313671, w))
355
356def kr26(q: Nat, win: ShaWindow, s: S.State) -> S.State:
357 match q win:
358 case 0n _:
359 s
360 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
361 +w = (small1(b) + g + small0(t) + u : U32)
362 kr27(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2952996808, w))
363
364def kr25(q: Nat, win: ShaWindow, s: S.State) -> S.State:
365 match q win:
366 case 0n _:
367 s
368 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
369 +w = (small1(b) + g + small0(t) + u : U32)
370 kr26(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2821834349, w))
371
372def kr24(q: Nat, win: ShaWindow, s: S.State) -> S.State:
373 match q win:
374 case 0n _:
375 s
376 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
377 +w = (small1(b) + g + small0(t) + u : U32)
378 kr25(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2554220882, w))
379
380def kr23(q: Nat, win: ShaWindow, s: S.State) -> S.State:
381 match q win:
382 case 0n _:
383 s
384 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
385 +w = (small1(b) + g + small0(t) + u : U32)
386 kr24(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1996064986, w))
387
388def kr22(q: Nat, win: ShaWindow, s: S.State) -> S.State:
389 match q win:
390 case 0n _:
391 s
392 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
393 +w = (small1(b) + g + small0(t) + u : U32)
394 kr23(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1555081692, w))
395
396def kr21(q: Nat, win: ShaWindow, s: S.State) -> S.State:
397 match q win:
398 case 0n _:
399 s
400 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
401 +w = (small1(b) + g + small0(t) + u : U32)
402 kr22(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1249150122, w))
403
404def kr20(q: Nat, win: ShaWindow, s: S.State) -> S.State:
405 match q win:
406 case 0n _:
407 s
408 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
409 +w = (small1(b) + g + small0(t) + u : U32)
410 kr21(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 770255983, w))
411
412def kr19(q: Nat, win: ShaWindow, s: S.State) -> S.State:
413 match q win:
414 case 0n _:
415 s
416 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
417 +w = (small1(b) + g + small0(t) + u : U32)
418 kr20(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 604807628, w))
419
420def kr18(q: Nat, win: ShaWindow, s: S.State) -> S.State:
421 match q win:
422 case 0n _:
423 s
424 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
425 +w = (small1(b) + g + small0(t) + u : U32)
426 kr19(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 264347078, w))
427
428def kr17(q: Nat, win: ShaWindow, s: S.State) -> S.State:
429 match q win:
430 case 0n _:
431 s
432 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
433 +w = (small1(b) + g + small0(t) + u : U32)
434 kr18(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 4022224774, w))
435
436def kr16(q: Nat, win: ShaWindow, s: S.State) -> S.State:
437 match q win:
438 case 0n _:
439 s
440 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
441 +w = (small1(b) + g + small0(t) + u : U32)
442 kr17(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3835390401, w))
443
444
445def fips_compress16(+a: U32, +b: U32, +c: U32, +d: U32,
446 +e: U32, +f: U32, +g: U32, +h: U32,
447 +i: U32, +j: U32, +k: U32, +l: U32,
448 +m: U32, +n: U32, +o: U32, +p: U32, +q: Nat, +s: S.State) -> S.State:
449 s1 = step(s, 1116352408, a)
450 s2 = step(s1, 1899447441, b)
451 s3 = step(s2, 3049323471, c)
452 s4 = step(s3, 3921009573, d)
453 s5 = step(s4, 961987163, e)
454 s6 = step(s5, 1508970993, f)
455 s7 = step(s6, 2453635748, g)
456 s8 = step(s7, 2870763221, h)
457 s9 = step(s8, 3624381080, i)
458 s10 = step(s9, 310598401, j)
459 s11 = step(s10, 607225278, k)
460 s12 = step(s11, 1426881987, l)
461 s13 = step(s12, 1925078388, m)
462 s14 = step(s13, 2162078206, n)
463 s15 = step(s14, 2614888103, o)
464 s16 = step(s15, 3248222580, p)
465 feedforward(s, kr16(q, W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, s16))
466
467
468
469def len_hi(+n: Nat) -> U32:
470 +d0 = Nat.div(n, 32n)
471 +d1 = Nat.div(d0, 256n)
472 +d2 = Nat.div(d1, 256n)
473 +d3 = Nat.div(d2, 256n)
474 +d4 = Nat.div(d3, 256n)
475 +d5 = Nat.div(d4, 256n)
476 +d6 = Nat.div(d5, 256n)
477 pack(U32.from_nat(Nat.mod(d6, 256n)), U32.from_nat(Nat.mod(d5, 256n)),
478 U32.from_nat(Nat.mod(d4, 256n)), U32.from_nat(Nat.mod(d3, 256n)))
479
480def len_lo(+n: Nat) -> U32:
481 +d0 = Nat.div(n, 32n)
482 +d1 = Nat.div(d0, 256n)
483 +d2 = Nat.div(d1, 256n)
484 pack(U32.from_nat(Nat.mod(d2, 256n)), U32.from_nat(Nat.mod(d1, 256n)),
485 U32.from_nat(Nat.mod(d0, 256n)), U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n))
486
487
488
489
490