src/hub_sha/core.bend

mylsm-lsm-store@0.6.0.1 · 3,620 lines · 163 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.6.0.1/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()))