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