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