1	import Base
2	import ./state.bend as S
3	
4	type ShaWindow is Data:
5	  W{a: U32, b: U32, c: U32, d: U32, e: U32, f: U32, g: U32, h: U32,
6	    i: U32, j: U32, k: U32, l: U32, m: U32, n: U32, o: U32, p: U32}
7	
8	# SHA-256 for byte sequences. Each input U32 contributes its low 8 bits.
9	# SHA-256 arithmetic is native U32, hence addition wraps modulo 2^32.
10	def initial() -> S.State:
11	  S.H{1779033703, 3144134277, 1013904242, 2773480762,
12	    1359893119, 2600822924, 528734635, 1541459225}
13	
14	def rotr(+x: U32, +n: Nat) -> U32:
15	  (U32.shrn(x, n) .|. U32.shln(x, Nat.sub(32n, n)) : U32)
16	
17	def big0(+x: U32) -> U32:
18	  ((U32.shrn(x, 2n) .|. U32.shln(x, 30n))
19	    .^. (U32.shrn(x, 13n) .|. U32.shln(x, 19n))
20	    .^. (U32.shrn(x, 22n) .|. U32.shln(x, 10n)) : U32)
21	
22	def big1(+x: U32) -> U32:
23	  ((U32.shrn(x, 6n) .|. U32.shln(x, 26n))
24	    .^. (U32.shrn(x, 11n) .|. U32.shln(x, 21n))
25	    .^. (U32.shrn(x, 25n) .|. U32.shln(x, 7n)) : U32)
26	
27	def small0(+x: U32) -> U32:
28	  ((U32.shrn(x, 7n) .|. U32.shln(x, 25n))
29	    .^. (U32.shrn(x, 18n) .|. U32.shln(x, 14n))
30	    .^. U32.shrn(x, 3n) : U32)
31	
32	def small1(+x: U32) -> U32:
33	  ((U32.shrn(x, 17n) .|. U32.shln(x, 15n))
34	    .^. (U32.shrn(x, 19n) .|. U32.shln(x, 13n))
35	    .^. U32.shrn(x, 10n) : U32)
36	
37	def choose(+x: U32, y: U32, z: U32) -> U32:
38	  ((x .&. y) .^. (U32.not(x) .&. z) : U32)
39	
40	def majority(+x: U32, +y: U32, +z: U32) -> U32:
41	  ((x .&. y) .^. (x .&. z) .^. (y .&. z) : U32)
42	
43	def step(s: S.State, k: U32, w: U32) -> S.State:
44	  S.H{+a, +b, +c, d, +e, +f, +g, h} = s
45	  +t1 = (h + big1(e) + choose(e, f, g) + k + w : U32)
46	  t2 = (big0(a) + majority(a, b, c) : U32)
47	  S.H{(t1 + t2 : U32), a, b, c, (d + t1 : U32), e, f, g}
48	
49	def feedforward(x: S.State, y: S.State) -> S.State:
50	  S.H{a, b, c, d, e, f, g, h} = x
51	  S.H{i, j, k, l, m, n, o, p} = y
52	  S.H{(a + i : U32), (b + j : U32), (c + k : U32), (d + l : U32),
53	    (e + m : U32), (f + n : U32), (g + o : U32), (h + p : U32)}
54	
55	def get(xs: List<&2, U32>, n: Nat) -> U32:
56	  match xs n:
57	    case Nil{} _:
58	      0
59	    case h <> t 0n:
60	      h
61	    case h <> t 1n+p:
62	      get(t, p)
63	
64	# Reverse history: at round t, index j contains W[t-1-j].
65	def next_word_slow(+history: List<&2, U32>) -> U32:
66	  (small1(get(history, 1n)) + get(history, 6n)
67	    + small0(get(history, 14n)) + get(history, 15n) : U32)
68	
69	# Schedule histories always contain at least 16 words. Destructuring that prefix
70	# avoids four independent linked-list walks for every expanded word; the fallback
71	# preserves the total behavior used by the universal refinement theorem.
72	def next_word(+history: List<&2, U32>) -> U32:
73	  match history:
74	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> (p <> rest):
75	      (small1(b) + g + small0(o) + p : U32)
76	    case _:
77	      next_word_slow(history)
78	
79	def expand(n: Nat, +history: List<&2, U32>) -> List<&2, U32>:
80	  match n:
81	    case 0n:
82	      Nil{}
83	    case 1n+p:
84	      +w = next_word(history)
85	      w <> expand(p, w <> history)
86	
87	def schedule(extra: Nat, +block: List<&2, U32>) -> List<&2, U32>:
88	  List.append(&2, U32, block,
89	    expand(extra, List.reverse(&2, U32, block)))
90	
91	def rounds(ks: List<&2, U32>, ws: List<&2, U32>, s: S.State) -> S.State:
92	  match ks ws:
93	    case Nil{} _:
94	      s
95	    case k <> kt Nil{}:
96	      s
97	    case k <> kt w <> wt:
98	      rounds(kt, wt, step(s, k, w))
99	
100	# Compression consumes an already expanded 64-word schedule.
101	def compress(ws: List<&2, U32>, ks: List<&2, U32>, +s: S.State) -> S.State:
102	  feedforward(s, rounds(ks, ws, s))
103	
104	# Generate each derived schedule word immediately before its round. The reverse
105	# history is still retained for the recurrence, but the chronological 48-word
106	# extension is never materialized.
107	def expanded_rounds(n: Nat, +history: List<&2, U32>, ks: List<&2, U32>, s: S.State) -> S.State:
108	  match n ks:
109	    case 0n _:
110	      s
111	    case 1n+p Nil{}:
112	      s
113	    case 1n+p k <> kt:
114	      +w = next_word(history)
115	      expanded_rounds(p, w <> history, kt, step(s, k, w))
116	
117	# Consume the original block words, then continue directly with its expansion.
118	def schedule_rounds(ws: List<&2, U32>, +extra: Nat, +history: List<&2, U32>, ks: List<&2, U32>, s: S.State) -> S.State:
119	  match ws ks:
120	    case Nil{} _:
121	      expanded_rounds(extra, history, ks, s)
122	    case w <> wt Nil{}:
123	      s
124	    case w <> wt k <> kt:
125	      schedule_rounds(wt, extra, history, kt, step(s, k, w))
126	
127	# A fixed rolling window drops schedule words as soon as they are older than 16
128	# rounds. This avoids growing and reference-counting the reverse history list.
129	def window_rounds(n: Nat, win: ShaWindow, ks: List<&2, U32>, s: S.State) -> S.State:
130	  match n win ks:
131	    case 0n _ _:
132	      s
133	    case 1n+q _ Nil{}:
134	      s
135	    case 1n+q W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u} k <> kt:
136	      +w = (small1(b) + g + small0(t) + u : U32)
137	      window_rounds(q, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, kt,
138	        step(s, k, w))
139	
140	def window_schedule_rounds(ws: List<&2, U32>, +extra: Nat, win: ShaWindow, ks: List<&2, U32>, s: S.State) -> S.State:
141	  match ws ks:
142	    case Nil{} _:
143	      window_rounds(extra, win, ks, s)
144	    case w <> wt Nil{}:
145	      s
146	    case w <> wt k <> kt:
147	      window_schedule_rounds(wt, extra, win, kt, step(s, k, w))
148	
149	def fused_compress_slow(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:
150	  feedforward(s, schedule_rounds(block, extra, List.reverse(&2, U32, block), ks, s))
151	
152	def fused_compress(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:
153	  match block:
154	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}:
155	      feedforward(s, window_schedule_rounds(
156	        [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra,
157	        W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s))
158	    case _:
159	      fused_compress_slow(block, extra, ks, s)
160	
161	# Fast path for the 16-word blocks produced by block_bytes. It executes the
162	# seed rounds directly and constructs only the fixed rolling window.
163	def window_compress16(+a: U32, +b: U32, +c: U32, +d: U32,
164	  +e: U32, +f: U32, +g: U32, +h: U32,
165	  +i: U32, +j: U32, +k: U32, +l: U32,
166	  +m: U32, +n: U32, +o: U32, +p: U32,
167	  +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:
168	  match ks:
169	    case k0 <> k1 <> k2 <> k3 <> k4 <> k5 <> k6 <> k7 <>
170	      k8 <> k9 <> k10 <> k11 <> k12 <> k13 <> k14 <> k15 <> kt:
171	      s1 = step(s, k0, a)
172	      s2 = step(s1, k1, b)
173	      s3 = step(s2, k2, c)
174	      s4 = step(s3, k3, d)
175	      s5 = step(s4, k4, e)
176	      s6 = step(s5, k5, f)
177	      s7 = step(s6, k6, g)
178	      s8 = step(s7, k7, h)
179	      s9 = step(s8, k8, i)
180	      s10 = step(s9, k9, j)
181	      s11 = step(s10, k10, k)
182	      s12 = step(s11, k11, l)
183	      s13 = step(s12, k12, m)
184	      s14 = step(s13, k13, n)
185	      s15 = step(s14, k14, o)
186	      s16 = step(s15, k15, p)
187	      feedforward(s, window_rounds(extra,
188	        W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, kt, s16))
189	    case _:
190	      fused_compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, ks, s)
191	
192	def be32(+x: U32) -> List<&2, U32>:
193	  [U32.shrn(x, 24n), (U32.shrn(x, 16n) .&. 255 : U32),
194	   (U32.shrn(x, 8n) .&. 255 : U32), (x .&. 255 : U32)]
195	
196	def length_octets(count: Nat, +n: Nat, acc: List<&2, U32>) -> List<&2, U32>:
197	  match count:
198	    case 0n:
199	      acc
200	    case 1n+p:
201	      length_octets(p, Nat.div(n, 256n), U32.from_nat(Nat.mod(n, 256n)) <> acc)
202	
203	def bit_length(+n: Nat) -> List<&2, U32>:
204	  length_octets(7n, Nat.div(n, 32n),
205	    [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])
206	
207	def pack(a: U32, b: U32, c: U32, d: U32) -> U32:
208	  (U32.shln((a .&. 255 : U32), 24n)
209	    .|. U32.shln((b .&. 255 : U32), 16n)
210	    .|. U32.shln((c .&. 255 : U32), 8n) .|. (d .&. 255) : U32)
211	
212	def digest(s: S.State) -> List<&2, U32>:
213	  S.H{a, b, c, d, e, f, g, h} = s
214	  [a, b, c, d, e, f, g, h]
215	
216	# Generic block decoder over a padded byte list and any constant table. The
217	# fast path below is proved equal to it with the FIPS table.
218	def block_bytes(bytes: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, s: S.State) -> S.State:
219	  match bytes:
220	    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:
221	      block_bytes(rest, extra, ks, window_compress16(
222	        pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15),
223	        pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31),
224	        pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47),
225	        pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63),
226	        extra, ks, s))
227	    case _:
228	      s
229	
230	# FIPS 180-4 round constants, the table the specialized rounds below inline.
231	def round_constants() -> List<&2, U32>:
232	  [1116352408, 1899447441, 3049323471, 3921009573,
233	   961987163, 1508970993, 2453635748, 2870763221,
234	   3624381080, 310598401, 607225278, 1426881987,
235	   1925078388, 2162078206, 2614888103, 3248222580,
236	   3835390401, 4022224774, 264347078, 604807628,
237	   770255983, 1249150122, 1555081692, 1996064986,
238	   2554220882, 2821834349, 2952996808, 3210313671,
239	   3336571891, 3584528711, 113926993, 338241895,
240	   666307205, 773529912, 1294757372, 1396182291,
241	   1695183700, 1986661051, 2177026350, 2456956037,
242	   2730485921, 2820302411, 3259730800, 3345764771,
243	   3516065817, 3600352804, 4094571909, 275423344,
244	   430227734, 506948616, 659060556, 883997877,
245	   958139571, 1322822218, 1537002063, 1747873779,
246	   1955562222, 2024104815, 2227730452, 2361852424,
247	   2428436474, 2756734187, 3204031479, 3329325298]
248	
249	# SHA-256 round t (16 <= t < 64) with its constant as a literal. Like
250	# window_rounds, q bounds the remaining rounds (48 for SHA-256) and each round
251	# derives its schedule word from the rolling window before continuing with
252	# round t+1. Defined last-to-first because names must precede use.
253	def kr64(q: Nat, win: ShaWindow, s: S.State) -> S.State:
254	  s
255	
256	def kr63(q: Nat, win: ShaWindow, s: S.State) -> S.State:
257	  match q win:
258	    case 0n _:
259	      s
260	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
261	      +w = (small1(b) + g + small0(t) + u : U32)
262	      kr64(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3329325298, w))
263	
264	def kr62(q: Nat, win: ShaWindow, s: S.State) -> S.State:
265	  match q win:
266	    case 0n _:
267	      s
268	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
269	      +w = (small1(b) + g + small0(t) + u : U32)
270	      kr63(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3204031479, w))
271	
272	def kr61(q: Nat, win: ShaWindow, s: S.State) -> S.State:
273	  match q win:
274	    case 0n _:
275	      s
276	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
277	      +w = (small1(b) + g + small0(t) + u : U32)
278	      kr62(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2756734187, w))
279	
280	def kr60(q: Nat, win: ShaWindow, s: S.State) -> S.State:
281	  match q win:
282	    case 0n _:
283	      s
284	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
285	      +w = (small1(b) + g + small0(t) + u : U32)
286	      kr61(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2428436474, w))
287	
288	def kr59(q: Nat, win: ShaWindow, s: S.State) -> S.State:
289	  match q win:
290	    case 0n _:
291	      s
292	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
293	      +w = (small1(b) + g + small0(t) + u : U32)
294	      kr60(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2361852424, w))
295	
296	def kr58(q: Nat, win: ShaWindow, s: S.State) -> S.State:
297	  match q win:
298	    case 0n _:
299	      s
300	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
301	      +w = (small1(b) + g + small0(t) + u : U32)
302	      kr59(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2227730452, w))
303	
304	def kr57(q: Nat, win: ShaWindow, s: S.State) -> S.State:
305	  match q win:
306	    case 0n _:
307	      s
308	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
309	      +w = (small1(b) + g + small0(t) + u : U32)
310	      kr58(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2024104815, w))
311	
312	def kr56(q: Nat, win: ShaWindow, s: S.State) -> S.State:
313	  match q win:
314	    case 0n _:
315	      s
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	      kr57(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1955562222, w))
319	
320	def kr55(q: Nat, win: ShaWindow, s: S.State) -> S.State:
321	  match q win:
322	    case 0n _:
323	      s
324	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
325	      +w = (small1(b) + g + small0(t) + u : U32)
326	      kr56(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1747873779, w))
327	
328	def kr54(q: Nat, win: ShaWindow, s: S.State) -> S.State:
329	  match q win:
330	    case 0n _:
331	      s
332	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
333	      +w = (small1(b) + g + small0(t) + u : U32)
334	      kr55(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1537002063, w))
335	
336	def kr53(q: Nat, win: ShaWindow, s: S.State) -> S.State:
337	  match q win:
338	    case 0n _:
339	      s
340	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
341	      +w = (small1(b) + g + small0(t) + u : U32)
342	      kr54(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1322822218, w))
343	
344	def kr52(q: Nat, win: ShaWindow, s: S.State) -> S.State:
345	  match q win:
346	    case 0n _:
347	      s
348	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
349	      +w = (small1(b) + g + small0(t) + u : U32)
350	      kr53(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 958139571, w))
351	
352	def kr51(q: Nat, win: ShaWindow, s: S.State) -> S.State:
353	  match q win:
354	    case 0n _:
355	      s
356	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
357	      +w = (small1(b) + g + small0(t) + u : U32)
358	      kr52(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 883997877, w))
359	
360	def kr50(q: Nat, win: ShaWindow, s: S.State) -> S.State:
361	  match q win:
362	    case 0n _:
363	      s
364	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
365	      +w = (small1(b) + g + small0(t) + u : U32)
366	      kr51(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 659060556, w))
367	
368	def kr49(q: Nat, win: ShaWindow, s: S.State) -> S.State:
369	  match q win:
370	    case 0n _:
371	      s
372	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
373	      +w = (small1(b) + g + small0(t) + u : U32)
374	      kr50(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 506948616, w))
375	
376	def kr48(q: Nat, win: ShaWindow, s: S.State) -> S.State:
377	  match q win:
378	    case 0n _:
379	      s
380	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
381	      +w = (small1(b) + g + small0(t) + u : U32)
382	      kr49(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 430227734, w))
383	
384	def kr47(q: Nat, win: ShaWindow, s: S.State) -> S.State:
385	  match q win:
386	    case 0n _:
387	      s
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	      kr48(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 275423344, w))
391	
392	def kr46(q: Nat, win: ShaWindow, s: S.State) -> S.State:
393	  match q win:
394	    case 0n _:
395	      s
396	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
397	      +w = (small1(b) + g + small0(t) + u : U32)
398	      kr47(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 4094571909, w))
399	
400	def kr45(q: Nat, win: ShaWindow, s: S.State) -> S.State:
401	  match q win:
402	    case 0n _:
403	      s
404	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
405	      +w = (small1(b) + g + small0(t) + u : U32)
406	      kr46(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3600352804, w))
407	
408	def kr44(q: Nat, win: ShaWindow, s: S.State) -> S.State:
409	  match q win:
410	    case 0n _:
411	      s
412	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
413	      +w = (small1(b) + g + small0(t) + u : U32)
414	      kr45(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3516065817, w))
415	
416	def kr43(q: Nat, win: ShaWindow, s: S.State) -> S.State:
417	  match q win:
418	    case 0n _:
419	      s
420	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
421	      +w = (small1(b) + g + small0(t) + u : U32)
422	      kr44(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3345764771, w))
423	
424	def kr42(q: Nat, win: ShaWindow, s: S.State) -> S.State:
425	  match q win:
426	    case 0n _:
427	      s
428	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
429	      +w = (small1(b) + g + small0(t) + u : U32)
430	      kr43(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3259730800, w))
431	
432	def kr41(q: Nat, win: ShaWindow, s: S.State) -> S.State:
433	  match q win:
434	    case 0n _:
435	      s
436	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
437	      +w = (small1(b) + g + small0(t) + u : U32)
438	      kr42(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2820302411, w))
439	
440	def kr40(q: Nat, win: ShaWindow, s: S.State) -> S.State:
441	  match q win:
442	    case 0n _:
443	      s
444	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
445	      +w = (small1(b) + g + small0(t) + u : U32)
446	      kr41(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2730485921, w))
447	
448	def kr39(q: Nat, win: ShaWindow, s: S.State) -> S.State:
449	  match q win:
450	    case 0n _:
451	      s
452	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
453	      +w = (small1(b) + g + small0(t) + u : U32)
454	      kr40(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2456956037, w))
455	
456	def kr38(q: Nat, win: ShaWindow, s: S.State) -> S.State:
457	  match q win:
458	    case 0n _:
459	      s
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	      kr39(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2177026350, w))
463	
464	def kr37(q: Nat, win: ShaWindow, s: S.State) -> S.State:
465	  match q win:
466	    case 0n _:
467	      s
468	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
469	      +w = (small1(b) + g + small0(t) + u : U32)
470	      kr38(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1986661051, w))
471	
472	def kr36(q: Nat, win: ShaWindow, s: S.State) -> S.State:
473	  match q win:
474	    case 0n _:
475	      s
476	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
477	      +w = (small1(b) + g + small0(t) + u : U32)
478	      kr37(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1695183700, w))
479	
480	def kr35(q: Nat, win: ShaWindow, s: S.State) -> S.State:
481	  match q win:
482	    case 0n _:
483	      s
484	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
485	      +w = (small1(b) + g + small0(t) + u : U32)
486	      kr36(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1396182291, w))
487	
488	def kr34(q: Nat, win: ShaWindow, s: S.State) -> S.State:
489	  match q win:
490	    case 0n _:
491	      s
492	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
493	      +w = (small1(b) + g + small0(t) + u : U32)
494	      kr35(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1294757372, w))
495	
496	def kr33(q: Nat, win: ShaWindow, s: S.State) -> S.State:
497	  match q win:
498	    case 0n _:
499	      s
500	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
501	      +w = (small1(b) + g + small0(t) + u : U32)
502	      kr34(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 773529912, w))
503	
504	def kr32(q: Nat, win: ShaWindow, s: S.State) -> S.State:
505	  match q win:
506	    case 0n _:
507	      s
508	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
509	      +w = (small1(b) + g + small0(t) + u : U32)
510	      kr33(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 666307205, w))
511	
512	def kr31(q: Nat, win: ShaWindow, s: S.State) -> S.State:
513	  match q win:
514	    case 0n _:
515	      s
516	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
517	      +w = (small1(b) + g + small0(t) + u : U32)
518	      kr32(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 338241895, w))
519	
520	def kr30(q: Nat, win: ShaWindow, s: S.State) -> S.State:
521	  match q win:
522	    case 0n _:
523	      s
524	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
525	      +w = (small1(b) + g + small0(t) + u : U32)
526	      kr31(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 113926993, w))
527	
528	def kr29(q: Nat, win: ShaWindow, s: S.State) -> S.State:
529	  match q win:
530	    case 0n _:
531	      s
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	      kr30(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3584528711, w))
535	
536	def kr28(q: Nat, win: ShaWindow, s: S.State) -> S.State:
537	  match q win:
538	    case 0n _:
539	      s
540	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
541	      +w = (small1(b) + g + small0(t) + u : U32)
542	      kr29(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3336571891, w))
543	
544	def kr27(q: Nat, win: ShaWindow, s: S.State) -> S.State:
545	  match q win:
546	    case 0n _:
547	      s
548	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
549	      +w = (small1(b) + g + small0(t) + u : U32)
550	      kr28(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3210313671, w))
551	
552	def kr26(q: Nat, win: ShaWindow, s: S.State) -> S.State:
553	  match q win:
554	    case 0n _:
555	      s
556	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
557	      +w = (small1(b) + g + small0(t) + u : U32)
558	      kr27(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2952996808, w))
559	
560	def kr25(q: Nat, win: ShaWindow, s: S.State) -> S.State:
561	  match q win:
562	    case 0n _:
563	      s
564	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
565	      +w = (small1(b) + g + small0(t) + u : U32)
566	      kr26(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2821834349, w))
567	
568	def kr24(q: Nat, win: ShaWindow, s: S.State) -> S.State:
569	  match q win:
570	    case 0n _:
571	      s
572	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
573	      +w = (small1(b) + g + small0(t) + u : U32)
574	      kr25(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2554220882, w))
575	
576	def kr23(q: Nat, win: ShaWindow, s: S.State) -> S.State:
577	  match q win:
578	    case 0n _:
579	      s
580	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
581	      +w = (small1(b) + g + small0(t) + u : U32)
582	      kr24(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1996064986, w))
583	
584	def kr22(q: Nat, win: ShaWindow, s: S.State) -> S.State:
585	  match q win:
586	    case 0n _:
587	      s
588	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
589	      +w = (small1(b) + g + small0(t) + u : U32)
590	      kr23(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1555081692, w))
591	
592	def kr21(q: Nat, win: ShaWindow, s: S.State) -> S.State:
593	  match q win:
594	    case 0n _:
595	      s
596	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
597	      +w = (small1(b) + g + small0(t) + u : U32)
598	      kr22(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1249150122, w))
599	
600	def kr20(q: Nat, win: ShaWindow, s: S.State) -> S.State:
601	  match q win:
602	    case 0n _:
603	      s
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	      kr21(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 770255983, w))
607	
608	def kr19(q: Nat, win: ShaWindow, s: S.State) -> S.State:
609	  match q win:
610	    case 0n _:
611	      s
612	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
613	      +w = (small1(b) + g + small0(t) + u : U32)
614	      kr20(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 604807628, w))
615	
616	def kr18(q: Nat, win: ShaWindow, s: S.State) -> S.State:
617	  match q win:
618	    case 0n _:
619	      s
620	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
621	      +w = (small1(b) + g + small0(t) + u : U32)
622	      kr19(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 264347078, w))
623	
624	def kr17(q: Nat, win: ShaWindow, s: S.State) -> S.State:
625	  match q win:
626	    case 0n _:
627	      s
628	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
629	      +w = (small1(b) + g + small0(t) + u : U32)
630	      kr18(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 4022224774, w))
631	
632	def kr16(q: Nat, win: ShaWindow, s: S.State) -> S.State:
633	  match q win:
634	    case 0n _:
635	      s
636	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
637	      +w = (small1(b) + g + small0(t) + u : U32)
638	      kr17(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3835390401, w))
639	
640	# window_compress16 specialized to the FIPS table: no constant list is walked.
641	def fips_compress16(+a: U32, +b: U32, +c: U32, +d: U32,
642	  +e: U32, +f: U32, +g: U32, +h: U32,
643	  +i: U32, +j: U32, +k: U32, +l: U32,
644	  +m: U32, +n: U32, +o: U32, +p: U32, +q: Nat, +s: S.State) -> S.State:
645	  s1 = step(s, 1116352408, a)
646	  s2 = step(s1, 1899447441, b)
647	  s3 = step(s2, 3049323471, c)
648	  s4 = step(s3, 3921009573, d)
649	  s5 = step(s4, 961987163, e)
650	  s6 = step(s5, 1508970993, f)
651	  s7 = step(s6, 2453635748, g)
652	  s8 = step(s7, 2870763221, h)
653	  s9 = step(s8, 3624381080, i)
654	  s10 = step(s9, 310598401, j)
655	  s11 = step(s10, 607225278, k)
656	  s12 = step(s11, 1426881987, l)
657	  s13 = step(s12, 1925078388, m)
658	  s14 = step(s13, 2162078206, n)
659	  s15 = step(s14, 2614888103, o)
660	  s16 = step(s15, 3248222580, p)
661	  feedforward(s, kr16(q, W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, s16))
662	
663	# FIPS padding suffix for a message of n bytes, computed with modular
664	# arithmetic. The proofs state the streaming hash in terms of it.
665	def suffix(+n: Nat) -> List<&2, U32>:
666	  128 <> List.append(&2, U32,
667	    List.replicate(U32, Nat.mod(Nat.sub(119n, Nat.mod(n, 64n)), 64n), 0), bit_length(n))
668	
669	# Big-endian words of the 64-bit message bit length 8n, computed from n with
670	# exactly the digit expressions bit_length produces, but without building and
671	# matching an eight-element list. bit_length(n) is [o(d6), .., o(d0), low]
672	# where d0 = n / 32, d(k+1) = dk / 256 and o(x) = x mod 256.
673	def len_hi(+n: Nat) -> U32:
674	  +d0 = Nat.div(n, 32n)
675	  +d1 = Nat.div(d0, 256n)
676	  +d2 = Nat.div(d1, 256n)
677	  +d3 = Nat.div(d2, 256n)
678	  +d4 = Nat.div(d3, 256n)
679	  +d5 = Nat.div(d4, 256n)
680	  +d6 = Nat.div(d5, 256n)
681	  pack(U32.from_nat(Nat.mod(d6, 256n)), U32.from_nat(Nat.mod(d5, 256n)),
682	    U32.from_nat(Nat.mod(d4, 256n)), U32.from_nat(Nat.mod(d3, 256n)))
683	
684	def len_lo(+n: Nat) -> U32:
685	  +d0 = Nat.div(n, 32n)
686	  +d1 = Nat.div(d0, 256n)
687	  +d2 = Nat.div(d1, 256n)
688	  pack(U32.from_nat(Nat.mod(d2, 256n)), U32.from_nat(Nat.mod(d1, 256n)),
689	    U32.from_nat(Nat.mod(d0, 256n)), U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n))
690	
691	# Final block(s) for an n-byte message ending in r = 0..63 tail bytes. Each
692	# tail length has its own padded layout: the tail bytes, the 0x80 marker, the
693	# zero fill and the big-endian bit length are packed straight into schedule
694	# words, so no padded list is built.
695	def fin0(+n: Nat, +extra: Nat, s: S.State) -> S.State:
696	  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(n), len_lo(n),
697	    extra, s)
698	
699	def fin1(+t0: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
700	  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(n), len_lo(n),
701	    extra, s)
702	
703	def fin2(+t0: U32, +t1: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
704	  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(n), len_lo(n),
705	    extra, s)
706	
707	def fin3(+t0: U32, +t1: U32, +t2: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
708	  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(n), len_lo(n),
709	    extra, s)
710	
711	def fin4(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
712	  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(n), len_lo(n),
713	    extra, s)
714	
715	def fin5(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
716	  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(n), len_lo(n),
717	    extra, s)
718	
719	def fin6(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
720	  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(n), len_lo(n),
721	    extra, s)
722	
723	def fin7(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
724	  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(n), len_lo(n),
725	    extra, s)
726	
727	def fin8(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
728	  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(n), len_lo(n),
729	    extra, s)
730	
731	def fin9(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
732	  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(n), len_lo(n),
733	    extra, s)
734	
735	def fin10(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
736	  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(n), len_lo(n),
737	    extra, s)
738	
739	def fin11(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
740	  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(n), len_lo(n),
741	    extra, s)
742	
743	def fin12(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
744	  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(n), len_lo(n),
745	    extra, s)
746	
747	def fin13(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
748	  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(n), len_lo(n),
749	    extra, s)
750	
751	def fin14(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
752	  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(n), len_lo(n),
753	    extra, s)
754	
755	def fin15(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
756	  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(n), len_lo(n),
757	    extra, s)
758	
759	def fin16(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
760	  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(n), len_lo(n),
761	    extra, s)
762	
763	def fin17(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
764	  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(n), len_lo(n),
765	    extra, s)
766	
767	def fin18(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
768	  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(n), len_lo(n),
769	    extra, s)
770	
771	def fin19(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
772	  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(n), len_lo(n),
773	    extra, s)
774	
775	def fin20(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
776	  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(n), len_lo(n),
777	    extra, s)
778	
779	def fin21(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
780	  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(n), len_lo(n),
781	    extra, s)
782	
783	def fin22(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
784	  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(n), len_lo(n),
785	    extra, s)
786	
787	def fin23(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
788	  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(n), len_lo(n),
789	    extra, s)
790	
791	def fin24(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
792	  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(n), len_lo(n),
793	    extra, s)
794	
795	def fin25(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
796	  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(n), len_lo(n),
797	    extra, s)
798	
799	def fin26(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
800	  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(n), len_lo(n),
801	    extra, s)
802	
803	def fin27(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
804	  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(n), len_lo(n),
805	    extra, s)
806	
807	def fin28(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
808	  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(n), len_lo(n),
809	    extra, s)
810	
811	def fin29(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
812	  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(n), len_lo(n),
813	    extra, s)
814	
815	def fin30(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
816	  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(n), len_lo(n),
817	    extra, s)
818	
819	def fin31(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
820	  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(n), len_lo(n),
821	    extra, s)
822	
823	def fin32(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
824	  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(n), len_lo(n),
825	    extra, s)
826	
827	def fin33(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
828	  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(n), len_lo(n),
829	    extra, s)
830	
831	def fin34(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
832	  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(n), len_lo(n),
833	    extra, s)
834	
835	def fin35(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
836	  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(n), len_lo(n),
837	    extra, s)
838	
839	def fin36(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
840	  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(n), len_lo(n),
841	    extra, s)
842	
843	def fin37(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
844	  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(n), len_lo(n),
845	    extra, s)
846	
847	def fin38(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
848	  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(n), len_lo(n),
849	    extra, s)
850	
851	def fin39(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
852	  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(n), len_lo(n),
853	    extra, s)
854	
855	def fin40(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
856	  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(n), len_lo(n),
857	    extra, s)
858	
859	def fin41(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
860	  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(n), len_lo(n),
861	    extra, s)
862	
863	def fin42(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
864	  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(n), len_lo(n),
865	    extra, s)
866	
867	def fin43(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
868	  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(n), len_lo(n),
869	    extra, s)
870	
871	def fin44(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
872	  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(n), len_lo(n),
873	    extra, s)
874	
875	def fin45(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
876	  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(n), len_lo(n),
877	    extra, s)
878	
879	def fin46(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
880	  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(n), len_lo(n),
881	    extra, s)
882	
883	def fin47(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
884	  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(n), len_lo(n),
885	    extra, s)
886	
887	def fin48(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
888	  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(n), len_lo(n),
889	    extra, s)
890	
891	def fin49(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
892	  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(n), len_lo(n),
893	    extra, s)
894	
895	def fin50(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
896	  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(n), len_lo(n),
897	    extra, s)
898	
899	def fin51(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
900	  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(n), len_lo(n),
901	    extra, s)
902	
903	def fin52(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
904	  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(n), len_lo(n),
905	    extra, s)
906	
907	def fin53(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
908	  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(n), len_lo(n),
909	    extra, s)
910	
911	def fin54(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
912	  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(n), len_lo(n),
913	    extra, s)
914	
915	def fin55(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
916	  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(n), len_lo(n),
917	    extra, s)
918	
919	def fin56(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
920	  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(n), len_lo(n),
921	    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),
922	    extra, s))
923	
924	def fin57(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
925	  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(n), len_lo(n),
926	    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),
927	    extra, s))
928	
929	def fin58(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
930	  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(n), len_lo(n),
931	    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),
932	    extra, s))
933	
934	def fin59(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
935	  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(n), len_lo(n),
936	    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),
937	    extra, s))
938	
939	def fin60(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
940	  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(n), len_lo(n),
941	    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),
942	    extra, s))
943	
944	def fin61(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +t60: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
945	  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(n), len_lo(n),
946	    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),
947	    extra, s))
948	
949	def fin62(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +t60: U32, +t61: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
950	  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(n), len_lo(n),
951	    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),
952	    extra, s))
953	
954	def fin63(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +t60: U32, +t61: U32, +t62: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
955	  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(n), len_lo(n),
956	    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),
957	    extra, s))
958	
959	# Tail-recursive block loop over an already padded byte list.
960	def fips_blocks(bytes: List<&2, U32>, +extra: Nat, s: S.State) -> S.State:
961	  match bytes:
962	    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:
963	      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, s))
964	    case _:
965	      s
966	
967	def zeros_onto(z: Nat, acc: List<&2, U32>) -> List<&2, U32>:
968	  match z:
969	    case 0n:
970	      acc
971	    case 1n+p:
972	      zeros_onto(p, 0 <> acc)
973	
974	# The padding suffix built only with tail-recursive loops.
975	def padding(+n: Nat) -> List<&2, U32>:
976	  128 <> zeros_onto(Nat.mod(Nat.sub(119n, Nat.mod(n, 64n)), 64n), bit_length(n))
977	
978	def byte_count(bytes: List<&2, U32>, acc: Nat) -> Nat:
979	  match bytes:
980	    case Nil{}:
981	      acc
982	    case h <> t:
983	      byte_count(t, 1n+acc)
984	
985	# Final block(s) of an n-byte message whose tail has fewer than 64 bytes.
986	# stream never passes 64 or more bytes; that case pads with tail-recursive
987	# loops. The match is exhaustive: a default case would make Bend rebuild the
988	# consumed cells at every depth. Length words are computed directly from n; note
989	# that sharing any List<U32> would make Bend reference-count every list match,
990	# including the input loop in stream.
991	def finish_n(+tail: List<&2, U32>, +n: Nat, +extra: Nat, s: S.State) -> S.State:
992	  match tail:
993	    case Nil{}:
994	      fin0(n, extra, s)
995	    case t0 <> Nil{}:
996	      fin1(t0, n, extra, s)
997	    case t0 <> t1 <> Nil{}:
998	      fin2(t0, t1, n, extra, s)
999	    case t0 <> t1 <> t2 <> Nil{}:
1000	      fin3(t0, t1, t2, n, extra, s)
1001	    case t0 <> t1 <> t2 <> t3 <> Nil{}:
1002	      fin4(t0, t1, t2, t3, n, extra, s)
1003	    case t0 <> t1 <> t2 <> t3 <> t4 <> Nil{}:
1004	      fin5(t0, t1, t2, t3, t4, n, extra, s)
1005	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> Nil{}:
1006	      fin6(t0, t1, t2, t3, t4, t5, n, extra, s)
1007	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> Nil{}:
1008	      fin7(t0, t1, t2, t3, t4, t5, t6, n, extra, s)
1009	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> Nil{}:
1010	      fin8(t0, t1, t2, t3, t4, t5, t6, t7, n, extra, s)
1011	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> Nil{}:
1012	      fin9(t0, t1, t2, t3, t4, t5, t6, t7, t8, n, extra, s)
1013	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> Nil{}:
1014	      fin10(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, n, extra, s)
1015	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> Nil{}:
1016	      fin11(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, n, extra, s)
1017	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> Nil{}:
1018	      fin12(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, n, extra, s)
1019	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> Nil{}:
1020	      fin13(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, n, extra, s)
1021	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> Nil{}:
1022	      fin14(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, n, extra, s)
1023	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> Nil{}:
1024	      fin15(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, n, extra, s)
1025	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> Nil{}:
1026	      fin16(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, n, extra, s)
1027	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> Nil{}:
1028	      fin17(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, n, extra, s)
1029	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> Nil{}:
1030	      fin18(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, n, extra, s)
1031	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> Nil{}:
1032	      fin19(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, n, extra, s)
1033	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> Nil{}:
1034	      fin20(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, n, extra, s)
1035	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> Nil{}:
1036	      fin21(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, n, extra, s)
1037	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> Nil{}:
1038	      fin22(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, n, extra, s)
1039	    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{}:
1040	      fin23(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, n, extra, s)
1041	    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{}:
1042	      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, n, extra, s)
1043	    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{}:
1044	      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, n, extra, s)
1045	    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{}:
1046	      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, n, extra, s)
1047	    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{}:
1048	      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, n, extra, s)
1049	    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{}:
1050	      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, n, extra, s)
1051	    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{}:
1052	      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, n, extra, s)
1053	    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{}:
1054	      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, n, extra, s)
1055	    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{}:
1056	      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, n, extra, s)
1057	    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{}:
1058	      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, n, extra, s)
1059	    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{}:
1060	      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, n, extra, s)
1061	    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{}:
1062	      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, n, extra, s)
1063	    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{}:
1064	      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, n, extra, s)
1065	    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{}:
1066	      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, n, extra, s)
1067	    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{}:
1068	      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, n, extra, s)
1069	    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{}:
1070	      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, n, extra, s)
1071	    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{}:
1072	      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, n, extra, s)
1073	    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{}:
1074	      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, n, extra, s)
1075	    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{}:
1076	      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, n, extra, s)
1077	    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{}:
1078	      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, n, extra, s)
1079	    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{}:
1080	      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, n, extra, s)
1081	    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{}:
1082	      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, n, extra, s)
1083	    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{}:
1084	      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, n, extra, s)
1085	    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{}:
1086	      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, n, extra, s)
1087	    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{}:
1088	      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, n, extra, s)
1089	    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{}:
1090	      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, n, extra, s)
1091	    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{}:
1092	      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, n, extra, s)
1093	    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{}:
1094	      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, n, extra, s)
1095	    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{}:
1096	      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, n, extra, s)
1097	    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{}:
1098	      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, n, extra, s)
1099	    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{}:
1100	      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, n, extra, s)
1101	    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{}:
1102	      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, n, extra, s)
1103	    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{}:
1104	      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, n, extra, s)
1105	    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{}:
1106	      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, n, extra, s)
1107	    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{}:
1108	      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, n, extra, s)
1109	    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{}:
1110	      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, n, extra, s)
1111	    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{}:
1112	      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, n, extra, s)
1113	    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{}:
1114	      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, n, extra, s)
1115	    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{}:
1116	      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, n, extra, s)
1117	    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{}:
1118	      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, n, extra, s)
1119	    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{}:
1120	      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, n, extra, s)
1121	    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:
1122	      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(n)), extra, s)
1123	
1124	# count is the number of bytes already hashed, always a multiple of 64.
1125	def finish(+tail: List<&2, U32>, count: Nat, +extra: Nat, s: S.State) -> S.State:
1126	  finish_n(tail, byte_count(tail, count), extra, s)
1127	
1128	# Compress complete 64-byte blocks straight from the input list, so the
1129	# message is never copied, counted or reversed. count is the number of bytes
1130	# already hashed and extra the number of derived schedule words (48).
1131	def stream(+bytes: List<&2, U32>, count: Nat, +extra: Nat, s: S.State) -> S.State:
1132	  match bytes:
1133	    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:
1134	      stream(rest, Nat.add(64n, count), extra, fips_compress16(
1135	        pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15),
1136	        pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31),
1137	        pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47),
1138	        pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63),
1139	        extra, s))
1140	    case _:
1141	      finish(bytes, count, extra, s)
1142	
1143	# ASCII convenience only; binary inputs use sha256 directly.
1144	def ascii(s: String) -> List<&2, U32>:
1145	  match s:
1146	    case SNil{}:
1147	      Nil{}
1148	    case SCon{Chr{c}, t}:
1149	      c <> ascii(t)
1150	
1151	def hex_digit_if(x: U32, small: Bool) -> Char:
1152	  match small:
1153	    case True{}:
1154	      Chr{(48 + x : U32)}
1155	    case False{}:
1156	      Chr{(87 + x : U32)}
1157	
1158	def hex_digit(+x: U32) -> Char:
1159	  hex_digit_if(x, U32.is_lt(x, 10))
1160	
1161	def hex_word_go(n: Nat, +x: U32, acc: String) -> String:
1162	  match n:
1163	    case 0n:
1164	      acc
1165	    case 1n+p:
1166	      hex_word_go(p, U32.shrn(x, 4n), SCon{hex_digit((x .&. 15 : U32)), acc})
1167	
1168	def hex_word(x: U32) -> String:
1169	  hex_word_go(8n, x, "")
1170	
1171	def hex(ws: List<&2, U32>) -> String:
1172	  match ws:
1173	    case Nil{}:
1174	      ""
1175	    case w <> t:
1176	      hex_word(w) ++ hex(t)
1177	
1178	def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
1179	  digest(stream(bytes, 0n, 48n, initial()))