src/hub_sha/core.bend
mylsm-lsm-store@0.5.0.0 · 3,620 lines · 0 definitions
1# Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f
2# (src/crypto/sha/core.bend), byte-identical except `Window` renamed to
3# `ShaWindow`: Bend 2.0.28 Base added a GUI `Window` type that collides with
4# this module's schedule-window type. Verify against NIST vectors, not the
5# upstream PROOF.bend (which covers the original names).
6import Base
7import mylsm-lsm-store@0.5.0.0/src/hub_sha/state.bend as S
8
9# Represent ShaWindow data used by the SHA-256 compression implementation.
10type ShaWindow is Data:
11 W{a: U32, b: U32, c: U32, d: U32, e: U32, f: U32, g: U32, h: U32,
12 i: U32, j: U32, k: U32, l: U32, m: U32, n: U32, o: U32, p: U32}
13
14# SHA-256 for byte sequences. Each input U32 contributes its low 8 bits.
15# SHA-256 arithmetic is native U32, hence addition wraps modulo 2^32.
16def initial() -> S.State:
17 S.H{1779033703, 3144134277, 1013904242, 2773480762,
18 1359893119, 2600822924, 528734635, 1541459225}
19
20# Handle rotr in the SHA-256 compression implementation.
21def rotr(+word: U32, +bit_shift: Nat) -> U32:
22 (U32.shrn(word, bit_shift) .|. U32.shln(word, Nat.sub(32n, bit_shift)) : U32)
23
24# Compute the big sigma function for 0 for the SHA-256 compression implementation.
25def big0(+word: U32) -> U32:
26 ((U32.shrn(word, 2n) .|. U32.shln(word, 30n))
27 .^. (U32.shrn(word, 13n) .|. U32.shln(word, 19n))
28 .^. (U32.shrn(word, 22n) .|. U32.shln(word, 10n)) : U32)
29
30# Compute the big sigma function for 1 for the SHA-256 compression implementation.
31def big1(+word: U32) -> U32:
32 ((U32.shrn(word, 6n) .|. U32.shln(word, 26n))
33 .^. (U32.shrn(word, 11n) .|. U32.shln(word, 21n))
34 .^. (U32.shrn(word, 25n) .|. U32.shln(word, 7n)) : U32)
35
36# Compute the small sigma function for 0 for the SHA-256 compression implementation.
37def small0(+word: U32) -> U32:
38 ((U32.shrn(word, 7n) .|. U32.shln(word, 25n))
39 .^. (U32.shrn(word, 18n) .|. U32.shln(word, 14n))
40 .^. U32.shrn(word, 3n) : U32)
41
42# Compute the small sigma function for 1 for the SHA-256 compression implementation.
43def small1(+word: U32) -> U32:
44 ((U32.shrn(word, 17n) .|. U32.shln(word, 15n))
45 .^. (U32.shrn(word, 19n) .|. U32.shln(word, 13n))
46 .^. U32.shrn(word, 10n) : U32)
47
48# Handle choose in the SHA-256 compression implementation.
49def choose(+word_x: U32, word_y: U32, word_z: U32) -> U32:
50 ((word_x .&. word_y) .^. (U32.not(word_x) .&. word_z) : U32)
51
52# Handle majority in the SHA-256 compression implementation.
53def majority(+word_x: U32, +word_y: U32, +word_z: U32) -> U32:
54 ((word_x .&. word_y) .^. (word_x .&. word_z) .^. (word_y .&. word_z) : U32)
55
56# Handle step in the SHA-256 compression implementation.
57def step(state: S.State, round_constant: U32, schedule_word: U32) -> S.State:
58 S.H{+a, +b, +c, d, +e, +f, +g, h} = state
59 +t1 = (h + big1(e) + choose(e, f, g) + round_constant + schedule_word : U32)
60 t2 = (big0(a) + majority(a, b, c) : U32)
61 S.H{(t1 + t2 : U32), a, b, c, (d + t1 : U32), e, f, g}
62
63# Feed forward for the SHA-256 compression implementation.
64def feedforward(prior_state: S.State, round_state: S.State) -> S.State:
65 S.H{a, b, c, d, e, f, g, h} = prior_state
66 S.H{i, j, k, l, m, n, o, p} = round_state
67 S.H{(a + i : U32), (b + j : U32), (c + k : U32), (d + l : U32),
68 (e + m : U32), (f + n : U32), (g + o : U32), (h + p : U32)}
69
70# Handle get in the SHA-256 compression implementation.
71def get(xs: List<&2, U32>, index: Nat) -> U32:
72 match xs index:
73 case Nil{} _:
74 0
75 case h <> t 0n:
76 h
77 case h <> t 1n+p:
78 get(t, p)
79
80# Reverse history: at round t, index j contains W[t-1-j].
81def next_word_slow(+history: List<&2, U32>) -> U32:
82 (small1(get(history, 1n)) + get(history, 6n)
83 + small0(get(history, 14n)) + get(history, 15n) : U32)
84
85# Schedule histories always contain at least 16 words. Destructuring that prefix
86# avoids four independent linked-list walks for every expanded word; the fallback
87# preserves the total behavior used by the universal refinement theorem.
88def next_word(+history: List<&2, U32>) -> U32:
89 match history:
90 case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> (p <> rest):
91 (small1(b) + g + small0(o) + p : U32)
92 case _:
93 next_word_slow(history)
94
95# Handle expand in the SHA-256 compression implementation.
96def expand(rounds_left: Nat, +history: List<&2, U32>) -> List<&2, U32>:
97 match rounds_left:
98 case 0n:
99 Nil{}
100 case 1n+p:
101 +w = next_word(history)
102 w <> expand(p, w <> history)
103
104# Handle schedule in the SHA-256 compression implementation.
105def schedule(extra: Nat, +block: List<&2, U32>) -> List<&2, U32>:
106 List.append(&2, U32, block,
107 expand(extra, List.reverse(&2, U32, block)))
108
109# Handle rounds in the SHA-256 compression implementation.
110def rounds(ks: List<&2, U32>, ws: List<&2, U32>, state: S.State) -> S.State:
111 match ks ws:
112 case Nil{} _:
113 state
114 case k <> kt Nil{}:
115 state
116 case k <> kt w <> wt:
117 rounds(kt, wt, step(state, k, w))
118
119# Compression consumes an already expanded 64-word schedule.
120def compress(ws: List<&2, U32>, ks: List<&2, U32>, +state: S.State) -> S.State:
121 feedforward(state, rounds(ks, ws, state))
122
123# Generate each derived schedule word immediately before its round. The reverse
124# history is still retained for the recurrence, but the chronological 48-word
125# extension is never materialized.
126def expanded_rounds(rounds_left: Nat, +history: List<&2, U32>, ks: List<&2, U32>, state: S.State) -> S.State:
127 match rounds_left ks:
128 case 0n _:
129 state
130 case 1n+p Nil{}:
131 state
132 case 1n+p k <> kt:
133 +w = next_word(history)
134 expanded_rounds(p, w <> history, kt, step(state, k, w))
135
136# Consume the original block words, then continue directly with its expansion.
137def schedule_rounds(
138 ws: List<&2, U32>,
139 +extra: Nat,
140 +history: List<&2, U32>,
141 ks: List<&2, U32>,
142 state: S.State
143) -> S.State:
144 match ws ks:
145 case Nil{} _:
146 expanded_rounds(extra, history, ks, state)
147 case w <> wt Nil{}:
148 state
149 case w <> wt k <> kt:
150 schedule_rounds(wt, extra, history, kt, step(state, k, w))
151
152# A fixed rolling window drops schedule words as soon as they are older than 16
153# rounds. This avoids growing and reference-counting the reverse history list.
154def window_rounds(rounds_left: Nat, win: ShaWindow, ks: List<&2, U32>, state: S.State) -> S.State:
155 match rounds_left win ks:
156 case 0n _ _:
157 state
158 case 1n+q _ Nil{}:
159 state
160 case 1n+q W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u} k <> kt:
161 +w = (small1(b) + g + small0(t) + u : U32)
162 window_rounds(q, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, kt,
163 step(state, k, w))
164
165# Handle window schedule rounds in the SHA-256 compression implementation.
166def window_schedule_rounds(
167 ws: List<&2, U32>,
168 +extra: Nat,
169 win: ShaWindow,
170 ks: List<&2, U32>,
171 state: S.State
172) -> S.State:
173 match ws ks:
174 case Nil{} _:
175 window_rounds(extra, win, ks, state)
176 case w <> wt Nil{}:
177 state
178 case w <> wt k <> kt:
179 window_schedule_rounds(wt, extra, win, kt, step(state, k, w))
180
181# Handle fused compress slow in the SHA-256 compression implementation.
182def fused_compress_slow(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +state: S.State) -> S.State:
183 feedforward(state, schedule_rounds(block, extra, List.reverse(&2, U32, block), ks, state))
184
185# Handle fused compress in the SHA-256 compression implementation.
186def fused_compress(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +state: S.State) -> S.State:
187 match block:
188 case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}:
189 feedforward(state, window_schedule_rounds(
190 [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra,
191 W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, state))
192 case _:
193 fused_compress_slow(block, extra, ks, state)
194
195# Fast path for the 16-word blocks produced by block_bytes. It executes the
196# seed rounds directly and constructs only the fixed rolling window.
197def window_compress16(
198 +word_a: U32,
199 +word_b: U32,
200 +word_c: U32,
201 +word_d: U32,
202 +word_e: U32,
203 +word_f: U32,
204 +word_g: U32,
205 +word_h: U32,
206 +word_i: U32,
207 +word_j: U32,
208 +round_constant: U32,
209 +word_l: U32,
210 +word_m: U32,
211 +count: U32,
212 +word_o: U32,
213 +word_p: U32,
214 +extra: Nat,
215 +ks: List<&2, U32>,
216 +state: S.State
217) -> S.State:
218 match ks:
219 case k0 <> k1 <> k2 <> k3 <> k4 <> k5 <> k6 <> k7 <>
220 k8 <> k9 <> k10 <> k11 <> k12 <> k13 <> k14 <> k15 <> kt:
221 s1 = step(state, k0, word_a)
222 s2 = step(s1, k1, word_b)
223 s3 = step(s2, k2, word_c)
224 s4 = step(s3, k3, word_d)
225 s5 = step(s4, k4, word_e)
226 s6 = step(s5, k5, word_f)
227 s7 = step(s6, k6, word_g)
228 s8 = step(s7, k7, word_h)
229 s9 = step(s8, k8, word_i)
230 s10 = step(s9, k9, word_j)
231 s11 = step(s10, k10, round_constant)
232 s12 = step(s11, k11, word_l)
233 s13 = step(s12, k12, word_m)
234 s14 = step(s13, k13, count)
235 s15 = step(s14, k14, word_o)
236 s16 = step(s15, k15, word_p)
237 feedforward(state, window_rounds(extra,
238 W{word_p, word_o, count, word_m, word_l, round_constant, word_j, word_i, word_h, word_g, word_f, word_e, word_d, word_c, word_b, word_a}, kt, s16))
239 case _:
240 fused_compress([word_a, word_b, word_c, word_d, word_e, word_f, word_g, word_h, word_i, word_j, round_constant, word_l, word_m, count, word_o, word_p], extra, ks, state)
241
242# Handle be32 in the SHA-256 compression implementation.
243def be32(+word: U32) -> List<&2, U32>:
244 [U32.shrn(word, 24n), (U32.shrn(word, 16n) .&. 255 : U32),
245 (U32.shrn(word, 8n) .&. 255 : U32), (word .&. 255 : U32)]
246
247# Return the length of gth octets in the SHA-256 compression implementation.
248def length_octets(count: Nat, +byte_length: Nat, acc: List<&2, U32>) -> List<&2, U32>:
249 match count:
250 case 0n:
251 acc
252 case 1n+p:
253 length_octets(p, Nat.div(byte_length, 256n), U32.from_nat(Nat.mod(byte_length, 256n)) <> acc)
254
255# Handle bit length in the SHA-256 compression implementation.
256def bit_length(+byte_length: Nat) -> List<&2, U32>:
257 length_octets(7n, Nat.div(byte_length, 32n),
258 [U32.shln(U32.from_nat(Nat.mod(byte_length, 32n)), 3n)])
259
260# Handle pack in the SHA-256 compression implementation.
261def pack(word_a: U32, word_b: U32, word_c: U32, word_d: U32) -> U32:
262 (U32.shln((word_a .&. 255 : U32), 24n)
263 .|. U32.shln((word_b .&. 255 : U32), 16n)
264 .|. U32.shln((word_c .&. 255 : U32), 8n) .|. (word_d .&. 255) : U32)
265
266# Handle digest in the SHA-256 compression implementation.
267def digest(state: S.State) -> List<&2, U32>:
268 S.H{a, b, c, d, e, f, g, h} = state
269 [a, b, c, d, e, f, g, h]
270
271# Generic block decoder over a padded byte list and any constant table. The
272# fast path below is proved equal to it with the FIPS table.
273def block_bytes(bytes: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, state: S.State) -> S.State:
274 match bytes:
275 case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
276 block_bytes(rest, extra, ks, window_compress16(
277 pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15),
278 pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31),
279 pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47),
280 pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63),
281 extra, ks, state))
282 case _:
283 state
284
285# FIPS 180-4 round constants, the table the specialized rounds below inline.
286def round_constants() -> List<&2, U32>:
287 [1116352408, 1899447441, 3049323471, 3921009573,
288 961987163, 1508970993, 2453635748, 2870763221,
289 3624381080, 310598401, 607225278, 1426881987,
290 1925078388, 2162078206, 2614888103, 3248222580,
291 3835390401, 4022224774, 264347078, 604807628,
292 770255983, 1249150122, 1555081692, 1996064986,
293 2554220882, 2821834349, 2952996808, 3210313671,
294 3336571891, 3584528711, 113926993, 338241895,
295 666307205, 773529912, 1294757372, 1396182291,
296 1695183700, 1986661051, 2177026350, 2456956037,
297 2730485921, 2820302411, 3259730800, 3345764771,
298 3516065817, 3600352804, 4094571909, 275423344,
299 430227734, 506948616, 659060556, 883997877,
300 958139571, 1322822218, 1537002063, 1747873779,
301 1955562222, 2024104815, 2227730452, 2361852424,
302 2428436474, 2756734187, 3204031479, 3329325298]
303
304# SHA-256 round t (16 <= t < 64) with its constant as a literal. Like
305# window_rounds, q bounds the remaining rounds (48 for SHA-256) and each round
306# derives its schedule word from the rolling window before continuing with
307# round t+1. Defined last-to-first because names must precede use.
308def kr64(state: S.State) -> S.State:
309 state
310
311# Return the SHA-256 round constant for schedule index 63.
312def kr63(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
313 match rounds_left win:
314 case 0n _:
315 state
316 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
317 +w = (small1(b) + g + small0(t) + u : U32)
318 kr64(step(state, 3329325298, w))
319
320# Return the SHA-256 round constant for schedule index 62.
321def kr62(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
322 match rounds_left win:
323 case 0n _:
324 state
325 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
326 +w = (small1(b) + g + small0(t) + u : U32)
327 kr63(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3204031479, w))
328
329# Return the SHA-256 round constant for schedule index 61.
330def kr61(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
331 match rounds_left win:
332 case 0n _:
333 state
334 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
335 +w = (small1(b) + g + small0(t) + u : U32)
336 kr62(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2756734187, w))
337
338# Return the SHA-256 round constant for schedule index 60.
339def kr60(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
340 match rounds_left win:
341 case 0n _:
342 state
343 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
344 +w = (small1(b) + g + small0(t) + u : U32)
345 kr61(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2428436474, w))
346
347# Return the SHA-256 round constant for schedule index 59.
348def kr59(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
349 match rounds_left win:
350 case 0n _:
351 state
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 kr60(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2361852424, w))
355
356# Return the SHA-256 round constant for schedule index 58.
357def kr58(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
358 match rounds_left win:
359 case 0n _:
360 state
361 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
362 +w = (small1(b) + g + small0(t) + u : U32)
363 kr59(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2227730452, w))
364
365# Return the SHA-256 round constant for schedule index 57.
366def kr57(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
367 match rounds_left win:
368 case 0n _:
369 state
370 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
371 +w = (small1(b) + g + small0(t) + u : U32)
372 kr58(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2024104815, w))
373
374# Return the SHA-256 round constant for schedule index 56.
375def kr56(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
376 match rounds_left win:
377 case 0n _:
378 state
379 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
380 +w = (small1(b) + g + small0(t) + u : U32)
381 kr57(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1955562222, w))
382
383# Return the SHA-256 round constant for schedule index 55.
384def kr55(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
385 match rounds_left win:
386 case 0n _:
387 state
388 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
389 +w = (small1(b) + g + small0(t) + u : U32)
390 kr56(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1747873779, w))
391
392# Return the SHA-256 round constant for schedule index 54.
393def kr54(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
394 match rounds_left win:
395 case 0n _:
396 state
397 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
398 +w = (small1(b) + g + small0(t) + u : U32)
399 kr55(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1537002063, w))
400
401# Return the SHA-256 round constant for schedule index 53.
402def kr53(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
403 match rounds_left win:
404 case 0n _:
405 state
406 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
407 +w = (small1(b) + g + small0(t) + u : U32)
408 kr54(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1322822218, w))
409
410# Return the SHA-256 round constant for schedule index 52.
411def kr52(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
412 match rounds_left win:
413 case 0n _:
414 state
415 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
416 +w = (small1(b) + g + small0(t) + u : U32)
417 kr53(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 958139571, w))
418
419# Return the SHA-256 round constant for schedule index 51.
420def kr51(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
421 match rounds_left win:
422 case 0n _:
423 state
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 kr52(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 883997877, w))
427
428# Return the SHA-256 round constant for schedule index 50.
429def kr50(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
430 match rounds_left win:
431 case 0n _:
432 state
433 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
434 +w = (small1(b) + g + small0(t) + u : U32)
435 kr51(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 659060556, w))
436
437# Return the SHA-256 round constant for schedule index 49.
438def kr49(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
439 match rounds_left win:
440 case 0n _:
441 state
442 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
443 +w = (small1(b) + g + small0(t) + u : U32)
444 kr50(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 506948616, w))
445
446# Return the SHA-256 round constant for schedule index 48.
447def kr48(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
448 match rounds_left win:
449 case 0n _:
450 state
451 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
452 +w = (small1(b) + g + small0(t) + u : U32)
453 kr49(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 430227734, w))
454
455# Return the SHA-256 round constant for schedule index 47.
456def kr47(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
457 match rounds_left win:
458 case 0n _:
459 state
460 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
461 +w = (small1(b) + g + small0(t) + u : U32)
462 kr48(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 275423344, w))
463
464# Return the SHA-256 round constant for schedule index 46.
465def kr46(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
466 match rounds_left win:
467 case 0n _:
468 state
469 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
470 +w = (small1(b) + g + small0(t) + u : U32)
471 kr47(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 4094571909, w))
472
473# Return the SHA-256 round constant for schedule index 45.
474def kr45(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
475 match rounds_left win:
476 case 0n _:
477 state
478 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
479 +w = (small1(b) + g + small0(t) + u : U32)
480 kr46(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3600352804, w))
481
482# Return the SHA-256 round constant for schedule index 44.
483def kr44(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
484 match rounds_left win:
485 case 0n _:
486 state
487 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
488 +w = (small1(b) + g + small0(t) + u : U32)
489 kr45(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3516065817, w))
490
491# Return the SHA-256 round constant for schedule index 43.
492def kr43(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
493 match rounds_left win:
494 case 0n _:
495 state
496 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
497 +w = (small1(b) + g + small0(t) + u : U32)
498 kr44(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3345764771, w))
499
500# Return the SHA-256 round constant for schedule index 42.
501def kr42(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
502 match rounds_left win:
503 case 0n _:
504 state
505 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
506 +w = (small1(b) + g + small0(t) + u : U32)
507 kr43(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3259730800, w))
508
509# Return the SHA-256 round constant for schedule index 41.
510def kr41(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
511 match rounds_left win:
512 case 0n _:
513 state
514 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
515 +w = (small1(b) + g + small0(t) + u : U32)
516 kr42(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2820302411, w))
517
518# Return the SHA-256 round constant for schedule index 40.
519def kr40(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
520 match rounds_left win:
521 case 0n _:
522 state
523 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
524 +w = (small1(b) + g + small0(t) + u : U32)
525 kr41(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2730485921, w))
526
527# Return the SHA-256 round constant for schedule index 39.
528def kr39(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
529 match rounds_left win:
530 case 0n _:
531 state
532 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
533 +w = (small1(b) + g + small0(t) + u : U32)
534 kr40(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2456956037, w))
535
536# Return the SHA-256 round constant for schedule index 38.
537def kr38(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
538 match rounds_left win:
539 case 0n _:
540 state
541 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
542 +w = (small1(b) + g + small0(t) + u : U32)
543 kr39(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2177026350, w))
544
545# Return the SHA-256 round constant for schedule index 37.
546def kr37(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
547 match rounds_left win:
548 case 0n _:
549 state
550 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
551 +w = (small1(b) + g + small0(t) + u : U32)
552 kr38(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1986661051, w))
553
554# Return the SHA-256 round constant for schedule index 36.
555def kr36(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
556 match rounds_left win:
557 case 0n _:
558 state
559 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
560 +w = (small1(b) + g + small0(t) + u : U32)
561 kr37(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1695183700, w))
562
563# Return the SHA-256 round constant for schedule index 35.
564def kr35(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
565 match rounds_left win:
566 case 0n _:
567 state
568 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
569 +w = (small1(b) + g + small0(t) + u : U32)
570 kr36(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1396182291, w))
571
572# Return the SHA-256 round constant for schedule index 34.
573def kr34(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
574 match rounds_left win:
575 case 0n _:
576 state
577 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
578 +w = (small1(b) + g + small0(t) + u : U32)
579 kr35(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1294757372, w))
580
581# Return the SHA-256 round constant for schedule index 33.
582def kr33(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
583 match rounds_left win:
584 case 0n _:
585 state
586 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
587 +w = (small1(b) + g + small0(t) + u : U32)
588 kr34(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 773529912, w))
589
590# Return the SHA-256 round constant for schedule index 32.
591def kr32(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
592 match rounds_left win:
593 case 0n _:
594 state
595 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
596 +w = (small1(b) + g + small0(t) + u : U32)
597 kr33(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 666307205, w))
598
599# Return the SHA-256 round constant for schedule index 31.
600def kr31(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
601 match rounds_left win:
602 case 0n _:
603 state
604 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
605 +w = (small1(b) + g + small0(t) + u : U32)
606 kr32(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 338241895, w))
607
608# Return the SHA-256 round constant for schedule index 30.
609def kr30(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
610 match rounds_left win:
611 case 0n _:
612 state
613 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
614 +w = (small1(b) + g + small0(t) + u : U32)
615 kr31(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 113926993, w))
616
617# Return the SHA-256 round constant for schedule index 29.
618def kr29(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
619 match rounds_left win:
620 case 0n _:
621 state
622 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
623 +w = (small1(b) + g + small0(t) + u : U32)
624 kr30(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3584528711, w))
625
626# Return the SHA-256 round constant for schedule index 28.
627def kr28(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
628 match rounds_left win:
629 case 0n _:
630 state
631 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
632 +w = (small1(b) + g + small0(t) + u : U32)
633 kr29(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3336571891, w))
634
635# Return the SHA-256 round constant for schedule index 27.
636def kr27(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
637 match rounds_left win:
638 case 0n _:
639 state
640 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
641 +w = (small1(b) + g + small0(t) + u : U32)
642 kr28(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3210313671, w))
643
644# Return the SHA-256 round constant for schedule index 26.
645def kr26(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
646 match rounds_left win:
647 case 0n _:
648 state
649 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
650 +w = (small1(b) + g + small0(t) + u : U32)
651 kr27(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2952996808, w))
652
653# Return the SHA-256 round constant for schedule index 25.
654def kr25(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
655 match rounds_left win:
656 case 0n _:
657 state
658 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
659 +w = (small1(b) + g + small0(t) + u : U32)
660 kr26(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2821834349, w))
661
662# Return the SHA-256 round constant for schedule index 24.
663def kr24(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
664 match rounds_left win:
665 case 0n _:
666 state
667 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
668 +w = (small1(b) + g + small0(t) + u : U32)
669 kr25(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2554220882, w))
670
671# Return the SHA-256 round constant for schedule index 23.
672def kr23(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
673 match rounds_left win:
674 case 0n _:
675 state
676 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
677 +w = (small1(b) + g + small0(t) + u : U32)
678 kr24(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1996064986, w))
679
680# Return the SHA-256 round constant for schedule index 22.
681def kr22(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
682 match rounds_left win:
683 case 0n _:
684 state
685 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
686 +w = (small1(b) + g + small0(t) + u : U32)
687 kr23(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1555081692, w))
688
689# Return the SHA-256 round constant for schedule index 21.
690def kr21(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
691 match rounds_left win:
692 case 0n _:
693 state
694 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
695 +w = (small1(b) + g + small0(t) + u : U32)
696 kr22(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1249150122, w))
697
698# Return the SHA-256 round constant for schedule index 20.
699def kr20(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
700 match rounds_left win:
701 case 0n _:
702 state
703 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
704 +w = (small1(b) + g + small0(t) + u : U32)
705 kr21(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 770255983, w))
706
707# Return the SHA-256 round constant for schedule index 19.
708def kr19(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
709 match rounds_left win:
710 case 0n _:
711 state
712 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
713 +w = (small1(b) + g + small0(t) + u : U32)
714 kr20(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 604807628, w))
715
716# Return the SHA-256 round constant for schedule index 18.
717def kr18(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
718 match rounds_left win:
719 case 0n _:
720 state
721 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
722 +w = (small1(b) + g + small0(t) + u : U32)
723 kr19(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 264347078, w))
724
725# Return the SHA-256 round constant for schedule index 17.
726def kr17(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
727 match rounds_left win:
728 case 0n _:
729 state
730 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
731 +w = (small1(b) + g + small0(t) + u : U32)
732 kr18(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 4022224774, w))
733
734# Return the SHA-256 round constant for schedule index 16.
735def kr16(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
736 match rounds_left win:
737 case 0n _:
738 state
739 case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
740 +w = (small1(b) + g + small0(t) + u : U32)
741 kr17(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3835390401, w))
742
743# window_compress16 specialized to the FIPS table: no constant list is walked.
744def fips_compress16(
745 +word_a: U32,
746 +word_b: U32,
747 +word_c: U32,
748 +word_d: U32,
749 +word_e: U32,
750 +word_f: U32,
751 +word_g: U32,
752 +word_h: U32,
753 +word_i: U32,
754 +word_j: U32,
755 +round_constant: U32,
756 +word_l: U32,
757 +word_m: U32,
758 +count: U32,
759 +word_o: U32,
760 +word_p: U32,
761 +rounds_left: Nat,
762 +state: S.State
763) -> S.State:
764 s1 = step(state, 1116352408, word_a)
765 s2 = step(s1, 1899447441, word_b)
766 s3 = step(s2, 3049323471, word_c)
767 s4 = step(s3, 3921009573, word_d)
768 s5 = step(s4, 961987163, word_e)
769 s6 = step(s5, 1508970993, word_f)
770 s7 = step(s6, 2453635748, word_g)
771 s8 = step(s7, 2870763221, word_h)
772 s9 = step(s8, 3624381080, word_i)
773 s10 = step(s9, 310598401, word_j)
774 s11 = step(s10, 607225278, round_constant)
775 s12 = step(s11, 1426881987, word_l)
776 s13 = step(s12, 1925078388, word_m)
777 s14 = step(s13, 2162078206, count)
778 s15 = step(s14, 2614888103, word_o)
779 s16 = step(s15, 3248222580, word_p)
780 feedforward(state, kr16(rounds_left, W{word_p, word_o, count, word_m, word_l, round_constant, word_j, word_i, word_h, word_g, word_f, word_e, word_d, word_c, word_b, word_a}, s16))
781
782# FIPS padding suffix for a message of n bytes, computed with modular
783# arithmetic. The proofs state the streaming hash in terms of it.
784def suffix(+byte_length: Nat) -> List<&2, U32>:
785 128 <> List.append(&2, U32,
786 List.replicate(U32, Nat.mod(Nat.sub(119n, Nat.mod(byte_length, 64n)), 64n), 0), bit_length(byte_length))
787
788# Big-endian words of the 64-bit message bit length 8n, computed from n with
789# exactly the digit expressions bit_length produces, but without building and
790# matching an eight-element list. bit_length(n) is [o(d6), .., o(d0), low]
791# where d0 = n / 32, d(k+1) = dk / 256 and o(x) = x mod 256.
792def len_hi(+byte_length: Nat) -> U32:
793 +d0 = Nat.div(byte_length, 32n)
794 +d1 = Nat.div(d0, 256n)
795 +d2 = Nat.div(d1, 256n)
796 +d3 = Nat.div(d2, 256n)
797 +d4 = Nat.div(d3, 256n)
798 +d5 = Nat.div(d4, 256n)
799 +d6 = Nat.div(d5, 256n)
800 pack(U32.from_nat(Nat.mod(d6, 256n)), U32.from_nat(Nat.mod(d5, 256n)),
801 U32.from_nat(Nat.mod(d4, 256n)), U32.from_nat(Nat.mod(d3, 256n)))
802
803# Return the length of lo in the SHA-256 compression implementation.
804def len_lo(+byte_length: Nat) -> U32:
805 +d0 = Nat.div(byte_length, 32n)
806 +d1 = Nat.div(d0, 256n)
807 +d2 = Nat.div(d1, 256n)
808 pack(U32.from_nat(Nat.mod(d2, 256n)), U32.from_nat(Nat.mod(d1, 256n)),
809 U32.from_nat(Nat.mod(d0, 256n)), U32.shln(U32.from_nat(Nat.mod(byte_length, 32n)), 3n))
810
811# Final block(s) for an n-byte message ending in r = 0..63 tail bytes. Each
812# tail length has its own padded layout: the tail bytes, the 0x80 marker, the
813# zero fill and the big-endian bit length are packed straight into schedule
814# words, so no padded list is built.
815def fin0(+byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
816 fips_compress16(pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
817 extra, state)
818
819# Apply SHA-256 round 1 to the compression state.
820def fin1(+t0: U32, +byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
821 fips_compress16(pack(t0, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
822 extra, state)
823
824# Apply SHA-256 round 2 to the compression state.
825def fin2(+t0: U32, +t1: U32, +byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
826 fips_compress16(pack(t0, t1, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
827 extra, state)
828
829# Apply SHA-256 round 3 to the compression state.
830def fin3(+t0: U32, +t1: U32, +t2: U32, +byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
831 fips_compress16(pack(t0, t1, t2, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
832 extra, state)
833
834# Apply SHA-256 round 4 to the compression state.
835def fin4(
836 +t0: U32,
837 +t1: U32,
838 +t2: U32,
839 +t3: U32,
840 +byte_length: Nat,
841 +extra: Nat,
842 state: S.State
843) -> S.State:
844 fips_compress16(pack(t0, t1, t2, t3), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
845 extra, state)
846
847# Apply SHA-256 round 5 to the compression state.
848def fin5(
849 +t0: U32,
850 +t1: U32,
851 +t2: U32,
852 +t3: U32,
853 +t4: U32,
854 +byte_length: Nat,
855 +extra: Nat,
856 state: S.State
857) -> S.State:
858 fips_compress16(pack(t0, t1, t2, t3), pack(t4, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
859 extra, state)
860
861# Apply SHA-256 round 6 to the compression state.
862def fin6(
863 +t0: U32,
864 +t1: U32,
865 +t2: U32,
866 +t3: U32,
867 +t4: U32,
868 +t5: U32,
869 +byte_length: Nat,
870 +extra: Nat,
871 state: S.State
872) -> S.State:
873 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
874 extra, state)
875
876# Apply SHA-256 round 7 to the compression state.
877def fin7(
878 +t0: U32,
879 +t1: U32,
880 +t2: U32,
881 +t3: U32,
882 +t4: U32,
883 +t5: U32,
884 +t6: U32,
885 +byte_length: Nat,
886 +extra: Nat,
887 state: S.State
888) -> S.State:
889 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
890 extra, state)
891
892# Apply SHA-256 round 8 to the compression state.
893def fin8(
894 +t0: U32,
895 +t1: U32,
896 +t2: U32,
897 +t3: U32,
898 +t4: U32,
899 +t5: U32,
900 +t6: U32,
901 +t7: U32,
902 +byte_length: Nat,
903 +extra: Nat,
904 state: S.State
905) -> S.State:
906 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
907 extra, state)
908
909# Apply SHA-256 round 9 to the compression state.
910def fin9(
911 +t0: U32,
912 +t1: U32,
913 +t2: U32,
914 +t3: U32,
915 +t4: U32,
916 +t5: U32,
917 +t6: U32,
918 +t7: U32,
919 +t8: U32,
920 +byte_length: Nat,
921 +extra: Nat,
922 state: S.State
923) -> S.State:
924 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
925 extra, state)
926
927# Apply SHA-256 round 10 to the compression state.
928def fin10(
929 +t0: U32,
930 +t1: U32,
931 +t2: U32,
932 +t3: U32,
933 +t4: U32,
934 +t5: U32,
935 +t6: U32,
936 +t7: U32,
937 +t8: U32,
938 +t9: U32,
939 +byte_length: Nat,
940 +extra: Nat,
941 state: S.State
942) -> S.State:
943 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
944 extra, state)
945
946# Apply SHA-256 round 11 to the compression state.
947def fin11(
948 +t0: U32,
949 +t1: U32,
950 +t2: U32,
951 +t3: U32,
952 +t4: U32,
953 +t5: U32,
954 +t6: U32,
955 +t7: U32,
956 +t8: U32,
957 +t9: U32,
958 +t10: U32,
959 +byte_length: Nat,
960 +extra: Nat,
961 state: S.State
962) -> S.State:
963 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
964 extra, state)
965
966# Apply SHA-256 round 12 to the compression state.
967def fin12(
968 +t0: U32,
969 +t1: U32,
970 +t2: U32,
971 +t3: U32,
972 +t4: U32,
973 +t5: U32,
974 +t6: U32,
975 +t7: U32,
976 +t8: U32,
977 +t9: U32,
978 +t10: U32,
979 +t11: U32,
980 +byte_length: Nat,
981 +extra: Nat,
982 state: S.State
983) -> S.State:
984 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
985 extra, state)
986
987# Apply SHA-256 round 13 to the compression state.
988def fin13(
989 +t0: U32,
990 +t1: U32,
991 +t2: U32,
992 +t3: U32,
993 +t4: U32,
994 +t5: U32,
995 +t6: U32,
996 +t7: U32,
997 +t8: U32,
998 +t9: U32,
999 +t10: U32,
1000 +t11: U32,
1001 +t12: U32,
1002 +byte_length: Nat,
1003 +extra: Nat,
1004 state: S.State
1005) -> S.State:
1006 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1007 extra, state)
1008
1009# Apply SHA-256 round 14 to the compression state.
1010def fin14(
1011 +t0: U32,
1012 +t1: U32,
1013 +t2: U32,
1014 +t3: U32,
1015 +t4: U32,
1016 +t5: U32,
1017 +t6: U32,
1018 +t7: U32,
1019 +t8: U32,
1020 +t9: U32,
1021 +t10: U32,
1022 +t11: U32,
1023 +t12: U32,
1024 +t13: U32,
1025 +byte_length: Nat,
1026 +extra: Nat,
1027 state: S.State
1028) -> S.State:
1029 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1030 extra, state)
1031
1032# Apply SHA-256 round 15 to the compression state.
1033def fin15(
1034 +t0: U32,
1035 +t1: U32,
1036 +t2: U32,
1037 +t3: U32,
1038 +t4: U32,
1039 +t5: U32,
1040 +t6: U32,
1041 +t7: U32,
1042 +t8: U32,
1043 +t9: U32,
1044 +t10: U32,
1045 +t11: U32,
1046 +t12: U32,
1047 +t13: U32,
1048 +t14: U32,
1049 +byte_length: Nat,
1050 +extra: Nat,
1051 state: S.State
1052) -> S.State:
1053 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1054 extra, state)
1055
1056# Apply SHA-256 round 16 to the compression state.
1057def fin16(
1058 +t0: U32,
1059 +t1: U32,
1060 +t2: U32,
1061 +t3: U32,
1062 +t4: U32,
1063 +t5: U32,
1064 +t6: U32,
1065 +t7: U32,
1066 +t8: U32,
1067 +t9: U32,
1068 +t10: U32,
1069 +t11: U32,
1070 +t12: U32,
1071 +t13: U32,
1072 +t14: U32,
1073 +t15: U32,
1074 +byte_length: Nat,
1075 +extra: Nat,
1076 state: S.State
1077) -> S.State:
1078 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1079 extra, state)
1080
1081# Apply SHA-256 round 17 to the compression state.
1082def fin17(
1083 +t0: U32,
1084 +t1: U32,
1085 +t2: U32,
1086 +t3: U32,
1087 +t4: U32,
1088 +t5: U32,
1089 +t6: U32,
1090 +t7: U32,
1091 +t8: U32,
1092 +t9: U32,
1093 +t10: U32,
1094 +t11: U32,
1095 +t12: U32,
1096 +t13: U32,
1097 +t14: U32,
1098 +t15: U32,
1099 +t16: U32,
1100 +byte_length: Nat,
1101 +extra: Nat,
1102 state: S.State
1103) -> S.State:
1104 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1105 extra, state)
1106
1107# Apply SHA-256 round 18 to the compression state.
1108def fin18(
1109 +t0: U32,
1110 +t1: U32,
1111 +t2: U32,
1112 +t3: U32,
1113 +t4: U32,
1114 +t5: U32,
1115 +t6: U32,
1116 +t7: U32,
1117 +t8: U32,
1118 +t9: U32,
1119 +t10: U32,
1120 +t11: U32,
1121 +t12: U32,
1122 +t13: U32,
1123 +t14: U32,
1124 +t15: U32,
1125 +t16: U32,
1126 +t17: U32,
1127 +byte_length: Nat,
1128 +extra: Nat,
1129 state: S.State
1130) -> S.State:
1131 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1132 extra, state)
1133
1134# Apply SHA-256 round 19 to the compression state.
1135def fin19(
1136 +t0: U32,
1137 +t1: U32,
1138 +t2: U32,
1139 +t3: U32,
1140 +t4: U32,
1141 +t5: U32,
1142 +t6: U32,
1143 +t7: U32,
1144 +t8: U32,
1145 +t9: U32,
1146 +t10: U32,
1147 +t11: U32,
1148 +t12: U32,
1149 +t13: U32,
1150 +t14: U32,
1151 +t15: U32,
1152 +t16: U32,
1153 +t17: U32,
1154 +t18: U32,
1155 +byte_length: Nat,
1156 +extra: Nat,
1157 state: S.State
1158) -> S.State:
1159 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1160 extra, state)
1161
1162# Apply SHA-256 round 20 to the compression state.
1163def fin20(
1164 +t0: U32,
1165 +t1: U32,
1166 +t2: U32,
1167 +t3: U32,
1168 +t4: U32,
1169 +t5: U32,
1170 +t6: U32,
1171 +t7: U32,
1172 +t8: U32,
1173 +t9: U32,
1174 +t10: U32,
1175 +t11: U32,
1176 +t12: U32,
1177 +t13: U32,
1178 +t14: U32,
1179 +t15: U32,
1180 +t16: U32,
1181 +t17: U32,
1182 +t18: U32,
1183 +t19: U32,
1184 +byte_length: Nat,
1185 +extra: Nat,
1186 state: S.State
1187) -> S.State:
1188 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1189 extra, state)
1190
1191# Apply SHA-256 round 21 to the compression state.
1192def fin21(
1193 +t0: U32,
1194 +t1: U32,
1195 +t2: U32,
1196 +t3: U32,
1197 +t4: U32,
1198 +t5: U32,
1199 +t6: U32,
1200 +t7: U32,
1201 +t8: U32,
1202 +t9: U32,
1203 +t10: U32,
1204 +t11: U32,
1205 +t12: U32,
1206 +t13: U32,
1207 +t14: U32,
1208 +t15: U32,
1209 +t16: U32,
1210 +t17: U32,
1211 +t18: U32,
1212 +t19: U32,
1213 +t20: U32,
1214 +byte_length: Nat,
1215 +extra: Nat,
1216 state: S.State
1217) -> S.State:
1218 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1219 extra, state)
1220
1221# Apply SHA-256 round 22 to the compression state.
1222def fin22(
1223 +t0: U32,
1224 +t1: U32,
1225 +t2: U32,
1226 +t3: U32,
1227 +t4: U32,
1228 +t5: U32,
1229 +t6: U32,
1230 +t7: U32,
1231 +t8: U32,
1232 +t9: U32,
1233 +t10: U32,
1234 +t11: U32,
1235 +t12: U32,
1236 +t13: U32,
1237 +t14: U32,
1238 +t15: U32,
1239 +t16: U32,
1240 +t17: U32,
1241 +t18: U32,
1242 +t19: U32,
1243 +t20: U32,
1244 +t21: U32,
1245 +byte_length: Nat,
1246 +extra: Nat,
1247 state: S.State
1248) -> S.State:
1249 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1250 extra, state)
1251
1252# Apply SHA-256 round 23 to the compression state.
1253def fin23(
1254 +t0: U32,
1255 +t1: U32,
1256 +t2: U32,
1257 +t3: U32,
1258 +t4: U32,
1259 +t5: U32,
1260 +t6: U32,
1261 +t7: U32,
1262 +t8: U32,
1263 +t9: U32,
1264 +t10: U32,
1265 +t11: U32,
1266 +t12: U32,
1267 +t13: U32,
1268 +t14: U32,
1269 +t15: U32,
1270 +t16: U32,
1271 +t17: U32,
1272 +t18: U32,
1273 +t19: U32,
1274 +t20: U32,
1275 +t21: U32,
1276 +t22: U32,
1277 +byte_length: Nat,
1278 +extra: Nat,
1279 state: S.State
1280) -> S.State:
1281 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1282 extra, state)
1283
1284# Apply SHA-256 round 24 to the compression state.
1285def fin24(
1286 +t0: U32,
1287 +t1: U32,
1288 +t2: U32,
1289 +t3: U32,
1290 +t4: U32,
1291 +t5: U32,
1292 +t6: U32,
1293 +t7: U32,
1294 +t8: U32,
1295 +t9: U32,
1296 +t10: U32,
1297 +t11: U32,
1298 +t12: U32,
1299 +t13: U32,
1300 +t14: U32,
1301 +t15: U32,
1302 +t16: U32,
1303 +t17: U32,
1304 +t18: U32,
1305 +t19: U32,
1306 +t20: U32,
1307 +t21: U32,
1308 +t22: U32,
1309 +t23: U32,
1310 +byte_length: Nat,
1311 +extra: Nat,
1312 state: S.State
1313) -> S.State:
1314 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1315 extra, state)
1316
1317# Apply SHA-256 round 25 to the compression state.
1318def fin25(
1319 +t0: U32,
1320 +t1: U32,
1321 +t2: U32,
1322 +t3: U32,
1323 +t4: U32,
1324 +t5: U32,
1325 +t6: U32,
1326 +t7: U32,
1327 +t8: U32,
1328 +t9: U32,
1329 +t10: U32,
1330 +t11: U32,
1331 +t12: U32,
1332 +t13: U32,
1333 +t14: U32,
1334 +t15: U32,
1335 +t16: U32,
1336 +t17: U32,
1337 +t18: U32,
1338 +t19: U32,
1339 +t20: U32,
1340 +t21: U32,
1341 +t22: U32,
1342 +t23: U32,
1343 +t24: U32,
1344 +byte_length: Nat,
1345 +extra: Nat,
1346 state: S.State
1347) -> S.State:
1348 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1349 extra, state)
1350
1351# Apply SHA-256 round 26 to the compression state.
1352def fin26(
1353 +t0: U32,
1354 +t1: U32,
1355 +t2: U32,
1356 +t3: U32,
1357 +t4: U32,
1358 +t5: U32,
1359 +t6: U32,
1360 +t7: U32,
1361 +t8: U32,
1362 +t9: U32,
1363 +t10: U32,
1364 +t11: U32,
1365 +t12: U32,
1366 +t13: U32,
1367 +t14: U32,
1368 +t15: U32,
1369 +t16: U32,
1370 +t17: U32,
1371 +t18: U32,
1372 +t19: U32,
1373 +t20: U32,
1374 +t21: U32,
1375 +t22: U32,
1376 +t23: U32,
1377 +t24: U32,
1378 +t25: U32,
1379 +byte_length: Nat,
1380 +extra: Nat,
1381 state: S.State
1382) -> S.State:
1383 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1384 extra, state)
1385
1386# Apply SHA-256 round 27 to the compression state.
1387def fin27(
1388 +t0: U32,
1389 +t1: U32,
1390 +t2: U32,
1391 +t3: U32,
1392 +t4: U32,
1393 +t5: U32,
1394 +t6: U32,
1395 +t7: U32,
1396 +t8: U32,
1397 +t9: U32,
1398 +t10: U32,
1399 +t11: U32,
1400 +t12: U32,
1401 +t13: U32,
1402 +t14: U32,
1403 +t15: U32,
1404 +t16: U32,
1405 +t17: U32,
1406 +t18: U32,
1407 +t19: U32,
1408 +t20: U32,
1409 +t21: U32,
1410 +t22: U32,
1411 +t23: U32,
1412 +t24: U32,
1413 +t25: U32,
1414 +t26: U32,
1415 +byte_length: Nat,
1416 +extra: Nat,
1417 state: S.State
1418) -> S.State:
1419 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1420 extra, state)
1421
1422# Apply SHA-256 round 28 to the compression state.
1423def fin28(
1424 +t0: U32,
1425 +t1: U32,
1426 +t2: U32,
1427 +t3: U32,
1428 +t4: U32,
1429 +t5: U32,
1430 +t6: U32,
1431 +t7: U32,
1432 +t8: U32,
1433 +t9: U32,
1434 +t10: U32,
1435 +t11: U32,
1436 +t12: U32,
1437 +t13: U32,
1438 +t14: U32,
1439 +t15: U32,
1440 +t16: U32,
1441 +t17: U32,
1442 +t18: U32,
1443 +t19: U32,
1444 +t20: U32,
1445 +t21: U32,
1446 +t22: U32,
1447 +t23: U32,
1448 +t24: U32,
1449 +t25: U32,
1450 +t26: U32,
1451 +t27: U32,
1452 +byte_length: Nat,
1453 +extra: Nat,
1454 state: S.State
1455) -> S.State:
1456 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1457 extra, state)
1458
1459# Apply SHA-256 round 29 to the compression state.
1460def fin29(
1461 +t0: U32,
1462 +t1: U32,
1463 +t2: U32,
1464 +t3: U32,
1465 +t4: U32,
1466 +t5: U32,
1467 +t6: U32,
1468 +t7: U32,
1469 +t8: U32,
1470 +t9: U32,
1471 +t10: U32,
1472 +t11: U32,
1473 +t12: U32,
1474 +t13: U32,
1475 +t14: U32,
1476 +t15: U32,
1477 +t16: U32,
1478 +t17: U32,
1479 +t18: U32,
1480 +t19: U32,
1481 +t20: U32,
1482 +t21: U32,
1483 +t22: U32,
1484 +t23: U32,
1485 +t24: U32,
1486 +t25: U32,
1487 +t26: U32,
1488 +t27: U32,
1489 +t28: U32,
1490 +byte_length: Nat,
1491 +extra: Nat,
1492 state: S.State
1493) -> S.State:
1494 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1495 extra, state)
1496
1497# Apply SHA-256 round 30 to the compression state.
1498def fin30(
1499 +t0: U32,
1500 +t1: U32,
1501 +t2: U32,
1502 +t3: U32,
1503 +t4: U32,
1504 +t5: U32,
1505 +t6: U32,
1506 +t7: U32,
1507 +t8: U32,
1508 +t9: U32,
1509 +t10: U32,
1510 +t11: U32,
1511 +t12: U32,
1512 +t13: U32,
1513 +t14: U32,
1514 +t15: U32,
1515 +t16: U32,
1516 +t17: U32,
1517 +t18: U32,
1518 +t19: U32,
1519 +t20: U32,
1520 +t21: U32,
1521 +t22: U32,
1522 +t23: U32,
1523 +t24: U32,
1524 +t25: U32,
1525 +t26: U32,
1526 +t27: U32,
1527 +t28: U32,
1528 +t29: U32,
1529 +byte_length: Nat,
1530 +extra: Nat,
1531 state: S.State
1532) -> S.State:
1533 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1534 extra, state)
1535
1536# Apply SHA-256 round 31 to the compression state.
1537def fin31(
1538 +t0: U32,
1539 +t1: U32,
1540 +t2: U32,
1541 +t3: U32,
1542 +t4: U32,
1543 +t5: U32,
1544 +t6: U32,
1545 +t7: U32,
1546 +t8: U32,
1547 +t9: U32,
1548 +t10: U32,
1549 +t11: U32,
1550 +t12: U32,
1551 +t13: U32,
1552 +t14: U32,
1553 +t15: U32,
1554 +t16: U32,
1555 +t17: U32,
1556 +t18: U32,
1557 +t19: U32,
1558 +t20: U32,
1559 +t21: U32,
1560 +t22: U32,
1561 +t23: U32,
1562 +t24: U32,
1563 +t25: U32,
1564 +t26: U32,
1565 +t27: U32,
1566 +t28: U32,
1567 +t29: U32,
1568 +t30: U32,
1569 +byte_length: Nat,
1570 +extra: Nat,
1571 state: S.State
1572) -> S.State:
1573 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1574 extra, state)
1575
1576# Apply SHA-256 round 32 to the compression state.
1577def fin32(
1578 +t0: U32,
1579 +t1: U32,
1580 +t2: U32,
1581 +t3: U32,
1582 +t4: U32,
1583 +t5: U32,
1584 +t6: U32,
1585 +t7: U32,
1586 +t8: U32,
1587 +t9: U32,
1588 +t10: U32,
1589 +t11: U32,
1590 +t12: U32,
1591 +t13: U32,
1592 +t14: U32,
1593 +t15: U32,
1594 +t16: U32,
1595 +t17: U32,
1596 +t18: U32,
1597 +t19: U32,
1598 +t20: U32,
1599 +t21: U32,
1600 +t22: U32,
1601 +t23: U32,
1602 +t24: U32,
1603 +t25: U32,
1604 +t26: U32,
1605 +t27: U32,
1606 +t28: U32,
1607 +t29: U32,
1608 +t30: U32,
1609 +t31: U32,
1610 +byte_length: Nat,
1611 +extra: Nat,
1612 state: S.State
1613) -> S.State:
1614 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1615 extra, state)
1616
1617# Apply SHA-256 round 33 to the compression state.
1618def fin33(
1619 +t0: U32,
1620 +t1: U32,
1621 +t2: U32,
1622 +t3: U32,
1623 +t4: U32,
1624 +t5: U32,
1625 +t6: U32,
1626 +t7: U32,
1627 +t8: U32,
1628 +t9: U32,
1629 +t10: U32,
1630 +t11: U32,
1631 +t12: U32,
1632 +t13: U32,
1633 +t14: U32,
1634 +t15: U32,
1635 +t16: U32,
1636 +t17: U32,
1637 +t18: U32,
1638 +t19: U32,
1639 +t20: U32,
1640 +t21: U32,
1641 +t22: U32,
1642 +t23: U32,
1643 +t24: U32,
1644 +t25: U32,
1645 +t26: U32,
1646 +t27: U32,
1647 +t28: U32,
1648 +t29: U32,
1649 +t30: U32,
1650 +t31: U32,
1651 +t32: U32,
1652 +byte_length: Nat,
1653 +extra: Nat,
1654 state: S.State
1655) -> S.State:
1656 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1657 extra, state)
1658
1659# Apply SHA-256 round 34 to the compression state.
1660def fin34(
1661 +t0: U32,
1662 +t1: U32,
1663 +t2: U32,
1664 +t3: U32,
1665 +t4: U32,
1666 +t5: U32,
1667 +t6: U32,
1668 +t7: U32,
1669 +t8: U32,
1670 +t9: U32,
1671 +t10: U32,
1672 +t11: U32,
1673 +t12: U32,
1674 +t13: U32,
1675 +t14: U32,
1676 +t15: U32,
1677 +t16: U32,
1678 +t17: U32,
1679 +t18: U32,
1680 +t19: U32,
1681 +t20: U32,
1682 +t21: U32,
1683 +t22: U32,
1684 +t23: U32,
1685 +t24: U32,
1686 +t25: U32,
1687 +t26: U32,
1688 +t27: U32,
1689 +t28: U32,
1690 +t29: U32,
1691 +t30: U32,
1692 +t31: U32,
1693 +t32: U32,
1694 +t33: U32,
1695 +byte_length: Nat,
1696 +extra: Nat,
1697 state: S.State
1698) -> S.State:
1699 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1700 extra, state)
1701
1702# Apply SHA-256 round 35 to the compression state.
1703def fin35(
1704 +t0: U32,
1705 +t1: U32,
1706 +t2: U32,
1707 +t3: U32,
1708 +t4: U32,
1709 +t5: U32,
1710 +t6: U32,
1711 +t7: U32,
1712 +t8: U32,
1713 +t9: U32,
1714 +t10: U32,
1715 +t11: U32,
1716 +t12: U32,
1717 +t13: U32,
1718 +t14: U32,
1719 +t15: U32,
1720 +t16: U32,
1721 +t17: U32,
1722 +t18: U32,
1723 +t19: U32,
1724 +t20: U32,
1725 +t21: U32,
1726 +t22: U32,
1727 +t23: U32,
1728 +t24: U32,
1729 +t25: U32,
1730 +t26: U32,
1731 +t27: U32,
1732 +t28: U32,
1733 +t29: U32,
1734 +t30: U32,
1735 +t31: U32,
1736 +t32: U32,
1737 +t33: U32,
1738 +t34: U32,
1739 +byte_length: Nat,
1740 +extra: Nat,
1741 state: S.State
1742) -> S.State:
1743 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1744 extra, state)
1745
1746# Apply SHA-256 round 36 to the compression state.
1747def fin36(
1748 +t0: U32,
1749 +t1: U32,
1750 +t2: U32,
1751 +t3: U32,
1752 +t4: U32,
1753 +t5: U32,
1754 +t6: U32,
1755 +t7: U32,
1756 +t8: U32,
1757 +t9: U32,
1758 +t10: U32,
1759 +t11: U32,
1760 +t12: U32,
1761 +t13: U32,
1762 +t14: U32,
1763 +t15: U32,
1764 +t16: U32,
1765 +t17: U32,
1766 +t18: U32,
1767 +t19: U32,
1768 +t20: U32,
1769 +t21: U32,
1770 +t22: U32,
1771 +t23: U32,
1772 +t24: U32,
1773 +t25: U32,
1774 +t26: U32,
1775 +t27: U32,
1776 +t28: U32,
1777 +t29: U32,
1778 +t30: U32,
1779 +t31: U32,
1780 +t32: U32,
1781 +t33: U32,
1782 +t34: U32,
1783 +t35: U32,
1784 +byte_length: Nat,
1785 +extra: Nat,
1786 state: S.State
1787) -> S.State:
1788 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1789 extra, state)
1790
1791# Apply SHA-256 round 37 to the compression state.
1792def fin37(
1793 +t0: U32,
1794 +t1: U32,
1795 +t2: U32,
1796 +t3: U32,
1797 +t4: U32,
1798 +t5: U32,
1799 +t6: U32,
1800 +t7: U32,
1801 +t8: U32,
1802 +t9: U32,
1803 +t10: U32,
1804 +t11: U32,
1805 +t12: U32,
1806 +t13: U32,
1807 +t14: U32,
1808 +t15: U32,
1809 +t16: U32,
1810 +t17: U32,
1811 +t18: U32,
1812 +t19: U32,
1813 +t20: U32,
1814 +t21: U32,
1815 +t22: U32,
1816 +t23: U32,
1817 +t24: U32,
1818 +t25: U32,
1819 +t26: U32,
1820 +t27: U32,
1821 +t28: U32,
1822 +t29: U32,
1823 +t30: U32,
1824 +t31: U32,
1825 +t32: U32,
1826 +t33: U32,
1827 +t34: U32,
1828 +t35: U32,
1829 +t36: U32,
1830 +byte_length: Nat,
1831 +extra: Nat,
1832 state: S.State
1833) -> S.State:
1834 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1835 extra, state)
1836
1837# Apply SHA-256 round 38 to the compression state.
1838def fin38(
1839 +t0: U32,
1840 +t1: U32,
1841 +t2: U32,
1842 +t3: U32,
1843 +t4: U32,
1844 +t5: U32,
1845 +t6: U32,
1846 +t7: U32,
1847 +t8: U32,
1848 +t9: U32,
1849 +t10: U32,
1850 +t11: U32,
1851 +t12: U32,
1852 +t13: U32,
1853 +t14: U32,
1854 +t15: U32,
1855 +t16: U32,
1856 +t17: U32,
1857 +t18: U32,
1858 +t19: U32,
1859 +t20: U32,
1860 +t21: U32,
1861 +t22: U32,
1862 +t23: U32,
1863 +t24: U32,
1864 +t25: U32,
1865 +t26: U32,
1866 +t27: U32,
1867 +t28: U32,
1868 +t29: U32,
1869 +t30: U32,
1870 +t31: U32,
1871 +t32: U32,
1872 +t33: U32,
1873 +t34: U32,
1874 +t35: U32,
1875 +t36: U32,
1876 +t37: U32,
1877 +byte_length: Nat,
1878 +extra: Nat,
1879 state: S.State
1880) -> S.State:
1881 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1882 extra, state)
1883
1884# Apply SHA-256 round 39 to the compression state.
1885def fin39(
1886 +t0: U32,
1887 +t1: U32,
1888 +t2: U32,
1889 +t3: U32,
1890 +t4: U32,
1891 +t5: U32,
1892 +t6: U32,
1893 +t7: U32,
1894 +t8: U32,
1895 +t9: U32,
1896 +t10: U32,
1897 +t11: U32,
1898 +t12: U32,
1899 +t13: U32,
1900 +t14: U32,
1901 +t15: U32,
1902 +t16: U32,
1903 +t17: U32,
1904 +t18: U32,
1905 +t19: U32,
1906 +t20: U32,
1907 +t21: U32,
1908 +t22: U32,
1909 +t23: U32,
1910 +t24: U32,
1911 +t25: U32,
1912 +t26: U32,
1913 +t27: U32,
1914 +t28: U32,
1915 +t29: U32,
1916 +t30: U32,
1917 +t31: U32,
1918 +t32: U32,
1919 +t33: U32,
1920 +t34: U32,
1921 +t35: U32,
1922 +t36: U32,
1923 +t37: U32,
1924 +t38: U32,
1925 +byte_length: Nat,
1926 +extra: Nat,
1927 state: S.State
1928) -> S.State:
1929 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1930 extra, state)
1931
1932# Apply SHA-256 round 40 to the compression state.
1933def fin40(
1934 +t0: U32,
1935 +t1: U32,
1936 +t2: U32,
1937 +t3: U32,
1938 +t4: U32,
1939 +t5: U32,
1940 +t6: U32,
1941 +t7: U32,
1942 +t8: U32,
1943 +t9: U32,
1944 +t10: U32,
1945 +t11: U32,
1946 +t12: U32,
1947 +t13: U32,
1948 +t14: U32,
1949 +t15: U32,
1950 +t16: U32,
1951 +t17: U32,
1952 +t18: U32,
1953 +t19: U32,
1954 +t20: U32,
1955 +t21: U32,
1956 +t22: U32,
1957 +t23: U32,
1958 +t24: U32,
1959 +t25: U32,
1960 +t26: U32,
1961 +t27: U32,
1962 +t28: U32,
1963 +t29: U32,
1964 +t30: U32,
1965 +t31: U32,
1966 +t32: U32,
1967 +t33: U32,
1968 +t34: U32,
1969 +t35: U32,
1970 +t36: U32,
1971 +t37: U32,
1972 +t38: U32,
1973 +t39: U32,
1974 +byte_length: Nat,
1975 +extra: Nat,
1976 state: S.State
1977) -> S.State:
1978 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1979 extra, state)
1980
1981# Apply SHA-256 round 41 to the compression state.
1982def fin41(
1983 +t0: U32,
1984 +t1: U32,
1985 +t2: U32,
1986 +t3: U32,
1987 +t4: U32,
1988 +t5: U32,
1989 +t6: U32,
1990 +t7: U32,
1991 +t8: U32,
1992 +t9: U32,
1993 +t10: U32,
1994 +t11: U32,
1995 +t12: U32,
1996 +t13: U32,
1997 +t14: U32,
1998 +t15: U32,
1999 +t16: U32,
2000 +t17: U32,
2001 +t18: U32,
2002 +t19: U32,
2003 +t20: U32,
2004 +t21: U32,
2005 +t22: U32,
2006 +t23: U32,
2007 +t24: U32,
2008 +t25: U32,
2009 +t26: U32,
2010 +t27: U32,
2011 +t28: U32,
2012 +t29: U32,
2013 +t30: U32,
2014 +t31: U32,
2015 +t32: U32,
2016 +t33: U32,
2017 +t34: U32,
2018 +t35: U32,
2019 +t36: U32,
2020 +t37: U32,
2021 +t38: U32,
2022 +t39: U32,
2023 +t40: U32,
2024 +byte_length: Nat,
2025 +extra: Nat,
2026 state: S.State
2027) -> S.State:
2028 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2029 extra, state)
2030
2031# Apply SHA-256 round 42 to the compression state.
2032def fin42(
2033 +t0: U32,
2034 +t1: U32,
2035 +t2: U32,
2036 +t3: U32,
2037 +t4: U32,
2038 +t5: U32,
2039 +t6: U32,
2040 +t7: U32,
2041 +t8: U32,
2042 +t9: U32,
2043 +t10: U32,
2044 +t11: U32,
2045 +t12: U32,
2046 +t13: U32,
2047 +t14: U32,
2048 +t15: U32,
2049 +t16: U32,
2050 +t17: U32,
2051 +t18: U32,
2052 +t19: U32,
2053 +t20: U32,
2054 +t21: U32,
2055 +t22: U32,
2056 +t23: U32,
2057 +t24: U32,
2058 +t25: U32,
2059 +t26: U32,
2060 +t27: U32,
2061 +t28: U32,
2062 +t29: U32,
2063 +t30: U32,
2064 +t31: U32,
2065 +t32: U32,
2066 +t33: U32,
2067 +t34: U32,
2068 +t35: U32,
2069 +t36: U32,
2070 +t37: U32,
2071 +t38: U32,
2072 +t39: U32,
2073 +t40: U32,
2074 +t41: U32,
2075 +byte_length: Nat,
2076 +extra: Nat,
2077 state: S.State
2078) -> S.State:
2079 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2080 extra, state)
2081
2082# Apply SHA-256 round 43 to the compression state.
2083def fin43(
2084 +t0: U32,
2085 +t1: U32,
2086 +t2: U32,
2087 +t3: U32,
2088 +t4: U32,
2089 +t5: U32,
2090 +t6: U32,
2091 +t7: U32,
2092 +t8: U32,
2093 +t9: U32,
2094 +t10: U32,
2095 +t11: U32,
2096 +t12: U32,
2097 +t13: U32,
2098 +t14: U32,
2099 +t15: U32,
2100 +t16: U32,
2101 +t17: U32,
2102 +t18: U32,
2103 +t19: U32,
2104 +t20: U32,
2105 +t21: U32,
2106 +t22: U32,
2107 +t23: U32,
2108 +t24: U32,
2109 +t25: U32,
2110 +t26: U32,
2111 +t27: U32,
2112 +t28: U32,
2113 +t29: U32,
2114 +t30: U32,
2115 +t31: U32,
2116 +t32: U32,
2117 +t33: U32,
2118 +t34: U32,
2119 +t35: U32,
2120 +t36: U32,
2121 +t37: U32,
2122 +t38: U32,
2123 +t39: U32,
2124 +t40: U32,
2125 +t41: U32,
2126 +t42: U32,
2127 +byte_length: Nat,
2128 +extra: Nat,
2129 state: S.State
2130) -> S.State:
2131 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2132 extra, state)
2133
2134# Apply SHA-256 round 44 to the compression state.
2135def fin44(
2136 +t0: U32,
2137 +t1: U32,
2138 +t2: U32,
2139 +t3: U32,
2140 +t4: U32,
2141 +t5: U32,
2142 +t6: U32,
2143 +t7: U32,
2144 +t8: U32,
2145 +t9: U32,
2146 +t10: U32,
2147 +t11: U32,
2148 +t12: U32,
2149 +t13: U32,
2150 +t14: U32,
2151 +t15: U32,
2152 +t16: U32,
2153 +t17: U32,
2154 +t18: U32,
2155 +t19: U32,
2156 +t20: U32,
2157 +t21: U32,
2158 +t22: U32,
2159 +t23: U32,
2160 +t24: U32,
2161 +t25: U32,
2162 +t26: U32,
2163 +t27: U32,
2164 +t28: U32,
2165 +t29: U32,
2166 +t30: U32,
2167 +t31: U32,
2168 +t32: U32,
2169 +t33: U32,
2170 +t34: U32,
2171 +t35: U32,
2172 +t36: U32,
2173 +t37: U32,
2174 +t38: U32,
2175 +t39: U32,
2176 +t40: U32,
2177 +t41: U32,
2178 +t42: U32,
2179 +t43: U32,
2180 +byte_length: Nat,
2181 +extra: Nat,
2182 state: S.State
2183) -> S.State:
2184 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2185 extra, state)
2186
2187# Apply SHA-256 round 45 to the compression state.
2188def fin45(
2189 +t0: U32,
2190 +t1: U32,
2191 +t2: U32,
2192 +t3: U32,
2193 +t4: U32,
2194 +t5: U32,
2195 +t6: U32,
2196 +t7: U32,
2197 +t8: U32,
2198 +t9: U32,
2199 +t10: U32,
2200 +t11: U32,
2201 +t12: U32,
2202 +t13: U32,
2203 +t14: U32,
2204 +t15: U32,
2205 +t16: U32,
2206 +t17: U32,
2207 +t18: U32,
2208 +t19: U32,
2209 +t20: U32,
2210 +t21: U32,
2211 +t22: U32,
2212 +t23: U32,
2213 +t24: U32,
2214 +t25: U32,
2215 +t26: U32,
2216 +t27: U32,
2217 +t28: U32,
2218 +t29: U32,
2219 +t30: U32,
2220 +t31: U32,
2221 +t32: U32,
2222 +t33: U32,
2223 +t34: U32,
2224 +t35: U32,
2225 +t36: U32,
2226 +t37: U32,
2227 +t38: U32,
2228 +t39: U32,
2229 +t40: U32,
2230 +t41: U32,
2231 +t42: U32,
2232 +t43: U32,
2233 +t44: U32,
2234 +byte_length: Nat,
2235 +extra: Nat,
2236 state: S.State
2237) -> S.State:
2238 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2239 extra, state)
2240
2241# Apply SHA-256 round 46 to the compression state.
2242def fin46(
2243 +t0: U32,
2244 +t1: U32,
2245 +t2: U32,
2246 +t3: U32,
2247 +t4: U32,
2248 +t5: U32,
2249 +t6: U32,
2250 +t7: U32,
2251 +t8: U32,
2252 +t9: U32,
2253 +t10: U32,
2254 +t11: U32,
2255 +t12: U32,
2256 +t13: U32,
2257 +t14: U32,
2258 +t15: U32,
2259 +t16: U32,
2260 +t17: U32,
2261 +t18: U32,
2262 +t19: U32,
2263 +t20: U32,
2264 +t21: U32,
2265 +t22: U32,
2266 +t23: U32,
2267 +t24: U32,
2268 +t25: U32,
2269 +t26: U32,
2270 +t27: U32,
2271 +t28: U32,
2272 +t29: U32,
2273 +t30: U32,
2274 +t31: U32,
2275 +t32: U32,
2276 +t33: U32,
2277 +t34: U32,
2278 +t35: U32,
2279 +t36: U32,
2280 +t37: U32,
2281 +t38: U32,
2282 +t39: U32,
2283 +t40: U32,
2284 +t41: U32,
2285 +t42: U32,
2286 +t43: U32,
2287 +t44: U32,
2288 +t45: U32,
2289 +byte_length: Nat,
2290 +extra: Nat,
2291 state: S.State
2292) -> S.State:
2293 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2294 extra, state)
2295
2296# Apply SHA-256 round 47 to the compression state.
2297def fin47(
2298 +t0: U32,
2299 +t1: U32,
2300 +t2: U32,
2301 +t3: U32,
2302 +t4: U32,
2303 +t5: U32,
2304 +t6: U32,
2305 +t7: U32,
2306 +t8: U32,
2307 +t9: U32,
2308 +t10: U32,
2309 +t11: U32,
2310 +t12: U32,
2311 +t13: U32,
2312 +t14: U32,
2313 +t15: U32,
2314 +t16: U32,
2315 +t17: U32,
2316 +t18: U32,
2317 +t19: U32,
2318 +t20: U32,
2319 +t21: U32,
2320 +t22: U32,
2321 +t23: U32,
2322 +t24: U32,
2323 +t25: U32,
2324 +t26: U32,
2325 +t27: U32,
2326 +t28: U32,
2327 +t29: U32,
2328 +t30: U32,
2329 +t31: U32,
2330 +t32: U32,
2331 +t33: U32,
2332 +t34: U32,
2333 +t35: U32,
2334 +t36: U32,
2335 +t37: U32,
2336 +t38: U32,
2337 +t39: U32,
2338 +t40: U32,
2339 +t41: U32,
2340 +t42: U32,
2341 +t43: U32,
2342 +t44: U32,
2343 +t45: U32,
2344 +t46: U32,
2345 +byte_length: Nat,
2346 +extra: Nat,
2347 state: S.State
2348) -> S.State:
2349 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2350 extra, state)
2351
2352# Apply SHA-256 round 48 to the compression state.
2353def fin48(
2354 +t0: U32,
2355 +t1: U32,
2356 +t2: U32,
2357 +t3: U32,
2358 +t4: U32,
2359 +t5: U32,
2360 +t6: U32,
2361 +t7: U32,
2362 +t8: U32,
2363 +t9: U32,
2364 +t10: U32,
2365 +t11: U32,
2366 +t12: U32,
2367 +t13: U32,
2368 +t14: U32,
2369 +t15: U32,
2370 +t16: U32,
2371 +t17: U32,
2372 +t18: U32,
2373 +t19: U32,
2374 +t20: U32,
2375 +t21: U32,
2376 +t22: U32,
2377 +t23: U32,
2378 +t24: U32,
2379 +t25: U32,
2380 +t26: U32,
2381 +t27: U32,
2382 +t28: U32,
2383 +t29: U32,
2384 +t30: U32,
2385 +t31: U32,
2386 +t32: U32,
2387 +t33: U32,
2388 +t34: U32,
2389 +t35: U32,
2390 +t36: U32,
2391 +t37: U32,
2392 +t38: U32,
2393 +t39: U32,
2394 +t40: U32,
2395 +t41: U32,
2396 +t42: U32,
2397 +t43: U32,
2398 +t44: U32,
2399 +t45: U32,
2400 +t46: U32,
2401 +t47: U32,
2402 +byte_length: Nat,
2403 +extra: Nat,
2404 state: S.State
2405) -> S.State:
2406 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(128, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2407 extra, state)
2408
2409# Apply SHA-256 round 49 to the compression state.
2410def fin49(
2411 +t0: U32,
2412 +t1: U32,
2413 +t2: U32,
2414 +t3: U32,
2415 +t4: U32,
2416 +t5: U32,
2417 +t6: U32,
2418 +t7: U32,
2419 +t8: U32,
2420 +t9: U32,
2421 +t10: U32,
2422 +t11: U32,
2423 +t12: U32,
2424 +t13: U32,
2425 +t14: U32,
2426 +t15: U32,
2427 +t16: U32,
2428 +t17: U32,
2429 +t18: U32,
2430 +t19: U32,
2431 +t20: U32,
2432 +t21: U32,
2433 +t22: U32,
2434 +t23: U32,
2435 +t24: U32,
2436 +t25: U32,
2437 +t26: U32,
2438 +t27: U32,
2439 +t28: U32,
2440 +t29: U32,
2441 +t30: U32,
2442 +t31: U32,
2443 +t32: U32,
2444 +t33: U32,
2445 +t34: U32,
2446 +t35: U32,
2447 +t36: U32,
2448 +t37: U32,
2449 +t38: U32,
2450 +t39: U32,
2451 +t40: U32,
2452 +t41: U32,
2453 +t42: U32,
2454 +t43: U32,
2455 +t44: U32,
2456 +t45: U32,
2457 +t46: U32,
2458 +t47: U32,
2459 +t48: U32,
2460 +byte_length: Nat,
2461 +extra: Nat,
2462 state: S.State
2463) -> S.State:
2464 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, 128, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2465 extra, state)
2466
2467# Apply SHA-256 round 50 to the compression state.
2468def fin50(
2469 +t0: U32,
2470 +t1: U32,
2471 +t2: U32,
2472 +t3: U32,
2473 +t4: U32,
2474 +t5: U32,
2475 +t6: U32,
2476 +t7: U32,
2477 +t8: U32,
2478 +t9: U32,
2479 +t10: U32,
2480 +t11: U32,
2481 +t12: U32,
2482 +t13: U32,
2483 +t14: U32,
2484 +t15: U32,
2485 +t16: U32,
2486 +t17: U32,
2487 +t18: U32,
2488 +t19: U32,
2489 +t20: U32,
2490 +t21: U32,
2491 +t22: U32,
2492 +t23: U32,
2493 +t24: U32,
2494 +t25: U32,
2495 +t26: U32,
2496 +t27: U32,
2497 +t28: U32,
2498 +t29: U32,
2499 +t30: U32,
2500 +t31: U32,
2501 +t32: U32,
2502 +t33: U32,
2503 +t34: U32,
2504 +t35: U32,
2505 +t36: U32,
2506 +t37: U32,
2507 +t38: U32,
2508 +t39: U32,
2509 +t40: U32,
2510 +t41: U32,
2511 +t42: U32,
2512 +t43: U32,
2513 +t44: U32,
2514 +t45: U32,
2515 +t46: U32,
2516 +t47: U32,
2517 +t48: U32,
2518 +t49: U32,
2519 +byte_length: Nat,
2520 +extra: Nat,
2521 state: S.State
2522) -> S.State:
2523 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, 128, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2524 extra, state)
2525
2526# Apply SHA-256 round 51 to the compression state.
2527def fin51(
2528 +t0: U32,
2529 +t1: U32,
2530 +t2: U32,
2531 +t3: U32,
2532 +t4: U32,
2533 +t5: U32,
2534 +t6: U32,
2535 +t7: U32,
2536 +t8: U32,
2537 +t9: U32,
2538 +t10: U32,
2539 +t11: U32,
2540 +t12: U32,
2541 +t13: U32,
2542 +t14: U32,
2543 +t15: U32,
2544 +t16: U32,
2545 +t17: U32,
2546 +t18: U32,
2547 +t19: U32,
2548 +t20: U32,
2549 +t21: U32,
2550 +t22: U32,
2551 +t23: U32,
2552 +t24: U32,
2553 +t25: U32,
2554 +t26: U32,
2555 +t27: U32,
2556 +t28: U32,
2557 +t29: U32,
2558 +t30: U32,
2559 +t31: U32,
2560 +t32: U32,
2561 +t33: U32,
2562 +t34: U32,
2563 +t35: U32,
2564 +t36: U32,
2565 +t37: U32,
2566 +t38: U32,
2567 +t39: U32,
2568 +t40: U32,
2569 +t41: U32,
2570 +t42: U32,
2571 +t43: U32,
2572 +t44: U32,
2573 +t45: U32,
2574 +t46: U32,
2575 +t47: U32,
2576 +t48: U32,
2577 +t49: U32,
2578 +t50: U32,
2579 +byte_length: Nat,
2580 +extra: Nat,
2581 state: S.State
2582) -> S.State:
2583 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, 128), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2584 extra, state)
2585
2586# Apply SHA-256 round 52 to the compression state.
2587def fin52(
2588 +t0: U32,
2589 +t1: U32,
2590 +t2: U32,
2591 +t3: U32,
2592 +t4: U32,
2593 +t5: U32,
2594 +t6: U32,
2595 +t7: U32,
2596 +t8: U32,
2597 +t9: U32,
2598 +t10: U32,
2599 +t11: U32,
2600 +t12: U32,
2601 +t13: U32,
2602 +t14: U32,
2603 +t15: U32,
2604 +t16: U32,
2605 +t17: U32,
2606 +t18: U32,
2607 +t19: U32,
2608 +t20: U32,
2609 +t21: U32,
2610 +t22: U32,
2611 +t23: U32,
2612 +t24: U32,
2613 +t25: U32,
2614 +t26: U32,
2615 +t27: U32,
2616 +t28: U32,
2617 +t29: U32,
2618 +t30: U32,
2619 +t31: U32,
2620 +t32: U32,
2621 +t33: U32,
2622 +t34: U32,
2623 +t35: U32,
2624 +t36: U32,
2625 +t37: U32,
2626 +t38: U32,
2627 +t39: U32,
2628 +t40: U32,
2629 +t41: U32,
2630 +t42: U32,
2631 +t43: U32,
2632 +t44: U32,
2633 +t45: U32,
2634 +t46: U32,
2635 +t47: U32,
2636 +t48: U32,
2637 +t49: U32,
2638 +t50: U32,
2639 +t51: U32,
2640 +byte_length: Nat,
2641 +extra: Nat,
2642 state: S.State
2643) -> S.State:
2644 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(128, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2645 extra, state)
2646
2647# Apply SHA-256 round 53 to the compression state.
2648def fin53(
2649 +t0: U32,
2650 +t1: U32,
2651 +t2: U32,
2652 +t3: U32,
2653 +t4: U32,
2654 +t5: U32,
2655 +t6: U32,
2656 +t7: U32,
2657 +t8: U32,
2658 +t9: U32,
2659 +t10: U32,
2660 +t11: U32,
2661 +t12: U32,
2662 +t13: U32,
2663 +t14: U32,
2664 +t15: U32,
2665 +t16: U32,
2666 +t17: U32,
2667 +t18: U32,
2668 +t19: U32,
2669 +t20: U32,
2670 +t21: U32,
2671 +t22: U32,
2672 +t23: U32,
2673 +t24: U32,
2674 +t25: U32,
2675 +t26: U32,
2676 +t27: U32,
2677 +t28: U32,
2678 +t29: U32,
2679 +t30: U32,
2680 +t31: U32,
2681 +t32: U32,
2682 +t33: U32,
2683 +t34: U32,
2684 +t35: U32,
2685 +t36: U32,
2686 +t37: U32,
2687 +t38: U32,
2688 +t39: U32,
2689 +t40: U32,
2690 +t41: U32,
2691 +t42: U32,
2692 +t43: U32,
2693 +t44: U32,
2694 +t45: U32,
2695 +t46: U32,
2696 +t47: U32,
2697 +t48: U32,
2698 +t49: U32,
2699 +t50: U32,
2700 +t51: U32,
2701 +t52: U32,
2702 +byte_length: Nat,
2703 +extra: Nat,
2704 state: S.State
2705) -> S.State:
2706 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, 128, 0, 0), len_hi(byte_length), len_lo(byte_length),
2707 extra, state)
2708
2709# Apply SHA-256 round 54 to the compression state.
2710def fin54(
2711 +t0: U32,
2712 +t1: U32,
2713 +t2: U32,
2714 +t3: U32,
2715 +t4: U32,
2716 +t5: U32,
2717 +t6: U32,
2718 +t7: U32,
2719 +t8: U32,
2720 +t9: U32,
2721 +t10: U32,
2722 +t11: U32,
2723 +t12: U32,
2724 +t13: U32,
2725 +t14: U32,
2726 +t15: U32,
2727 +t16: U32,
2728 +t17: U32,
2729 +t18: U32,
2730 +t19: U32,
2731 +t20: U32,
2732 +t21: U32,
2733 +t22: U32,
2734 +t23: U32,
2735 +t24: U32,
2736 +t25: U32,
2737 +t26: U32,
2738 +t27: U32,
2739 +t28: U32,
2740 +t29: U32,
2741 +t30: U32,
2742 +t31: U32,
2743 +t32: U32,
2744 +t33: U32,
2745 +t34: U32,
2746 +t35: U32,
2747 +t36: U32,
2748 +t37: U32,
2749 +t38: U32,
2750 +t39: U32,
2751 +t40: U32,
2752 +t41: U32,
2753 +t42: U32,
2754 +t43: U32,
2755 +t44: U32,
2756 +t45: U32,
2757 +t46: U32,
2758 +t47: U32,
2759 +t48: U32,
2760 +t49: U32,
2761 +t50: U32,
2762 +t51: U32,
2763 +t52: U32,
2764 +t53: U32,
2765 +byte_length: Nat,
2766 +extra: Nat,
2767 state: S.State
2768) -> S.State:
2769 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, 128, 0), len_hi(byte_length), len_lo(byte_length),
2770 extra, state)
2771
2772# Apply SHA-256 round 55 to the compression state.
2773def fin55(
2774 +t0: U32,
2775 +t1: U32,
2776 +t2: U32,
2777 +t3: U32,
2778 +t4: U32,
2779 +t5: U32,
2780 +t6: U32,
2781 +t7: U32,
2782 +t8: U32,
2783 +t9: U32,
2784 +t10: U32,
2785 +t11: U32,
2786 +t12: U32,
2787 +t13: U32,
2788 +t14: U32,
2789 +t15: U32,
2790 +t16: U32,
2791 +t17: U32,
2792 +t18: U32,
2793 +t19: U32,
2794 +t20: U32,
2795 +t21: U32,
2796 +t22: U32,
2797 +t23: U32,
2798 +t24: U32,
2799 +t25: U32,
2800 +t26: U32,
2801 +t27: U32,
2802 +t28: U32,
2803 +t29: U32,
2804 +t30: U32,
2805 +t31: U32,
2806 +t32: U32,
2807 +t33: U32,
2808 +t34: U32,
2809 +t35: U32,
2810 +t36: U32,
2811 +t37: U32,
2812 +t38: U32,
2813 +t39: U32,
2814 +t40: U32,
2815 +t41: U32,
2816 +t42: U32,
2817 +t43: U32,
2818 +t44: U32,
2819 +t45: U32,
2820 +t46: U32,
2821 +t47: U32,
2822 +t48: U32,
2823 +t49: U32,
2824 +t50: U32,
2825 +t51: U32,
2826 +t52: U32,
2827 +t53: U32,
2828 +t54: U32,
2829 +byte_length: Nat,
2830 +extra: Nat,
2831 state: S.State
2832) -> S.State:
2833 fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, 128), len_hi(byte_length), len_lo(byte_length),
2834 extra, state)
2835
2836# Apply SHA-256 round 56 to the compression state.
2837def fin56(
2838 +t0: U32,
2839 +t1: U32,
2840 +t2: U32,
2841 +t3: U32,
2842 +t4: U32,
2843 +t5: U32,
2844 +t6: U32,
2845 +t7: U32,
2846 +t8: U32,
2847 +t9: U32,
2848 +t10: U32,
2849 +t11: U32,
2850 +t12: U32,
2851 +t13: U32,
2852 +t14: U32,
2853 +t15: U32,
2854 +t16: U32,
2855 +t17: U32,
2856 +t18: U32,
2857 +t19: U32,
2858 +t20: U32,
2859 +t21: U32,
2860 +t22: U32,
2861 +t23: U32,
2862 +t24: U32,
2863 +t25: U32,
2864 +t26: U32,
2865 +t27: U32,
2866 +t28: U32,
2867 +t29: U32,
2868 +t30: U32,
2869 +t31: U32,
2870 +t32: U32,
2871 +t33: U32,
2872 +t34: U32,
2873 +t35: U32,
2874 +t36: U32,
2875 +t37: U32,
2876 +t38: U32,
2877 +t39: U32,
2878 +t40: U32,
2879 +t41: U32,
2880 +t42: U32,
2881 +t43: U32,
2882 +t44: U32,
2883 +t45: U32,
2884 +t46: U32,
2885 +t47: U32,
2886 +t48: U32,
2887 +t49: U32,
2888 +t50: U32,
2889 +t51: U32,
2890 +t52: U32,
2891 +t53: U32,
2892 +t54: U32,
2893 +t55: U32,
2894 +byte_length: Nat,
2895 +extra: Nat,
2896 state: S.State
2897) -> S.State:
2898 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2899 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(128, 0, 0, 0), pack(0, 0, 0, 0),
2900 extra, state))
2901
2902# Apply SHA-256 round 57 to the compression state.
2903def fin57(
2904 +t0: U32,
2905 +t1: U32,
2906 +t2: U32,
2907 +t3: U32,
2908 +t4: U32,
2909 +t5: U32,
2910 +t6: U32,
2911 +t7: U32,
2912 +t8: U32,
2913 +t9: U32,
2914 +t10: U32,
2915 +t11: U32,
2916 +t12: U32,
2917 +t13: U32,
2918 +t14: U32,
2919 +t15: U32,
2920 +t16: U32,
2921 +t17: U32,
2922 +t18: U32,
2923 +t19: U32,
2924 +t20: U32,
2925 +t21: U32,
2926 +t22: U32,
2927 +t23: U32,
2928 +t24: U32,
2929 +t25: U32,
2930 +t26: U32,
2931 +t27: U32,
2932 +t28: U32,
2933 +t29: U32,
2934 +t30: U32,
2935 +t31: U32,
2936 +t32: U32,
2937 +t33: U32,
2938 +t34: U32,
2939 +t35: U32,
2940 +t36: U32,
2941 +t37: U32,
2942 +t38: U32,
2943 +t39: U32,
2944 +t40: U32,
2945 +t41: U32,
2946 +t42: U32,
2947 +t43: U32,
2948 +t44: U32,
2949 +t45: U32,
2950 +t46: U32,
2951 +t47: U32,
2952 +t48: U32,
2953 +t49: U32,
2954 +t50: U32,
2955 +t51: U32,
2956 +t52: U32,
2957 +t53: U32,
2958 +t54: U32,
2959 +t55: U32,
2960 +t56: U32,
2961 +byte_length: Nat,
2962 +extra: Nat,
2963 state: S.State
2964) -> S.State:
2965 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
2966 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, 128, 0, 0), pack(0, 0, 0, 0),
2967 extra, state))
2968
2969# Apply SHA-256 round 58 to the compression state.
2970def fin58(
2971 +t0: U32,
2972 +t1: U32,
2973 +t2: U32,
2974 +t3: U32,
2975 +t4: U32,
2976 +t5: U32,
2977 +t6: U32,
2978 +t7: U32,
2979 +t8: U32,
2980 +t9: U32,
2981 +t10: U32,
2982 +t11: U32,
2983 +t12: U32,
2984 +t13: U32,
2985 +t14: U32,
2986 +t15: U32,
2987 +t16: U32,
2988 +t17: U32,
2989 +t18: U32,
2990 +t19: U32,
2991 +t20: U32,
2992 +t21: U32,
2993 +t22: U32,
2994 +t23: U32,
2995 +t24: U32,
2996 +t25: U32,
2997 +t26: U32,
2998 +t27: U32,
2999 +t28: U32,
3000 +t29: U32,
3001 +t30: U32,
3002 +t31: U32,
3003 +t32: U32,
3004 +t33: U32,
3005 +t34: U32,
3006 +t35: U32,
3007 +t36: U32,
3008 +t37: U32,
3009 +t38: U32,
3010 +t39: U32,
3011 +t40: U32,
3012 +t41: U32,
3013 +t42: U32,
3014 +t43: U32,
3015 +t44: U32,
3016 +t45: U32,
3017 +t46: U32,
3018 +t47: U32,
3019 +t48: U32,
3020 +t49: U32,
3021 +t50: U32,
3022 +t51: U32,
3023 +t52: U32,
3024 +t53: U32,
3025 +t54: U32,
3026 +t55: U32,
3027 +t56: U32,
3028 +t57: U32,
3029 +byte_length: Nat,
3030 +extra: Nat,
3031 state: S.State
3032) -> S.State:
3033 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
3034 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, 128, 0), pack(0, 0, 0, 0),
3035 extra, state))
3036
3037# Apply SHA-256 round 59 to the compression state.
3038def fin59(
3039 +t0: U32,
3040 +t1: U32,
3041 +t2: U32,
3042 +t3: U32,
3043 +t4: U32,
3044 +t5: U32,
3045 +t6: U32,
3046 +t7: U32,
3047 +t8: U32,
3048 +t9: U32,
3049 +t10: U32,
3050 +t11: U32,
3051 +t12: U32,
3052 +t13: U32,
3053 +t14: U32,
3054 +t15: U32,
3055 +t16: U32,
3056 +t17: U32,
3057 +t18: U32,
3058 +t19: U32,
3059 +t20: U32,
3060 +t21: U32,
3061 +t22: U32,
3062 +t23: U32,
3063 +t24: U32,
3064 +t25: U32,
3065 +t26: U32,
3066 +t27: U32,
3067 +t28: U32,
3068 +t29: U32,
3069 +t30: U32,
3070 +t31: U32,
3071 +t32: U32,
3072 +t33: U32,
3073 +t34: U32,
3074 +t35: U32,
3075 +t36: U32,
3076 +t37: U32,
3077 +t38: U32,
3078 +t39: U32,
3079 +t40: U32,
3080 +t41: U32,
3081 +t42: U32,
3082 +t43: U32,
3083 +t44: U32,
3084 +t45: U32,
3085 +t46: U32,
3086 +t47: U32,
3087 +t48: U32,
3088 +t49: U32,
3089 +t50: U32,
3090 +t51: U32,
3091 +t52: U32,
3092 +t53: U32,
3093 +t54: U32,
3094 +t55: U32,
3095 +t56: U32,
3096 +t57: U32,
3097 +t58: U32,
3098 +byte_length: Nat,
3099 +extra: Nat,
3100 state: S.State
3101) -> S.State:
3102 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
3103 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, 128), pack(0, 0, 0, 0),
3104 extra, state))
3105
3106# Apply SHA-256 round 60 to the compression state.
3107def fin60(
3108 +t0: U32,
3109 +t1: U32,
3110 +t2: U32,
3111 +t3: U32,
3112 +t4: U32,
3113 +t5: U32,
3114 +t6: U32,
3115 +t7: U32,
3116 +t8: U32,
3117 +t9: U32,
3118 +t10: U32,
3119 +t11: U32,
3120 +t12: U32,
3121 +t13: U32,
3122 +t14: U32,
3123 +t15: U32,
3124 +t16: U32,
3125 +t17: U32,
3126 +t18: U32,
3127 +t19: U32,
3128 +t20: U32,
3129 +t21: U32,
3130 +t22: U32,
3131 +t23: U32,
3132 +t24: U32,
3133 +t25: U32,
3134 +t26: U32,
3135 +t27: U32,
3136 +t28: U32,
3137 +t29: U32,
3138 +t30: U32,
3139 +t31: U32,
3140 +t32: U32,
3141 +t33: U32,
3142 +t34: U32,
3143 +t35: U32,
3144 +t36: U32,
3145 +t37: U32,
3146 +t38: U32,
3147 +t39: U32,
3148 +t40: U32,
3149 +t41: U32,
3150 +t42: U32,
3151 +t43: U32,
3152 +t44: U32,
3153 +t45: U32,
3154 +t46: U32,
3155 +t47: U32,
3156 +t48: U32,
3157 +t49: U32,
3158 +t50: U32,
3159 +t51: U32,
3160 +t52: U32,
3161 +t53: U32,
3162 +t54: U32,
3163 +t55: U32,
3164 +t56: U32,
3165 +t57: U32,
3166 +t58: U32,
3167 +t59: U32,
3168 +byte_length: Nat,
3169 +extra: Nat,
3170 state: S.State
3171) -> S.State:
3172 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
3173 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(128, 0, 0, 0),
3174 extra, state))
3175
3176# Apply SHA-256 round 61 to the compression state.
3177def fin61(
3178 +t0: U32,
3179 +t1: U32,
3180 +t2: U32,
3181 +t3: U32,
3182 +t4: U32,
3183 +t5: U32,
3184 +t6: U32,
3185 +t7: U32,
3186 +t8: U32,
3187 +t9: U32,
3188 +t10: U32,
3189 +t11: U32,
3190 +t12: U32,
3191 +t13: U32,
3192 +t14: U32,
3193 +t15: U32,
3194 +t16: U32,
3195 +t17: U32,
3196 +t18: U32,
3197 +t19: U32,
3198 +t20: U32,
3199 +t21: U32,
3200 +t22: U32,
3201 +t23: U32,
3202 +t24: U32,
3203 +t25: U32,
3204 +t26: U32,
3205 +t27: U32,
3206 +t28: U32,
3207 +t29: U32,
3208 +t30: U32,
3209 +t31: U32,
3210 +t32: U32,
3211 +t33: U32,
3212 +t34: U32,
3213 +t35: U32,
3214 +t36: U32,
3215 +t37: U32,
3216 +t38: U32,
3217 +t39: U32,
3218 +t40: U32,
3219 +t41: U32,
3220 +t42: U32,
3221 +t43: U32,
3222 +t44: U32,
3223 +t45: U32,
3224 +t46: U32,
3225 +t47: U32,
3226 +t48: U32,
3227 +t49: U32,
3228 +t50: U32,
3229 +t51: U32,
3230 +t52: U32,
3231 +t53: U32,
3232 +t54: U32,
3233 +t55: U32,
3234 +t56: U32,
3235 +t57: U32,
3236 +t58: U32,
3237 +t59: U32,
3238 +t60: U32,
3239 +byte_length: Nat,
3240 +extra: Nat,
3241 state: S.State
3242) -> S.State:
3243 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
3244 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(t60, 128, 0, 0),
3245 extra, state))
3246
3247# Apply SHA-256 round 62 to the compression state.
3248def fin62(
3249 +t0: U32,
3250 +t1: U32,
3251 +t2: U32,
3252 +t3: U32,
3253 +t4: U32,
3254 +t5: U32,
3255 +t6: U32,
3256 +t7: U32,
3257 +t8: U32,
3258 +t9: U32,
3259 +t10: U32,
3260 +t11: U32,
3261 +t12: U32,
3262 +t13: U32,
3263 +t14: U32,
3264 +t15: U32,
3265 +t16: U32,
3266 +t17: U32,
3267 +t18: U32,
3268 +t19: U32,
3269 +t20: U32,
3270 +t21: U32,
3271 +t22: U32,
3272 +t23: U32,
3273 +t24: U32,
3274 +t25: U32,
3275 +t26: U32,
3276 +t27: U32,
3277 +t28: U32,
3278 +t29: U32,
3279 +t30: U32,
3280 +t31: U32,
3281 +t32: U32,
3282 +t33: U32,
3283 +t34: U32,
3284 +t35: U32,
3285 +t36: U32,
3286 +t37: U32,
3287 +t38: U32,
3288 +t39: U32,
3289 +t40: U32,
3290 +t41: U32,
3291 +t42: U32,
3292 +t43: U32,
3293 +t44: U32,
3294 +t45: U32,
3295 +t46: U32,
3296 +t47: U32,
3297 +t48: U32,
3298 +t49: U32,
3299 +t50: U32,
3300 +t51: U32,
3301 +t52: U32,
3302 +t53: U32,
3303 +t54: U32,
3304 +t55: U32,
3305 +t56: U32,
3306 +t57: U32,
3307 +t58: U32,
3308 +t59: U32,
3309 +t60: U32,
3310 +t61: U32,
3311 +byte_length: Nat,
3312 +extra: Nat,
3313 state: S.State
3314) -> S.State:
3315 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
3316 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(t60, t61, 128, 0),
3317 extra, state))
3318
3319# Apply SHA-256 round 63 to the compression state.
3320def fin63(
3321 +t0: U32,
3322 +t1: U32,
3323 +t2: U32,
3324 +t3: U32,
3325 +t4: U32,
3326 +t5: U32,
3327 +t6: U32,
3328 +t7: U32,
3329 +t8: U32,
3330 +t9: U32,
3331 +t10: U32,
3332 +t11: U32,
3333 +t12: U32,
3334 +t13: U32,
3335 +t14: U32,
3336 +t15: U32,
3337 +t16: U32,
3338 +t17: U32,
3339 +t18: U32,
3340 +t19: U32,
3341 +t20: U32,
3342 +t21: U32,
3343 +t22: U32,
3344 +t23: U32,
3345 +t24: U32,
3346 +t25: U32,
3347 +t26: U32,
3348 +t27: U32,
3349 +t28: U32,
3350 +t29: U32,
3351 +t30: U32,
3352 +t31: U32,
3353 +t32: U32,
3354 +t33: U32,
3355 +t34: U32,
3356 +t35: U32,
3357 +t36: U32,
3358 +t37: U32,
3359 +t38: U32,
3360 +t39: U32,
3361 +t40: U32,
3362 +t41: U32,
3363 +t42: U32,
3364 +t43: U32,
3365 +t44: U32,
3366 +t45: U32,
3367 +t46: U32,
3368 +t47: U32,
3369 +t48: U32,
3370 +t49: U32,
3371 +t50: U32,
3372 +t51: U32,
3373 +t52: U32,
3374 +t53: U32,
3375 +t54: U32,
3376 +t55: U32,
3377 +t56: U32,
3378 +t57: U32,
3379 +t58: U32,
3380 +t59: U32,
3381 +t60: U32,
3382 +t61: U32,
3383 +t62: U32,
3384 +byte_length: Nat,
3385 +extra: Nat,
3386 state: S.State
3387) -> S.State:
3388 fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
3389 extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(t60, t61, t62, 128),
3390 extra, state))
3391
3392# Tail-recursive block loop over an already padded byte list.
3393def fips_blocks(bytes: List<&2, U32>, +extra: Nat, state: S.State) -> S.State:
3394 match bytes:
3395 case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
3396 fips_blocks(rest, extra, fips_compress16(pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15), pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31), pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47), pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63), extra, state))
3397 case _:
3398 state
3399
3400# Append zero padding to onto for the SHA-256 compression implementation.
3401def zeros_onto(word_z: Nat, acc: List<&2, U32>) -> List<&2, U32>:
3402 match word_z:
3403 case 0n:
3404 acc
3405 case 1n+p:
3406 zeros_onto(p, 0 <> acc)
3407
3408# The padding suffix built only with tail-recursive loops.
3409def padding(+byte_length: Nat) -> List<&2, U32>:
3410 128 <> zeros_onto(Nat.mod(Nat.sub(119n, Nat.mod(byte_length, 64n)), 64n), bit_length(byte_length))
3411
3412# Handle byte lengths for count for the SHA-256 compression implementation.
3413def byte_count(bytes: List<&2, U32>, acc: Nat) -> Nat:
3414 match bytes:
3415 case Nil{}:
3416 acc
3417 case h <> t:
3418 byte_count(t, 1n+acc)
3419
3420# Final block(s) of an n-byte message whose tail has fewer than 64 bytes.
3421# stream never passes 64 or more bytes; that case pads with tail-recursive
3422# loops. The match is exhaustive: a default case would make Bend rebuild the
3423# consumed cells at every depth. Length words are computed directly from n; note
3424# that sharing any List<U32> would make Bend reference-count every list match,
3425# including the input loop in stream.
3426def finish_n(+tail: List<&2, U32>, +byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
3427 match tail:
3428 case Nil{}:
3429 fin0(byte_length, extra, state)
3430 case t0 <> Nil{}:
3431 fin1(t0, byte_length, extra, state)
3432 case t0 <> t1 <> Nil{}:
3433 fin2(t0, t1, byte_length, extra, state)
3434 case t0 <> t1 <> t2 <> Nil{}:
3435 fin3(t0, t1, t2, byte_length, extra, state)
3436 case t0 <> t1 <> t2 <> t3 <> Nil{}:
3437 fin4(t0, t1, t2, t3, byte_length, extra, state)
3438 case t0 <> t1 <> t2 <> t3 <> t4 <> Nil{}:
3439 fin5(t0, t1, t2, t3, t4, byte_length, extra, state)
3440 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> Nil{}:
3441 fin6(t0, t1, t2, t3, t4, t5, byte_length, extra, state)
3442 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> Nil{}:
3443 fin7(t0, t1, t2, t3, t4, t5, t6, byte_length, extra, state)
3444 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> Nil{}:
3445 fin8(t0, t1, t2, t3, t4, t5, t6, t7, byte_length, extra, state)
3446 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> Nil{}:
3447 fin9(t0, t1, t2, t3, t4, t5, t6, t7, t8, byte_length, extra, state)
3448 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> Nil{}:
3449 fin10(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, byte_length, extra, state)
3450 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> Nil{}:
3451 fin11(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, byte_length, extra, state)
3452 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> Nil{}:
3453 fin12(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, byte_length, extra, state)
3454 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> Nil{}:
3455 fin13(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, byte_length, extra, state)
3456 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> Nil{}:
3457 fin14(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, byte_length, extra, state)
3458 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> Nil{}:
3459 fin15(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, byte_length, extra, state)
3460 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> Nil{}:
3461 fin16(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, byte_length, extra, state)
3462 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> Nil{}:
3463 fin17(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, byte_length, extra, state)
3464 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> Nil{}:
3465 fin18(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, byte_length, extra, state)
3466 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> Nil{}:
3467 fin19(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, byte_length, extra, state)
3468 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> Nil{}:
3469 fin20(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, byte_length, extra, state)
3470 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> Nil{}:
3471 fin21(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, byte_length, extra, state)
3472 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> Nil{}:
3473 fin22(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, byte_length, extra, state)
3474 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> Nil{}:
3475 fin23(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, byte_length, extra, state)
3476 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> Nil{}:
3477 fin24(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, byte_length, extra, state)
3478 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> Nil{}:
3479 fin25(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, byte_length, extra, state)
3480 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> Nil{}:
3481 fin26(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, byte_length, extra, state)
3482 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> Nil{}:
3483 fin27(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, byte_length, extra, state)
3484 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> Nil{}:
3485 fin28(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, byte_length, extra, state)
3486 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> Nil{}:
3487 fin29(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, byte_length, extra, state)
3488 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> Nil{}:
3489 fin30(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, byte_length, extra, state)
3490 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> Nil{}:
3491 fin31(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, byte_length, extra, state)
3492 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> Nil{}:
3493 fin32(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, byte_length, extra, state)
3494 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> Nil{}:
3495 fin33(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, byte_length, extra, state)
3496 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> Nil{}:
3497 fin34(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, byte_length, extra, state)
3498 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> Nil{}:
3499 fin35(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, byte_length, extra, state)
3500 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> Nil{}:
3501 fin36(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, byte_length, extra, state)
3502 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> Nil{}:
3503 fin37(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, byte_length, extra, state)
3504 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> Nil{}:
3505 fin38(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, byte_length, extra, state)
3506 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> Nil{}:
3507 fin39(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, byte_length, extra, state)
3508 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> Nil{}:
3509 fin40(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, byte_length, extra, state)
3510 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> Nil{}:
3511 fin41(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, byte_length, extra, state)
3512 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> Nil{}:
3513 fin42(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, byte_length, extra, state)
3514 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> Nil{}:
3515 fin43(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, byte_length, extra, state)
3516 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> Nil{}:
3517 fin44(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, byte_length, extra, state)
3518 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> Nil{}:
3519 fin45(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, byte_length, extra, state)
3520 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> Nil{}:
3521 fin46(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, byte_length, extra, state)
3522 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> Nil{}:
3523 fin47(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, byte_length, extra, state)
3524 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> Nil{}:
3525 fin48(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, byte_length, extra, state)
3526 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> Nil{}:
3527 fin49(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, byte_length, extra, state)
3528 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> Nil{}:
3529 fin50(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, byte_length, extra, state)
3530 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> Nil{}:
3531 fin51(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, byte_length, extra, state)
3532 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> Nil{}:
3533 fin52(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, byte_length, extra, state)
3534 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> Nil{}:
3535 fin53(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, byte_length, extra, state)
3536 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> Nil{}:
3537 fin54(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, byte_length, extra, state)
3538 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> Nil{}:
3539 fin55(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, byte_length, extra, state)
3540 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> Nil{}:
3541 fin56(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, byte_length, extra, state)
3542 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> Nil{}:
3543 fin57(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, byte_length, extra, state)
3544 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> Nil{}:
3545 fin58(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, byte_length, extra, state)
3546 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> Nil{}:
3547 fin59(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, byte_length, extra, state)
3548 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> Nil{}:
3549 fin60(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, byte_length, extra, state)
3550 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> Nil{}:
3551 fin61(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, t60, byte_length, extra, state)
3552 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> Nil{}:
3553 fin62(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, t60, t61, byte_length, extra, state)
3554 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> t62 <> Nil{}:
3555 fin63(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, t60, t61, t62, byte_length, extra, state)
3556 case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> t62 <> t63 <> rest:
3557 fips_blocks(List.reverse.go(&2, U32, List.reverse(&2, U32, t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> t62 <> t63 <> rest), padding(byte_length)), extra, state)
3558
3559# count is the number of bytes already hashed, always a multiple of 64.
3560def finish(+tail: List<&2, U32>, count: Nat, +extra: Nat, state: S.State) -> S.State:
3561 finish_n(tail, byte_count(tail, count), extra, state)
3562
3563# Compress complete 64-byte blocks straight from the input list, so the
3564# message is never copied, counted or reversed. count is the number of bytes
3565# already hashed and extra the number of derived schedule words (48).
3566def stream(+bytes: List<&2, U32>, count: Nat, +extra: Nat, state: S.State) -> S.State:
3567 match bytes:
3568 case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
3569 stream(rest, Nat.add(64n, count), extra, fips_compress16(
3570 pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15),
3571 pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31),
3572 pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47),
3573 pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63),
3574 extra, state))
3575 case _:
3576 finish(bytes, count, extra, state)
3577
3578# ASCII convenience only; binary inputs use sha256 directly.
3579def ascii(arg_s: String) -> List<&2, U32>:
3580 match arg_s:
3581 case SNil{}:
3582 Nil{}
3583 case SCon{Chr{c}, t}:
3584 c <> ascii(t)
3585
3586# Decode hexadecimal digit if for the SHA-256 compression implementation.
3587def hex_digit_if(digit: U32, small: Bool) -> Char:
3588 match small:
3589 case True{}:
3590 Chr{(48 + digit : U32)}
3591 case False{}:
3592 Chr{(87 + digit : U32)}
3593
3594# Decode hexadecimal digit for the SHA-256 compression implementation.
3595def hex_digit(+digit: U32) -> Char:
3596 hex_digit_if(digit, U32.is_lt(digit, 10))
3597
3598# Decode hexadecimal word go for the SHA-256 compression implementation.
3599def hex_word_go(digit_count: Nat, +word: U32, acc: String) -> String:
3600 match digit_count:
3601 case 0n:
3602 acc
3603 case 1n+p:
3604 hex_word_go(p, U32.shrn(word, 4n), SCon{hex_digit((word .&. 15 : U32)), acc})
3605
3606# Decode hexadecimal word for the SHA-256 compression implementation.
3607def hex_word(word: U32) -> String:
3608 hex_word_go(8n, word, "")
3609
3610# Handle hex in the SHA-256 compression implementation.
3611def hex(ws: List<&2, U32>) -> String:
3612 match ws:
3613 case Nil{}:
3614 ""
3615 case w <> t:
3616 hex_word(w) ++ hex(t)
3617
3618# Handle sha256 in the SHA-256 compression implementation.
3619def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
3620 digest(stream(bytes, 0n, 48n, initial()))