1	# Generated by tools/generators/blake2s_gen.py; do not edit.
2	# Block reads, the last block, the block loop and the public API.
3	# The implementation keeps its own copy of the counter carry; each lemma
4	# carries the spec-side high counter half u1 with a proof e : t1 == u1.
5	import Base
6	import ../../../../src/crypto/blake/blake2s/types.bend as T
7	import ../../../../src/crypto/blake/blake2s/compress.bend as C
8	import ../../../../src/crypto/blake/blake2s/blake2s.bend as K
9	import ../../../../spec/crypto/blake/blake2s.bend as R
10	import ./compress.bend as P
11	import ./bytes.bend as B
12	import ./array.bend as A
13	
14	law carry_correct:
15	  for +c: Bool
16	  for +hi: U32
17	  {K.carry(c,hi) == R.carry(c,hi) : U32}
18	
19	def carry_correct(c,hi):
20	  match c:
21	    case True{}: {==}
22	    case False{}: {==}
23	
24	law count_correct:
25	  for +lo: U32
26	  for +hi: U32
27	  for +n: U32
28	  {K.count_hi(lo,hi,n) == R.count_hi(lo,hi,n) : U32}
29	
30	def count_correct(lo,hi,n):
31	  carry_correct(U32.is_lt(U32.add(lo,n),n),hi)
32	
33	law block_correct:
34	  for +h: T.State
35	  for +w0: U32
36	  for +w1: U32
37	  for +w2: U32
38	  for +w3: U32
39	  for +w4: U32
40	  for +w5: U32
41	  for +w6: U32
42	  for +w7: U32
43	  for +w8: U32
44	  for +w9: U32
45	  for +w10: U32
46	  for +w11: U32
47	  for +w12: U32
48	  for +w13: U32
49	  for +w14: U32
50	  for +w15: U32
51	  for +t0: U32
52	  for +t1: U32
53	  for +u1: U32
54	  for e: {t1 == u1 : U32}
55	  {C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}) == R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,u1,False{}) : T.State}
56	
57	def block_correct(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e):
58	  %e : {C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}) == R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,_,False{}) : T.State}
59	  Equal.trans(T.State,C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}),R.compress(10n,h,[w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],t0,t1,False{}),R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,t1,False{}),
60	    P.compress_correct(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}),
61	    Equal.cong(List<&2,U32>,T.State,l => R.compress(10n,h,l,t0,t1,False{}),[w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),Equal.sym(List<&2,U32>,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),[w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],B.words_serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]))))
62	
63	law last_correct:
64	  for +remain: Nat
65	  for +h: T.State
66	  for +w0: U32
67	  for +w1: U32
68	  for +w2: U32
69	  for +w3: U32
70	  for +w4: U32
71	  for +w5: U32
72	  for +w6: U32
73	  for +w7: U32
74	  for +w8: U32
75	  for +w9: U32
76	  for +w10: U32
77	  for +w11: U32
78	  for +w12: U32
79	  for +w13: U32
80	  for +w14: U32
81	  for +w15: U32
82	  for +t0: U32
83	  for +t1: U32
84	  for +u1: U32
85	  for e: {t1 == u1 : U32}
86	  {C.compress(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}) == R.compress(10n,h,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),t0,u1,True{}) : T.State}
87	
88	def last_correct(remain,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e):
89	  %e : {C.compress(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}) == R.compress(10n,h,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),t0,_,True{}) : T.State}
90	  Equal.trans(T.State,C.compress(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}),R.compress(10n,h,[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain)],t0,t1,True{}),R.compress(10n,h,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),t0,t1,True{}),
91	    P.compress_correct(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}),
92	    Equal.cong(List<&2,U32>,T.State,l => R.compress(10n,h,l,t0,t1,True{}),[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain)],R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),Equal.sym(List<&2,U32>,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain)],B.words_pad([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],0n,remain))))
93	
94	law read15_correct:
95	  for +index: U32
96	  for +h: T.State
97	  for +t0: U32
98	  for +t1: U32
99	  for +u1: U32
100	  for e: {t1 == u1 : U32}
101	  for +w0: U32
102	  for +w1: U32
103	  for +w2: U32
104	  for +w3: U32
105	  for +w4: U32
106	  for +w5: U32
107	  for +w6: U32
108	  for +w7: U32
109	  for +w8: U32
110	  for +w9: U32
111	  for +w10: U32
112	  for +w11: U32
113	  for +w12: U32
114	  for +w13: U32
115	  for +w14: U32
116	  for pair: Array<U32> & U32
117	  {K.read15(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == R.full_block(10n,R.gather(0n,index,16,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
118	
119	def read15_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
120	  (a,w15) = pair
121	  Equal.cong(T.State,Array<U32> & T.State,s => (a,s),C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}),R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,u1,False{}),block_correct(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e))
122	
123	law read14_correct:
124	  for +index: U32
125	  for +h: T.State
126	  for +t0: U32
127	  for +t1: U32
128	  for +u1: U32
129	  for e: {t1 == u1 : U32}
130	  for +w0: U32
131	  for +w1: U32
132	  for +w2: U32
133	  for +w3: U32
134	  for +w4: U32
135	  for +w5: U32
136	  for +w6: U32
137	  for +w7: U32
138	  for +w8: U32
139	  for +w9: U32
140	  for +w10: U32
141	  for +w11: U32
142	  for +w12: U32
143	  for +w13: U32
144	  for pair: Array<U32> & U32
145	  {K.read14(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == R.full_block(10n,R.gather(1n,index,15,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
146	
147	def read14_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
148	  (a,w14) = pair
149	  read15_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
150	
151	law read13_correct:
152	  for +index: U32
153	  for +h: T.State
154	  for +t0: U32
155	  for +t1: U32
156	  for +u1: U32
157	  for e: {t1 == u1 : U32}
158	  for +w0: U32
159	  for +w1: U32
160	  for +w2: U32
161	  for +w3: U32
162	  for +w4: U32
163	  for +w5: U32
164	  for +w6: U32
165	  for +w7: U32
166	  for +w8: U32
167	  for +w9: U32
168	  for +w10: U32
169	  for +w11: U32
170	  for +w12: U32
171	  for pair: Array<U32> & U32
172	  {K.read13(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == R.full_block(10n,R.gather(2n,index,14,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
173	
174	def read13_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
175	  (a,w13) = pair
176	  read14_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
177	
178	law read12_correct:
179	  for +index: U32
180	  for +h: T.State
181	  for +t0: U32
182	  for +t1: U32
183	  for +u1: U32
184	  for e: {t1 == u1 : U32}
185	  for +w0: U32
186	  for +w1: U32
187	  for +w2: U32
188	  for +w3: U32
189	  for +w4: U32
190	  for +w5: U32
191	  for +w6: U32
192	  for +w7: U32
193	  for +w8: U32
194	  for +w9: U32
195	  for +w10: U32
196	  for +w11: U32
197	  for pair: Array<U32> & U32
198	  {K.read12(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == R.full_block(10n,R.gather(3n,index,13,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
199	
200	def read12_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
201	  (a,w12) = pair
202	  read13_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
203	
204	law read11_correct:
205	  for +index: U32
206	  for +h: T.State
207	  for +t0: U32
208	  for +t1: U32
209	  for +u1: U32
210	  for e: {t1 == u1 : U32}
211	  for +w0: U32
212	  for +w1: U32
213	  for +w2: U32
214	  for +w3: U32
215	  for +w4: U32
216	  for +w5: U32
217	  for +w6: U32
218	  for +w7: U32
219	  for +w8: U32
220	  for +w9: U32
221	  for +w10: U32
222	  for pair: Array<U32> & U32
223	  {K.read11(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == R.full_block(10n,R.gather(4n,index,12,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
224	
225	def read11_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
226	  (a,w11) = pair
227	  read12_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
228	
229	law read10_correct:
230	  for +index: U32
231	  for +h: T.State
232	  for +t0: U32
233	  for +t1: U32
234	  for +u1: U32
235	  for e: {t1 == u1 : U32}
236	  for +w0: U32
237	  for +w1: U32
238	  for +w2: U32
239	  for +w3: U32
240	  for +w4: U32
241	  for +w5: U32
242	  for +w6: U32
243	  for +w7: U32
244	  for +w8: U32
245	  for +w9: U32
246	  for pair: Array<U32> & U32
247	  {K.read10(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == R.full_block(10n,R.gather(5n,index,11,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
248	
249	def read10_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
250	  (a,w10) = pair
251	  read11_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
252	
253	law read9_correct:
254	  for +index: U32
255	  for +h: T.State
256	  for +t0: U32
257	  for +t1: U32
258	  for +u1: U32
259	  for e: {t1 == u1 : U32}
260	  for +w0: U32
261	  for +w1: U32
262	  for +w2: U32
263	  for +w3: U32
264	  for +w4: U32
265	  for +w5: U32
266	  for +w6: U32
267	  for +w7: U32
268	  for +w8: U32
269	  for pair: Array<U32> & U32
270	  {K.read9(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == R.full_block(10n,R.gather(6n,index,10,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
271	
272	def read9_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
273	  (a,w9) = pair
274	  read10_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
275	
276	law read8_correct:
277	  for +index: U32
278	  for +h: T.State
279	  for +t0: U32
280	  for +t1: U32
281	  for +u1: U32
282	  for e: {t1 == u1 : U32}
283	  for +w0: U32
284	  for +w1: U32
285	  for +w2: U32
286	  for +w3: U32
287	  for +w4: U32
288	  for +w5: U32
289	  for +w6: U32
290	  for +w7: U32
291	  for pair: Array<U32> & U32
292	  {K.read8(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,pair) == R.full_block(10n,R.gather(7n,index,9,[w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
293	
294	def read8_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,pair):
295	  (a,w8) = pair
296	  read9_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
297	
298	law read7_correct:
299	  for +index: U32
300	  for +h: T.State
301	  for +t0: U32
302	  for +t1: U32
303	  for +u1: U32
304	  for e: {t1 == u1 : U32}
305	  for +w0: U32
306	  for +w1: U32
307	  for +w2: U32
308	  for +w3: U32
309	  for +w4: U32
310	  for +w5: U32
311	  for +w6: U32
312	  for pair: Array<U32> & U32
313	  {K.read7(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,pair) == R.full_block(10n,R.gather(8n,index,8,[w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
314	
315	def read7_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,pair):
316	  (a,w7) = pair
317	  read8_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
318	
319	law read6_correct:
320	  for +index: U32
321	  for +h: T.State
322	  for +t0: U32
323	  for +t1: U32
324	  for +u1: U32
325	  for e: {t1 == u1 : U32}
326	  for +w0: U32
327	  for +w1: U32
328	  for +w2: U32
329	  for +w3: U32
330	  for +w4: U32
331	  for +w5: U32
332	  for pair: Array<U32> & U32
333	  {K.read6(index,h,t0,t1,w0,w1,w2,w3,w4,w5,pair) == R.full_block(10n,R.gather(9n,index,7,[w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
334	
335	def read6_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,pair):
336	  (a,w6) = pair
337	  read7_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
338	
339	law read5_correct:
340	  for +index: U32
341	  for +h: T.State
342	  for +t0: U32
343	  for +t1: U32
344	  for +u1: U32
345	  for e: {t1 == u1 : U32}
346	  for +w0: U32
347	  for +w1: U32
348	  for +w2: U32
349	  for +w3: U32
350	  for +w4: U32
351	  for pair: Array<U32> & U32
352	  {K.read5(index,h,t0,t1,w0,w1,w2,w3,w4,pair) == R.full_block(10n,R.gather(10n,index,6,[w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
353	
354	def read5_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,pair):
355	  (a,w5) = pair
356	  read6_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
357	
358	law read4_correct:
359	  for +index: U32
360	  for +h: T.State
361	  for +t0: U32
362	  for +t1: U32
363	  for +u1: U32
364	  for e: {t1 == u1 : U32}
365	  for +w0: U32
366	  for +w1: U32
367	  for +w2: U32
368	  for +w3: U32
369	  for pair: Array<U32> & U32
370	  {K.read4(index,h,t0,t1,w0,w1,w2,w3,pair) == R.full_block(10n,R.gather(11n,index,5,[w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
371	
372	def read4_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,pair):
373	  (a,w4) = pair
374	  read5_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
375	
376	law read3_correct:
377	  for +index: U32
378	  for +h: T.State
379	  for +t0: U32
380	  for +t1: U32
381	  for +u1: U32
382	  for e: {t1 == u1 : U32}
383	  for +w0: U32
384	  for +w1: U32
385	  for +w2: U32
386	  for pair: Array<U32> & U32
387	  {K.read3(index,h,t0,t1,w0,w1,w2,pair) == R.full_block(10n,R.gather(12n,index,4,[w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
388	
389	def read3_correct(index,h,t0,t1,u1,e,w0,w1,w2,pair):
390	  (a,w3) = pair
391	  read4_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
392	
393	law read2_correct:
394	  for +index: U32
395	  for +h: T.State
396	  for +t0: U32
397	  for +t1: U32
398	  for +u1: U32
399	  for e: {t1 == u1 : U32}
400	  for +w0: U32
401	  for +w1: U32
402	  for pair: Array<U32> & U32
403	  {K.read2(index,h,t0,t1,w0,w1,pair) == R.full_block(10n,R.gather(13n,index,3,[w1,w0],pair),h,t0,u1) : Array<U32> & T.State}
404	
405	def read2_correct(index,h,t0,t1,u1,e,w0,w1,pair):
406	  (a,w2) = pair
407	  read3_correct(index,h,t0,t1,u1,e,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
408	
409	law read1_correct:
410	  for +index: U32
411	  for +h: T.State
412	  for +t0: U32
413	  for +t1: U32
414	  for +u1: U32
415	  for e: {t1 == u1 : U32}
416	  for +w0: U32
417	  for pair: Array<U32> & U32
418	  {K.read1(index,h,t0,t1,w0,pair) == R.full_block(10n,R.gather(14n,index,2,[w0],pair),h,t0,u1) : Array<U32> & T.State}
419	
420	def read1_correct(index,h,t0,t1,u1,e,w0,pair):
421	  (a,w1) = pair
422	  read2_correct(index,h,t0,t1,u1,e,w0,w1,Array.get(U32,a,U32.add(index,2)))
423	
424	law read0_correct:
425	  for +index: U32
426	  for +h: T.State
427	  for +t0: U32
428	  for +t1: U32
429	  for +u1: U32
430	  for e: {t1 == u1 : U32}
431	  for pair: Array<U32> & U32
432	  {K.read0(index,h,t0,t1,pair) == R.full_block(10n,R.gather(15n,index,1,[],pair),h,t0,u1) : Array<U32> & T.State}
433	
434	def read0_correct(index,h,t0,t1,u1,e,pair):
435	  (a,w0) = pair
436	  read1_correct(index,h,t0,t1,u1,e,w0,Array.get(U32,a,U32.add(index,1)))
437	
438	law pad15_correct:
439	  for +remain: Nat
440	  for +index: U32
441	  for +h: T.State
442	  for +t0: U32
443	  for +t1: U32
444	  for +u1: U32
445	  for e: {t1 == u1 : U32}
446	  for +w0: U32
447	  for +w1: U32
448	  for +w2: U32
449	  for +w3: U32
450	  for +w4: U32
451	  for +w5: U32
452	  for +w6: U32
453	  for +w7: U32
454	  for +w8: U32
455	  for +w9: U32
456	  for +w10: U32
457	  for +w11: U32
458	  for +w12: U32
459	  for +w13: U32
460	  for +w14: U32
461	  for pair: Array<U32> & U32
462	  {K.pad15(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == R.last_block(10n,R.gather(0n,index,16,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
463	
464	def pad15_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
465	  (a,w15) = pair
466	  last_correct(remain,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e)
467	
468	law pad14_correct:
469	  for +remain: Nat
470	  for +index: U32
471	  for +h: T.State
472	  for +t0: U32
473	  for +t1: U32
474	  for +u1: U32
475	  for e: {t1 == u1 : U32}
476	  for +w0: U32
477	  for +w1: U32
478	  for +w2: U32
479	  for +w3: U32
480	  for +w4: U32
481	  for +w5: U32
482	  for +w6: U32
483	  for +w7: U32
484	  for +w8: U32
485	  for +w9: U32
486	  for +w10: U32
487	  for +w11: U32
488	  for +w12: U32
489	  for +w13: U32
490	  for pair: Array<U32> & U32
491	  {K.pad14(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == R.last_block(10n,R.gather(1n,index,15,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
492	
493	def pad14_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
494	  (a,w14) = pair
495	  pad15_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
496	
497	law pad13_correct:
498	  for +remain: Nat
499	  for +index: U32
500	  for +h: T.State
501	  for +t0: U32
502	  for +t1: U32
503	  for +u1: U32
504	  for e: {t1 == u1 : U32}
505	  for +w0: U32
506	  for +w1: U32
507	  for +w2: U32
508	  for +w3: U32
509	  for +w4: U32
510	  for +w5: U32
511	  for +w6: U32
512	  for +w7: U32
513	  for +w8: U32
514	  for +w9: U32
515	  for +w10: U32
516	  for +w11: U32
517	  for +w12: U32
518	  for pair: Array<U32> & U32
519	  {K.pad13(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == R.last_block(10n,R.gather(2n,index,14,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
520	
521	def pad13_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
522	  (a,w13) = pair
523	  pad14_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
524	
525	law pad12_correct:
526	  for +remain: Nat
527	  for +index: U32
528	  for +h: T.State
529	  for +t0: U32
530	  for +t1: U32
531	  for +u1: U32
532	  for e: {t1 == u1 : U32}
533	  for +w0: U32
534	  for +w1: U32
535	  for +w2: U32
536	  for +w3: U32
537	  for +w4: U32
538	  for +w5: U32
539	  for +w6: U32
540	  for +w7: U32
541	  for +w8: U32
542	  for +w9: U32
543	  for +w10: U32
544	  for +w11: U32
545	  for pair: Array<U32> & U32
546	  {K.pad12(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == R.last_block(10n,R.gather(3n,index,13,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
547	
548	def pad12_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
549	  (a,w12) = pair
550	  pad13_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
551	
552	law pad11_correct:
553	  for +remain: Nat
554	  for +index: U32
555	  for +h: T.State
556	  for +t0: U32
557	  for +t1: U32
558	  for +u1: U32
559	  for e: {t1 == u1 : U32}
560	  for +w0: U32
561	  for +w1: U32
562	  for +w2: U32
563	  for +w3: U32
564	  for +w4: U32
565	  for +w5: U32
566	  for +w6: U32
567	  for +w7: U32
568	  for +w8: U32
569	  for +w9: U32
570	  for +w10: U32
571	  for pair: Array<U32> & U32
572	  {K.pad11(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == R.last_block(10n,R.gather(4n,index,12,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
573	
574	def pad11_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
575	  (a,w11) = pair
576	  pad12_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
577	
578	law pad10_correct:
579	  for +remain: Nat
580	  for +index: U32
581	  for +h: T.State
582	  for +t0: U32
583	  for +t1: U32
584	  for +u1: U32
585	  for e: {t1 == u1 : U32}
586	  for +w0: U32
587	  for +w1: U32
588	  for +w2: U32
589	  for +w3: U32
590	  for +w4: U32
591	  for +w5: U32
592	  for +w6: U32
593	  for +w7: U32
594	  for +w8: U32
595	  for +w9: U32
596	  for pair: Array<U32> & U32
597	  {K.pad10(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == R.last_block(10n,R.gather(5n,index,11,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
598	
599	def pad10_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
600	  (a,w10) = pair
601	  pad11_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
602	
603	law pad9_correct:
604	  for +remain: Nat
605	  for +index: U32
606	  for +h: T.State
607	  for +t0: U32
608	  for +t1: U32
609	  for +u1: U32
610	  for e: {t1 == u1 : U32}
611	  for +w0: U32
612	  for +w1: U32
613	  for +w2: U32
614	  for +w3: U32
615	  for +w4: U32
616	  for +w5: U32
617	  for +w6: U32
618	  for +w7: U32
619	  for +w8: U32
620	  for pair: Array<U32> & U32
621	  {K.pad9(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == R.last_block(10n,R.gather(6n,index,10,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
622	
623	def pad9_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
624	  (a,w9) = pair
625	  pad10_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
626	
627	law pad8_correct:
628	  for +remain: Nat
629	  for +index: U32
630	  for +h: T.State
631	  for +t0: U32
632	  for +t1: U32
633	  for +u1: U32
634	  for e: {t1 == u1 : U32}
635	  for +w0: U32
636	  for +w1: U32
637	  for +w2: U32
638	  for +w3: U32
639	  for +w4: U32
640	  for +w5: U32
641	  for +w6: U32
642	  for +w7: U32
643	  for pair: Array<U32> & U32
644	  {K.pad8(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,pair) == R.last_block(10n,R.gather(7n,index,9,[w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
645	
646	def pad8_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,pair):
647	  (a,w8) = pair
648	  pad9_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
649	
650	law pad7_correct:
651	  for +remain: Nat
652	  for +index: U32
653	  for +h: T.State
654	  for +t0: U32
655	  for +t1: U32
656	  for +u1: U32
657	  for e: {t1 == u1 : U32}
658	  for +w0: U32
659	  for +w1: U32
660	  for +w2: U32
661	  for +w3: U32
662	  for +w4: U32
663	  for +w5: U32
664	  for +w6: U32
665	  for pair: Array<U32> & U32
666	  {K.pad7(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,pair) == R.last_block(10n,R.gather(8n,index,8,[w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
667	
668	def pad7_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,pair):
669	  (a,w7) = pair
670	  pad8_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
671	
672	law pad6_correct:
673	  for +remain: Nat
674	  for +index: U32
675	  for +h: T.State
676	  for +t0: U32
677	  for +t1: U32
678	  for +u1: U32
679	  for e: {t1 == u1 : U32}
680	  for +w0: U32
681	  for +w1: U32
682	  for +w2: U32
683	  for +w3: U32
684	  for +w4: U32
685	  for +w5: U32
686	  for pair: Array<U32> & U32
687	  {K.pad6(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,pair) == R.last_block(10n,R.gather(9n,index,7,[w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
688	
689	def pad6_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,pair):
690	  (a,w6) = pair
691	  pad7_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
692	
693	law pad5_correct:
694	  for +remain: Nat
695	  for +index: U32
696	  for +h: T.State
697	  for +t0: U32
698	  for +t1: U32
699	  for +u1: U32
700	  for e: {t1 == u1 : U32}
701	  for +w0: U32
702	  for +w1: U32
703	  for +w2: U32
704	  for +w3: U32
705	  for +w4: U32
706	  for pair: Array<U32> & U32
707	  {K.pad5(remain,index,h,t0,t1,w0,w1,w2,w3,w4,pair) == R.last_block(10n,R.gather(10n,index,6,[w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
708	
709	def pad5_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,pair):
710	  (a,w5) = pair
711	  pad6_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
712	
713	law pad4_correct:
714	  for +remain: Nat
715	  for +index: U32
716	  for +h: T.State
717	  for +t0: U32
718	  for +t1: U32
719	  for +u1: U32
720	  for e: {t1 == u1 : U32}
721	  for +w0: U32
722	  for +w1: U32
723	  for +w2: U32
724	  for +w3: U32
725	  for pair: Array<U32> & U32
726	  {K.pad4(remain,index,h,t0,t1,w0,w1,w2,w3,pair) == R.last_block(10n,R.gather(11n,index,5,[w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}
727	
728	def pad4_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,pair):
729	  (a,w4) = pair
730	  pad5_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
731	
732	law pad3_correct:
733	  for +remain: Nat
734	  for +index: U32
735	  for +h: T.State
736	  for +t0: U32
737	  for +t1: U32
738	  for +u1: U32
739	  for e: {t1 == u1 : U32}
740	  for +w0: U32
741	  for +w1: U32
742	  for +w2: U32
743	  for pair: Array<U32> & U32
744	  {K.pad3(remain,index,h,t0,t1,w0,w1,w2,pair) == R.last_block(10n,R.gather(12n,index,4,[w2,w1,w0],pair),remain,h,t0,u1) : T.State}
745	
746	def pad3_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,pair):
747	  (a,w3) = pair
748	  pad4_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
749	
750	law pad2_correct:
751	  for +remain: Nat
752	  for +index: U32
753	  for +h: T.State
754	  for +t0: U32
755	  for +t1: U32
756	  for +u1: U32
757	  for e: {t1 == u1 : U32}
758	  for +w0: U32
759	  for +w1: U32
760	  for pair: Array<U32> & U32
761	  {K.pad2(remain,index,h,t0,t1,w0,w1,pair) == R.last_block(10n,R.gather(13n,index,3,[w1,w0],pair),remain,h,t0,u1) : T.State}
762	
763	def pad2_correct(remain,index,h,t0,t1,u1,e,w0,w1,pair):
764	  (a,w2) = pair
765	  pad3_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
766	
767	law pad1_correct:
768	  for +remain: Nat
769	  for +index: U32
770	  for +h: T.State
771	  for +t0: U32
772	  for +t1: U32
773	  for +u1: U32
774	  for e: {t1 == u1 : U32}
775	  for +w0: U32
776	  for pair: Array<U32> & U32
777	  {K.pad1(remain,index,h,t0,t1,w0,pair) == R.last_block(10n,R.gather(14n,index,2,[w0],pair),remain,h,t0,u1) : T.State}
778	
779	def pad1_correct(remain,index,h,t0,t1,u1,e,w0,pair):
780	  (a,w1) = pair
781	  pad2_correct(remain,index,h,t0,t1,u1,e,w0,w1,Array.get(U32,a,U32.add(index,2)))
782	
783	law pad0_correct:
784	  for +remain: Nat
785	  for +index: U32
786	  for +h: T.State
787	  for +t0: U32
788	  for +t1: U32
789	  for +u1: U32
790	  for e: {t1 == u1 : U32}
791	  for pair: Array<U32> & U32
792	  {K.pad0(remain,index,h,t0,t1,pair) == R.last_block(10n,R.gather(15n,index,1,[],pair),remain,h,t0,u1) : T.State}
793	
794	def pad0_correct(remain,index,h,t0,t1,u1,e,pair):
795	  (a,w0) = pair
796	  pad1_correct(remain,index,h,t0,t1,u1,e,w0,Array.get(U32,a,U32.add(index,1)))
797	
798	law absorb_correct:
799	  for a: Array<U32>
800	  for +index: U32
801	  for +h: T.State
802	  for +t0: U32
803	  for +t1: U32
804	  for +u1: U32
805	  for e: {t1 == u1 : U32}
806	  {K.absorb(a,index,h,t0,t1) == R.absorb(10n,a,index,h,t0,u1) : Array<U32> & T.State}
807	
808	def absorb_correct(a,index,h,t0,t1,u1,e):
809	  read0_correct(index,h,t0,t1,u1,e,Array.get(U32,a,index))
810	
811	law finish_correct:
812	  for a: Array<U32>
813	  for +index: U32
814	  for +t0: U32
815	  for +t1: U32
816	  for +remain: Nat
817	  for +h: T.State
818	  {K.finish(a,index,t0,t1,remain,h) == R.finish(10n,a,index,t0,t1,remain,h) : T.State}
819	
820	def finish_correct(a,index,t0,t1,remain,h):
821	  pad0_correct(remain,index,h,U32.add(t0,U32.from_nat(remain)),K.count_hi(t0,t1,U32.from_nat(remain)),R.count_hi(t0,t1,U32.from_nat(remain)),count_correct(t0,t1,U32.from_nat(remain)),Array.get(U32,a,index))
822	
823	law blocks_step:
824	  for +n: Nat
825	  for +index: U32
826	  for +t0: U32
827	  for +t1: U32
828	  for +remain: Nat
829	  for -a: Array<U32>
830	  for +h: T.State
831	  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
832	  for recurse: @pair: (Array<U32> & T.State) -> {K.blocks(n,U32.add(index,16),U32.add(t0,64),K.count_hi(t0,t1,64),remain,pair) == R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,pair) : T.State}
833	  {K.blocks(1n+n,index,t0,t1,remain,(a,h)) == R.blocks(10n,1n+n,index,t0,t1,remain,(a,h)) : T.State}
834	
835	def blocks_step(n,index,t0,t1,remain,a,h,view,recurse):
836	  match view:
837	    case Tuple{+tree,pf}:
838	      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.blocks(1n+n,index,t0,t1,remain,(_,h)) == R.blocks(10n,1n+n,index,t0,t1,remain,(_,h)) : T.State}
839	      Equal.trans(T.State,
840	        K.blocks(n,U32.add(index,16),U32.add(t0,64),K.count_hi(t0,t1,64),remain,K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64))),
841	        R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64))),
842	        R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,R.absorb(10n,A.thaw(tree),index,h,U32.add(t0,64),R.count_hi(t0,t1,64))),
843	        recurse(K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64))),
844	        Equal.cong(Array<U32> & T.State,T.State,pair => R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,pair),K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64)),R.absorb(10n,A.thaw(tree),index,h,U32.add(t0,64),R.count_hi(t0,t1,64)),absorb_correct(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64),R.count_hi(t0,t1,64),count_correct(t0,t1,64))))
845	
846	law blocks_correct:
847	  for +n: Nat
848	  for +index: U32
849	  for +t0: U32
850	  for +t1: U32
851	  for +u1: U32
852	  for e: {t1 == u1 : U32}
853	  for +remain: Nat
854	  for pair: Array<U32> & T.State
855	  {K.blocks(n,index,t0,t1,remain,pair) == R.blocks(10n,n,index,t0,u1,remain,pair) : T.State}
856	
857	def blocks_correct(n,index,t0,t1,u1,e,remain,pair):
858	  match n pair:
859	    case 0n Tuple{a,h}:
860	      %e : {K.blocks(0n,index,t0,t1,remain,(a,h)) == R.blocks(10n,0n,index,t0,_,remain,(a,h)) : T.State}
861	      finish_correct(a,index,t0,t1,remain,h)
862	    case 1n+p Tuple{a,h}:
863	      %e : {K.blocks(1n+p,index,t0,t1,remain,(a,h)) == R.blocks(10n,1n+p,index,t0,_,remain,(a,h)) : T.State}
864	      blocks_step(p,index,t0,t1,remain,a,h,A.reify(a),pair => blocks_correct(p,U32.add(index,16),U32.add(t0,64),K.count_hi(t0,t1,64),R.count_hi(t0,t1,64),count_correct(t0,t1,64),remain,pair))
865	
866	law leading_correct:
867	  for +length: Nat
868	  {K.leading(length) == Nat.sub(R.block_count(length),1n) : Nat}
869	
870	def leading_correct(length):
871	  match length:
872	    case 0n: {==}
873	    case 1n+p: {==}
874	
875	law hash_tail:
876	  for -a: Array<U32>
877	  for +length: Nat
878	  {R.blocks(10n,K.leading(length),0,0,0,Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())) == R.hash(10n,a,length) : T.State}
879	
880	def hash_tail(a,length):
881	  %leading_correct(length) : {R.blocks(10n,K.leading(length),0,0,0,Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())) == R.blocks(10n,_,0,0,0,Nat.sub(length,Nat.mul(64n,_)),(a,R.initial())) : T.State}
882	  {==}
883	
884	law unchecked_correct:
885	  for a: Array<U32>
886	  for +length: Nat
887	  {K.unchecked(a,length) == R.hash(10n,a,length) : T.State}
888	
889	def unchecked_correct(a,length):
890	  Equal.trans(T.State,K.unchecked(a,length),R.blocks(10n,K.leading(length),0,0,0,Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())),R.hash(10n,a,length),
891	    blocks_correct(K.leading(length),0,0,0,0,{==},Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())),
892	    hash_tail(a,length))
893	
894	law digest_correct:
895	  for +h: T.State
896	  {K.digest(h) == R.digest(h) : Array<U32>}
897	
898	def digest_correct(h):
899	  match h:
900	    case T.H{h0,h1,h2,h3,h4,h5,h6,h7}: {==}
901	
902	law checked_true:
903	  for -a: Array<U32>
904	  for +length: Nat
905	  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
906	  {K.checked(True{},a,length) == R.checked(10n,True{},a,length) : Maybe<&1,Array<U32>>}
907	
908	def checked_true(a,length,view):
909	  match view:
910	    case Tuple{+tree,pf}:
911	      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.checked(True{},_,length) == R.checked(10n,True{},_,length) : Maybe<&1,Array<U32>>}
912	      Equal.trans(Maybe<&1,Array<U32>>,
913	        Some{K.digest(K.unchecked(A.thaw(tree),length))},
914	        Some{K.digest(R.hash(10n,A.thaw(tree),length))},
915	        Some{R.digest(R.hash(10n,A.thaw(tree),length))},
916	        Equal.cong(T.State,Maybe<&1,Array<U32>>,s => Some{K.digest(s)},K.unchecked(A.thaw(tree),length),R.hash(10n,A.thaw(tree),length),unchecked_correct(A.thaw(tree),length)),
917	        Equal.cong(Array<U32>,Maybe<&1,Array<U32>>,d => Some{d},K.digest(R.hash(10n,A.thaw(tree),length)),R.digest(R.hash(10n,A.thaw(tree),length)),digest_correct(R.hash(10n,A.thaw(tree),length))))
918	
919	law checked_correct:
920	  for +valid: Bool
921	  for a: Array<U32>
922	  for +length: Nat
923	  {K.checked(valid,a,length) == R.checked(10n,valid,a,length) : Maybe<&1,Array<U32>>}
924	
925	def checked_correct(valid,a,length):
926	  match valid:
927	    case False{}: {==}
928	    case True{}: checked_true(a,length,A.reify(a))
929	
930	law sized_correct:
931	  for +length: Nat
932	  for pair: Array<U32> & U32
933	  {K.sized(length,pair) == R.sized(10n,length,pair) : Maybe<&1,Array<U32>>}
934	
935	def sized_correct(length,pair):
936	  (a,capacity) = pair
937	  checked_correct(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
938	
939	law blake2s_correct:
940	  for a: Array<U32>
941	  for +length: Nat
942	  {K.blake2s(a,length) == R.blake2s(a,length) : Maybe<&1,Array<U32>>}
943	
944	def blake2s_correct(a,length):
945	  sized_correct(length,Array.size(U32,a))