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