1	# Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f
2	# (src/crypto/sha/core.bend), byte-identical except `Window` renamed to
3	# `ShaWindow`: Bend 2.0.28 Base added a GUI `Window` type that collides with
4	# this module's schedule-window type. Verify against NIST vectors, not the
5	# upstream PROOF.bend (which covers the original names).
6	import Base
7	import ./state.bend as S
8	
9	# Represent ShaWindow data used by the SHA-256 compression implementation.
10	type ShaWindow is Data:
11	  W{a: U32, b: U32, c: U32, d: U32, e: U32, f: U32, g: U32, h: U32,
12	    i: U32, j: U32, k: U32, l: U32, m: U32, n: U32, o: U32, p: U32}
13	
14	# SHA-256 for byte sequences. Each input U32 contributes its low 8 bits.
15	# SHA-256 arithmetic is native U32, hence addition wraps modulo 2^32.
16	def initial() -> S.State:
17	  S.H{1779033703, 3144134277, 1013904242, 2773480762,
18	    1359893119, 2600822924, 528734635, 1541459225}
19	
20	# Handle rotr in the SHA-256 compression implementation.
21	def rotr(+word: U32, +bit_shift: Nat) -> U32:
22	  (U32.shrn(word, bit_shift) .|. U32.shln(word, Nat.sub(32n, bit_shift)) : U32)
23	
24	# Compute the big sigma function for 0 for the SHA-256 compression implementation.
25	def big0(+word: U32) -> U32:
26	  ((U32.shrn(word, 2n) .|. U32.shln(word, 30n))
27	    .^. (U32.shrn(word, 13n) .|. U32.shln(word, 19n))
28	    .^. (U32.shrn(word, 22n) .|. U32.shln(word, 10n)) : U32)
29	
30	# Compute the big sigma function for 1 for the SHA-256 compression implementation.
31	def big1(+word: U32) -> U32:
32	  ((U32.shrn(word, 6n) .|. U32.shln(word, 26n))
33	    .^. (U32.shrn(word, 11n) .|. U32.shln(word, 21n))
34	    .^. (U32.shrn(word, 25n) .|. U32.shln(word, 7n)) : U32)
35	
36	# Compute the small sigma function for 0 for the SHA-256 compression implementation.
37	def small0(+word: U32) -> U32:
38	  ((U32.shrn(word, 7n) .|. U32.shln(word, 25n))
39	    .^. (U32.shrn(word, 18n) .|. U32.shln(word, 14n))
40	    .^. U32.shrn(word, 3n) : U32)
41	
42	# Compute the small sigma function for 1 for the SHA-256 compression implementation.
43	def small1(+word: U32) -> U32:
44	  ((U32.shrn(word, 17n) .|. U32.shln(word, 15n))
45	    .^. (U32.shrn(word, 19n) .|. U32.shln(word, 13n))
46	    .^. U32.shrn(word, 10n) : U32)
47	
48	# Handle choose in the SHA-256 compression implementation.
49	def choose(+word_x: U32, word_y: U32, word_z: U32) -> U32:
50	  ((word_x .&. word_y) .^. (U32.not(word_x) .&. word_z) : U32)
51	
52	# Handle majority in the SHA-256 compression implementation.
53	def majority(+word_x: U32, +word_y: U32, +word_z: U32) -> U32:
54	  ((word_x .&. word_y) .^. (word_x .&. word_z) .^. (word_y .&. word_z) : U32)
55	
56	# Handle step in the SHA-256 compression implementation.
57	def step(state: S.State, round_constant: U32, schedule_word: U32) -> S.State:
58	  S.H{+a, +b, +c, d, +e, +f, +g, h} = state
59	  +t1 = (h + big1(e) + choose(e, f, g) + round_constant + schedule_word : U32)
60	  t2 = (big0(a) + majority(a, b, c) : U32)
61	  S.H{(t1 + t2 : U32), a, b, c, (d + t1 : U32), e, f, g}
62	
63	# Feed forward for the SHA-256 compression implementation.
64	def feedforward(prior_state: S.State, round_state: S.State) -> S.State:
65	  S.H{a, b, c, d, e, f, g, h} = prior_state
66	  S.H{i, j, k, l, m, n, o, p} = round_state
67	  S.H{(a + i : U32), (b + j : U32), (c + k : U32), (d + l : U32),
68	    (e + m : U32), (f + n : U32), (g + o : U32), (h + p : U32)}
69	
70	# Handle get in the SHA-256 compression implementation.
71	def get(xs: List<&2, U32>, index: Nat) -> U32:
72	  match xs index:
73	    case Nil{} _:
74	      0
75	    case h <> t 0n:
76	      h
77	    case h <> t 1n+p:
78	      get(t, p)
79	
80	# Reverse history: at round t, index j contains W[t-1-j].
81	def next_word_slow(+history: List<&2, U32>) -> U32:
82	  (small1(get(history, 1n)) + get(history, 6n)
83	    + small0(get(history, 14n)) + get(history, 15n) : U32)
84	
85	# Schedule histories always contain at least 16 words. Destructuring that prefix
86	# avoids four independent linked-list walks for every expanded word; the fallback
87	# preserves the total behavior used by the universal refinement theorem.
88	def next_word(+history: List<&2, U32>) -> U32:
89	  match history:
90	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> (p <> rest):
91	      (small1(b) + g + small0(o) + p : U32)
92	    case _:
93	      next_word_slow(history)
94	
95	# Handle expand in the SHA-256 compression implementation.
96	def expand(rounds_left: Nat, +history: List<&2, U32>) -> List<&2, U32>:
97	  match rounds_left:
98	    case 0n:
99	      Nil{}
100	    case 1n+p:
101	      +w = next_word(history)
102	      w <> expand(p, w <> history)
103	
104	# Handle schedule in the SHA-256 compression implementation.
105	def schedule(extra: Nat, +block: List<&2, U32>) -> List<&2, U32>:
106	  List.append(&2, U32, block,
107	    expand(extra, List.reverse(&2, U32, block)))
108	
109	# Handle rounds in the SHA-256 compression implementation.
110	def rounds(ks: List<&2, U32>, ws: List<&2, U32>, state: S.State) -> S.State:
111	  match ks ws:
112	    case Nil{} _:
113	      state
114	    case k <> kt Nil{}:
115	      state
116	    case k <> kt w <> wt:
117	      rounds(kt, wt, step(state, k, w))
118	
119	# Compression consumes an already expanded 64-word schedule.
120	def compress(ws: List<&2, U32>, ks: List<&2, U32>, +state: S.State) -> S.State:
121	  feedforward(state, rounds(ks, ws, state))
122	
123	# Generate each derived schedule word immediately before its round. The reverse
124	# history is still retained for the recurrence, but the chronological 48-word
125	# extension is never materialized.
126	def expanded_rounds(rounds_left: Nat, +history: List<&2, U32>, ks: List<&2, U32>, state: S.State) -> S.State:
127	  match rounds_left ks:
128	    case 0n _:
129	      state
130	    case 1n+p Nil{}:
131	      state
132	    case 1n+p k <> kt:
133	      +w = next_word(history)
134	      expanded_rounds(p, w <> history, kt, step(state, k, w))
135	
136	# Consume the original block words, then continue directly with its expansion.
137	def schedule_rounds(
138	  ws: List<&2, U32>,
139	  +extra: Nat,
140	  +history: List<&2, U32>,
141	  ks: List<&2, U32>,
142	  state: S.State
143	) -> S.State:
144	  match ws ks:
145	    case Nil{} _:
146	      expanded_rounds(extra, history, ks, state)
147	    case w <> wt Nil{}:
148	      state
149	    case w <> wt k <> kt:
150	      schedule_rounds(wt, extra, history, kt, step(state, k, w))
151	
152	# A fixed rolling window drops schedule words as soon as they are older than 16
153	# rounds. This avoids growing and reference-counting the reverse history list.
154	def window_rounds(rounds_left: Nat, win: ShaWindow, ks: List<&2, U32>, state: S.State) -> S.State:
155	  match rounds_left win ks:
156	    case 0n _ _:
157	      state
158	    case 1n+q _ Nil{}:
159	      state
160	    case 1n+q W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u} k <> kt:
161	      +w = (small1(b) + g + small0(t) + u : U32)
162	      window_rounds(q, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, kt,
163	        step(state, k, w))
164	
165	# Handle window schedule rounds in the SHA-256 compression implementation.
166	def window_schedule_rounds(
167	  ws: List<&2, U32>,
168	  +extra: Nat,
169	  win: ShaWindow,
170	  ks: List<&2, U32>,
171	  state: S.State
172	) -> S.State:
173	  match ws ks:
174	    case Nil{} _:
175	      window_rounds(extra, win, ks, state)
176	    case w <> wt Nil{}:
177	      state
178	    case w <> wt k <> kt:
179	      window_schedule_rounds(wt, extra, win, kt, step(state, k, w))
180	
181	# Handle fused compress slow in the SHA-256 compression implementation.
182	def fused_compress_slow(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +state: S.State) -> S.State:
183	  feedforward(state, schedule_rounds(block, extra, List.reverse(&2, U32, block), ks, state))
184	
185	# Handle fused compress in the SHA-256 compression implementation.
186	def fused_compress(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +state: S.State) -> S.State:
187	  match block:
188	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}:
189	      feedforward(state, window_schedule_rounds(
190	        [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra,
191	        W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, state))
192	    case _:
193	      fused_compress_slow(block, extra, ks, state)
194	
195	# Fast path for the 16-word blocks produced by block_bytes. It executes the
196	# seed rounds directly and constructs only the fixed rolling window.
197	def window_compress16(
198	  +word_a: U32,
199	  +word_b: U32,
200	  +word_c: U32,
201	  +word_d: U32,
202	  +word_e: U32,
203	  +word_f: U32,
204	  +word_g: U32,
205	  +word_h: U32,
206	  +word_i: U32,
207	  +word_j: U32,
208	  +round_constant: U32,
209	  +word_l: U32,
210	  +word_m: U32,
211	  +count: U32,
212	  +word_o: U32,
213	  +word_p: U32,
214	  +extra: Nat,
215	  +ks: List<&2, U32>,
216	  +state: S.State
217	) -> S.State:
218	  match ks:
219	    case k0 <> k1 <> k2 <> k3 <> k4 <> k5 <> k6 <> k7 <>
220	      k8 <> k9 <> k10 <> k11 <> k12 <> k13 <> k14 <> k15 <> kt:
221	      s1 = step(state, k0, word_a)
222	      s2 = step(s1, k1, word_b)
223	      s3 = step(s2, k2, word_c)
224	      s4 = step(s3, k3, word_d)
225	      s5 = step(s4, k4, word_e)
226	      s6 = step(s5, k5, word_f)
227	      s7 = step(s6, k6, word_g)
228	      s8 = step(s7, k7, word_h)
229	      s9 = step(s8, k8, word_i)
230	      s10 = step(s9, k9, word_j)
231	      s11 = step(s10, k10, round_constant)
232	      s12 = step(s11, k11, word_l)
233	      s13 = step(s12, k12, word_m)
234	      s14 = step(s13, k13, count)
235	      s15 = step(s14, k14, word_o)
236	      s16 = step(s15, k15, word_p)
237	      feedforward(state, window_rounds(extra,
238	        W{word_p, word_o, count, word_m, word_l, round_constant, word_j, word_i, word_h, word_g, word_f, word_e, word_d, word_c, word_b, word_a}, kt, s16))
239	    case _:
240	      fused_compress([word_a, word_b, word_c, word_d, word_e, word_f, word_g, word_h, word_i, word_j, round_constant, word_l, word_m, count, word_o, word_p], extra, ks, state)
241	
242	# Handle be32 in the SHA-256 compression implementation.
243	def be32(+word: U32) -> List<&2, U32>:
244	  [U32.shrn(word, 24n), (U32.shrn(word, 16n) .&. 255 : U32),
245	   (U32.shrn(word, 8n) .&. 255 : U32), (word .&. 255 : U32)]
246	
247	# Return the length of gth octets in the SHA-256 compression implementation.
248	def length_octets(count: Nat, +byte_length: Nat, acc: List<&2, U32>) -> List<&2, U32>:
249	  match count:
250	    case 0n:
251	      acc
252	    case 1n+p:
253	      length_octets(p, Nat.div(byte_length, 256n), U32.from_nat(Nat.mod(byte_length, 256n)) <> acc)
254	
255	# Handle bit length in the SHA-256 compression implementation.
256	def bit_length(+byte_length: Nat) -> List<&2, U32>:
257	  length_octets(7n, Nat.div(byte_length, 32n),
258	    [U32.shln(U32.from_nat(Nat.mod(byte_length, 32n)), 3n)])
259	
260	# Handle pack in the SHA-256 compression implementation.
261	def pack(word_a: U32, word_b: U32, word_c: U32, word_d: U32) -> U32:
262	  (U32.shln((word_a .&. 255 : U32), 24n)
263	    .|. U32.shln((word_b .&. 255 : U32), 16n)
264	    .|. U32.shln((word_c .&. 255 : U32), 8n) .|. (word_d .&. 255) : U32)
265	
266	# Handle digest in the SHA-256 compression implementation.
267	def digest(state: S.State) -> List<&2, U32>:
268	  S.H{a, b, c, d, e, f, g, h} = state
269	  [a, b, c, d, e, f, g, h]
270	
271	# Generic block decoder over a padded byte list and any constant table. The
272	# fast path below is proved equal to it with the FIPS table.
273	def block_bytes(bytes: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, state: S.State) -> S.State:
274	  match bytes:
275	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
276	      block_bytes(rest, extra, ks, window_compress16(
277	        pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15),
278	        pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31),
279	        pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47),
280	        pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63),
281	        extra, ks, state))
282	    case _:
283	      state
284	
285	# FIPS 180-4 round constants, the table the specialized rounds below inline.
286	def round_constants() -> List<&2, U32>:
287	  [1116352408, 1899447441, 3049323471, 3921009573,
288	   961987163, 1508970993, 2453635748, 2870763221,
289	   3624381080, 310598401, 607225278, 1426881987,
290	   1925078388, 2162078206, 2614888103, 3248222580,
291	   3835390401, 4022224774, 264347078, 604807628,
292	   770255983, 1249150122, 1555081692, 1996064986,
293	   2554220882, 2821834349, 2952996808, 3210313671,
294	   3336571891, 3584528711, 113926993, 338241895,
295	   666307205, 773529912, 1294757372, 1396182291,
296	   1695183700, 1986661051, 2177026350, 2456956037,
297	   2730485921, 2820302411, 3259730800, 3345764771,
298	   3516065817, 3600352804, 4094571909, 275423344,
299	   430227734, 506948616, 659060556, 883997877,
300	   958139571, 1322822218, 1537002063, 1747873779,
301	   1955562222, 2024104815, 2227730452, 2361852424,
302	   2428436474, 2756734187, 3204031479, 3329325298]
303	
304	# SHA-256 round t (16 <= t < 64) with its constant as a literal. Like
305	# window_rounds, q bounds the remaining rounds (48 for SHA-256) and each round
306	# derives its schedule word from the rolling window before continuing with
307	# round t+1. Defined last-to-first because names must precede use.
308	def kr64(state: S.State) -> S.State:
309	  state
310	
311	# Return the SHA-256 round constant for schedule index 63.
312	def kr63(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
313	  match rounds_left win:
314	    case 0n _:
315	      state
316	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
317	      +w = (small1(b) + g + small0(t) + u : U32)
318	      kr64(step(state, 3329325298, w))
319	
320	# Return the SHA-256 round constant for schedule index 62.
321	def kr62(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
322	  match rounds_left win:
323	    case 0n _:
324	      state
325	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
326	      +w = (small1(b) + g + small0(t) + u : U32)
327	      kr63(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3204031479, w))
328	
329	# Return the SHA-256 round constant for schedule index 61.
330	def kr61(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
331	  match rounds_left win:
332	    case 0n _:
333	      state
334	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
335	      +w = (small1(b) + g + small0(t) + u : U32)
336	      kr62(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2756734187, w))
337	
338	# Return the SHA-256 round constant for schedule index 60.
339	def kr60(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
340	  match rounds_left win:
341	    case 0n _:
342	      state
343	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
344	      +w = (small1(b) + g + small0(t) + u : U32)
345	      kr61(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2428436474, w))
346	
347	# Return the SHA-256 round constant for schedule index 59.
348	def kr59(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
349	  match rounds_left win:
350	    case 0n _:
351	      state
352	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
353	      +w = (small1(b) + g + small0(t) + u : U32)
354	      kr60(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2361852424, w))
355	
356	# Return the SHA-256 round constant for schedule index 58.
357	def kr58(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
358	  match rounds_left win:
359	    case 0n _:
360	      state
361	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
362	      +w = (small1(b) + g + small0(t) + u : U32)
363	      kr59(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2227730452, w))
364	
365	# Return the SHA-256 round constant for schedule index 57.
366	def kr57(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
367	  match rounds_left win:
368	    case 0n _:
369	      state
370	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
371	      +w = (small1(b) + g + small0(t) + u : U32)
372	      kr58(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2024104815, w))
373	
374	# Return the SHA-256 round constant for schedule index 56.
375	def kr56(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
376	  match rounds_left win:
377	    case 0n _:
378	      state
379	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
380	      +w = (small1(b) + g + small0(t) + u : U32)
381	      kr57(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1955562222, w))
382	
383	# Return the SHA-256 round constant for schedule index 55.
384	def kr55(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
385	  match rounds_left win:
386	    case 0n _:
387	      state
388	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
389	      +w = (small1(b) + g + small0(t) + u : U32)
390	      kr56(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1747873779, w))
391	
392	# Return the SHA-256 round constant for schedule index 54.
393	def kr54(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
394	  match rounds_left win:
395	    case 0n _:
396	      state
397	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
398	      +w = (small1(b) + g + small0(t) + u : U32)
399	      kr55(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1537002063, w))
400	
401	# Return the SHA-256 round constant for schedule index 53.
402	def kr53(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
403	  match rounds_left win:
404	    case 0n _:
405	      state
406	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
407	      +w = (small1(b) + g + small0(t) + u : U32)
408	      kr54(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1322822218, w))
409	
410	# Return the SHA-256 round constant for schedule index 52.
411	def kr52(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
412	  match rounds_left win:
413	    case 0n _:
414	      state
415	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
416	      +w = (small1(b) + g + small0(t) + u : U32)
417	      kr53(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 958139571, w))
418	
419	# Return the SHA-256 round constant for schedule index 51.
420	def kr51(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
421	  match rounds_left win:
422	    case 0n _:
423	      state
424	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
425	      +w = (small1(b) + g + small0(t) + u : U32)
426	      kr52(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 883997877, w))
427	
428	# Return the SHA-256 round constant for schedule index 50.
429	def kr50(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
430	  match rounds_left win:
431	    case 0n _:
432	      state
433	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
434	      +w = (small1(b) + g + small0(t) + u : U32)
435	      kr51(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 659060556, w))
436	
437	# Return the SHA-256 round constant for schedule index 49.
438	def kr49(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
439	  match rounds_left win:
440	    case 0n _:
441	      state
442	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
443	      +w = (small1(b) + g + small0(t) + u : U32)
444	      kr50(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 506948616, w))
445	
446	# Return the SHA-256 round constant for schedule index 48.
447	def kr48(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
448	  match rounds_left win:
449	    case 0n _:
450	      state
451	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
452	      +w = (small1(b) + g + small0(t) + u : U32)
453	      kr49(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 430227734, w))
454	
455	# Return the SHA-256 round constant for schedule index 47.
456	def kr47(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
457	  match rounds_left win:
458	    case 0n _:
459	      state
460	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
461	      +w = (small1(b) + g + small0(t) + u : U32)
462	      kr48(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 275423344, w))
463	
464	# Return the SHA-256 round constant for schedule index 46.
465	def kr46(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
466	  match rounds_left win:
467	    case 0n _:
468	      state
469	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
470	      +w = (small1(b) + g + small0(t) + u : U32)
471	      kr47(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 4094571909, w))
472	
473	# Return the SHA-256 round constant for schedule index 45.
474	def kr45(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
475	  match rounds_left win:
476	    case 0n _:
477	      state
478	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
479	      +w = (small1(b) + g + small0(t) + u : U32)
480	      kr46(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3600352804, w))
481	
482	# Return the SHA-256 round constant for schedule index 44.
483	def kr44(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
484	  match rounds_left win:
485	    case 0n _:
486	      state
487	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
488	      +w = (small1(b) + g + small0(t) + u : U32)
489	      kr45(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3516065817, w))
490	
491	# Return the SHA-256 round constant for schedule index 43.
492	def kr43(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
493	  match rounds_left win:
494	    case 0n _:
495	      state
496	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
497	      +w = (small1(b) + g + small0(t) + u : U32)
498	      kr44(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3345764771, w))
499	
500	# Return the SHA-256 round constant for schedule index 42.
501	def kr42(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
502	  match rounds_left win:
503	    case 0n _:
504	      state
505	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
506	      +w = (small1(b) + g + small0(t) + u : U32)
507	      kr43(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3259730800, w))
508	
509	# Return the SHA-256 round constant for schedule index 41.
510	def kr41(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
511	  match rounds_left win:
512	    case 0n _:
513	      state
514	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
515	      +w = (small1(b) + g + small0(t) + u : U32)
516	      kr42(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2820302411, w))
517	
518	# Return the SHA-256 round constant for schedule index 40.
519	def kr40(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
520	  match rounds_left win:
521	    case 0n _:
522	      state
523	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
524	      +w = (small1(b) + g + small0(t) + u : U32)
525	      kr41(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2730485921, w))
526	
527	# Return the SHA-256 round constant for schedule index 39.
528	def kr39(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
529	  match rounds_left win:
530	    case 0n _:
531	      state
532	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
533	      +w = (small1(b) + g + small0(t) + u : U32)
534	      kr40(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2456956037, w))
535	
536	# Return the SHA-256 round constant for schedule index 38.
537	def kr38(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
538	  match rounds_left win:
539	    case 0n _:
540	      state
541	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
542	      +w = (small1(b) + g + small0(t) + u : U32)
543	      kr39(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2177026350, w))
544	
545	# Return the SHA-256 round constant for schedule index 37.
546	def kr37(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
547	  match rounds_left win:
548	    case 0n _:
549	      state
550	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
551	      +w = (small1(b) + g + small0(t) + u : U32)
552	      kr38(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1986661051, w))
553	
554	# Return the SHA-256 round constant for schedule index 36.
555	def kr36(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
556	  match rounds_left win:
557	    case 0n _:
558	      state
559	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
560	      +w = (small1(b) + g + small0(t) + u : U32)
561	      kr37(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1695183700, w))
562	
563	# Return the SHA-256 round constant for schedule index 35.
564	def kr35(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
565	  match rounds_left win:
566	    case 0n _:
567	      state
568	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
569	      +w = (small1(b) + g + small0(t) + u : U32)
570	      kr36(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1396182291, w))
571	
572	# Return the SHA-256 round constant for schedule index 34.
573	def kr34(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
574	  match rounds_left win:
575	    case 0n _:
576	      state
577	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
578	      +w = (small1(b) + g + small0(t) + u : U32)
579	      kr35(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1294757372, w))
580	
581	# Return the SHA-256 round constant for schedule index 33.
582	def kr33(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
583	  match rounds_left win:
584	    case 0n _:
585	      state
586	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
587	      +w = (small1(b) + g + small0(t) + u : U32)
588	      kr34(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 773529912, w))
589	
590	# Return the SHA-256 round constant for schedule index 32.
591	def kr32(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
592	  match rounds_left win:
593	    case 0n _:
594	      state
595	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
596	      +w = (small1(b) + g + small0(t) + u : U32)
597	      kr33(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 666307205, w))
598	
599	# Return the SHA-256 round constant for schedule index 31.
600	def kr31(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
601	  match rounds_left win:
602	    case 0n _:
603	      state
604	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
605	      +w = (small1(b) + g + small0(t) + u : U32)
606	      kr32(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 338241895, w))
607	
608	# Return the SHA-256 round constant for schedule index 30.
609	def kr30(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
610	  match rounds_left win:
611	    case 0n _:
612	      state
613	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
614	      +w = (small1(b) + g + small0(t) + u : U32)
615	      kr31(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 113926993, w))
616	
617	# Return the SHA-256 round constant for schedule index 29.
618	def kr29(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
619	  match rounds_left win:
620	    case 0n _:
621	      state
622	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
623	      +w = (small1(b) + g + small0(t) + u : U32)
624	      kr30(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3584528711, w))
625	
626	# Return the SHA-256 round constant for schedule index 28.
627	def kr28(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
628	  match rounds_left win:
629	    case 0n _:
630	      state
631	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
632	      +w = (small1(b) + g + small0(t) + u : U32)
633	      kr29(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3336571891, w))
634	
635	# Return the SHA-256 round constant for schedule index 27.
636	def kr27(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
637	  match rounds_left win:
638	    case 0n _:
639	      state
640	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
641	      +w = (small1(b) + g + small0(t) + u : U32)
642	      kr28(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3210313671, w))
643	
644	# Return the SHA-256 round constant for schedule index 26.
645	def kr26(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
646	  match rounds_left win:
647	    case 0n _:
648	      state
649	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
650	      +w = (small1(b) + g + small0(t) + u : U32)
651	      kr27(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2952996808, w))
652	
653	# Return the SHA-256 round constant for schedule index 25.
654	def kr25(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
655	  match rounds_left win:
656	    case 0n _:
657	      state
658	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
659	      +w = (small1(b) + g + small0(t) + u : U32)
660	      kr26(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2821834349, w))
661	
662	# Return the SHA-256 round constant for schedule index 24.
663	def kr24(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
664	  match rounds_left win:
665	    case 0n _:
666	      state
667	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
668	      +w = (small1(b) + g + small0(t) + u : U32)
669	      kr25(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 2554220882, w))
670	
671	# Return the SHA-256 round constant for schedule index 23.
672	def kr23(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
673	  match rounds_left win:
674	    case 0n _:
675	      state
676	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
677	      +w = (small1(b) + g + small0(t) + u : U32)
678	      kr24(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1996064986, w))
679	
680	# Return the SHA-256 round constant for schedule index 22.
681	def kr22(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
682	  match rounds_left win:
683	    case 0n _:
684	      state
685	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
686	      +w = (small1(b) + g + small0(t) + u : U32)
687	      kr23(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1555081692, w))
688	
689	# Return the SHA-256 round constant for schedule index 21.
690	def kr21(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
691	  match rounds_left win:
692	    case 0n _:
693	      state
694	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
695	      +w = (small1(b) + g + small0(t) + u : U32)
696	      kr22(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 1249150122, w))
697	
698	# Return the SHA-256 round constant for schedule index 20.
699	def kr20(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
700	  match rounds_left win:
701	    case 0n _:
702	      state
703	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
704	      +w = (small1(b) + g + small0(t) + u : U32)
705	      kr21(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 770255983, w))
706	
707	# Return the SHA-256 round constant for schedule index 19.
708	def kr19(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
709	  match rounds_left win:
710	    case 0n _:
711	      state
712	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
713	      +w = (small1(b) + g + small0(t) + u : U32)
714	      kr20(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 604807628, w))
715	
716	# Return the SHA-256 round constant for schedule index 18.
717	def kr18(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
718	  match rounds_left win:
719	    case 0n _:
720	      state
721	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
722	      +w = (small1(b) + g + small0(t) + u : U32)
723	      kr19(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 264347078, w))
724	
725	# Return the SHA-256 round constant for schedule index 17.
726	def kr17(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
727	  match rounds_left win:
728	    case 0n _:
729	      state
730	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
731	      +w = (small1(b) + g + small0(t) + u : U32)
732	      kr18(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 4022224774, w))
733	
734	# Return the SHA-256 round constant for schedule index 16.
735	def kr16(rounds_left: Nat, win: ShaWindow, state: S.State) -> S.State:
736	  match rounds_left win:
737	    case 0n _:
738	      state
739	    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:
740	      +w = (small1(b) + g + small0(t) + u : U32)
741	      kr17(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(state, 3835390401, w))
742	
743	# window_compress16 specialized to the FIPS table: no constant list is walked.
744	def fips_compress16(
745	  +word_a: U32,
746	  +word_b: U32,
747	  +word_c: U32,
748	  +word_d: U32,
749	  +word_e: U32,
750	  +word_f: U32,
751	  +word_g: U32,
752	  +word_h: U32,
753	  +word_i: U32,
754	  +word_j: U32,
755	  +round_constant: U32,
756	  +word_l: U32,
757	  +word_m: U32,
758	  +count: U32,
759	  +word_o: U32,
760	  +word_p: U32,
761	  +rounds_left: Nat,
762	  +state: S.State
763	) -> S.State:
764	  s1 = step(state, 1116352408, word_a)
765	  s2 = step(s1, 1899447441, word_b)
766	  s3 = step(s2, 3049323471, word_c)
767	  s4 = step(s3, 3921009573, word_d)
768	  s5 = step(s4, 961987163, word_e)
769	  s6 = step(s5, 1508970993, word_f)
770	  s7 = step(s6, 2453635748, word_g)
771	  s8 = step(s7, 2870763221, word_h)
772	  s9 = step(s8, 3624381080, word_i)
773	  s10 = step(s9, 310598401, word_j)
774	  s11 = step(s10, 607225278, round_constant)
775	  s12 = step(s11, 1426881987, word_l)
776	  s13 = step(s12, 1925078388, word_m)
777	  s14 = step(s13, 2162078206, count)
778	  s15 = step(s14, 2614888103, word_o)
779	  s16 = step(s15, 3248222580, word_p)
780	  feedforward(state, kr16(rounds_left, W{word_p, word_o, count, word_m, word_l, round_constant, word_j, word_i, word_h, word_g, word_f, word_e, word_d, word_c, word_b, word_a}, s16))
781	
782	# FIPS padding suffix for a message of n bytes, computed with modular
783	# arithmetic. The proofs state the streaming hash in terms of it.
784	def suffix(+byte_length: Nat) -> List<&2, U32>:
785	  128 <> List.append(&2, U32,
786	    List.replicate(U32, Nat.mod(Nat.sub(119n, Nat.mod(byte_length, 64n)), 64n), 0), bit_length(byte_length))
787	
788	# Big-endian words of the 64-bit message bit length 8n, computed from n with
789	# exactly the digit expressions bit_length produces, but without building and
790	# matching an eight-element list. bit_length(n) is [o(d6), .., o(d0), low]
791	# where d0 = n / 32, d(k+1) = dk / 256 and o(x) = x mod 256.
792	def len_hi(+byte_length: Nat) -> U32:
793	  +d0 = Nat.div(byte_length, 32n)
794	  +d1 = Nat.div(d0, 256n)
795	  +d2 = Nat.div(d1, 256n)
796	  +d3 = Nat.div(d2, 256n)
797	  +d4 = Nat.div(d3, 256n)
798	  +d5 = Nat.div(d4, 256n)
799	  +d6 = Nat.div(d5, 256n)
800	  pack(U32.from_nat(Nat.mod(d6, 256n)), U32.from_nat(Nat.mod(d5, 256n)),
801	    U32.from_nat(Nat.mod(d4, 256n)), U32.from_nat(Nat.mod(d3, 256n)))
802	
803	# Return the length of lo in the SHA-256 compression implementation.
804	def len_lo(+byte_length: Nat) -> U32:
805	  +d0 = Nat.div(byte_length, 32n)
806	  +d1 = Nat.div(d0, 256n)
807	  +d2 = Nat.div(d1, 256n)
808	  pack(U32.from_nat(Nat.mod(d2, 256n)), U32.from_nat(Nat.mod(d1, 256n)),
809	    U32.from_nat(Nat.mod(d0, 256n)), U32.shln(U32.from_nat(Nat.mod(byte_length, 32n)), 3n))
810	
811	# Final block(s) for an n-byte message ending in r = 0..63 tail bytes. Each
812	# tail length has its own padded layout: the tail bytes, the 0x80 marker, the
813	# zero fill and the big-endian bit length are packed straight into schedule
814	# words, so no padded list is built.
815	def fin0(+byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
816	  fips_compress16(pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
817	    extra, state)
818	
819	# Apply SHA-256 round 1 to the compression state.
820	def fin1(+t0: U32, +byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
821	  fips_compress16(pack(t0, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
822	    extra, state)
823	
824	# Apply SHA-256 round 2 to the compression state.
825	def fin2(+t0: U32, +t1: U32, +byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
826	  fips_compress16(pack(t0, t1, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
827	    extra, state)
828	
829	# Apply SHA-256 round 3 to the compression state.
830	def fin3(+t0: U32, +t1: U32, +t2: U32, +byte_length: Nat, +extra: Nat, state: S.State) -> S.State:
831	  fips_compress16(pack(t0, t1, t2, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
832	    extra, state)
833	
834	# Apply SHA-256 round 4 to the compression state.
835	def fin4(
836	  +t0: U32,
837	  +t1: U32,
838	  +t2: U32,
839	  +t3: U32,
840	  +byte_length: Nat,
841	  +extra: Nat,
842	  state: S.State
843	) -> S.State:
844	  fips_compress16(pack(t0, t1, t2, t3), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
845	    extra, state)
846	
847	# Apply SHA-256 round 5 to the compression state.
848	def fin5(
849	  +t0: U32,
850	  +t1: U32,
851	  +t2: U32,
852	  +t3: U32,
853	  +t4: U32,
854	  +byte_length: Nat,
855	  +extra: Nat,
856	  state: S.State
857	) -> S.State:
858	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
859	    extra, state)
860	
861	# Apply SHA-256 round 6 to the compression state.
862	def fin6(
863	  +t0: U32,
864	  +t1: U32,
865	  +t2: U32,
866	  +t3: U32,
867	  +t4: U32,
868	  +t5: U32,
869	  +byte_length: Nat,
870	  +extra: Nat,
871	  state: S.State
872	) -> S.State:
873	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
874	    extra, state)
875	
876	# Apply SHA-256 round 7 to the compression state.
877	def fin7(
878	  +t0: U32,
879	  +t1: U32,
880	  +t2: U32,
881	  +t3: U32,
882	  +t4: U32,
883	  +t5: U32,
884	  +t6: U32,
885	  +byte_length: Nat,
886	  +extra: Nat,
887	  state: S.State
888	) -> S.State:
889	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
890	    extra, state)
891	
892	# Apply SHA-256 round 8 to the compression state.
893	def fin8(
894	  +t0: U32,
895	  +t1: U32,
896	  +t2: U32,
897	  +t3: U32,
898	  +t4: U32,
899	  +t5: U32,
900	  +t6: U32,
901	  +t7: U32,
902	  +byte_length: Nat,
903	  +extra: Nat,
904	  state: S.State
905	) -> S.State:
906	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
907	    extra, state)
908	
909	# Apply SHA-256 round 9 to the compression state.
910	def fin9(
911	  +t0: U32,
912	  +t1: U32,
913	  +t2: U32,
914	  +t3: U32,
915	  +t4: U32,
916	  +t5: U32,
917	  +t6: U32,
918	  +t7: U32,
919	  +t8: U32,
920	  +byte_length: Nat,
921	  +extra: Nat,
922	  state: S.State
923	) -> S.State:
924	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
925	    extra, state)
926	
927	# Apply SHA-256 round 10 to the compression state.
928	def fin10(
929	  +t0: U32,
930	  +t1: U32,
931	  +t2: U32,
932	  +t3: U32,
933	  +t4: U32,
934	  +t5: U32,
935	  +t6: U32,
936	  +t7: U32,
937	  +t8: U32,
938	  +t9: U32,
939	  +byte_length: Nat,
940	  +extra: Nat,
941	  state: S.State
942	) -> S.State:
943	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
944	    extra, state)
945	
946	# Apply SHA-256 round 11 to the compression state.
947	def fin11(
948	  +t0: U32,
949	  +t1: U32,
950	  +t2: U32,
951	  +t3: U32,
952	  +t4: U32,
953	  +t5: U32,
954	  +t6: U32,
955	  +t7: U32,
956	  +t8: U32,
957	  +t9: U32,
958	  +t10: U32,
959	  +byte_length: Nat,
960	  +extra: Nat,
961	  state: S.State
962	) -> S.State:
963	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
964	    extra, state)
965	
966	# Apply SHA-256 round 12 to the compression state.
967	def fin12(
968	  +t0: U32,
969	  +t1: U32,
970	  +t2: U32,
971	  +t3: U32,
972	  +t4: U32,
973	  +t5: U32,
974	  +t6: U32,
975	  +t7: U32,
976	  +t8: U32,
977	  +t9: U32,
978	  +t10: U32,
979	  +t11: U32,
980	  +byte_length: Nat,
981	  +extra: Nat,
982	  state: S.State
983	) -> S.State:
984	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
985	    extra, state)
986	
987	# Apply SHA-256 round 13 to the compression state.
988	def fin13(
989	  +t0: U32,
990	  +t1: U32,
991	  +t2: U32,
992	  +t3: U32,
993	  +t4: U32,
994	  +t5: U32,
995	  +t6: U32,
996	  +t7: U32,
997	  +t8: U32,
998	  +t9: U32,
999	  +t10: U32,
1000	  +t11: U32,
1001	  +t12: U32,
1002	  +byte_length: Nat,
1003	  +extra: Nat,
1004	  state: S.State
1005	) -> S.State:
1006	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1007	    extra, state)
1008	
1009	# Apply SHA-256 round 14 to the compression state.
1010	def fin14(
1011	  +t0: U32,
1012	  +t1: U32,
1013	  +t2: U32,
1014	  +t3: U32,
1015	  +t4: U32,
1016	  +t5: U32,
1017	  +t6: U32,
1018	  +t7: U32,
1019	  +t8: U32,
1020	  +t9: U32,
1021	  +t10: U32,
1022	  +t11: U32,
1023	  +t12: U32,
1024	  +t13: U32,
1025	  +byte_length: Nat,
1026	  +extra: Nat,
1027	  state: S.State
1028	) -> S.State:
1029	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1030	    extra, state)
1031	
1032	# Apply SHA-256 round 15 to the compression state.
1033	def fin15(
1034	  +t0: U32,
1035	  +t1: U32,
1036	  +t2: U32,
1037	  +t3: U32,
1038	  +t4: U32,
1039	  +t5: U32,
1040	  +t6: U32,
1041	  +t7: U32,
1042	  +t8: U32,
1043	  +t9: U32,
1044	  +t10: U32,
1045	  +t11: U32,
1046	  +t12: U32,
1047	  +t13: U32,
1048	  +t14: U32,
1049	  +byte_length: Nat,
1050	  +extra: Nat,
1051	  state: S.State
1052	) -> S.State:
1053	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1054	    extra, state)
1055	
1056	# Apply SHA-256 round 16 to the compression state.
1057	def fin16(
1058	  +t0: U32,
1059	  +t1: U32,
1060	  +t2: U32,
1061	  +t3: U32,
1062	  +t4: U32,
1063	  +t5: U32,
1064	  +t6: U32,
1065	  +t7: U32,
1066	  +t8: U32,
1067	  +t9: U32,
1068	  +t10: U32,
1069	  +t11: U32,
1070	  +t12: U32,
1071	  +t13: U32,
1072	  +t14: U32,
1073	  +t15: U32,
1074	  +byte_length: Nat,
1075	  +extra: Nat,
1076	  state: S.State
1077	) -> S.State:
1078	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1079	    extra, state)
1080	
1081	# Apply SHA-256 round 17 to the compression state.
1082	def fin17(
1083	  +t0: U32,
1084	  +t1: U32,
1085	  +t2: U32,
1086	  +t3: U32,
1087	  +t4: U32,
1088	  +t5: U32,
1089	  +t6: U32,
1090	  +t7: U32,
1091	  +t8: U32,
1092	  +t9: U32,
1093	  +t10: U32,
1094	  +t11: U32,
1095	  +t12: U32,
1096	  +t13: U32,
1097	  +t14: U32,
1098	  +t15: U32,
1099	  +t16: U32,
1100	  +byte_length: Nat,
1101	  +extra: Nat,
1102	  state: S.State
1103	) -> S.State:
1104	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1105	    extra, state)
1106	
1107	# Apply SHA-256 round 18 to the compression state.
1108	def fin18(
1109	  +t0: U32,
1110	  +t1: U32,
1111	  +t2: U32,
1112	  +t3: U32,
1113	  +t4: U32,
1114	  +t5: U32,
1115	  +t6: U32,
1116	  +t7: U32,
1117	  +t8: U32,
1118	  +t9: U32,
1119	  +t10: U32,
1120	  +t11: U32,
1121	  +t12: U32,
1122	  +t13: U32,
1123	  +t14: U32,
1124	  +t15: U32,
1125	  +t16: U32,
1126	  +t17: U32,
1127	  +byte_length: Nat,
1128	  +extra: Nat,
1129	  state: S.State
1130	) -> S.State:
1131	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1132	    extra, state)
1133	
1134	# Apply SHA-256 round 19 to the compression state.
1135	def fin19(
1136	  +t0: U32,
1137	  +t1: U32,
1138	  +t2: U32,
1139	  +t3: U32,
1140	  +t4: U32,
1141	  +t5: U32,
1142	  +t6: U32,
1143	  +t7: U32,
1144	  +t8: U32,
1145	  +t9: U32,
1146	  +t10: U32,
1147	  +t11: U32,
1148	  +t12: U32,
1149	  +t13: U32,
1150	  +t14: U32,
1151	  +t15: U32,
1152	  +t16: U32,
1153	  +t17: U32,
1154	  +t18: U32,
1155	  +byte_length: Nat,
1156	  +extra: Nat,
1157	  state: S.State
1158	) -> S.State:
1159	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1160	    extra, state)
1161	
1162	# Apply SHA-256 round 20 to the compression state.
1163	def fin20(
1164	  +t0: U32,
1165	  +t1: U32,
1166	  +t2: U32,
1167	  +t3: U32,
1168	  +t4: U32,
1169	  +t5: U32,
1170	  +t6: U32,
1171	  +t7: U32,
1172	  +t8: U32,
1173	  +t9: U32,
1174	  +t10: U32,
1175	  +t11: U32,
1176	  +t12: U32,
1177	  +t13: U32,
1178	  +t14: U32,
1179	  +t15: U32,
1180	  +t16: U32,
1181	  +t17: U32,
1182	  +t18: U32,
1183	  +t19: U32,
1184	  +byte_length: Nat,
1185	  +extra: Nat,
1186	  state: S.State
1187	) -> S.State:
1188	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1189	    extra, state)
1190	
1191	# Apply SHA-256 round 21 to the compression state.
1192	def fin21(
1193	  +t0: U32,
1194	  +t1: U32,
1195	  +t2: U32,
1196	  +t3: U32,
1197	  +t4: U32,
1198	  +t5: U32,
1199	  +t6: U32,
1200	  +t7: U32,
1201	  +t8: U32,
1202	  +t9: U32,
1203	  +t10: U32,
1204	  +t11: U32,
1205	  +t12: U32,
1206	  +t13: U32,
1207	  +t14: U32,
1208	  +t15: U32,
1209	  +t16: U32,
1210	  +t17: U32,
1211	  +t18: U32,
1212	  +t19: U32,
1213	  +t20: U32,
1214	  +byte_length: Nat,
1215	  +extra: Nat,
1216	  state: S.State
1217	) -> S.State:
1218	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1219	    extra, state)
1220	
1221	# Apply SHA-256 round 22 to the compression state.
1222	def fin22(
1223	  +t0: U32,
1224	  +t1: U32,
1225	  +t2: U32,
1226	  +t3: U32,
1227	  +t4: U32,
1228	  +t5: U32,
1229	  +t6: U32,
1230	  +t7: U32,
1231	  +t8: U32,
1232	  +t9: U32,
1233	  +t10: U32,
1234	  +t11: U32,
1235	  +t12: U32,
1236	  +t13: U32,
1237	  +t14: U32,
1238	  +t15: U32,
1239	  +t16: U32,
1240	  +t17: U32,
1241	  +t18: U32,
1242	  +t19: U32,
1243	  +t20: U32,
1244	  +t21: U32,
1245	  +byte_length: Nat,
1246	  +extra: Nat,
1247	  state: S.State
1248	) -> S.State:
1249	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1250	    extra, state)
1251	
1252	# Apply SHA-256 round 23 to the compression state.
1253	def fin23(
1254	  +t0: U32,
1255	  +t1: U32,
1256	  +t2: U32,
1257	  +t3: U32,
1258	  +t4: U32,
1259	  +t5: U32,
1260	  +t6: U32,
1261	  +t7: U32,
1262	  +t8: U32,
1263	  +t9: U32,
1264	  +t10: U32,
1265	  +t11: U32,
1266	  +t12: U32,
1267	  +t13: U32,
1268	  +t14: U32,
1269	  +t15: U32,
1270	  +t16: U32,
1271	  +t17: U32,
1272	  +t18: U32,
1273	  +t19: U32,
1274	  +t20: U32,
1275	  +t21: U32,
1276	  +t22: U32,
1277	  +byte_length: Nat,
1278	  +extra: Nat,
1279	  state: S.State
1280	) -> S.State:
1281	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1282	    extra, state)
1283	
1284	# Apply SHA-256 round 24 to the compression state.
1285	def fin24(
1286	  +t0: U32,
1287	  +t1: U32,
1288	  +t2: U32,
1289	  +t3: U32,
1290	  +t4: U32,
1291	  +t5: U32,
1292	  +t6: U32,
1293	  +t7: U32,
1294	  +t8: U32,
1295	  +t9: U32,
1296	  +t10: U32,
1297	  +t11: U32,
1298	  +t12: U32,
1299	  +t13: U32,
1300	  +t14: U32,
1301	  +t15: U32,
1302	  +t16: U32,
1303	  +t17: U32,
1304	  +t18: U32,
1305	  +t19: U32,
1306	  +t20: U32,
1307	  +t21: U32,
1308	  +t22: U32,
1309	  +t23: U32,
1310	  +byte_length: Nat,
1311	  +extra: Nat,
1312	  state: S.State
1313	) -> S.State:
1314	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1315	    extra, state)
1316	
1317	# Apply SHA-256 round 25 to the compression state.
1318	def fin25(
1319	  +t0: U32,
1320	  +t1: U32,
1321	  +t2: U32,
1322	  +t3: U32,
1323	  +t4: U32,
1324	  +t5: U32,
1325	  +t6: U32,
1326	  +t7: U32,
1327	  +t8: U32,
1328	  +t9: U32,
1329	  +t10: U32,
1330	  +t11: U32,
1331	  +t12: U32,
1332	  +t13: U32,
1333	  +t14: U32,
1334	  +t15: U32,
1335	  +t16: U32,
1336	  +t17: U32,
1337	  +t18: U32,
1338	  +t19: U32,
1339	  +t20: U32,
1340	  +t21: U32,
1341	  +t22: U32,
1342	  +t23: U32,
1343	  +t24: U32,
1344	  +byte_length: Nat,
1345	  +extra: Nat,
1346	  state: S.State
1347	) -> S.State:
1348	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1349	    extra, state)
1350	
1351	# Apply SHA-256 round 26 to the compression state.
1352	def fin26(
1353	  +t0: U32,
1354	  +t1: U32,
1355	  +t2: U32,
1356	  +t3: U32,
1357	  +t4: U32,
1358	  +t5: U32,
1359	  +t6: U32,
1360	  +t7: U32,
1361	  +t8: U32,
1362	  +t9: U32,
1363	  +t10: U32,
1364	  +t11: U32,
1365	  +t12: U32,
1366	  +t13: U32,
1367	  +t14: U32,
1368	  +t15: U32,
1369	  +t16: U32,
1370	  +t17: U32,
1371	  +t18: U32,
1372	  +t19: U32,
1373	  +t20: U32,
1374	  +t21: U32,
1375	  +t22: U32,
1376	  +t23: U32,
1377	  +t24: U32,
1378	  +t25: U32,
1379	  +byte_length: Nat,
1380	  +extra: Nat,
1381	  state: S.State
1382	) -> S.State:
1383	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1384	    extra, state)
1385	
1386	# Apply SHA-256 round 27 to the compression state.
1387	def fin27(
1388	  +t0: U32,
1389	  +t1: U32,
1390	  +t2: U32,
1391	  +t3: U32,
1392	  +t4: U32,
1393	  +t5: U32,
1394	  +t6: U32,
1395	  +t7: U32,
1396	  +t8: U32,
1397	  +t9: U32,
1398	  +t10: U32,
1399	  +t11: U32,
1400	  +t12: U32,
1401	  +t13: U32,
1402	  +t14: U32,
1403	  +t15: U32,
1404	  +t16: U32,
1405	  +t17: U32,
1406	  +t18: U32,
1407	  +t19: U32,
1408	  +t20: U32,
1409	  +t21: U32,
1410	  +t22: U32,
1411	  +t23: U32,
1412	  +t24: U32,
1413	  +t25: U32,
1414	  +t26: U32,
1415	  +byte_length: Nat,
1416	  +extra: Nat,
1417	  state: S.State
1418	) -> S.State:
1419	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1420	    extra, state)
1421	
1422	# Apply SHA-256 round 28 to the compression state.
1423	def fin28(
1424	  +t0: U32,
1425	  +t1: U32,
1426	  +t2: U32,
1427	  +t3: U32,
1428	  +t4: U32,
1429	  +t5: U32,
1430	  +t6: U32,
1431	  +t7: U32,
1432	  +t8: U32,
1433	  +t9: U32,
1434	  +t10: U32,
1435	  +t11: U32,
1436	  +t12: U32,
1437	  +t13: U32,
1438	  +t14: U32,
1439	  +t15: U32,
1440	  +t16: U32,
1441	  +t17: U32,
1442	  +t18: U32,
1443	  +t19: U32,
1444	  +t20: U32,
1445	  +t21: U32,
1446	  +t22: U32,
1447	  +t23: U32,
1448	  +t24: U32,
1449	  +t25: U32,
1450	  +t26: U32,
1451	  +t27: U32,
1452	  +byte_length: Nat,
1453	  +extra: Nat,
1454	  state: S.State
1455	) -> S.State:
1456	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1457	    extra, state)
1458	
1459	# Apply SHA-256 round 29 to the compression state.
1460	def fin29(
1461	  +t0: U32,
1462	  +t1: U32,
1463	  +t2: U32,
1464	  +t3: U32,
1465	  +t4: U32,
1466	  +t5: U32,
1467	  +t6: U32,
1468	  +t7: U32,
1469	  +t8: U32,
1470	  +t9: U32,
1471	  +t10: U32,
1472	  +t11: U32,
1473	  +t12: U32,
1474	  +t13: U32,
1475	  +t14: U32,
1476	  +t15: U32,
1477	  +t16: U32,
1478	  +t17: U32,
1479	  +t18: U32,
1480	  +t19: U32,
1481	  +t20: U32,
1482	  +t21: U32,
1483	  +t22: U32,
1484	  +t23: U32,
1485	  +t24: U32,
1486	  +t25: U32,
1487	  +t26: U32,
1488	  +t27: U32,
1489	  +t28: U32,
1490	  +byte_length: Nat,
1491	  +extra: Nat,
1492	  state: S.State
1493	) -> S.State:
1494	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1495	    extra, state)
1496	
1497	# Apply SHA-256 round 30 to the compression state.
1498	def fin30(
1499	  +t0: U32,
1500	  +t1: U32,
1501	  +t2: U32,
1502	  +t3: U32,
1503	  +t4: U32,
1504	  +t5: U32,
1505	  +t6: U32,
1506	  +t7: U32,
1507	  +t8: U32,
1508	  +t9: U32,
1509	  +t10: U32,
1510	  +t11: U32,
1511	  +t12: U32,
1512	  +t13: U32,
1513	  +t14: U32,
1514	  +t15: U32,
1515	  +t16: U32,
1516	  +t17: U32,
1517	  +t18: U32,
1518	  +t19: U32,
1519	  +t20: U32,
1520	  +t21: U32,
1521	  +t22: U32,
1522	  +t23: U32,
1523	  +t24: U32,
1524	  +t25: U32,
1525	  +t26: U32,
1526	  +t27: U32,
1527	  +t28: U32,
1528	  +t29: U32,
1529	  +byte_length: Nat,
1530	  +extra: Nat,
1531	  state: S.State
1532	) -> S.State:
1533	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1534	    extra, state)
1535	
1536	# Apply SHA-256 round 31 to the compression state.
1537	def fin31(
1538	  +t0: U32,
1539	  +t1: U32,
1540	  +t2: U32,
1541	  +t3: U32,
1542	  +t4: U32,
1543	  +t5: U32,
1544	  +t6: U32,
1545	  +t7: U32,
1546	  +t8: U32,
1547	  +t9: U32,
1548	  +t10: U32,
1549	  +t11: U32,
1550	  +t12: U32,
1551	  +t13: U32,
1552	  +t14: U32,
1553	  +t15: U32,
1554	  +t16: U32,
1555	  +t17: U32,
1556	  +t18: U32,
1557	  +t19: U32,
1558	  +t20: U32,
1559	  +t21: U32,
1560	  +t22: U32,
1561	  +t23: U32,
1562	  +t24: U32,
1563	  +t25: U32,
1564	  +t26: U32,
1565	  +t27: U32,
1566	  +t28: U32,
1567	  +t29: U32,
1568	  +t30: U32,
1569	  +byte_length: Nat,
1570	  +extra: Nat,
1571	  state: S.State
1572	) -> S.State:
1573	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1574	    extra, state)
1575	
1576	# Apply SHA-256 round 32 to the compression state.
1577	def fin32(
1578	  +t0: U32,
1579	  +t1: U32,
1580	  +t2: U32,
1581	  +t3: U32,
1582	  +t4: U32,
1583	  +t5: U32,
1584	  +t6: U32,
1585	  +t7: U32,
1586	  +t8: U32,
1587	  +t9: U32,
1588	  +t10: U32,
1589	  +t11: U32,
1590	  +t12: U32,
1591	  +t13: U32,
1592	  +t14: U32,
1593	  +t15: U32,
1594	  +t16: U32,
1595	  +t17: U32,
1596	  +t18: U32,
1597	  +t19: U32,
1598	  +t20: U32,
1599	  +t21: U32,
1600	  +t22: U32,
1601	  +t23: U32,
1602	  +t24: U32,
1603	  +t25: U32,
1604	  +t26: U32,
1605	  +t27: U32,
1606	  +t28: U32,
1607	  +t29: U32,
1608	  +t30: U32,
1609	  +t31: U32,
1610	  +byte_length: Nat,
1611	  +extra: Nat,
1612	  state: S.State
1613	) -> S.State:
1614	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1615	    extra, state)
1616	
1617	# Apply SHA-256 round 33 to the compression state.
1618	def fin33(
1619	  +t0: U32,
1620	  +t1: U32,
1621	  +t2: U32,
1622	  +t3: U32,
1623	  +t4: U32,
1624	  +t5: U32,
1625	  +t6: U32,
1626	  +t7: U32,
1627	  +t8: U32,
1628	  +t9: U32,
1629	  +t10: U32,
1630	  +t11: U32,
1631	  +t12: U32,
1632	  +t13: U32,
1633	  +t14: U32,
1634	  +t15: U32,
1635	  +t16: U32,
1636	  +t17: U32,
1637	  +t18: U32,
1638	  +t19: U32,
1639	  +t20: U32,
1640	  +t21: U32,
1641	  +t22: U32,
1642	  +t23: U32,
1643	  +t24: U32,
1644	  +t25: U32,
1645	  +t26: U32,
1646	  +t27: U32,
1647	  +t28: U32,
1648	  +t29: U32,
1649	  +t30: U32,
1650	  +t31: U32,
1651	  +t32: U32,
1652	  +byte_length: Nat,
1653	  +extra: Nat,
1654	  state: S.State
1655	) -> S.State:
1656	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1657	    extra, state)
1658	
1659	# Apply SHA-256 round 34 to the compression state.
1660	def fin34(
1661	  +t0: U32,
1662	  +t1: U32,
1663	  +t2: U32,
1664	  +t3: U32,
1665	  +t4: U32,
1666	  +t5: U32,
1667	  +t6: U32,
1668	  +t7: U32,
1669	  +t8: U32,
1670	  +t9: U32,
1671	  +t10: U32,
1672	  +t11: U32,
1673	  +t12: U32,
1674	  +t13: U32,
1675	  +t14: U32,
1676	  +t15: U32,
1677	  +t16: U32,
1678	  +t17: U32,
1679	  +t18: U32,
1680	  +t19: U32,
1681	  +t20: U32,
1682	  +t21: U32,
1683	  +t22: U32,
1684	  +t23: U32,
1685	  +t24: U32,
1686	  +t25: U32,
1687	  +t26: U32,
1688	  +t27: U32,
1689	  +t28: U32,
1690	  +t29: U32,
1691	  +t30: U32,
1692	  +t31: U32,
1693	  +t32: U32,
1694	  +t33: U32,
1695	  +byte_length: Nat,
1696	  +extra: Nat,
1697	  state: S.State
1698	) -> S.State:
1699	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1700	    extra, state)
1701	
1702	# Apply SHA-256 round 35 to the compression state.
1703	def fin35(
1704	  +t0: U32,
1705	  +t1: U32,
1706	  +t2: U32,
1707	  +t3: U32,
1708	  +t4: U32,
1709	  +t5: U32,
1710	  +t6: U32,
1711	  +t7: U32,
1712	  +t8: U32,
1713	  +t9: U32,
1714	  +t10: U32,
1715	  +t11: U32,
1716	  +t12: U32,
1717	  +t13: U32,
1718	  +t14: U32,
1719	  +t15: U32,
1720	  +t16: U32,
1721	  +t17: U32,
1722	  +t18: U32,
1723	  +t19: U32,
1724	  +t20: U32,
1725	  +t21: U32,
1726	  +t22: U32,
1727	  +t23: U32,
1728	  +t24: U32,
1729	  +t25: U32,
1730	  +t26: U32,
1731	  +t27: U32,
1732	  +t28: U32,
1733	  +t29: U32,
1734	  +t30: U32,
1735	  +t31: U32,
1736	  +t32: U32,
1737	  +t33: U32,
1738	  +t34: U32,
1739	  +byte_length: Nat,
1740	  +extra: Nat,
1741	  state: S.State
1742	) -> S.State:
1743	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1744	    extra, state)
1745	
1746	# Apply SHA-256 round 36 to the compression state.
1747	def fin36(
1748	  +t0: U32,
1749	  +t1: U32,
1750	  +t2: U32,
1751	  +t3: U32,
1752	  +t4: U32,
1753	  +t5: U32,
1754	  +t6: U32,
1755	  +t7: U32,
1756	  +t8: U32,
1757	  +t9: U32,
1758	  +t10: U32,
1759	  +t11: U32,
1760	  +t12: U32,
1761	  +t13: U32,
1762	  +t14: U32,
1763	  +t15: U32,
1764	  +t16: U32,
1765	  +t17: U32,
1766	  +t18: U32,
1767	  +t19: U32,
1768	  +t20: U32,
1769	  +t21: U32,
1770	  +t22: U32,
1771	  +t23: U32,
1772	  +t24: U32,
1773	  +t25: U32,
1774	  +t26: U32,
1775	  +t27: U32,
1776	  +t28: U32,
1777	  +t29: U32,
1778	  +t30: U32,
1779	  +t31: U32,
1780	  +t32: U32,
1781	  +t33: U32,
1782	  +t34: U32,
1783	  +t35: U32,
1784	  +byte_length: Nat,
1785	  +extra: Nat,
1786	  state: S.State
1787	) -> S.State:
1788	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1789	    extra, state)
1790	
1791	# Apply SHA-256 round 37 to the compression state.
1792	def fin37(
1793	  +t0: U32,
1794	  +t1: U32,
1795	  +t2: U32,
1796	  +t3: U32,
1797	  +t4: U32,
1798	  +t5: U32,
1799	  +t6: U32,
1800	  +t7: U32,
1801	  +t8: U32,
1802	  +t9: U32,
1803	  +t10: U32,
1804	  +t11: U32,
1805	  +t12: U32,
1806	  +t13: U32,
1807	  +t14: U32,
1808	  +t15: U32,
1809	  +t16: U32,
1810	  +t17: U32,
1811	  +t18: U32,
1812	  +t19: U32,
1813	  +t20: U32,
1814	  +t21: U32,
1815	  +t22: U32,
1816	  +t23: U32,
1817	  +t24: U32,
1818	  +t25: U32,
1819	  +t26: U32,
1820	  +t27: U32,
1821	  +t28: U32,
1822	  +t29: U32,
1823	  +t30: U32,
1824	  +t31: U32,
1825	  +t32: U32,
1826	  +t33: U32,
1827	  +t34: U32,
1828	  +t35: U32,
1829	  +t36: U32,
1830	  +byte_length: Nat,
1831	  +extra: Nat,
1832	  state: S.State
1833	) -> S.State:
1834	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1835	    extra, state)
1836	
1837	# Apply SHA-256 round 38 to the compression state.
1838	def fin38(
1839	  +t0: U32,
1840	  +t1: U32,
1841	  +t2: U32,
1842	  +t3: U32,
1843	  +t4: U32,
1844	  +t5: U32,
1845	  +t6: U32,
1846	  +t7: U32,
1847	  +t8: U32,
1848	  +t9: U32,
1849	  +t10: U32,
1850	  +t11: U32,
1851	  +t12: U32,
1852	  +t13: U32,
1853	  +t14: U32,
1854	  +t15: U32,
1855	  +t16: U32,
1856	  +t17: U32,
1857	  +t18: U32,
1858	  +t19: U32,
1859	  +t20: U32,
1860	  +t21: U32,
1861	  +t22: U32,
1862	  +t23: U32,
1863	  +t24: U32,
1864	  +t25: U32,
1865	  +t26: U32,
1866	  +t27: U32,
1867	  +t28: U32,
1868	  +t29: U32,
1869	  +t30: U32,
1870	  +t31: U32,
1871	  +t32: U32,
1872	  +t33: U32,
1873	  +t34: U32,
1874	  +t35: U32,
1875	  +t36: U32,
1876	  +t37: U32,
1877	  +byte_length: Nat,
1878	  +extra: Nat,
1879	  state: S.State
1880	) -> S.State:
1881	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1882	    extra, state)
1883	
1884	# Apply SHA-256 round 39 to the compression state.
1885	def fin39(
1886	  +t0: U32,
1887	  +t1: U32,
1888	  +t2: U32,
1889	  +t3: U32,
1890	  +t4: U32,
1891	  +t5: U32,
1892	  +t6: U32,
1893	  +t7: U32,
1894	  +t8: U32,
1895	  +t9: U32,
1896	  +t10: U32,
1897	  +t11: U32,
1898	  +t12: U32,
1899	  +t13: U32,
1900	  +t14: U32,
1901	  +t15: U32,
1902	  +t16: U32,
1903	  +t17: U32,
1904	  +t18: U32,
1905	  +t19: U32,
1906	  +t20: U32,
1907	  +t21: U32,
1908	  +t22: U32,
1909	  +t23: U32,
1910	  +t24: U32,
1911	  +t25: U32,
1912	  +t26: U32,
1913	  +t27: U32,
1914	  +t28: U32,
1915	  +t29: U32,
1916	  +t30: U32,
1917	  +t31: U32,
1918	  +t32: U32,
1919	  +t33: U32,
1920	  +t34: U32,
1921	  +t35: U32,
1922	  +t36: U32,
1923	  +t37: U32,
1924	  +t38: U32,
1925	  +byte_length: Nat,
1926	  +extra: Nat,
1927	  state: S.State
1928	) -> S.State:
1929	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1930	    extra, state)
1931	
1932	# Apply SHA-256 round 40 to the compression state.
1933	def fin40(
1934	  +t0: U32,
1935	  +t1: U32,
1936	  +t2: U32,
1937	  +t3: U32,
1938	  +t4: U32,
1939	  +t5: U32,
1940	  +t6: U32,
1941	  +t7: U32,
1942	  +t8: U32,
1943	  +t9: U32,
1944	  +t10: U32,
1945	  +t11: U32,
1946	  +t12: U32,
1947	  +t13: U32,
1948	  +t14: U32,
1949	  +t15: U32,
1950	  +t16: U32,
1951	  +t17: U32,
1952	  +t18: U32,
1953	  +t19: U32,
1954	  +t20: U32,
1955	  +t21: U32,
1956	  +t22: U32,
1957	  +t23: U32,
1958	  +t24: U32,
1959	  +t25: U32,
1960	  +t26: U32,
1961	  +t27: U32,
1962	  +t28: U32,
1963	  +t29: U32,
1964	  +t30: U32,
1965	  +t31: U32,
1966	  +t32: U32,
1967	  +t33: U32,
1968	  +t34: U32,
1969	  +t35: U32,
1970	  +t36: U32,
1971	  +t37: U32,
1972	  +t38: U32,
1973	  +t39: U32,
1974	  +byte_length: Nat,
1975	  +extra: Nat,
1976	  state: S.State
1977	) -> S.State:
1978	  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(byte_length), len_lo(byte_length),
1979	    extra, state)
1980	
1981	# Apply SHA-256 round 41 to the compression state.
1982	def fin41(
1983	  +t0: U32,
1984	  +t1: U32,
1985	  +t2: U32,
1986	  +t3: U32,
1987	  +t4: U32,
1988	  +t5: U32,
1989	  +t6: U32,
1990	  +t7: U32,
1991	  +t8: U32,
1992	  +t9: U32,
1993	  +t10: U32,
1994	  +t11: U32,
1995	  +t12: U32,
1996	  +t13: U32,
1997	  +t14: U32,
1998	  +t15: U32,
1999	  +t16: U32,
2000	  +t17: U32,
Lines 1-2000 of 3620. More: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.4.0.0/src/hub_sha/core.bend&start_line=2001