proofs/crypto/blake/blake2b/blocks.bend

bend-collections-laws-crypto@1.0.0.0 · 1,943 lines · 76 definitions

1# Generated by tools/generators/blake2b_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/compress.bend as F
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend as I
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as S
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/compress.bend as C
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/array.bend as A
9
10law read31_correct:
11  for +index: U32
12  for +t: T.Counter
13  for +h: T.Chain
14  for +w0: U32
15  for +w1: U32
16  for +w2: U32
17  for +w3: U32
18  for +w4: U32
19  for +w5: U32
20  for +w6: U32
21  for +w7: U32
22  for +w8: U32
23  for +w9: U32
24  for +w10: U32
25  for +w11: U32
26  for +w12: U32
27  for +w13: U32
28  for +w14: U32
29  for +w15: U32
30  for +w16: U32
31  for +w17: U32
32  for +w18: U32
33  for +w19: U32
34  for +w20: U32
35  for +w21: U32
36  for +w22: U32
37  for +w23: U32
38  for +w24: U32
39  for +w25: U32
40  for +w26: U32
41  for +w27: U32
42  for +w28: U32
43  for +w29: U32
44  for +w30: U32
45  for pair: Array<U32> & U32
46  {I.read31(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair) == S.gather(0n,index,32,False{},0n,t,h,[w30,w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
47
48def read31_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair):
49  (a,w31) = pair
50  Equal.cong(T.Chain,Array<U32> & T.Chain,x => (a,x),F.compress(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31),S.compress(h,[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}],t,False{}),C.compress_correct(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31))
51
52law read30_correct:
53  for +index: U32
54  for +t: T.Counter
55  for +h: T.Chain
56  for +w0: U32
57  for +w1: U32
58  for +w2: U32
59  for +w3: U32
60  for +w4: U32
61  for +w5: U32
62  for +w6: U32
63  for +w7: U32
64  for +w8: U32
65  for +w9: U32
66  for +w10: U32
67  for +w11: U32
68  for +w12: U32
69  for +w13: U32
70  for +w14: U32
71  for +w15: U32
72  for +w16: U32
73  for +w17: U32
74  for +w18: U32
75  for +w19: U32
76  for +w20: U32
77  for +w21: U32
78  for +w22: U32
79  for +w23: U32
80  for +w24: U32
81  for +w25: U32
82  for +w26: U32
83  for +w27: U32
84  for +w28: U32
85  for +w29: U32
86  for pair: Array<U32> & U32
87  {I.read30(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair) == S.gather(1n,index,31,False{},0n,t,h,[w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
88
89def read30_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair):
90  (a,w30) = pair
91  read31_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,Array.get(U32,a,U32.add(index,31)))
92
93law read29_correct:
94  for +index: U32
95  for +t: T.Counter
96  for +h: T.Chain
97  for +w0: U32
98  for +w1: U32
99  for +w2: U32
100  for +w3: U32
101  for +w4: U32
102  for +w5: U32
103  for +w6: U32
104  for +w7: U32
105  for +w8: U32
106  for +w9: U32
107  for +w10: U32
108  for +w11: U32
109  for +w12: U32
110  for +w13: U32
111  for +w14: U32
112  for +w15: U32
113  for +w16: U32
114  for +w17: U32
115  for +w18: U32
116  for +w19: U32
117  for +w20: U32
118  for +w21: U32
119  for +w22: U32
120  for +w23: U32
121  for +w24: U32
122  for +w25: U32
123  for +w26: U32
124  for +w27: U32
125  for +w28: U32
126  for pair: Array<U32> & U32
127  {I.read29(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair) == S.gather(2n,index,30,False{},0n,t,h,[w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
128
129def read29_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair):
130  (a,w29) = pair
131  read30_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,Array.get(U32,a,U32.add(index,30)))
132
133law read28_correct:
134  for +index: U32
135  for +t: T.Counter
136  for +h: T.Chain
137  for +w0: U32
138  for +w1: U32
139  for +w2: U32
140  for +w3: U32
141  for +w4: U32
142  for +w5: U32
143  for +w6: U32
144  for +w7: U32
145  for +w8: U32
146  for +w9: U32
147  for +w10: U32
148  for +w11: U32
149  for +w12: U32
150  for +w13: U32
151  for +w14: U32
152  for +w15: U32
153  for +w16: U32
154  for +w17: U32
155  for +w18: U32
156  for +w19: U32
157  for +w20: U32
158  for +w21: U32
159  for +w22: U32
160  for +w23: U32
161  for +w24: U32
162  for +w25: U32
163  for +w26: U32
164  for +w27: U32
165  for pair: Array<U32> & U32
166  {I.read28(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair) == S.gather(3n,index,29,False{},0n,t,h,[w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
167
168def read28_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair):
169  (a,w28) = pair
170  read29_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,Array.get(U32,a,U32.add(index,29)))
171
172law read27_correct:
173  for +index: U32
174  for +t: T.Counter
175  for +h: T.Chain
176  for +w0: U32
177  for +w1: U32
178  for +w2: U32
179  for +w3: U32
180  for +w4: U32
181  for +w5: U32
182  for +w6: U32
183  for +w7: U32
184  for +w8: U32
185  for +w9: U32
186  for +w10: U32
187  for +w11: U32
188  for +w12: U32
189  for +w13: U32
190  for +w14: U32
191  for +w15: U32
192  for +w16: U32
193  for +w17: U32
194  for +w18: U32
195  for +w19: U32
196  for +w20: U32
197  for +w21: U32
198  for +w22: U32
199  for +w23: U32
200  for +w24: U32
201  for +w25: U32
202  for +w26: U32
203  for pair: Array<U32> & U32
204  {I.read27(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair) == S.gather(4n,index,28,False{},0n,t,h,[w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
205
206def read27_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair):
207  (a,w27) = pair
208  read28_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,Array.get(U32,a,U32.add(index,28)))
209
210law read26_correct:
211  for +index: U32
212  for +t: T.Counter
213  for +h: T.Chain
214  for +w0: U32
215  for +w1: U32
216  for +w2: U32
217  for +w3: U32
218  for +w4: U32
219  for +w5: U32
220  for +w6: U32
221  for +w7: U32
222  for +w8: U32
223  for +w9: U32
224  for +w10: U32
225  for +w11: U32
226  for +w12: U32
227  for +w13: U32
228  for +w14: U32
229  for +w15: U32
230  for +w16: U32
231  for +w17: U32
232  for +w18: U32
233  for +w19: U32
234  for +w20: U32
235  for +w21: U32
236  for +w22: U32
237  for +w23: U32
238  for +w24: U32
239  for +w25: U32
240  for pair: Array<U32> & U32
241  {I.read26(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair) == S.gather(5n,index,27,False{},0n,t,h,[w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
242
243def read26_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair):
244  (a,w26) = pair
245  read27_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,Array.get(U32,a,U32.add(index,27)))
246
247law read25_correct:
248  for +index: U32
249  for +t: T.Counter
250  for +h: T.Chain
251  for +w0: U32
252  for +w1: U32
253  for +w2: U32
254  for +w3: U32
255  for +w4: U32
256  for +w5: U32
257  for +w6: U32
258  for +w7: U32
259  for +w8: U32
260  for +w9: U32
261  for +w10: U32
262  for +w11: U32
263  for +w12: U32
264  for +w13: U32
265  for +w14: U32
266  for +w15: U32
267  for +w16: U32
268  for +w17: U32
269  for +w18: U32
270  for +w19: U32
271  for +w20: U32
272  for +w21: U32
273  for +w22: U32
274  for +w23: U32
275  for +w24: U32
276  for pair: Array<U32> & U32
277  {I.read25(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair) == S.gather(6n,index,26,False{},0n,t,h,[w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
278
279def read25_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair):
280  (a,w25) = pair
281  read26_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,Array.get(U32,a,U32.add(index,26)))
282
283law read24_correct:
284  for +index: U32
285  for +t: T.Counter
286  for +h: T.Chain
287  for +w0: U32
288  for +w1: U32
289  for +w2: U32
290  for +w3: U32
291  for +w4: U32
292  for +w5: U32
293  for +w6: U32
294  for +w7: U32
295  for +w8: U32
296  for +w9: U32
297  for +w10: U32
298  for +w11: U32
299  for +w12: U32
300  for +w13: U32
301  for +w14: U32
302  for +w15: U32
303  for +w16: U32
304  for +w17: U32
305  for +w18: U32
306  for +w19: U32
307  for +w20: U32
308  for +w21: U32
309  for +w22: U32
310  for +w23: U32
311  for pair: Array<U32> & U32
312  {I.read24(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair) == S.gather(7n,index,25,False{},0n,t,h,[w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
313
314def read24_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair):
315  (a,w24) = pair
316  read25_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,Array.get(U32,a,U32.add(index,25)))
317
318law read23_correct:
319  for +index: U32
320  for +t: T.Counter
321  for +h: T.Chain
322  for +w0: U32
323  for +w1: U32
324  for +w2: U32
325  for +w3: U32
326  for +w4: U32
327  for +w5: U32
328  for +w6: U32
329  for +w7: U32
330  for +w8: U32
331  for +w9: U32
332  for +w10: U32
333  for +w11: U32
334  for +w12: U32
335  for +w13: U32
336  for +w14: U32
337  for +w15: U32
338  for +w16: U32
339  for +w17: U32
340  for +w18: U32
341  for +w19: U32
342  for +w20: U32
343  for +w21: U32
344  for +w22: U32
345  for pair: Array<U32> & U32
346  {I.read23(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair) == S.gather(8n,index,24,False{},0n,t,h,[w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
347
348def read23_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair):
349  (a,w23) = pair
350  read24_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,Array.get(U32,a,U32.add(index,24)))
351
352law read22_correct:
353  for +index: U32
354  for +t: T.Counter
355  for +h: T.Chain
356  for +w0: U32
357  for +w1: U32
358  for +w2: U32
359  for +w3: U32
360  for +w4: U32
361  for +w5: U32
362  for +w6: U32
363  for +w7: U32
364  for +w8: U32
365  for +w9: U32
366  for +w10: U32
367  for +w11: U32
368  for +w12: U32
369  for +w13: U32
370  for +w14: U32
371  for +w15: U32
372  for +w16: U32
373  for +w17: U32
374  for +w18: U32
375  for +w19: U32
376  for +w20: U32
377  for +w21: U32
378  for pair: Array<U32> & U32
379  {I.read22(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair) == S.gather(9n,index,23,False{},0n,t,h,[w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
380
381def read22_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair):
382  (a,w22) = pair
383  read23_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,Array.get(U32,a,U32.add(index,23)))
384
385law read21_correct:
386  for +index: U32
387  for +t: T.Counter
388  for +h: T.Chain
389  for +w0: U32
390  for +w1: U32
391  for +w2: U32
392  for +w3: U32
393  for +w4: U32
394  for +w5: U32
395  for +w6: U32
396  for +w7: U32
397  for +w8: U32
398  for +w9: U32
399  for +w10: U32
400  for +w11: U32
401  for +w12: U32
402  for +w13: U32
403  for +w14: U32
404  for +w15: U32
405  for +w16: U32
406  for +w17: U32
407  for +w18: U32
408  for +w19: U32
409  for +w20: U32
410  for pair: Array<U32> & U32
411  {I.read21(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair) == S.gather(10n,index,22,False{},0n,t,h,[w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
412
413def read21_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair):
414  (a,w21) = pair
415  read22_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,Array.get(U32,a,U32.add(index,22)))
416
417law read20_correct:
418  for +index: U32
419  for +t: T.Counter
420  for +h: T.Chain
421  for +w0: U32
422  for +w1: U32
423  for +w2: U32
424  for +w3: U32
425  for +w4: U32
426  for +w5: U32
427  for +w6: U32
428  for +w7: U32
429  for +w8: U32
430  for +w9: U32
431  for +w10: U32
432  for +w11: U32
433  for +w12: U32
434  for +w13: U32
435  for +w14: U32
436  for +w15: U32
437  for +w16: U32
438  for +w17: U32
439  for +w18: U32
440  for +w19: U32
441  for pair: Array<U32> & U32
442  {I.read20(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair) == S.gather(11n,index,21,False{},0n,t,h,[w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
443
444def read20_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair):
445  (a,w20) = pair
446  read21_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,Array.get(U32,a,U32.add(index,21)))
447
448law read19_correct:
449  for +index: U32
450  for +t: T.Counter
451  for +h: T.Chain
452  for +w0: U32
453  for +w1: U32
454  for +w2: U32
455  for +w3: U32
456  for +w4: U32
457  for +w5: U32
458  for +w6: U32
459  for +w7: U32
460  for +w8: U32
461  for +w9: U32
462  for +w10: U32
463  for +w11: U32
464  for +w12: U32
465  for +w13: U32
466  for +w14: U32
467  for +w15: U32
468  for +w16: U32
469  for +w17: U32
470  for +w18: U32
471  for pair: Array<U32> & U32
472  {I.read19(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair) == S.gather(12n,index,20,False{},0n,t,h,[w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
473
474def read19_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair):
475  (a,w19) = pair
476  read20_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,Array.get(U32,a,U32.add(index,20)))
477
478law read18_correct:
479  for +index: U32
480  for +t: T.Counter
481  for +h: T.Chain
482  for +w0: U32
483  for +w1: U32
484  for +w2: U32
485  for +w3: U32
486  for +w4: U32
487  for +w5: U32
488  for +w6: U32
489  for +w7: U32
490  for +w8: U32
491  for +w9: U32
492  for +w10: U32
493  for +w11: U32
494  for +w12: U32
495  for +w13: U32
496  for +w14: U32
497  for +w15: U32
498  for +w16: U32
499  for +w17: U32
500  for pair: Array<U32> & U32
501  {I.read18(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair) == S.gather(13n,index,19,False{},0n,t,h,[w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
502
503def read18_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair):
504  (a,w18) = pair
505  read19_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,Array.get(U32,a,U32.add(index,19)))
506
507law read17_correct:
508  for +index: U32
509  for +t: T.Counter
510  for +h: T.Chain
511  for +w0: U32
512  for +w1: U32
513  for +w2: U32
514  for +w3: U32
515  for +w4: U32
516  for +w5: U32
517  for +w6: U32
518  for +w7: U32
519  for +w8: U32
520  for +w9: U32
521  for +w10: U32
522  for +w11: U32
523  for +w12: U32
524  for +w13: U32
525  for +w14: U32
526  for +w15: U32
527  for +w16: U32
528  for pair: Array<U32> & U32
529  {I.read17(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair) == S.gather(14n,index,18,False{},0n,t,h,[w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
530
531def read17_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair):
532  (a,w17) = pair
533  read18_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,Array.get(U32,a,U32.add(index,18)))
534
535law read16_correct:
536  for +index: U32
537  for +t: T.Counter
538  for +h: T.Chain
539  for +w0: U32
540  for +w1: U32
541  for +w2: U32
542  for +w3: U32
543  for +w4: U32
544  for +w5: U32
545  for +w6: U32
546  for +w7: U32
547  for +w8: U32
548  for +w9: U32
549  for +w10: U32
550  for +w11: U32
551  for +w12: U32
552  for +w13: U32
553  for +w14: U32
554  for +w15: U32
555  for pair: Array<U32> & U32
556  {I.read16(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair) == S.gather(15n,index,17,False{},0n,t,h,[w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
557
558def read16_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair):
559  (a,w16) = pair
560  read17_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,Array.get(U32,a,U32.add(index,17)))
561
562law read15_correct:
563  for +index: U32
564  for +t: T.Counter
565  for +h: T.Chain
566  for +w0: U32
567  for +w1: U32
568  for +w2: U32
569  for +w3: U32
570  for +w4: U32
571  for +w5: U32
572  for +w6: U32
573  for +w7: U32
574  for +w8: U32
575  for +w9: U32
576  for +w10: U32
577  for +w11: U32
578  for +w12: U32
579  for +w13: U32
580  for +w14: U32
581  for pair: Array<U32> & U32
582  {I.read15(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == S.gather(16n,index,16,False{},0n,t,h,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
583
584def read15_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
585  (a,w15) = pair
586  read16_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
587
588law read14_correct:
589  for +index: U32
590  for +t: T.Counter
591  for +h: T.Chain
592  for +w0: U32
593  for +w1: U32
594  for +w2: U32
595  for +w3: U32
596  for +w4: U32
597  for +w5: U32
598  for +w6: U32
599  for +w7: U32
600  for +w8: U32
601  for +w9: U32
602  for +w10: U32
603  for +w11: U32
604  for +w12: U32
605  for +w13: U32
606  for pair: Array<U32> & U32
607  {I.read14(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == S.gather(17n,index,15,False{},0n,t,h,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
608
609def read14_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
610  (a,w14) = pair
611  read15_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
612
613law read13_correct:
614  for +index: U32
615  for +t: T.Counter
616  for +h: T.Chain
617  for +w0: U32
618  for +w1: U32
619  for +w2: U32
620  for +w3: U32
621  for +w4: U32
622  for +w5: U32
623  for +w6: U32
624  for +w7: U32
625  for +w8: U32
626  for +w9: U32
627  for +w10: U32
628  for +w11: U32
629  for +w12: U32
630  for pair: Array<U32> & U32
631  {I.read13(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == S.gather(18n,index,14,False{},0n,t,h,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
632
633def read13_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
634  (a,w13) = pair
635  read14_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
636
637law read12_correct:
638  for +index: U32
639  for +t: T.Counter
640  for +h: T.Chain
641  for +w0: U32
642  for +w1: U32
643  for +w2: U32
644  for +w3: U32
645  for +w4: U32
646  for +w5: U32
647  for +w6: U32
648  for +w7: U32
649  for +w8: U32
650  for +w9: U32
651  for +w10: U32
652  for +w11: U32
653  for pair: Array<U32> & U32
654  {I.read12(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == S.gather(19n,index,13,False{},0n,t,h,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
655
656def read12_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
657  (a,w12) = pair
658  read13_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
659
660law read11_correct:
661  for +index: U32
662  for +t: T.Counter
663  for +h: T.Chain
664  for +w0: U32
665  for +w1: U32
666  for +w2: U32
667  for +w3: U32
668  for +w4: U32
669  for +w5: U32
670  for +w6: U32
671  for +w7: U32
672  for +w8: U32
673  for +w9: U32
674  for +w10: U32
675  for pair: Array<U32> & U32
676  {I.read11(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == S.gather(20n,index,12,False{},0n,t,h,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
677
678def read11_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
679  (a,w11) = pair
680  read12_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
681
682law read10_correct:
683  for +index: U32
684  for +t: T.Counter
685  for +h: T.Chain
686  for +w0: U32
687  for +w1: U32
688  for +w2: U32
689  for +w3: U32
690  for +w4: U32
691  for +w5: U32
692  for +w6: U32
693  for +w7: U32
694  for +w8: U32
695  for +w9: U32
696  for pair: Array<U32> & U32
697  {I.read10(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == S.gather(21n,index,11,False{},0n,t,h,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
698
699def read10_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
700  (a,w10) = pair
701  read11_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
702
703law read9_correct:
704  for +index: U32
705  for +t: T.Counter
706  for +h: T.Chain
707  for +w0: U32
708  for +w1: U32
709  for +w2: U32
710  for +w3: U32
711  for +w4: U32
712  for +w5: U32
713  for +w6: U32
714  for +w7: U32
715  for +w8: U32
716  for pair: Array<U32> & U32
717  {I.read9(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == S.gather(22n,index,10,False{},0n,t,h,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
718
719def read9_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
720  (a,w9) = pair
721  read10_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
722
723law read8_correct:
724  for +index: U32
725  for +t: T.Counter
726  for +h: T.Chain
727  for +w0: U32
728  for +w1: U32
729  for +w2: U32
730  for +w3: U32
731  for +w4: U32
732  for +w5: U32
733  for +w6: U32
734  for +w7: U32
735  for pair: Array<U32> & U32
736  {I.read8(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair) == S.gather(23n,index,9,False{},0n,t,h,[w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
737
738def read8_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair):
739  (a,w8) = pair
740  read9_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
741
742law read7_correct:
743  for +index: U32
744  for +t: T.Counter
745  for +h: T.Chain
746  for +w0: U32
747  for +w1: U32
748  for +w2: U32
749  for +w3: U32
750  for +w4: U32
751  for +w5: U32
752  for +w6: U32
753  for pair: Array<U32> & U32
754  {I.read7(index,t,h,w0,w1,w2,w3,w4,w5,w6,pair) == S.gather(24n,index,8,False{},0n,t,h,[w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
755
756def read7_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,pair):
757  (a,w7) = pair
758  read8_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
759
760law read6_correct:
761  for +index: U32
762  for +t: T.Counter
763  for +h: T.Chain
764  for +w0: U32
765  for +w1: U32
766  for +w2: U32
767  for +w3: U32
768  for +w4: U32
769  for +w5: U32
770  for pair: Array<U32> & U32
771  {I.read6(index,t,h,w0,w1,w2,w3,w4,w5,pair) == S.gather(25n,index,7,False{},0n,t,h,[w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
772
773def read6_correct(index,t,h,w0,w1,w2,w3,w4,w5,pair):
774  (a,w6) = pair
775  read7_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
776
777law read5_correct:
778  for +index: U32
779  for +t: T.Counter
780  for +h: T.Chain
781  for +w0: U32
782  for +w1: U32
783  for +w2: U32
784  for +w3: U32
785  for +w4: U32
786  for pair: Array<U32> & U32
787  {I.read5(index,t,h,w0,w1,w2,w3,w4,pair) == S.gather(26n,index,6,False{},0n,t,h,[w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
788
789def read5_correct(index,t,h,w0,w1,w2,w3,w4,pair):
790  (a,w5) = pair
791  read6_correct(index,t,h,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
792
793law read4_correct:
794  for +index: U32
795  for +t: T.Counter
796  for +h: T.Chain
797  for +w0: U32
798  for +w1: U32
799  for +w2: U32
800  for +w3: U32
801  for pair: Array<U32> & U32
802  {I.read4(index,t,h,w0,w1,w2,w3,pair) == S.gather(27n,index,5,False{},0n,t,h,[w3,w2,w1,w0],pair) : Array<U32> & T.Chain}
803
804def read4_correct(index,t,h,w0,w1,w2,w3,pair):
805  (a,w4) = pair
806  read5_correct(index,t,h,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
807
808law read3_correct:
809  for +index: U32
810  for +t: T.Counter
811  for +h: T.Chain
812  for +w0: U32
813  for +w1: U32
814  for +w2: U32
815  for pair: Array<U32> & U32
816  {I.read3(index,t,h,w0,w1,w2,pair) == S.gather(28n,index,4,False{},0n,t,h,[w2,w1,w0],pair) : Array<U32> & T.Chain}
817
818def read3_correct(index,t,h,w0,w1,w2,pair):
819  (a,w3) = pair
820  read4_correct(index,t,h,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
821
822law read2_correct:
823  for +index: U32
824  for +t: T.Counter
825  for +h: T.Chain
826  for +w0: U32
827  for +w1: U32
828  for pair: Array<U32> & U32
829  {I.read2(index,t,h,w0,w1,pair) == S.gather(29n,index,3,False{},0n,t,h,[w1,w0],pair) : Array<U32> & T.Chain}
830
831def read2_correct(index,t,h,w0,w1,pair):
832  (a,w2) = pair
833  read3_correct(index,t,h,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
834
835law read1_correct:
836  for +index: U32
837  for +t: T.Counter
838  for +h: T.Chain
839  for +w0: U32
840  for pair: Array<U32> & U32
841  {I.read1(index,t,h,w0,pair) == S.gather(30n,index,2,False{},0n,t,h,[w0],pair) : Array<U32> & T.Chain}
842
843def read1_correct(index,t,h,w0,pair):
844  (a,w1) = pair
845  read2_correct(index,t,h,w0,w1,Array.get(U32,a,U32.add(index,2)))
846
847law read0_correct:
848  for +index: U32
849  for +t: T.Counter
850  for +h: T.Chain
851  for pair: Array<U32> & U32
852  {I.read0(index,t,h,pair) == S.gather(31n,index,1,False{},0n,t,h,[],pair) : Array<U32> & T.Chain}
853
854def read0_correct(index,t,h,pair):
855  (a,w0) = pair
856  read1_correct(index,t,h,w0,Array.get(U32,a,U32.add(index,1)))
857
858law absorb_correct:
859  for a: Array<U32>
860  for +index: U32
861  for +t: T.Counter
862  for +h: T.Chain
863  {I.absorb(a,index,t,h) == S.absorb(a,index,t,h) : Array<U32> & T.Chain}
864
865def absorb_correct(a,index,t,h):
866  read0_correct(index,t,h,Array.get(U32,a,index))
867
868law keep_correct:
869  for +w: U32
870  for +n: Nat
871  {I.keep(w,n) == S.keep(w,n) : U32}
872
873def keep_correct(w,n):
874  match n:
875    case 0n: {==}
876    case 1n: {==}
877    case 2n: {==}
878    case 3n: {==}
879    case 4n+p: {==}
880
881law masks_correct:
882  for +remain: Nat
883  for +w0: U32
884  for +w1: U32
885  for +w2: U32
886  for +w3: U32
887  for +w4: U32
888  for +w5: U32
889  for +w6: U32
890  for +w7: U32
891  for +w8: U32
892  for +w9: U32
893  for +w10: U32
894  for +w11: U32
895  for +w12: U32
896  for +w13: U32
897  for +w14: U32
898  for +w15: U32
899  for +w16: U32
900  for +w17: U32
901  for +w18: U32
902  for +w19: U32
903  for +w20: U32
904  for +w21: U32
905  for +w22: U32
906  for +w23: U32
907  for +w24: U32
908  for +w25: U32
909  for +w26: U32
910  for +w27: U32
911  for +w28: U32
912  for +w29: U32
913  for +w30: U32
914  for +w31: U32
915  {[I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
916
917def masks_correct(remain,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31):
918  %Equal.sym(U32,I.mask(w0,0n,remain),S.mask(w0,0n,remain),keep_correct(w0,Nat.sub(remain,0n))) : {[_,I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
919  %Equal.sym(U32,I.mask(w1,4n,remain),S.mask(w1,4n,remain),keep_correct(w1,Nat.sub(remain,4n))) : {[S.mask(w0,0n,remain),_,I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
920  %Equal.sym(U32,I.mask(w2,8n,remain),S.mask(w2,8n,remain),keep_correct(w2,Nat.sub(remain,8n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),_,I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
921  %Equal.sym(U32,I.mask(w3,12n,remain),S.mask(w3,12n,remain),keep_correct(w3,Nat.sub(remain,12n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),_,I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
922  %Equal.sym(U32,I.mask(w4,16n,remain),S.mask(w4,16n,remain),keep_correct(w4,Nat.sub(remain,16n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),_,I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
923  %Equal.sym(U32,I.mask(w5,20n,remain),S.mask(w5,20n,remain),keep_correct(w5,Nat.sub(remain,20n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),_,I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
924  %Equal.sym(U32,I.mask(w6,24n,remain),S.mask(w6,24n,remain),keep_correct(w6,Nat.sub(remain,24n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),_,I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
925  %Equal.sym(U32,I.mask(w7,28n,remain),S.mask(w7,28n,remain),keep_correct(w7,Nat.sub(remain,28n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),_,I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
926  %Equal.sym(U32,I.mask(w8,32n,remain),S.mask(w8,32n,remain),keep_correct(w8,Nat.sub(remain,32n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),_,I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
927  %Equal.sym(U32,I.mask(w9,36n,remain),S.mask(w9,36n,remain),keep_correct(w9,Nat.sub(remain,36n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),_,I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
928  %Equal.sym(U32,I.mask(w10,40n,remain),S.mask(w10,40n,remain),keep_correct(w10,Nat.sub(remain,40n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),_,I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
929  %Equal.sym(U32,I.mask(w11,44n,remain),S.mask(w11,44n,remain),keep_correct(w11,Nat.sub(remain,44n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),_,I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
930  %Equal.sym(U32,I.mask(w12,48n,remain),S.mask(w12,48n,remain),keep_correct(w12,Nat.sub(remain,48n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),_,I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
931  %Equal.sym(U32,I.mask(w13,52n,remain),S.mask(w13,52n,remain),keep_correct(w13,Nat.sub(remain,52n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),_,I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
932  %Equal.sym(U32,I.mask(w14,56n,remain),S.mask(w14,56n,remain),keep_correct(w14,Nat.sub(remain,56n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),_,I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
933  %Equal.sym(U32,I.mask(w15,60n,remain),S.mask(w15,60n,remain),keep_correct(w15,Nat.sub(remain,60n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),_,I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
934  %Equal.sym(U32,I.mask(w16,64n,remain),S.mask(w16,64n,remain),keep_correct(w16,Nat.sub(remain,64n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),_,I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
935  %Equal.sym(U32,I.mask(w17,68n,remain),S.mask(w17,68n,remain),keep_correct(w17,Nat.sub(remain,68n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),_,I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
936  %Equal.sym(U32,I.mask(w18,72n,remain),S.mask(w18,72n,remain),keep_correct(w18,Nat.sub(remain,72n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),_,I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
937  %Equal.sym(U32,I.mask(w19,76n,remain),S.mask(w19,76n,remain),keep_correct(w19,Nat.sub(remain,76n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),_,I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
938  %Equal.sym(U32,I.mask(w20,80n,remain),S.mask(w20,80n,remain),keep_correct(w20,Nat.sub(remain,80n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),_,I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
939  %Equal.sym(U32,I.mask(w21,84n,remain),S.mask(w21,84n,remain),keep_correct(w21,Nat.sub(remain,84n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),_,I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
940  %Equal.sym(U32,I.mask(w22,88n,remain),S.mask(w22,88n,remain),keep_correct(w22,Nat.sub(remain,88n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),_,I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
941  %Equal.sym(U32,I.mask(w23,92n,remain),S.mask(w23,92n,remain),keep_correct(w23,Nat.sub(remain,92n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),_,I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
942  %Equal.sym(U32,I.mask(w24,96n,remain),S.mask(w24,96n,remain),keep_correct(w24,Nat.sub(remain,96n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),_,I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
943  %Equal.sym(U32,I.mask(w25,100n,remain),S.mask(w25,100n,remain),keep_correct(w25,Nat.sub(remain,100n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),_,I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
944  %Equal.sym(U32,I.mask(w26,104n,remain),S.mask(w26,104n,remain),keep_correct(w26,Nat.sub(remain,104n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),_,I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
945  %Equal.sym(U32,I.mask(w27,108n,remain),S.mask(w27,108n,remain),keep_correct(w27,Nat.sub(remain,108n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),_,I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
946  %Equal.sym(U32,I.mask(w28,112n,remain),S.mask(w28,112n,remain),keep_correct(w28,Nat.sub(remain,112n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),_,I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
947  %Equal.sym(U32,I.mask(w29,116n,remain),S.mask(w29,116n,remain),keep_correct(w29,Nat.sub(remain,116n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),S.mask(w28,112n,remain),_,I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
948  %Equal.sym(U32,I.mask(w30,120n,remain),S.mask(w30,120n,remain),keep_correct(w30,Nat.sub(remain,120n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),S.mask(w28,112n,remain),S.mask(w29,116n,remain),_,I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
949  %Equal.sym(U32,I.mask(w31,124n,remain),S.mask(w31,124n,remain),keep_correct(w31,Nat.sub(remain,124n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),S.mask(w28,112n,remain),S.mask(w29,116n,remain),S.mask(w30,120n,remain),_] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}
950  {==}
951
952law last31_correct:
953  for +remain: Nat
954  for +index: U32
955  for +t: T.Counter
956  for +h: T.Chain
957  for +w0: U32
958  for +w1: U32
959  for +w2: U32
960  for +w3: U32
961  for +w4: U32
962  for +w5: U32
963  for +w6: U32
964  for +w7: U32
965  for +w8: U32
966  for +w9: U32
967  for +w10: U32
968  for +w11: U32
969  for +w12: U32
970  for +w13: U32
971  for +w14: U32
972  for +w15: U32
973  for +w16: U32
974  for +w17: U32
975  for +w18: U32
976  for +w19: U32
977  for +w20: U32
978  for +w21: U32
979  for +w22: U32
980  for +w23: U32
981  for +w24: U32
982  for +w25: U32
983  for +w26: U32
984  for +w27: U32
985  for +w28: U32
986  for +w29: U32
987  for +w30: U32
988  for pair: Array<U32> & U32
989  {I.last31(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(0n,index,32,True{},remain,t,h,[w30,w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
990
991def last31_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair):
992  (a,+w31) = pair
993  Equal.trans(T.Chain,F.compress_last(h,t,I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)),S.compress(h,[T.W{I.mask(w0,0n,remain),I.mask(w1,4n,remain)},T.W{I.mask(w2,8n,remain),I.mask(w3,12n,remain)},T.W{I.mask(w4,16n,remain),I.mask(w5,20n,remain)},T.W{I.mask(w6,24n,remain),I.mask(w7,28n,remain)},T.W{I.mask(w8,32n,remain),I.mask(w9,36n,remain)},T.W{I.mask(w10,40n,remain),I.mask(w11,44n,remain)},T.W{I.mask(w12,48n,remain),I.mask(w13,52n,remain)},T.W{I.mask(w14,56n,remain),I.mask(w15,60n,remain)},T.W{I.mask(w16,64n,remain),I.mask(w17,68n,remain)},T.W{I.mask(w18,72n,remain),I.mask(w19,76n,remain)},T.W{I.mask(w20,80n,remain),I.mask(w21,84n,remain)},T.W{I.mask(w22,88n,remain),I.mask(w23,92n,remain)},T.W{I.mask(w24,96n,remain),I.mask(w25,100n,remain)},T.W{I.mask(w26,104n,remain),I.mask(w27,108n,remain)},T.W{I.mask(w28,112n,remain),I.mask(w29,116n,remain)},T.W{I.mask(w30,120n,remain),I.mask(w31,124n,remain)}],t,True{}),S.compress(h,S.lanes(S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain)),t,True{}),
994    C.compress_last_correct(h,t,I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)),
995    Equal.cong(List<&2,U32>,T.Chain,x => S.compress(h,S.lanes(x),t,True{}),[I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)],S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain),masks_correct(remain,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31)))
996
997law last30_correct:
998  for +remain: Nat
999  for +index: U32
1000  for +t: T.Counter
1001  for +h: T.Chain
1002  for +w0: U32
1003  for +w1: U32
1004  for +w2: U32
1005  for +w3: U32
1006  for +w4: U32
1007  for +w5: U32
1008  for +w6: U32
1009  for +w7: U32
1010  for +w8: U32
1011  for +w9: U32
1012  for +w10: U32
1013  for +w11: U32
1014  for +w12: U32
1015  for +w13: U32
1016  for +w14: U32
1017  for +w15: U32
1018  for +w16: U32
1019  for +w17: U32
1020  for +w18: U32
1021  for +w19: U32
1022  for +w20: U32
1023  for +w21: U32
1024  for +w22: U32
1025  for +w23: U32
1026  for +w24: U32
1027  for +w25: U32
1028  for +w26: U32
1029  for +w27: U32
1030  for +w28: U32
1031  for +w29: U32
1032  for pair: Array<U32> & U32
1033  {I.last30(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(1n,index,31,True{},remain,t,h,[w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1034
1035def last30_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair):
1036  (a,+w30) = pair
1037  last31_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,Array.get(U32,a,U32.add(index,31)))
1038
1039law last29_correct:
1040  for +remain: Nat
1041  for +index: U32
1042  for +t: T.Counter
1043  for +h: T.Chain
1044  for +w0: U32
1045  for +w1: U32
1046  for +w2: U32
1047  for +w3: U32
1048  for +w4: U32
1049  for +w5: U32
1050  for +w6: U32
1051  for +w7: U32
1052  for +w8: U32
1053  for +w9: U32
1054  for +w10: U32
1055  for +w11: U32
1056  for +w12: U32
1057  for +w13: U32
1058  for +w14: U32
1059  for +w15: U32
1060  for +w16: U32
1061  for +w17: U32
1062  for +w18: U32
1063  for +w19: U32
1064  for +w20: U32
1065  for +w21: U32
1066  for +w22: U32
1067  for +w23: U32
1068  for +w24: U32
1069  for +w25: U32
1070  for +w26: U32
1071  for +w27: U32
1072  for +w28: U32
1073  for pair: Array<U32> & U32
1074  {I.last29(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(2n,index,30,True{},remain,t,h,[w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1075
1076def last29_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair):
1077  (a,+w29) = pair
1078  last30_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,Array.get(U32,a,U32.add(index,30)))
1079
1080law last28_correct:
1081  for +remain: Nat
1082  for +index: U32
1083  for +t: T.Counter
1084  for +h: T.Chain
1085  for +w0: U32
1086  for +w1: U32
1087  for +w2: U32
1088  for +w3: U32
1089  for +w4: U32
1090  for +w5: U32
1091  for +w6: U32
1092  for +w7: U32
1093  for +w8: U32
1094  for +w9: U32
1095  for +w10: U32
1096  for +w11: U32
1097  for +w12: U32
1098  for +w13: U32
1099  for +w14: U32
1100  for +w15: U32
1101  for +w16: U32
1102  for +w17: U32
1103  for +w18: U32
1104  for +w19: U32
1105  for +w20: U32
1106  for +w21: U32
1107  for +w22: U32
1108  for +w23: U32
1109  for +w24: U32
1110  for +w25: U32
1111  for +w26: U32
1112  for +w27: U32
1113  for pair: Array<U32> & U32
1114  {I.last28(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(3n,index,29,True{},remain,t,h,[w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1115
1116def last28_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair):
1117  (a,+w28) = pair
1118  last29_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,Array.get(U32,a,U32.add(index,29)))
1119
1120law last27_correct:
1121  for +remain: Nat
1122  for +index: U32
1123  for +t: T.Counter
1124  for +h: T.Chain
1125  for +w0: U32
1126  for +w1: U32
1127  for +w2: U32
1128  for +w3: U32
1129  for +w4: U32
1130  for +w5: U32
1131  for +w6: U32
1132  for +w7: U32
1133  for +w8: U32
1134  for +w9: U32
1135  for +w10: U32
1136  for +w11: U32
1137  for +w12: U32
1138  for +w13: U32
1139  for +w14: U32
1140  for +w15: U32
1141  for +w16: U32
1142  for +w17: U32
1143  for +w18: U32
1144  for +w19: U32
1145  for +w20: U32
1146  for +w21: U32
1147  for +w22: U32
1148  for +w23: U32
1149  for +w24: U32
1150  for +w25: U32
1151  for +w26: U32
1152  for pair: Array<U32> & U32
1153  {I.last27(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(4n,index,28,True{},remain,t,h,[w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1154
1155def last27_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair):
1156  (a,+w27) = pair
1157  last28_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,Array.get(U32,a,U32.add(index,28)))
1158
1159law last26_correct:
1160  for +remain: Nat
1161  for +index: U32
1162  for +t: T.Counter
1163  for +h: T.Chain
1164  for +w0: U32
1165  for +w1: U32
1166  for +w2: U32
1167  for +w3: U32
1168  for +w4: U32
1169  for +w5: U32
1170  for +w6: U32
1171  for +w7: U32
1172  for +w8: U32
1173  for +w9: U32
1174  for +w10: U32
1175  for +w11: U32
1176  for +w12: U32
1177  for +w13: U32
1178  for +w14: U32
1179  for +w15: U32
1180  for +w16: U32
1181  for +w17: U32
1182  for +w18: U32
1183  for +w19: U32
1184  for +w20: U32
1185  for +w21: U32
1186  for +w22: U32
1187  for +w23: U32
1188  for +w24: U32
1189  for +w25: U32
1190  for pair: Array<U32> & U32
1191  {I.last26(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(5n,index,27,True{},remain,t,h,[w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1192
1193def last26_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair):
1194  (a,+w26) = pair
1195  last27_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,Array.get(U32,a,U32.add(index,27)))
1196
1197law last25_correct:
1198  for +remain: Nat
1199  for +index: U32
1200  for +t: T.Counter
1201  for +h: T.Chain
1202  for +w0: U32
1203  for +w1: U32
1204  for +w2: U32
1205  for +w3: U32
1206  for +w4: U32
1207  for +w5: U32
1208  for +w6: U32
1209  for +w7: U32
1210  for +w8: U32
1211  for +w9: U32
1212  for +w10: U32
1213  for +w11: U32
1214  for +w12: U32
1215  for +w13: U32
1216  for +w14: U32
1217  for +w15: U32
1218  for +w16: U32
1219  for +w17: U32
1220  for +w18: U32
1221  for +w19: U32
1222  for +w20: U32
1223  for +w21: U32
1224  for +w22: U32
1225  for +w23: U32
1226  for +w24: U32
1227  for pair: Array<U32> & U32
1228  {I.last25(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(6n,index,26,True{},remain,t,h,[w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1229
1230def last25_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair):
1231  (a,+w25) = pair
1232  last26_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,Array.get(U32,a,U32.add(index,26)))
1233
1234law last24_correct:
1235  for +remain: Nat
1236  for +index: U32
1237  for +t: T.Counter
1238  for +h: T.Chain
1239  for +w0: U32
1240  for +w1: U32
1241  for +w2: U32
1242  for +w3: U32
1243  for +w4: U32
1244  for +w5: U32
1245  for +w6: U32
1246  for +w7: U32
1247  for +w8: U32
1248  for +w9: U32
1249  for +w10: U32
1250  for +w11: U32
1251  for +w12: U32
1252  for +w13: U32
1253  for +w14: U32
1254  for +w15: U32
1255  for +w16: U32
1256  for +w17: U32
1257  for +w18: U32
1258  for +w19: U32
1259  for +w20: U32
1260  for +w21: U32
1261  for +w22: U32
1262  for +w23: U32
1263  for pair: Array<U32> & U32
1264  {I.last24(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(7n,index,25,True{},remain,t,h,[w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1265
1266def last24_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair):
1267  (a,+w24) = pair
1268  last25_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,Array.get(U32,a,U32.add(index,25)))
1269
1270law last23_correct:
1271  for +remain: Nat
1272  for +index: U32
1273  for +t: T.Counter
1274  for +h: T.Chain
1275  for +w0: U32
1276  for +w1: U32
1277  for +w2: U32
1278  for +w3: U32
1279  for +w4: U32
1280  for +w5: U32
1281  for +w6: U32
1282  for +w7: U32
1283  for +w8: U32
1284  for +w9: U32
1285  for +w10: U32
1286  for +w11: U32
1287  for +w12: U32
1288  for +w13: U32
1289  for +w14: U32
1290  for +w15: U32
1291  for +w16: U32
1292  for +w17: U32
1293  for +w18: U32
1294  for +w19: U32
1295  for +w20: U32
1296  for +w21: U32
1297  for +w22: U32
1298  for pair: Array<U32> & U32
1299  {I.last23(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(8n,index,24,True{},remain,t,h,[w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1300
1301def last23_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair):
1302  (a,+w23) = pair
1303  last24_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,Array.get(U32,a,U32.add(index,24)))
1304
1305law last22_correct:
1306  for +remain: Nat
1307  for +index: U32
1308  for +t: T.Counter
1309  for +h: T.Chain
1310  for +w0: U32
1311  for +w1: U32
1312  for +w2: U32
1313  for +w3: U32
1314  for +w4: U32
1315  for +w5: U32
1316  for +w6: U32
1317  for +w7: U32
1318  for +w8: U32
1319  for +w9: U32
1320  for +w10: U32
1321  for +w11: U32
1322  for +w12: U32
1323  for +w13: U32
1324  for +w14: U32
1325  for +w15: U32
1326  for +w16: U32
1327  for +w17: U32
1328  for +w18: U32
1329  for +w19: U32
1330  for +w20: U32
1331  for +w21: U32
1332  for pair: Array<U32> & U32
1333  {I.last22(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(9n,index,23,True{},remain,t,h,[w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1334
1335def last22_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair):
1336  (a,+w22) = pair
1337  last23_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,Array.get(U32,a,U32.add(index,23)))
1338
1339law last21_correct:
1340  for +remain: Nat
1341  for +index: U32
1342  for +t: T.Counter
1343  for +h: T.Chain
1344  for +w0: U32
1345  for +w1: U32
1346  for +w2: U32
1347  for +w3: U32
1348  for +w4: U32
1349  for +w5: U32
1350  for +w6: U32
1351  for +w7: U32
1352  for +w8: U32
1353  for +w9: U32
1354  for +w10: U32
1355  for +w11: U32
1356  for +w12: U32
1357  for +w13: U32
1358  for +w14: U32
1359  for +w15: U32
1360  for +w16: U32
1361  for +w17: U32
1362  for +w18: U32
1363  for +w19: U32
1364  for +w20: U32
1365  for pair: Array<U32> & U32
1366  {I.last21(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(10n,index,22,True{},remain,t,h,[w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1367
1368def last21_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair):
1369  (a,+w21) = pair
1370  last22_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,Array.get(U32,a,U32.add(index,22)))
1371
1372law last20_correct:
1373  for +remain: Nat
1374  for +index: U32
1375  for +t: T.Counter
1376  for +h: T.Chain
1377  for +w0: U32
1378  for +w1: U32
1379  for +w2: U32
1380  for +w3: U32
1381  for +w4: U32
1382  for +w5: U32
1383  for +w6: U32
1384  for +w7: U32
1385  for +w8: U32
1386  for +w9: U32
1387  for +w10: U32
1388  for +w11: U32
1389  for +w12: U32
1390  for +w13: U32
1391  for +w14: U32
1392  for +w15: U32
1393  for +w16: U32
1394  for +w17: U32
1395  for +w18: U32
1396  for +w19: U32
1397  for pair: Array<U32> & U32
1398  {I.last20(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(11n,index,21,True{},remain,t,h,[w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1399
1400def last20_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair):
1401  (a,+w20) = pair
1402  last21_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,Array.get(U32,a,U32.add(index,21)))
1403
1404law last19_correct:
1405  for +remain: Nat
1406  for +index: U32
1407  for +t: T.Counter
1408  for +h: T.Chain
1409  for +w0: U32
1410  for +w1: U32
1411  for +w2: U32
1412  for +w3: U32
1413  for +w4: U32
1414  for +w5: U32
1415  for +w6: U32
1416  for +w7: U32
1417  for +w8: U32
1418  for +w9: U32
1419  for +w10: U32
1420  for +w11: U32
1421  for +w12: U32
1422  for +w13: U32
1423  for +w14: U32
1424  for +w15: U32
1425  for +w16: U32
1426  for +w17: U32
1427  for +w18: U32
1428  for pair: Array<U32> & U32
1429  {I.last19(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(12n,index,20,True{},remain,t,h,[w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1430
1431def last19_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair):
1432  (a,+w19) = pair
1433  last20_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,Array.get(U32,a,U32.add(index,20)))
1434
1435law last18_correct:
1436  for +remain: Nat
1437  for +index: U32
1438  for +t: T.Counter
1439  for +h: T.Chain
1440  for +w0: U32
1441  for +w1: U32
1442  for +w2: U32
1443  for +w3: U32
1444  for +w4: U32
1445  for +w5: U32
1446  for +w6: U32
1447  for +w7: U32
1448  for +w8: U32
1449  for +w9: U32
1450  for +w10: U32
1451  for +w11: U32
1452  for +w12: U32
1453  for +w13: U32
1454  for +w14: U32
1455  for +w15: U32
1456  for +w16: U32
1457  for +w17: U32
1458  for pair: Array<U32> & U32
1459  {I.last18(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(13n,index,19,True{},remain,t,h,[w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1460
1461def last18_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair):
1462  (a,+w18) = pair
1463  last19_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,Array.get(U32,a,U32.add(index,19)))
1464
1465law last17_correct:
1466  for +remain: Nat
1467  for +index: U32
1468  for +t: T.Counter
1469  for +h: T.Chain
1470  for +w0: U32
1471  for +w1: U32
1472  for +w2: U32
1473  for +w3: U32
1474  for +w4: U32
1475  for +w5: U32
1476  for +w6: U32
1477  for +w7: U32
1478  for +w8: U32
1479  for +w9: U32
1480  for +w10: U32
1481  for +w11: U32
1482  for +w12: U32
1483  for +w13: U32
1484  for +w14: U32
1485  for +w15: U32
1486  for +w16: U32
1487  for pair: Array<U32> & U32
1488  {I.last17(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(14n,index,18,True{},remain,t,h,[w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1489
1490def last17_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair):
1491  (a,+w17) = pair
1492  last18_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,Array.get(U32,a,U32.add(index,18)))
1493
1494law last16_correct:
1495  for +remain: Nat
1496  for +index: U32
1497  for +t: T.Counter
1498  for +h: T.Chain
1499  for +w0: U32
1500  for +w1: U32
1501  for +w2: U32
1502  for +w3: U32
1503  for +w4: U32
1504  for +w5: U32
1505  for +w6: U32
1506  for +w7: U32
1507  for +w8: U32
1508  for +w9: U32
1509  for +w10: U32
1510  for +w11: U32
1511  for +w12: U32
1512  for +w13: U32
1513  for +w14: U32
1514  for +w15: U32
1515  for pair: Array<U32> & U32
1516  {I.last16(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(15n,index,17,True{},remain,t,h,[w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1517
1518def last16_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair):
1519  (a,+w16) = pair
1520  last17_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,Array.get(U32,a,U32.add(index,17)))
1521
1522law last15_correct:
1523  for +remain: Nat
1524  for +index: U32
1525  for +t: T.Counter
1526  for +h: T.Chain
1527  for +w0: U32
1528  for +w1: U32
1529  for +w2: U32
1530  for +w3: U32
1531  for +w4: U32
1532  for +w5: U32
1533  for +w6: U32
1534  for +w7: U32
1535  for +w8: U32
1536  for +w9: U32
1537  for +w10: U32
1538  for +w11: U32
1539  for +w12: U32
1540  for +w13: U32
1541  for +w14: U32
1542  for pair: Array<U32> & U32
1543  {I.last15(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(16n,index,16,True{},remain,t,h,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1544
1545def last15_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
1546  (a,+w15) = pair
1547  last16_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
1548
1549law last14_correct:
1550  for +remain: Nat
1551  for +index: U32
1552  for +t: T.Counter
1553  for +h: T.Chain
1554  for +w0: U32
1555  for +w1: U32
1556  for +w2: U32
1557  for +w3: U32
1558  for +w4: U32
1559  for +w5: U32
1560  for +w6: U32
1561  for +w7: U32
1562  for +w8: U32
1563  for +w9: U32
1564  for +w10: U32
1565  for +w11: U32
1566  for +w12: U32
1567  for +w13: U32
1568  for pair: Array<U32> & U32
1569  {I.last14(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(17n,index,15,True{},remain,t,h,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1570
1571def last14_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
1572  (a,+w14) = pair
1573  last15_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
1574
1575law last13_correct:
1576  for +remain: Nat
1577  for +index: U32
1578  for +t: T.Counter
1579  for +h: T.Chain
1580  for +w0: U32
1581  for +w1: U32
1582  for +w2: U32
1583  for +w3: U32
1584  for +w4: U32
1585  for +w5: U32
1586  for +w6: U32
1587  for +w7: U32
1588  for +w8: U32
1589  for +w9: U32
1590  for +w10: U32
1591  for +w11: U32
1592  for +w12: U32
1593  for pair: Array<U32> & U32
1594  {I.last13(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(18n,index,14,True{},remain,t,h,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1595
1596def last13_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
1597  (a,+w13) = pair
1598  last14_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
1599
1600law last12_correct:
1601  for +remain: Nat
1602  for +index: U32
1603  for +t: T.Counter
1604  for +h: T.Chain
1605  for +w0: U32
1606  for +w1: U32
1607  for +w2: U32
1608  for +w3: U32
1609  for +w4: U32
1610  for +w5: U32
1611  for +w6: U32
1612  for +w7: U32
1613  for +w8: U32
1614  for +w9: U32
1615  for +w10: U32
1616  for +w11: U32
1617  for pair: Array<U32> & U32
1618  {I.last12(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(19n,index,13,True{},remain,t,h,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1619
1620def last12_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
1621  (a,+w12) = pair
1622  last13_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
1623
1624law last11_correct:
1625  for +remain: Nat
1626  for +index: U32
1627  for +t: T.Counter
1628  for +h: T.Chain
1629  for +w0: U32
1630  for +w1: U32
1631  for +w2: U32
1632  for +w3: U32
1633  for +w4: U32
1634  for +w5: U32
1635  for +w6: U32
1636  for +w7: U32
1637  for +w8: U32
1638  for +w9: U32
1639  for +w10: U32
1640  for pair: Array<U32> & U32
1641  {I.last11(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(20n,index,12,True{},remain,t,h,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1642
1643def last11_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
1644  (a,+w11) = pair
1645  last12_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
1646
1647law last10_correct:
1648  for +remain: Nat
1649  for +index: U32
1650  for +t: T.Counter
1651  for +h: T.Chain
1652  for +w0: U32
1653  for +w1: U32
1654  for +w2: U32
1655  for +w3: U32
1656  for +w4: U32
1657  for +w5: U32
1658  for +w6: U32
1659  for +w7: U32
1660  for +w8: U32
1661  for +w9: U32
1662  for pair: Array<U32> & U32
1663  {I.last10(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(21n,index,11,True{},remain,t,h,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1664
1665def last10_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
1666  (a,+w10) = pair
1667  last11_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
1668
1669law last9_correct:
1670  for +remain: Nat
1671  for +index: U32
1672  for +t: T.Counter
1673  for +h: T.Chain
1674  for +w0: U32
1675  for +w1: U32
1676  for +w2: U32
1677  for +w3: U32
1678  for +w4: U32
1679  for +w5: U32
1680  for +w6: U32
1681  for +w7: U32
1682  for +w8: U32
1683  for pair: Array<U32> & U32
1684  {I.last9(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(22n,index,10,True{},remain,t,h,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1685
1686def last9_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
1687  (a,+w9) = pair
1688  last10_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
1689
1690law last8_correct:
1691  for +remain: Nat
1692  for +index: U32
1693  for +t: T.Counter
1694  for +h: T.Chain
1695  for +w0: U32
1696  for +w1: U32
1697  for +w2: U32
1698  for +w3: U32
1699  for +w4: U32
1700  for +w5: U32
1701  for +w6: U32
1702  for +w7: U32
1703  for pair: Array<U32> & U32
1704  {I.last8(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(23n,index,9,True{},remain,t,h,[w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1705
1706def last8_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair):
1707  (a,+w8) = pair
1708  last9_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
1709
1710law last7_correct:
1711  for +remain: Nat
1712  for +index: U32
1713  for +t: T.Counter
1714  for +h: T.Chain
1715  for +w0: U32
1716  for +w1: U32
1717  for +w2: U32
1718  for +w3: U32
1719  for +w4: U32
1720  for +w5: U32
1721  for +w6: U32
1722  for pair: Array<U32> & U32
1723  {I.last7(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(24n,index,8,True{},remain,t,h,[w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1724
1725def last7_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,pair):
1726  (a,+w7) = pair
1727  last8_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
1728
1729law last6_correct:
1730  for +remain: Nat
1731  for +index: U32
1732  for +t: T.Counter
1733  for +h: T.Chain
1734  for +w0: U32
1735  for +w1: U32
1736  for +w2: U32
1737  for +w3: U32
1738  for +w4: U32
1739  for +w5: U32
1740  for pair: Array<U32> & U32
1741  {I.last6(remain,index,t,h,w0,w1,w2,w3,w4,w5,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(25n,index,7,True{},remain,t,h,[w5,w4,w3,w2,w1,w0],pair)) : T.Chain}
1742
1743def last6_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,pair):
1744  (a,+w6) = pair
1745  last7_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
1746
1747law last5_correct:
1748  for +remain: Nat
1749  for +index: U32
1750  for +t: T.Counter
1751  for +h: T.Chain
1752  for +w0: U32
1753  for +w1: U32
1754  for +w2: U32
1755  for +w3: U32
1756  for +w4: U32
1757  for pair: Array<U32> & U32
1758  {I.last5(remain,index,t,h,w0,w1,w2,w3,w4,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(26n,index,6,True{},remain,t,h,[w4,w3,w2,w1,w0],pair)) : T.Chain}
1759
1760def last5_correct(remain,index,t,h,w0,w1,w2,w3,w4,pair):
1761  (a,+w5) = pair
1762  last6_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
1763
1764law last4_correct:
1765  for +remain: Nat
1766  for +index: U32
1767  for +t: T.Counter
1768  for +h: T.Chain
1769  for +w0: U32
1770  for +w1: U32
1771  for +w2: U32
1772  for +w3: U32
1773  for pair: Array<U32> & U32
1774  {I.last4(remain,index,t,h,w0,w1,w2,w3,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(27n,index,5,True{},remain,t,h,[w3,w2,w1,w0],pair)) : T.Chain}
1775
1776def last4_correct(remain,index,t,h,w0,w1,w2,w3,pair):
1777  (a,+w4) = pair
1778  last5_correct(remain,index,t,h,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
1779
1780law last3_correct:
1781  for +remain: Nat
1782  for +index: U32
1783  for +t: T.Counter
1784  for +h: T.Chain
1785  for +w0: U32
1786  for +w1: U32
1787  for +w2: U32
1788  for pair: Array<U32> & U32
1789  {I.last3(remain,index,t,h,w0,w1,w2,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(28n,index,4,True{},remain,t,h,[w2,w1,w0],pair)) : T.Chain}
1790
1791def last3_correct(remain,index,t,h,w0,w1,w2,pair):
1792  (a,+w3) = pair
1793  last4_correct(remain,index,t,h,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
1794
1795law last2_correct:
1796  for +remain: Nat
1797  for +index: U32
1798  for +t: T.Counter
1799  for +h: T.Chain
1800  for +w0: U32
1801  for +w1: U32
1802  for pair: Array<U32> & U32
1803  {I.last2(remain,index,t,h,w0,w1,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(29n,index,3,True{},remain,t,h,[w1,w0],pair)) : T.Chain}
1804
1805def last2_correct(remain,index,t,h,w0,w1,pair):
1806  (a,+w2) = pair
1807  last3_correct(remain,index,t,h,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
1808
1809law last1_correct:
1810  for +remain: Nat
1811  for +index: U32
1812  for +t: T.Counter
1813  for +h: T.Chain
1814  for +w0: U32
1815  for pair: Array<U32> & U32
1816  {I.last1(remain,index,t,h,w0,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(30n,index,2,True{},remain,t,h,[w0],pair)) : T.Chain}
1817
1818def last1_correct(remain,index,t,h,w0,pair):
1819  (a,+w1) = pair
1820  last2_correct(remain,index,t,h,w0,w1,Array.get(U32,a,U32.add(index,2)))
1821
1822law last0_correct:
1823  for +remain: Nat
1824  for +index: U32
1825  for +t: T.Counter
1826  for +h: T.Chain
1827  for pair: Array<U32> & U32
1828  {I.last0(remain,index,t,h,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(31n,index,1,True{},remain,t,h,[],pair)) : T.Chain}
1829
1830def last0_correct(remain,index,t,h,pair):
1831  (a,+w0) = pair
1832  last1_correct(remain,index,t,h,w0,Array.get(U32,a,U32.add(index,1)))
1833
1834law final_correct:
1835  for a: Array<U32>
1836  for +index: U32
1837  for +remain: Nat
1838  for +t: T.Counter
1839  for +h: T.Chain
1840  {I.final(a,index,remain,t,h) == S.final(a,index,remain,t,h) : T.Chain}
1841
1842def final_correct(a,index,remain,t,h):
1843  %Equal.sym(T.Counter,F.bump(t,U32.from_nat(remain)),S.advance(t,U32.from_nat(remain)),C.bump_correct(t,U32.from_nat(remain))) : {I.last0(remain,index,_,h,Array.get(U32,a,index)) == S.final(a,index,remain,t,h) : T.Chain}
1844  last0_correct(remain,index,S.advance(t,U32.from_nat(remain)),h,Array.get(U32,a,index))
1845
1846law blocks_step:
1847  for +n: Nat
1848  for +index: U32
1849  for +remain: Nat
1850  for +t: T.Counter
1851  for -a: Array<U32>
1852  for +h: T.Chain
1853  for view: Sigma<&2,&1,A.Tree,z => {a == A.thaw(z) : Array<U32>}>
1854  for recurse: @pair: (Array<U32> & T.Chain) -> {I.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair) == S.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair) : T.Chain}
1855  {I.blocks(1n+n,index,remain,t,(a,h)) == S.blocks(1n+n,index,remain,t,(a,h)) : T.Chain}
1856
1857def blocks_step(n,index,remain,t,a,h,view,recurse):
1858  match view:
1859    case Tuple{+tree,pf}:
1860      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {I.blocks(1n+n,index,remain,t,(_,h)) == S.blocks(1n+n,index,remain,t,(_,h)) : T.Chain}
1861      %Equal.sym(T.Counter,F.bump(t,128),S.advance(t,128),C.bump_correct(t,128)) : {I.blocks(n,U32.add(index,32),remain,_,I.absorb(A.thaw(tree),index,_,h)) == S.blocks(1n+n,index,remain,t,(A.thaw(tree),h)) : T.Chain}
1862      Equal.trans(T.Chain,
1863        I.blocks(n,U32.add(index,32),remain,S.advance(t,128),I.absorb(A.thaw(tree),index,S.advance(t,128),h)),
1864        S.blocks(n,U32.add(index,32),remain,S.advance(t,128),I.absorb(A.thaw(tree),index,S.advance(t,128),h)),
1865        S.blocks(n,U32.add(index,32),remain,S.advance(t,128),S.absorb(A.thaw(tree),index,S.advance(t,128),h)),
1866        recurse(I.absorb(A.thaw(tree),index,S.advance(t,128),h)),
1867        Equal.cong(Array<U32> & T.Chain,T.Chain,pair => S.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair),
1868          I.absorb(A.thaw(tree),index,S.advance(t,128),h),S.absorb(A.thaw(tree),index,S.advance(t,128),h),absorb_correct(A.thaw(tree),index,S.advance(t,128),h)))
1869
1870law blocks_correct:
1871  for +n: Nat
1872  for +index: U32
1873  for +remain: Nat
1874  for +t: T.Counter
1875  for pair: Array<U32> & T.Chain
1876  {I.blocks(n,index,remain,t,pair) == S.blocks(n,index,remain,t,pair) : T.Chain}
1877
1878def blocks_correct(n,index,remain,t,pair):
1879  match n pair:
1880    case 0n Tuple{a,h}: final_correct(a,index,remain,t,h)
1881    case 1n+p Tuple{a,h}:
1882      blocks_step(p,index,remain,t,a,h,A.reify(a),pair => blocks_correct(p,U32.add(index,32),remain,S.advance(t,128),pair))
1883
1884law unchecked_correct:
1885  for a: Array<U32>
1886  for +length: Nat
1887  {I.unchecked(a,length) == S.unchecked(a,length) : T.Chain}
1888
1889def unchecked_correct(a,length):
1890  blocks_correct(Nat.div(Nat.sub(length,1n),128n),0,Nat.sub(length,Nat.mul(Nat.div(Nat.sub(length,1n),128n),128n)),T.C{0,0,0,0},(a,I.initial()))
1891
1892law digest_correct:
1893  for +h: T.Chain
1894  {I.digest(h) == S.digest(h) : Array<U32>}
1895
1896def digest_correct(h):
1897  match h:
1898    case T.H{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7}}: {==}
1899
1900law checked_true_reified:
1901  for -a: Array<U32>
1902  for +length: Nat
1903  for view: Sigma<&2,&1,A.Tree,z => {a == A.thaw(z) : Array<U32>}>
1904  {I.checked(True{},a,length) == S.checked(True{},a,length) : Maybe<&1,Array<U32>>}
1905
1906def checked_true_reified(a,length,view):
1907  match view:
1908    case Tuple{+tree,pf}:
1909      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {I.checked(True{},_,length) == S.checked(True{},_,length) : Maybe<&1,Array<U32>>}
1910      Equal.trans(Maybe<&1,Array<U32>>,
1911        Some{I.digest(I.unchecked(A.thaw(tree),length))},
1912        Some{I.digest(S.unchecked(A.thaw(tree),length))},
1913        Some{S.digest(S.unchecked(A.thaw(tree),length))},
1914        Equal.cong(T.Chain,Maybe<&1,Array<U32>>,x => Some{I.digest(x)},I.unchecked(A.thaw(tree),length),S.unchecked(A.thaw(tree),length),unchecked_correct(A.thaw(tree),length)),
1915        Equal.cong(Array<U32>,Maybe<&1,Array<U32>>,x => Some{x},I.digest(S.unchecked(A.thaw(tree),length)),S.digest(S.unchecked(A.thaw(tree),length)),digest_correct(S.unchecked(A.thaw(tree),length))))
1916
1917law checked_correct:
1918  for +valid: Bool
1919  for a: Array<U32>
1920  for +length: Nat
1921  {I.checked(valid,a,length) == S.checked(valid,a,length) : Maybe<&1,Array<U32>>}
1922
1923def checked_correct(valid,a,length):
1924  match valid:
1925    case False{}: {==}
1926    case True{}: checked_true_reified(a,length,A.reify(a))
1927
1928law sized_correct:
1929  for +length: Nat
1930  for pair: Array<U32> & U32
1931  {I.sized(length,pair) == S.sized(length,pair) : Maybe<&1,Array<U32>>}
1932
1933def sized_correct(length,pair):
1934  (a,capacity) = pair
1935  checked_correct(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
1936
1937law blake2b_correct:
1938  for words: Array<U32>
1939  for +byte_length: Nat
1940  {I.blake2b(words,byte_length) == S.blake2b(words,byte_length) : Maybe<&1,Array<U32>>}
1941
1942def blake2b_correct(words,byte_length):
1943  sized_correct(byte_length,Array.size(U32,words))