proofs/crypto/keccak/sponge.bend

bend-collections-laws-crypto@1.0.0.0 · 2,363 lines · 84 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/keccak.bend as K
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as P
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/permutation.bend as F
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/main.bend as R
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/permutation.bend as Q
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/array.bend as A
9
10law mix_correct:
11  for +s: T.State
12  for +w0: U32
13  for +w1: U32
14  for +w2: U32
15  for +w3: U32
16  for +w4: U32
17  for +w5: U32
18  for +w6: U32
19  for +w7: U32
20  for +w8: U32
21  for +w9: U32
22  for +w10: U32
23  for +w11: U32
24  for +w12: U32
25  for +w13: U32
26  for +w14: U32
27  for +w15: U32
28  for +w16: U32
29  for +w17: U32
30  for +w18: U32
31  for +w19: U32
32  for +w20: U32
33  for +w21: U32
34  for +w22: U32
35  for +w23: U32
36  for +w24: U32
37  for +w25: U32
38  for +w26: U32
39  for +w27: U32
40  for +w28: U32
41  for +w29: U32
42  for +w30: U32
43  for +w31: U32
44  for +w32: U32
45  for +w33: U32
46  {K.mix(s,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,w32,w33) == R.inject(s,[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,w32,w33]) : T.State}
47
48def mix_correct(s,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,w32,w33):
49  match s:
50    case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},T.W{a4,b4},T.W{a5,b5},T.W{a6,b6},T.W{a7,b7},T.W{a8,b8},T.W{a9,b9},T.W{a10,b10},T.W{a11,b11},T.W{a12,b12},T.W{a13,b13},T.W{a14,b14},T.W{a15,b15},T.W{a16,b16},T.W{a17,b17},T.W{a18,b18},T.W{a19,b19},T.W{a20,b20},T.W{a21,b21},T.W{a22,b22},T.W{a23,b23},T.W{a24,b24}}: {==}
51
52law compress_correct:
53  for +r: Nat
54  for +s: T.State
55  for +w0: U32
56  for +w1: U32
57  for +w2: U32
58  for +w3: U32
59  for +w4: U32
60  for +w5: U32
61  for +w6: U32
62  for +w7: U32
63  for +w8: U32
64  for +w9: U32
65  for +w10: U32
66  for +w11: U32
67  for +w12: U32
68  for +w13: U32
69  for +w14: U32
70  for +w15: U32
71  for +w16: U32
72  for +w17: U32
73  for +w18: U32
74  for +w19: U32
75  for +w20: U32
76  for +w21: U32
77  for +w22: U32
78  for +w23: U32
79  for +w24: U32
80  for +w25: U32
81  for +w26: U32
82  for +w27: U32
83  for +w28: U32
84  for +w29: U32
85  for +w30: U32
86  for +w31: U32
87  for +w32: U32
88  for +w33: U32
89  {P.rounds(r,0n,K.mix(s,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,w32,w33)) == F.rounds(r,0n,R.inject(s,[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,w32,w33])) : T.State}
90
91def compress_correct(r,s,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,w32,w33):
92  Equal.trans(T.State,P.rounds(r,0n,K.mix(s,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,w32,w33)),F.rounds(r,0n,K.mix(s,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,w32,w33)),F.rounds(r,0n,R.inject(s,[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,w32,w33])),
93    Q.rounds_correct(r,0n,K.mix(s,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,w32,w33)),
94    Equal.cong(T.State,T.State,t => F.rounds(r,0n,t),K.mix(s,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,w32,w33),R.inject(s,[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,w32,w33]),mix_correct(s,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,w32,w33)))
95
96law read33_correct:
97  for +r: Nat
98  for +index: U32
99  for +s: T.State
100  for +w0: U32
101  for +w1: U32
102  for +w2: U32
103  for +w3: U32
104  for +w4: U32
105  for +w5: U32
106  for +w6: U32
107  for +w7: U32
108  for +w8: U32
109  for +w9: U32
110  for +w10: U32
111  for +w11: U32
112  for +w12: U32
113  for +w13: U32
114  for +w14: U32
115  for +w15: U32
116  for +w16: U32
117  for +w17: U32
118  for +w18: U32
119  for +w19: U32
120  for +w20: U32
121  for +w21: U32
122  for +w22: U32
123  for +w23: U32
124  for +w24: U32
125  for +w25: U32
126  for +w26: U32
127  for +w27: U32
128  for +w28: U32
129  for +w29: U32
130  for +w30: U32
131  for +w31: U32
132  for +w32: U32
133  for pair: Array<U32> & U32
134  {K.read33(r,index,s,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,w32,pair) == R.gather(r,0n,index,34,False{},0n,s,[w32,w31,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.State}
135
136def read33_correct(r,index,s,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,w32,pair):
137  (a,w33) = pair
138  Equal.cong(T.State,Array<U32> & T.State,t => (a,t),P.rounds(r,0n,K.mix(s,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,w32,w33)),F.rounds(r,0n,R.inject(s,[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,w32,w33])),compress_correct(r,s,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,w32,w33))
139
140law read32_correct:
141  for +r: Nat
142  for +index: U32
143  for +s: T.State
144  for +w0: U32
145  for +w1: U32
146  for +w2: U32
147  for +w3: U32
148  for +w4: U32
149  for +w5: U32
150  for +w6: U32
151  for +w7: U32
152  for +w8: U32
153  for +w9: U32
154  for +w10: U32
155  for +w11: U32
156  for +w12: U32
157  for +w13: U32
158  for +w14: U32
159  for +w15: U32
160  for +w16: U32
161  for +w17: U32
162  for +w18: U32
163  for +w19: U32
164  for +w20: U32
165  for +w21: U32
166  for +w22: U32
167  for +w23: U32
168  for +w24: U32
169  for +w25: U32
170  for +w26: U32
171  for +w27: U32
172  for +w28: U32
173  for +w29: U32
174  for +w30: U32
175  for +w31: U32
176  for pair: Array<U32> & U32
177  {K.read32(r,index,s,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,pair) == R.gather(r,1n,index,33,False{},0n,s,[w31,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.State}
178
179def read32_correct(r,index,s,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,pair):
180  (a,w32) = pair
181  read33_correct(r,index,s,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,w32,Array.get(U32,a,U32.add(index,33)))
182
183law read31_correct:
184  for +r: Nat
185  for +index: U32
186  for +s: T.State
187  for +w0: U32
188  for +w1: U32
189  for +w2: U32
190  for +w3: U32
191  for +w4: U32
192  for +w5: U32
193  for +w6: U32
194  for +w7: U32
195  for +w8: U32
196  for +w9: U32
197  for +w10: U32
198  for +w11: U32
199  for +w12: U32
200  for +w13: U32
201  for +w14: U32
202  for +w15: U32
203  for +w16: U32
204  for +w17: U32
205  for +w18: U32
206  for +w19: U32
207  for +w20: U32
208  for +w21: U32
209  for +w22: U32
210  for +w23: U32
211  for +w24: U32
212  for +w25: U32
213  for +w26: U32
214  for +w27: U32
215  for +w28: U32
216  for +w29: U32
217  for +w30: U32
218  for pair: Array<U32> & U32
219  {K.read31(r,index,s,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) == R.gather(r,2n,index,32,False{},0n,s,[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.State}
220
221def read31_correct(r,index,s,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):
222  (a,w31) = pair
223  read32_correct(r,index,s,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,Array.get(U32,a,U32.add(index,32)))
224
225law read30_correct:
226  for +r: Nat
227  for +index: U32
228  for +s: T.State
229  for +w0: U32
230  for +w1: U32
231  for +w2: U32
232  for +w3: U32
233  for +w4: U32
234  for +w5: U32
235  for +w6: U32
236  for +w7: U32
237  for +w8: U32
238  for +w9: U32
239  for +w10: U32
240  for +w11: U32
241  for +w12: U32
242  for +w13: U32
243  for +w14: U32
244  for +w15: U32
245  for +w16: U32
246  for +w17: U32
247  for +w18: U32
248  for +w19: U32
249  for +w20: U32
250  for +w21: U32
251  for +w22: U32
252  for +w23: U32
253  for +w24: U32
254  for +w25: U32
255  for +w26: U32
256  for +w27: U32
257  for +w28: U32
258  for +w29: U32
259  for pair: Array<U32> & U32
260  {K.read30(r,index,s,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) == R.gather(r,3n,index,31,False{},0n,s,[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.State}
261
262def read30_correct(r,index,s,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):
263  (a,w30) = pair
264  read31_correct(r,index,s,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)))
265
266law read29_correct:
267  for +r: Nat
268  for +index: U32
269  for +s: T.State
270  for +w0: U32
271  for +w1: U32
272  for +w2: U32
273  for +w3: U32
274  for +w4: U32
275  for +w5: U32
276  for +w6: U32
277  for +w7: U32
278  for +w8: U32
279  for +w9: U32
280  for +w10: U32
281  for +w11: U32
282  for +w12: U32
283  for +w13: U32
284  for +w14: U32
285  for +w15: U32
286  for +w16: U32
287  for +w17: U32
288  for +w18: U32
289  for +w19: U32
290  for +w20: U32
291  for +w21: U32
292  for +w22: U32
293  for +w23: U32
294  for +w24: U32
295  for +w25: U32
296  for +w26: U32
297  for +w27: U32
298  for +w28: U32
299  for pair: Array<U32> & U32
300  {K.read29(r,index,s,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) == R.gather(r,4n,index,30,False{},0n,s,[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.State}
301
302def read29_correct(r,index,s,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):
303  (a,w29) = pair
304  read30_correct(r,index,s,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)))
305
306law read28_correct:
307  for +r: Nat
308  for +index: U32
309  for +s: T.State
310  for +w0: U32
311  for +w1: U32
312  for +w2: U32
313  for +w3: U32
314  for +w4: U32
315  for +w5: U32
316  for +w6: U32
317  for +w7: U32
318  for +w8: U32
319  for +w9: U32
320  for +w10: U32
321  for +w11: U32
322  for +w12: U32
323  for +w13: U32
324  for +w14: U32
325  for +w15: U32
326  for +w16: U32
327  for +w17: U32
328  for +w18: U32
329  for +w19: U32
330  for +w20: U32
331  for +w21: U32
332  for +w22: U32
333  for +w23: U32
334  for +w24: U32
335  for +w25: U32
336  for +w26: U32
337  for +w27: U32
338  for pair: Array<U32> & U32
339  {K.read28(r,index,s,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) == R.gather(r,5n,index,29,False{},0n,s,[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.State}
340
341def read28_correct(r,index,s,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):
342  (a,w28) = pair
343  read29_correct(r,index,s,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)))
344
345law read27_correct:
346  for +r: Nat
347  for +index: U32
348  for +s: T.State
349  for +w0: U32
350  for +w1: U32
351  for +w2: U32
352  for +w3: U32
353  for +w4: U32
354  for +w5: U32
355  for +w6: U32
356  for +w7: U32
357  for +w8: U32
358  for +w9: U32
359  for +w10: U32
360  for +w11: U32
361  for +w12: U32
362  for +w13: U32
363  for +w14: U32
364  for +w15: U32
365  for +w16: U32
366  for +w17: U32
367  for +w18: U32
368  for +w19: U32
369  for +w20: U32
370  for +w21: U32
371  for +w22: U32
372  for +w23: U32
373  for +w24: U32
374  for +w25: U32
375  for +w26: U32
376  for pair: Array<U32> & U32
377  {K.read27(r,index,s,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) == R.gather(r,6n,index,28,False{},0n,s,[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.State}
378
379def read27_correct(r,index,s,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):
380  (a,w27) = pair
381  read28_correct(r,index,s,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)))
382
383law read26_correct:
384  for +r: Nat
385  for +index: U32
386  for +s: T.State
387  for +w0: U32
388  for +w1: U32
389  for +w2: U32
390  for +w3: U32
391  for +w4: U32
392  for +w5: U32
393  for +w6: U32
394  for +w7: U32
395  for +w8: U32
396  for +w9: U32
397  for +w10: U32
398  for +w11: U32
399  for +w12: U32
400  for +w13: U32
401  for +w14: U32
402  for +w15: U32
403  for +w16: U32
404  for +w17: U32
405  for +w18: U32
406  for +w19: U32
407  for +w20: U32
408  for +w21: U32
409  for +w22: U32
410  for +w23: U32
411  for +w24: U32
412  for +w25: U32
413  for pair: Array<U32> & U32
414  {K.read26(r,index,s,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) == R.gather(r,7n,index,27,False{},0n,s,[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.State}
415
416def read26_correct(r,index,s,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):
417  (a,w26) = pair
418  read27_correct(r,index,s,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)))
419
420law read25_correct:
421  for +r: Nat
422  for +index: U32
423  for +s: T.State
424  for +w0: U32
425  for +w1: U32
426  for +w2: U32
427  for +w3: U32
428  for +w4: U32
429  for +w5: U32
430  for +w6: U32
431  for +w7: U32
432  for +w8: U32
433  for +w9: U32
434  for +w10: U32
435  for +w11: U32
436  for +w12: U32
437  for +w13: U32
438  for +w14: U32
439  for +w15: U32
440  for +w16: U32
441  for +w17: U32
442  for +w18: U32
443  for +w19: U32
444  for +w20: U32
445  for +w21: U32
446  for +w22: U32
447  for +w23: U32
448  for +w24: U32
449  for pair: Array<U32> & U32
450  {K.read25(r,index,s,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) == R.gather(r,8n,index,26,False{},0n,s,[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.State}
451
452def read25_correct(r,index,s,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):
453  (a,w25) = pair
454  read26_correct(r,index,s,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)))
455
456law read24_correct:
457  for +r: Nat
458  for +index: U32
459  for +s: T.State
460  for +w0: U32
461  for +w1: U32
462  for +w2: U32
463  for +w3: U32
464  for +w4: U32
465  for +w5: U32
466  for +w6: U32
467  for +w7: U32
468  for +w8: U32
469  for +w9: U32
470  for +w10: U32
471  for +w11: U32
472  for +w12: U32
473  for +w13: U32
474  for +w14: U32
475  for +w15: U32
476  for +w16: U32
477  for +w17: U32
478  for +w18: U32
479  for +w19: U32
480  for +w20: U32
481  for +w21: U32
482  for +w22: U32
483  for +w23: U32
484  for pair: Array<U32> & U32
485  {K.read24(r,index,s,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) == R.gather(r,9n,index,25,False{},0n,s,[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.State}
486
487def read24_correct(r,index,s,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):
488  (a,w24) = pair
489  read25_correct(r,index,s,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)))
490
491law read23_correct:
492  for +r: Nat
493  for +index: U32
494  for +s: T.State
495  for +w0: U32
496  for +w1: U32
497  for +w2: U32
498  for +w3: U32
499  for +w4: U32
500  for +w5: U32
501  for +w6: U32
502  for +w7: U32
503  for +w8: U32
504  for +w9: U32
505  for +w10: U32
506  for +w11: U32
507  for +w12: U32
508  for +w13: U32
509  for +w14: U32
510  for +w15: U32
511  for +w16: U32
512  for +w17: U32
513  for +w18: U32
514  for +w19: U32
515  for +w20: U32
516  for +w21: U32
517  for +w22: U32
518  for pair: Array<U32> & U32
519  {K.read23(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair) == R.gather(r,10n,index,24,False{},0n,s,[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.State}
520
521def read23_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair):
522  (a,w23) = pair
523  read24_correct(r,index,s,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)))
524
525law read22_correct:
526  for +r: Nat
527  for +index: U32
528  for +s: T.State
529  for +w0: U32
530  for +w1: U32
531  for +w2: U32
532  for +w3: U32
533  for +w4: U32
534  for +w5: U32
535  for +w6: U32
536  for +w7: U32
537  for +w8: U32
538  for +w9: U32
539  for +w10: U32
540  for +w11: U32
541  for +w12: U32
542  for +w13: U32
543  for +w14: U32
544  for +w15: U32
545  for +w16: U32
546  for +w17: U32
547  for +w18: U32
548  for +w19: U32
549  for +w20: U32
550  for +w21: U32
551  for pair: Array<U32> & U32
552  {K.read22(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair) == R.gather(r,11n,index,23,False{},0n,s,[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.State}
553
554def read22_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair):
555  (a,w22) = pair
556  read23_correct(r,index,s,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)))
557
558law read21_correct:
559  for +r: Nat
560  for +index: U32
561  for +s: T.State
562  for +w0: U32
563  for +w1: U32
564  for +w2: U32
565  for +w3: U32
566  for +w4: U32
567  for +w5: U32
568  for +w6: U32
569  for +w7: U32
570  for +w8: U32
571  for +w9: U32
572  for +w10: U32
573  for +w11: U32
574  for +w12: U32
575  for +w13: U32
576  for +w14: U32
577  for +w15: U32
578  for +w16: U32
579  for +w17: U32
580  for +w18: U32
581  for +w19: U32
582  for +w20: U32
583  for pair: Array<U32> & U32
584  {K.read21(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair) == R.gather(r,12n,index,22,False{},0n,s,[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.State}
585
586def read21_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair):
587  (a,w21) = pair
588  read22_correct(r,index,s,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)))
589
590law read20_correct:
591  for +r: Nat
592  for +index: U32
593  for +s: T.State
594  for +w0: U32
595  for +w1: U32
596  for +w2: U32
597  for +w3: U32
598  for +w4: U32
599  for +w5: U32
600  for +w6: U32
601  for +w7: U32
602  for +w8: U32
603  for +w9: U32
604  for +w10: U32
605  for +w11: U32
606  for +w12: U32
607  for +w13: U32
608  for +w14: U32
609  for +w15: U32
610  for +w16: U32
611  for +w17: U32
612  for +w18: U32
613  for +w19: U32
614  for pair: Array<U32> & U32
615  {K.read20(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair) == R.gather(r,13n,index,21,False{},0n,s,[w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
616
617def read20_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair):
618  (a,w20) = pair
619  read21_correct(r,index,s,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)))
620
621law read19_correct:
622  for +r: Nat
623  for +index: U32
624  for +s: T.State
625  for +w0: U32
626  for +w1: U32
627  for +w2: U32
628  for +w3: U32
629  for +w4: U32
630  for +w5: U32
631  for +w6: U32
632  for +w7: U32
633  for +w8: U32
634  for +w9: U32
635  for +w10: U32
636  for +w11: U32
637  for +w12: U32
638  for +w13: U32
639  for +w14: U32
640  for +w15: U32
641  for +w16: U32
642  for +w17: U32
643  for +w18: U32
644  for pair: Array<U32> & U32
645  {K.read19(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair) == R.gather(r,14n,index,20,False{},0n,s,[w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
646
647def read19_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair):
648  (a,w19) = pair
649  read20_correct(r,index,s,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)))
650
651law read18_correct:
652  for +r: Nat
653  for +index: U32
654  for +s: T.State
655  for +w0: U32
656  for +w1: U32
657  for +w2: U32
658  for +w3: U32
659  for +w4: U32
660  for +w5: U32
661  for +w6: U32
662  for +w7: U32
663  for +w8: U32
664  for +w9: U32
665  for +w10: U32
666  for +w11: U32
667  for +w12: U32
668  for +w13: U32
669  for +w14: U32
670  for +w15: U32
671  for +w16: U32
672  for +w17: U32
673  for pair: Array<U32> & U32
674  {K.read18(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair) == R.gather(r,15n,index,19,False{},0n,s,[w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
675
676def read18_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair):
677  (a,w18) = pair
678  read19_correct(r,index,s,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)))
679
680law read17_correct:
681  for +r: Nat
682  for +index: U32
683  for +s: T.State
684  for +w0: U32
685  for +w1: U32
686  for +w2: U32
687  for +w3: U32
688  for +w4: U32
689  for +w5: U32
690  for +w6: U32
691  for +w7: U32
692  for +w8: U32
693  for +w9: U32
694  for +w10: U32
695  for +w11: U32
696  for +w12: U32
697  for +w13: U32
698  for +w14: U32
699  for +w15: U32
700  for +w16: U32
701  for pair: Array<U32> & U32
702  {K.read17(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair) == R.gather(r,16n,index,18,False{},0n,s,[w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
703
704def read17_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair):
705  (a,w17) = pair
706  read18_correct(r,index,s,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)))
707
708law read16_correct:
709  for +r: Nat
710  for +index: U32
711  for +s: T.State
712  for +w0: U32
713  for +w1: U32
714  for +w2: U32
715  for +w3: U32
716  for +w4: U32
717  for +w5: U32
718  for +w6: U32
719  for +w7: U32
720  for +w8: U32
721  for +w9: U32
722  for +w10: U32
723  for +w11: U32
724  for +w12: U32
725  for +w13: U32
726  for +w14: U32
727  for +w15: U32
728  for pair: Array<U32> & U32
729  {K.read16(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair) == R.gather(r,17n,index,17,False{},0n,s,[w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
730
731def read16_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair):
732  (a,w16) = pair
733  read17_correct(r,index,s,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)))
734
735law read15_correct:
736  for +r: Nat
737  for +index: U32
738  for +s: T.State
739  for +w0: U32
740  for +w1: U32
741  for +w2: U32
742  for +w3: U32
743  for +w4: U32
744  for +w5: U32
745  for +w6: U32
746  for +w7: U32
747  for +w8: U32
748  for +w9: U32
749  for +w10: U32
750  for +w11: U32
751  for +w12: U32
752  for +w13: U32
753  for +w14: U32
754  for pair: Array<U32> & U32
755  {K.read15(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == R.gather(r,18n,index,16,False{},0n,s,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
756
757def read15_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
758  (a,w15) = pair
759  read16_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
760
761law read14_correct:
762  for +r: Nat
763  for +index: U32
764  for +s: T.State
765  for +w0: U32
766  for +w1: U32
767  for +w2: U32
768  for +w3: U32
769  for +w4: U32
770  for +w5: U32
771  for +w6: U32
772  for +w7: U32
773  for +w8: U32
774  for +w9: U32
775  for +w10: U32
776  for +w11: U32
777  for +w12: U32
778  for +w13: U32
779  for pair: Array<U32> & U32
780  {K.read14(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == R.gather(r,19n,index,15,False{},0n,s,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
781
782def read14_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
783  (a,w14) = pair
784  read15_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
785
786law read13_correct:
787  for +r: Nat
788  for +index: U32
789  for +s: T.State
790  for +w0: U32
791  for +w1: U32
792  for +w2: U32
793  for +w3: U32
794  for +w4: U32
795  for +w5: U32
796  for +w6: U32
797  for +w7: U32
798  for +w8: U32
799  for +w9: U32
800  for +w10: U32
801  for +w11: U32
802  for +w12: U32
803  for pair: Array<U32> & U32
804  {K.read13(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == R.gather(r,20n,index,14,False{},0n,s,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
805
806def read13_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
807  (a,w13) = pair
808  read14_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
809
810law read12_correct:
811  for +r: Nat
812  for +index: U32
813  for +s: T.State
814  for +w0: U32
815  for +w1: U32
816  for +w2: U32
817  for +w3: U32
818  for +w4: U32
819  for +w5: U32
820  for +w6: U32
821  for +w7: U32
822  for +w8: U32
823  for +w9: U32
824  for +w10: U32
825  for +w11: U32
826  for pair: Array<U32> & U32
827  {K.read12(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == R.gather(r,21n,index,13,False{},0n,s,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
828
829def read12_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
830  (a,w12) = pair
831  read13_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
832
833law read11_correct:
834  for +r: Nat
835  for +index: U32
836  for +s: T.State
837  for +w0: U32
838  for +w1: U32
839  for +w2: U32
840  for +w3: U32
841  for +w4: U32
842  for +w5: U32
843  for +w6: U32
844  for +w7: U32
845  for +w8: U32
846  for +w9: U32
847  for +w10: U32
848  for pair: Array<U32> & U32
849  {K.read11(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == R.gather(r,22n,index,12,False{},0n,s,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
850
851def read11_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
852  (a,w11) = pair
853  read12_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
854
855law read10_correct:
856  for +r: Nat
857  for +index: U32
858  for +s: T.State
859  for +w0: U32
860  for +w1: U32
861  for +w2: U32
862  for +w3: U32
863  for +w4: U32
864  for +w5: U32
865  for +w6: U32
866  for +w7: U32
867  for +w8: U32
868  for +w9: U32
869  for pair: Array<U32> & U32
870  {K.read10(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == R.gather(r,23n,index,11,False{},0n,s,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
871
872def read10_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
873  (a,w10) = pair
874  read11_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
875
876law read9_correct:
877  for +r: Nat
878  for +index: U32
879  for +s: T.State
880  for +w0: U32
881  for +w1: U32
882  for +w2: U32
883  for +w3: U32
884  for +w4: U32
885  for +w5: U32
886  for +w6: U32
887  for +w7: U32
888  for +w8: U32
889  for pair: Array<U32> & U32
890  {K.read9(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == R.gather(r,24n,index,10,False{},0n,s,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
891
892def read9_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
893  (a,w9) = pair
894  read10_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
895
896law read8_correct:
897  for +r: Nat
898  for +index: U32
899  for +s: T.State
900  for +w0: U32
901  for +w1: U32
902  for +w2: U32
903  for +w3: U32
904  for +w4: U32
905  for +w5: U32
906  for +w6: U32
907  for +w7: U32
908  for pair: Array<U32> & U32
909  {K.read8(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,pair) == R.gather(r,25n,index,9,False{},0n,s,[w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
910
911def read8_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,pair):
912  (a,w8) = pair
913  read9_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
914
915law read7_correct:
916  for +r: Nat
917  for +index: U32
918  for +s: T.State
919  for +w0: U32
920  for +w1: U32
921  for +w2: U32
922  for +w3: U32
923  for +w4: U32
924  for +w5: U32
925  for +w6: U32
926  for pair: Array<U32> & U32
927  {K.read7(r,index,s,w0,w1,w2,w3,w4,w5,w6,pair) == R.gather(r,26n,index,8,False{},0n,s,[w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
928
929def read7_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,pair):
930  (a,w7) = pair
931  read8_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
932
933law read6_correct:
934  for +r: Nat
935  for +index: U32
936  for +s: T.State
937  for +w0: U32
938  for +w1: U32
939  for +w2: U32
940  for +w3: U32
941  for +w4: U32
942  for +w5: U32
943  for pair: Array<U32> & U32
944  {K.read6(r,index,s,w0,w1,w2,w3,w4,w5,pair) == R.gather(r,27n,index,7,False{},0n,s,[w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
945
946def read6_correct(r,index,s,w0,w1,w2,w3,w4,w5,pair):
947  (a,w6) = pair
948  read7_correct(r,index,s,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
949
950law read5_correct:
951  for +r: Nat
952  for +index: U32
953  for +s: T.State
954  for +w0: U32
955  for +w1: U32
956  for +w2: U32
957  for +w3: U32
958  for +w4: U32
959  for pair: Array<U32> & U32
960  {K.read5(r,index,s,w0,w1,w2,w3,w4,pair) == R.gather(r,28n,index,6,False{},0n,s,[w4,w3,w2,w1,w0],pair) : Array<U32> & T.State}
961
962def read5_correct(r,index,s,w0,w1,w2,w3,w4,pair):
963  (a,w5) = pair
964  read6_correct(r,index,s,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
965
966law read4_correct:
967  for +r: Nat
968  for +index: U32
969  for +s: T.State
970  for +w0: U32
971  for +w1: U32
972  for +w2: U32
973  for +w3: U32
974  for pair: Array<U32> & U32
975  {K.read4(r,index,s,w0,w1,w2,w3,pair) == R.gather(r,29n,index,5,False{},0n,s,[w3,w2,w1,w0],pair) : Array<U32> & T.State}
976
977def read4_correct(r,index,s,w0,w1,w2,w3,pair):
978  (a,w4) = pair
979  read5_correct(r,index,s,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
980
981law read3_correct:
982  for +r: Nat
983  for +index: U32
984  for +s: T.State
985  for +w0: U32
986  for +w1: U32
987  for +w2: U32
988  for pair: Array<U32> & U32
989  {K.read3(r,index,s,w0,w1,w2,pair) == R.gather(r,30n,index,4,False{},0n,s,[w2,w1,w0],pair) : Array<U32> & T.State}
990
991def read3_correct(r,index,s,w0,w1,w2,pair):
992  (a,w3) = pair
993  read4_correct(r,index,s,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
994
995law read2_correct:
996  for +r: Nat
997  for +index: U32
998  for +s: T.State
999  for +w0: U32
1000  for +w1: U32
1001  for pair: Array<U32> & U32
1002  {K.read2(r,index,s,w0,w1,pair) == R.gather(r,31n,index,3,False{},0n,s,[w1,w0],pair) : Array<U32> & T.State}
1003
1004def read2_correct(r,index,s,w0,w1,pair):
1005  (a,w2) = pair
1006  read3_correct(r,index,s,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
1007
1008law read1_correct:
1009  for +r: Nat
1010  for +index: U32
1011  for +s: T.State
1012  for +w0: U32
1013  for pair: Array<U32> & U32
1014  {K.read1(r,index,s,w0,pair) == R.gather(r,32n,index,2,False{},0n,s,[w0],pair) : Array<U32> & T.State}
1015
1016def read1_correct(r,index,s,w0,pair):
1017  (a,w1) = pair
1018  read2_correct(r,index,s,w0,w1,Array.get(U32,a,U32.add(index,2)))
1019
1020law read0_correct:
1021  for +r: Nat
1022  for +index: U32
1023  for +s: T.State
1024  for pair: Array<U32> & U32
1025  {K.read0(r,index,s,pair) == R.gather(r,33n,index,1,False{},0n,s,[],pair) : Array<U32> & T.State}
1026
1027def read0_correct(r,index,s,pair):
1028  (a,w0) = pair
1029  read1_correct(r,index,s,w0,Array.get(U32,a,U32.add(index,1)))
1030
1031law padding_correct:
1032  for +remain: Nat
1033  for +w0: U32
1034  for +w1: U32
1035  for +w2: U32
1036  for +w3: U32
1037  for +w4: U32
1038  for +w5: U32
1039  for +w6: U32
1040  for +w7: U32
1041  for +w8: U32
1042  for +w9: U32
1043  for +w10: U32
1044  for +w11: U32
1045  for +w12: U32
1046  for +w13: U32
1047  for +w14: U32
1048  for +w15: U32
1049  for +w16: U32
1050  for +w17: U32
1051  for +w18: U32
1052  for +w19: U32
1053  for +w20: U32
1054  for +w21: U32
1055  for +w22: U32
1056  for +w23: U32
1057  for +w24: U32
1058  for +w25: U32
1059  for +w26: U32
1060  for +w27: U32
1061  for +w28: U32
1062  for +w29: U32
1063  for +w30: U32
1064  for +w31: U32
1065  for +w32: U32
1066  for +w33: U32
1067  {[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),K.pad_word(w16,64n,remain),K.pad_word(w17,68n,remain),K.pad_word(w18,72n,remain),K.pad_word(w19,76n,remain),K.pad_word(w20,80n,remain),K.pad_word(w21,84n,remain),K.pad_word(w22,88n,remain),K.pad_word(w23,92n,remain),K.pad_word(w24,96n,remain),K.pad_word(w25,100n,remain),K.pad_word(w26,104n,remain),K.pad_word(w27,108n,remain),K.pad_word(w28,112n,remain),K.pad_word(w29,116n,remain),K.pad_word(w30,120n,remain),K.pad_word(w31,124n,remain),K.pad_word(w32,128n,remain),U32.or(K.pad_word(w33,132n,remain),2147483648)] == R.prepare(True{},[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,w32,w33],remain) : List<&2,U32>}
1068
1069def padding_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,w32,w33):
1070  match remain:
1071    case 0n: {==}
1072    case 1n: {==}
1073    case 2n: {==}
1074    case 3n: {==}
1075    case 4n: {==}
1076    case 5n: {==}
1077    case 6n: {==}
1078    case 7n: {==}
1079    case 8n: {==}
1080    case 9n: {==}
1081    case 10n: {==}
1082    case 11n: {==}
1083    case 12n: {==}
1084    case 13n: {==}
1085    case 14n: {==}
1086    case 15n: {==}
1087    case 16n: {==}
1088    case 17n: {==}
1089    case 18n: {==}
1090    case 19n: {==}
1091    case 20n: {==}
1092    case 21n: {==}
1093    case 22n: {==}
1094    case 23n: {==}
1095    case 24n: {==}
1096    case 25n: {==}
1097    case 26n: {==}
1098    case 27n: {==}
1099    case 28n: {==}
1100    case 29n: {==}
1101    case 30n: {==}
1102    case 31n: {==}
1103    case 32n: {==}
1104    case 33n: {==}
1105    case 34n: {==}
1106    case 35n: {==}
1107    case 36n: {==}
1108    case 37n: {==}
1109    case 38n: {==}
1110    case 39n: {==}
1111    case 40n: {==}
1112    case 41n: {==}
1113    case 42n: {==}
1114    case 43n: {==}
1115    case 44n: {==}
1116    case 45n: {==}
1117    case 46n: {==}
1118    case 47n: {==}
1119    case 48n: {==}
1120    case 49n: {==}
1121    case 50n: {==}
1122    case 51n: {==}
1123    case 52n: {==}
1124    case 53n: {==}
1125    case 54n: {==}
1126    case 55n: {==}
1127    case 56n: {==}
1128    case 57n: {==}
1129    case 58n: {==}
1130    case 59n: {==}
1131    case 60n: {==}
1132    case 61n: {==}
1133    case 62n: {==}
1134    case 63n: {==}
1135    case 64n: {==}
1136    case 65n: {==}
1137    case 66n: {==}
1138    case 67n: {==}
1139    case 68n: {==}
1140    case 69n: {==}
1141    case 70n: {==}
1142    case 71n: {==}
1143    case 72n: {==}
1144    case 73n: {==}
1145    case 74n: {==}
1146    case 75n: {==}
1147    case 76n: {==}
1148    case 77n: {==}
1149    case 78n: {==}
1150    case 79n: {==}
1151    case 80n: {==}
1152    case 81n: {==}
1153    case 82n: {==}
1154    case 83n: {==}
1155    case 84n: {==}
1156    case 85n: {==}
1157    case 86n: {==}
1158    case 87n: {==}
1159    case 88n: {==}
1160    case 89n: {==}
1161    case 90n: {==}
1162    case 91n: {==}
1163    case 92n: {==}
1164    case 93n: {==}
1165    case 94n: {==}
1166    case 95n: {==}
1167    case 96n: {==}
1168    case 97n: {==}
1169    case 98n: {==}
1170    case 99n: {==}
1171    case 100n: {==}
1172    case 101n: {==}
1173    case 102n: {==}
1174    case 103n: {==}
1175    case 104n: {==}
1176    case 105n: {==}
1177    case 106n: {==}
1178    case 107n: {==}
1179    case 108n: {==}
1180    case 109n: {==}
1181    case 110n: {==}
1182    case 111n: {==}
1183    case 112n: {==}
1184    case 113n: {==}
1185    case 114n: {==}
1186    case 115n: {==}
1187    case 116n: {==}
1188    case 117n: {==}
1189    case 118n: {==}
1190    case 119n: {==}
1191    case 120n: {==}
1192    case 121n: {==}
1193    case 122n: {==}
1194    case 123n: {==}
1195    case 124n: {==}
1196    case 125n: {==}
1197    case 126n: {==}
1198    case 127n: {==}
1199    case 128n: {==}
1200    case 129n: {==}
1201    case 130n: {==}
1202    case 131n: {==}
1203    case 132n: {==}
1204    case 133n: {==}
1205    case 134n: {==}
1206    case 135n: {==}
1207    case 136n+p: {==}
1208
1209law padded_compress_correct:
1210  for +r: Nat
1211  for +remain: Nat
1212  for +s: T.State
1213  for +w0: U32
1214  for +w1: U32
1215  for +w2: U32
1216  for +w3: U32
1217  for +w4: U32
1218  for +w5: U32
1219  for +w6: U32
1220  for +w7: U32
1221  for +w8: U32
1222  for +w9: U32
1223  for +w10: U32
1224  for +w11: U32
1225  for +w12: U32
1226  for +w13: U32
1227  for +w14: U32
1228  for +w15: U32
1229  for +w16: U32
1230  for +w17: U32
1231  for +w18: U32
1232  for +w19: U32
1233  for +w20: U32
1234  for +w21: U32
1235  for +w22: U32
1236  for +w23: U32
1237  for +w24: U32
1238  for +w25: U32
1239  for +w26: U32
1240  for +w27: U32
1241  for +w28: U32
1242  for +w29: U32
1243  for +w30: U32
1244  for +w31: U32
1245  for +w32: U32
1246  for +w33: U32
1247  {P.rounds(r,0n,K.mix(s,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),K.pad_word(w16,64n,remain),K.pad_word(w17,68n,remain),K.pad_word(w18,72n,remain),K.pad_word(w19,76n,remain),K.pad_word(w20,80n,remain),K.pad_word(w21,84n,remain),K.pad_word(w22,88n,remain),K.pad_word(w23,92n,remain),K.pad_word(w24,96n,remain),K.pad_word(w25,100n,remain),K.pad_word(w26,104n,remain),K.pad_word(w27,108n,remain),K.pad_word(w28,112n,remain),K.pad_word(w29,116n,remain),K.pad_word(w30,120n,remain),K.pad_word(w31,124n,remain),K.pad_word(w32,128n,remain),U32.or(K.pad_word(w33,132n,remain),2147483648))) == F.rounds(r,0n,R.inject(s,R.prepare(True{},[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,w32,w33],remain))) : T.State}
1248
1249def padded_compress_correct(r,remain,s,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,w32,w33):
1250  Equal.trans(T.State,
1251    P.rounds(r,0n,K.mix(s,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),K.pad_word(w16,64n,remain),K.pad_word(w17,68n,remain),K.pad_word(w18,72n,remain),K.pad_word(w19,76n,remain),K.pad_word(w20,80n,remain),K.pad_word(w21,84n,remain),K.pad_word(w22,88n,remain),K.pad_word(w23,92n,remain),K.pad_word(w24,96n,remain),K.pad_word(w25,100n,remain),K.pad_word(w26,104n,remain),K.pad_word(w27,108n,remain),K.pad_word(w28,112n,remain),K.pad_word(w29,116n,remain),K.pad_word(w30,120n,remain),K.pad_word(w31,124n,remain),K.pad_word(w32,128n,remain),U32.or(K.pad_word(w33,132n,remain),2147483648))),
1252    F.rounds(r,0n,R.inject(s,[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),K.pad_word(w16,64n,remain),K.pad_word(w17,68n,remain),K.pad_word(w18,72n,remain),K.pad_word(w19,76n,remain),K.pad_word(w20,80n,remain),K.pad_word(w21,84n,remain),K.pad_word(w22,88n,remain),K.pad_word(w23,92n,remain),K.pad_word(w24,96n,remain),K.pad_word(w25,100n,remain),K.pad_word(w26,104n,remain),K.pad_word(w27,108n,remain),K.pad_word(w28,112n,remain),K.pad_word(w29,116n,remain),K.pad_word(w30,120n,remain),K.pad_word(w31,124n,remain),K.pad_word(w32,128n,remain),U32.or(K.pad_word(w33,132n,remain),2147483648)])),
1253    F.rounds(r,0n,R.inject(s,R.prepare(True{},[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,w32,w33],remain))),
1254    compress_correct(r,s,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),K.pad_word(w16,64n,remain),K.pad_word(w17,68n,remain),K.pad_word(w18,72n,remain),K.pad_word(w19,76n,remain),K.pad_word(w20,80n,remain),K.pad_word(w21,84n,remain),K.pad_word(w22,88n,remain),K.pad_word(w23,92n,remain),K.pad_word(w24,96n,remain),K.pad_word(w25,100n,remain),K.pad_word(w26,104n,remain),K.pad_word(w27,108n,remain),K.pad_word(w28,112n,remain),K.pad_word(w29,116n,remain),K.pad_word(w30,120n,remain),K.pad_word(w31,124n,remain),K.pad_word(w32,128n,remain),U32.or(K.pad_word(w33,132n,remain),2147483648)),
1255    Equal.cong(List<&2,U32>,T.State,x => F.rounds(r,0n,R.inject(s,x)),[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),K.pad_word(w16,64n,remain),K.pad_word(w17,68n,remain),K.pad_word(w18,72n,remain),K.pad_word(w19,76n,remain),K.pad_word(w20,80n,remain),K.pad_word(w21,84n,remain),K.pad_word(w22,88n,remain),K.pad_word(w23,92n,remain),K.pad_word(w24,96n,remain),K.pad_word(w25,100n,remain),K.pad_word(w26,104n,remain),K.pad_word(w27,108n,remain),K.pad_word(w28,112n,remain),K.pad_word(w29,116n,remain),K.pad_word(w30,120n,remain),K.pad_word(w31,124n,remain),K.pad_word(w32,128n,remain),U32.or(K.pad_word(w33,132n,remain),2147483648)],R.prepare(True{},[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,w32,w33],remain),padding_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,w32,w33)))
1256
1257law pad33_correct:
1258  for +r: Nat
1259  for +remain: Nat
1260  for +index: U32
1261  for +s: T.State
1262  for +w0: U32
1263  for +w1: U32
1264  for +w2: U32
1265  for +w3: U32
1266  for +w4: U32
1267  for +w5: U32
1268  for +w6: U32
1269  for +w7: U32
1270  for +w8: U32
1271  for +w9: U32
1272  for +w10: U32
1273  for +w11: U32
1274  for +w12: U32
1275  for +w13: U32
1276  for +w14: U32
1277  for +w15: U32
1278  for +w16: U32
1279  for +w17: U32
1280  for +w18: U32
1281  for +w19: U32
1282  for +w20: U32
1283  for +w21: U32
1284  for +w22: U32
1285  for +w23: U32
1286  for +w24: U32
1287  for +w25: U32
1288  for +w26: U32
1289  for +w27: U32
1290  for +w28: U32
1291  for +w29: U32
1292  for +w30: U32
1293  for +w31: U32
1294  for +w32: U32
1295  for pair: Array<U32> & U32
1296  {K.pad33(r,remain,index,s,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,w32,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,0n,index,34,True{},remain,s,[w32,w31,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.State}
1297
1298def pad33_correct(r,remain,index,s,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,w32,pair):
1299  (a,w33) = pair
1300  padded_compress_correct(r,remain,s,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,w32,w33)
1301
1302law pad32_correct:
1303  for +r: Nat
1304  for +remain: Nat
1305  for +index: U32
1306  for +s: T.State
1307  for +w0: U32
1308  for +w1: U32
1309  for +w2: U32
1310  for +w3: U32
1311  for +w4: U32
1312  for +w5: U32
1313  for +w6: U32
1314  for +w7: U32
1315  for +w8: U32
1316  for +w9: U32
1317  for +w10: U32
1318  for +w11: U32
1319  for +w12: U32
1320  for +w13: U32
1321  for +w14: U32
1322  for +w15: U32
1323  for +w16: U32
1324  for +w17: U32
1325  for +w18: U32
1326  for +w19: U32
1327  for +w20: U32
1328  for +w21: U32
1329  for +w22: U32
1330  for +w23: U32
1331  for +w24: U32
1332  for +w25: U32
1333  for +w26: U32
1334  for +w27: U32
1335  for +w28: U32
1336  for +w29: U32
1337  for +w30: U32
1338  for +w31: U32
1339  for pair: Array<U32> & U32
1340  {K.pad32(r,remain,index,s,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,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,1n,index,33,True{},remain,s,[w31,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.State}
1341
1342def pad32_correct(r,remain,index,s,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,pair):
1343  (a,w32) = pair
1344  pad33_correct(r,remain,index,s,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,w32,Array.get(U32,a,U32.add(index,33)))
1345
1346law pad31_correct:
1347  for +r: Nat
1348  for +remain: Nat
1349  for +index: U32
1350  for +s: T.State
1351  for +w0: U32
1352  for +w1: U32
1353  for +w2: U32
1354  for +w3: U32
1355  for +w4: U32
1356  for +w5: U32
1357  for +w6: U32
1358  for +w7: U32
1359  for +w8: U32
1360  for +w9: U32
1361  for +w10: U32
1362  for +w11: U32
1363  for +w12: U32
1364  for +w13: U32
1365  for +w14: U32
1366  for +w15: U32
1367  for +w16: U32
1368  for +w17: U32
1369  for +w18: U32
1370  for +w19: U32
1371  for +w20: U32
1372  for +w21: U32
1373  for +w22: U32
1374  for +w23: U32
1375  for +w24: U32
1376  for +w25: U32
1377  for +w26: U32
1378  for +w27: U32
1379  for +w28: U32
1380  for +w29: U32
1381  for +w30: U32
1382  for pair: Array<U32> & U32
1383  {K.pad31(r,remain,index,s,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.State,R.gather(r,2n,index,32,True{},remain,s,[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.State}
1384
1385def pad31_correct(r,remain,index,s,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):
1386  (a,w31) = pair
1387  pad32_correct(r,remain,index,s,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,Array.get(U32,a,U32.add(index,32)))
1388
1389law pad30_correct:
1390  for +r: Nat
1391  for +remain: Nat
1392  for +index: U32
1393  for +s: T.State
1394  for +w0: U32
1395  for +w1: U32
1396  for +w2: U32
1397  for +w3: U32
1398  for +w4: U32
1399  for +w5: U32
1400  for +w6: U32
1401  for +w7: U32
1402  for +w8: U32
1403  for +w9: U32
1404  for +w10: U32
1405  for +w11: U32
1406  for +w12: U32
1407  for +w13: U32
1408  for +w14: U32
1409  for +w15: U32
1410  for +w16: U32
1411  for +w17: U32
1412  for +w18: U32
1413  for +w19: U32
1414  for +w20: U32
1415  for +w21: U32
1416  for +w22: U32
1417  for +w23: U32
1418  for +w24: U32
1419  for +w25: U32
1420  for +w26: U32
1421  for +w27: U32
1422  for +w28: U32
1423  for +w29: U32
1424  for pair: Array<U32> & U32
1425  {K.pad30(r,remain,index,s,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.State,R.gather(r,3n,index,31,True{},remain,s,[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.State}
1426
1427def pad30_correct(r,remain,index,s,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):
1428  (a,w30) = pair
1429  pad31_correct(r,remain,index,s,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)))
1430
1431law pad29_correct:
1432  for +r: Nat
1433  for +remain: Nat
1434  for +index: U32
1435  for +s: T.State
1436  for +w0: U32
1437  for +w1: U32
1438  for +w2: U32
1439  for +w3: U32
1440  for +w4: U32
1441  for +w5: U32
1442  for +w6: U32
1443  for +w7: U32
1444  for +w8: U32
1445  for +w9: U32
1446  for +w10: U32
1447  for +w11: U32
1448  for +w12: U32
1449  for +w13: U32
1450  for +w14: U32
1451  for +w15: U32
1452  for +w16: U32
1453  for +w17: U32
1454  for +w18: U32
1455  for +w19: U32
1456  for +w20: U32
1457  for +w21: U32
1458  for +w22: U32
1459  for +w23: U32
1460  for +w24: U32
1461  for +w25: U32
1462  for +w26: U32
1463  for +w27: U32
1464  for +w28: U32
1465  for pair: Array<U32> & U32
1466  {K.pad29(r,remain,index,s,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.State,R.gather(r,4n,index,30,True{},remain,s,[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.State}
1467
1468def pad29_correct(r,remain,index,s,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):
1469  (a,w29) = pair
1470  pad30_correct(r,remain,index,s,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)))
1471
1472law pad28_correct:
1473  for +r: Nat
1474  for +remain: Nat
1475  for +index: U32
1476  for +s: T.State
1477  for +w0: U32
1478  for +w1: U32
1479  for +w2: U32
1480  for +w3: U32
1481  for +w4: U32
1482  for +w5: U32
1483  for +w6: U32
1484  for +w7: U32
1485  for +w8: U32
1486  for +w9: U32
1487  for +w10: U32
1488  for +w11: U32
1489  for +w12: U32
1490  for +w13: U32
1491  for +w14: U32
1492  for +w15: U32
1493  for +w16: U32
1494  for +w17: U32
1495  for +w18: U32
1496  for +w19: U32
1497  for +w20: U32
1498  for +w21: U32
1499  for +w22: U32
1500  for +w23: U32
1501  for +w24: U32
1502  for +w25: U32
1503  for +w26: U32
1504  for +w27: U32
1505  for pair: Array<U32> & U32
1506  {K.pad28(r,remain,index,s,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.State,R.gather(r,5n,index,29,True{},remain,s,[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.State}
1507
1508def pad28_correct(r,remain,index,s,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):
1509  (a,w28) = pair
1510  pad29_correct(r,remain,index,s,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)))
1511
1512law pad27_correct:
1513  for +r: Nat
1514  for +remain: Nat
1515  for +index: U32
1516  for +s: T.State
1517  for +w0: U32
1518  for +w1: U32
1519  for +w2: U32
1520  for +w3: U32
1521  for +w4: U32
1522  for +w5: U32
1523  for +w6: U32
1524  for +w7: U32
1525  for +w8: U32
1526  for +w9: U32
1527  for +w10: U32
1528  for +w11: U32
1529  for +w12: U32
1530  for +w13: U32
1531  for +w14: U32
1532  for +w15: U32
1533  for +w16: U32
1534  for +w17: U32
1535  for +w18: U32
1536  for +w19: U32
1537  for +w20: U32
1538  for +w21: U32
1539  for +w22: U32
1540  for +w23: U32
1541  for +w24: U32
1542  for +w25: U32
1543  for +w26: U32
1544  for pair: Array<U32> & U32
1545  {K.pad27(r,remain,index,s,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.State,R.gather(r,6n,index,28,True{},remain,s,[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.State}
1546
1547def pad27_correct(r,remain,index,s,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):
1548  (a,w27) = pair
1549  pad28_correct(r,remain,index,s,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)))
1550
1551law pad26_correct:
1552  for +r: Nat
1553  for +remain: Nat
1554  for +index: U32
1555  for +s: T.State
1556  for +w0: U32
1557  for +w1: U32
1558  for +w2: U32
1559  for +w3: U32
1560  for +w4: U32
1561  for +w5: U32
1562  for +w6: U32
1563  for +w7: U32
1564  for +w8: U32
1565  for +w9: U32
1566  for +w10: U32
1567  for +w11: U32
1568  for +w12: U32
1569  for +w13: U32
1570  for +w14: U32
1571  for +w15: U32
1572  for +w16: U32
1573  for +w17: U32
1574  for +w18: U32
1575  for +w19: U32
1576  for +w20: U32
1577  for +w21: U32
1578  for +w22: U32
1579  for +w23: U32
1580  for +w24: U32
1581  for +w25: U32
1582  for pair: Array<U32> & U32
1583  {K.pad26(r,remain,index,s,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.State,R.gather(r,7n,index,27,True{},remain,s,[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.State}
1584
1585def pad26_correct(r,remain,index,s,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):
1586  (a,w26) = pair
1587  pad27_correct(r,remain,index,s,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)))
1588
1589law pad25_correct:
1590  for +r: Nat
1591  for +remain: Nat
1592  for +index: U32
1593  for +s: T.State
1594  for +w0: U32
1595  for +w1: U32
1596  for +w2: U32
1597  for +w3: U32
1598  for +w4: U32
1599  for +w5: U32
1600  for +w6: U32
1601  for +w7: U32
1602  for +w8: U32
1603  for +w9: U32
1604  for +w10: U32
1605  for +w11: U32
1606  for +w12: U32
1607  for +w13: U32
1608  for +w14: U32
1609  for +w15: U32
1610  for +w16: U32
1611  for +w17: U32
1612  for +w18: U32
1613  for +w19: U32
1614  for +w20: U32
1615  for +w21: U32
1616  for +w22: U32
1617  for +w23: U32
1618  for +w24: U32
1619  for pair: Array<U32> & U32
1620  {K.pad25(r,remain,index,s,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.State,R.gather(r,8n,index,26,True{},remain,s,[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.State}
1621
1622def pad25_correct(r,remain,index,s,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):
1623  (a,w25) = pair
1624  pad26_correct(r,remain,index,s,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)))
1625
1626law pad24_correct:
1627  for +r: Nat
1628  for +remain: Nat
1629  for +index: U32
1630  for +s: T.State
1631  for +w0: U32
1632  for +w1: U32
1633  for +w2: U32
1634  for +w3: U32
1635  for +w4: U32
1636  for +w5: U32
1637  for +w6: U32
1638  for +w7: U32
1639  for +w8: U32
1640  for +w9: U32
1641  for +w10: U32
1642  for +w11: U32
1643  for +w12: U32
1644  for +w13: U32
1645  for +w14: U32
1646  for +w15: U32
1647  for +w16: U32
1648  for +w17: U32
1649  for +w18: U32
1650  for +w19: U32
1651  for +w20: U32
1652  for +w21: U32
1653  for +w22: U32
1654  for +w23: U32
1655  for pair: Array<U32> & U32
1656  {K.pad24(r,remain,index,s,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.State,R.gather(r,9n,index,25,True{},remain,s,[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.State}
1657
1658def pad24_correct(r,remain,index,s,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):
1659  (a,w24) = pair
1660  pad25_correct(r,remain,index,s,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)))
1661
1662law pad23_correct:
1663  for +r: Nat
1664  for +remain: Nat
1665  for +index: U32
1666  for +s: T.State
1667  for +w0: U32
1668  for +w1: U32
1669  for +w2: U32
1670  for +w3: U32
1671  for +w4: U32
1672  for +w5: U32
1673  for +w6: U32
1674  for +w7: U32
1675  for +w8: U32
1676  for +w9: U32
1677  for +w10: U32
1678  for +w11: U32
1679  for +w12: U32
1680  for +w13: U32
1681  for +w14: U32
1682  for +w15: U32
1683  for +w16: U32
1684  for +w17: U32
1685  for +w18: U32
1686  for +w19: U32
1687  for +w20: U32
1688  for +w21: U32
1689  for +w22: U32
1690  for pair: Array<U32> & U32
1691  {K.pad23(r,remain,index,s,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.State,R.gather(r,10n,index,24,True{},remain,s,[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.State}
1692
1693def pad23_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair):
1694  (a,w23) = pair
1695  pad24_correct(r,remain,index,s,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)))
1696
1697law pad22_correct:
1698  for +r: Nat
1699  for +remain: Nat
1700  for +index: U32
1701  for +s: T.State
1702  for +w0: U32
1703  for +w1: U32
1704  for +w2: U32
1705  for +w3: U32
1706  for +w4: U32
1707  for +w5: U32
1708  for +w6: U32
1709  for +w7: U32
1710  for +w8: U32
1711  for +w9: U32
1712  for +w10: U32
1713  for +w11: U32
1714  for +w12: U32
1715  for +w13: U32
1716  for +w14: U32
1717  for +w15: U32
1718  for +w16: U32
1719  for +w17: U32
1720  for +w18: U32
1721  for +w19: U32
1722  for +w20: U32
1723  for +w21: U32
1724  for pair: Array<U32> & U32
1725  {K.pad22(r,remain,index,s,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.State,R.gather(r,11n,index,23,True{},remain,s,[w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1726
1727def pad22_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair):
1728  (a,w22) = pair
1729  pad23_correct(r,remain,index,s,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)))
1730
1731law pad21_correct:
1732  for +r: Nat
1733  for +remain: Nat
1734  for +index: U32
1735  for +s: T.State
1736  for +w0: U32
1737  for +w1: U32
1738  for +w2: U32
1739  for +w3: U32
1740  for +w4: U32
1741  for +w5: U32
1742  for +w6: U32
1743  for +w7: U32
1744  for +w8: U32
1745  for +w9: U32
1746  for +w10: U32
1747  for +w11: U32
1748  for +w12: U32
1749  for +w13: U32
1750  for +w14: U32
1751  for +w15: U32
1752  for +w16: U32
1753  for +w17: U32
1754  for +w18: U32
1755  for +w19: U32
1756  for +w20: U32
1757  for pair: Array<U32> & U32
1758  {K.pad21(r,remain,index,s,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.State,R.gather(r,12n,index,22,True{},remain,s,[w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1759
1760def pad21_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair):
1761  (a,w21) = pair
1762  pad22_correct(r,remain,index,s,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)))
1763
1764law pad20_correct:
1765  for +r: Nat
1766  for +remain: Nat
1767  for +index: U32
1768  for +s: T.State
1769  for +w0: U32
1770  for +w1: U32
1771  for +w2: U32
1772  for +w3: U32
1773  for +w4: U32
1774  for +w5: U32
1775  for +w6: U32
1776  for +w7: U32
1777  for +w8: U32
1778  for +w9: U32
1779  for +w10: U32
1780  for +w11: U32
1781  for +w12: U32
1782  for +w13: U32
1783  for +w14: U32
1784  for +w15: U32
1785  for +w16: U32
1786  for +w17: U32
1787  for +w18: U32
1788  for +w19: U32
1789  for pair: Array<U32> & U32
1790  {K.pad20(r,remain,index,s,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.State,R.gather(r,13n,index,21,True{},remain,s,[w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1791
1792def pad20_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair):
1793  (a,w20) = pair
1794  pad21_correct(r,remain,index,s,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)))
1795
1796law pad19_correct:
1797  for +r: Nat
1798  for +remain: Nat
1799  for +index: U32
1800  for +s: T.State
1801  for +w0: U32
1802  for +w1: U32
1803  for +w2: U32
1804  for +w3: U32
1805  for +w4: U32
1806  for +w5: U32
1807  for +w6: U32
1808  for +w7: U32
1809  for +w8: U32
1810  for +w9: U32
1811  for +w10: U32
1812  for +w11: U32
1813  for +w12: U32
1814  for +w13: U32
1815  for +w14: U32
1816  for +w15: U32
1817  for +w16: U32
1818  for +w17: U32
1819  for +w18: U32
1820  for pair: Array<U32> & U32
1821  {K.pad19(r,remain,index,s,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.State,R.gather(r,14n,index,20,True{},remain,s,[w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1822
1823def pad19_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair):
1824  (a,w19) = pair
1825  pad20_correct(r,remain,index,s,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)))
1826
1827law pad18_correct:
1828  for +r: Nat
1829  for +remain: Nat
1830  for +index: U32
1831  for +s: T.State
1832  for +w0: U32
1833  for +w1: U32
1834  for +w2: U32
1835  for +w3: U32
1836  for +w4: U32
1837  for +w5: U32
1838  for +w6: U32
1839  for +w7: U32
1840  for +w8: U32
1841  for +w9: U32
1842  for +w10: U32
1843  for +w11: U32
1844  for +w12: U32
1845  for +w13: U32
1846  for +w14: U32
1847  for +w15: U32
1848  for +w16: U32
1849  for +w17: U32
1850  for pair: Array<U32> & U32
1851  {K.pad18(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,15n,index,19,True{},remain,s,[w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1852
1853def pad18_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair):
1854  (a,w18) = pair
1855  pad19_correct(r,remain,index,s,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)))
1856
1857law pad17_correct:
1858  for +r: Nat
1859  for +remain: Nat
1860  for +index: U32
1861  for +s: T.State
1862  for +w0: U32
1863  for +w1: U32
1864  for +w2: U32
1865  for +w3: U32
1866  for +w4: U32
1867  for +w5: U32
1868  for +w6: U32
1869  for +w7: U32
1870  for +w8: U32
1871  for +w9: U32
1872  for +w10: U32
1873  for +w11: U32
1874  for +w12: U32
1875  for +w13: U32
1876  for +w14: U32
1877  for +w15: U32
1878  for +w16: U32
1879  for pair: Array<U32> & U32
1880  {K.pad17(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,16n,index,18,True{},remain,s,[w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1881
1882def pad17_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair):
1883  (a,w17) = pair
1884  pad18_correct(r,remain,index,s,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)))
1885
1886law pad16_correct:
1887  for +r: Nat
1888  for +remain: Nat
1889  for +index: U32
1890  for +s: T.State
1891  for +w0: U32
1892  for +w1: U32
1893  for +w2: U32
1894  for +w3: U32
1895  for +w4: U32
1896  for +w5: U32
1897  for +w6: U32
1898  for +w7: U32
1899  for +w8: U32
1900  for +w9: U32
1901  for +w10: U32
1902  for +w11: U32
1903  for +w12: U32
1904  for +w13: U32
1905  for +w14: U32
1906  for +w15: U32
1907  for pair: Array<U32> & U32
1908  {K.pad16(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,17n,index,17,True{},remain,s,[w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1909
1910def pad16_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair):
1911  (a,w16) = pair
1912  pad17_correct(r,remain,index,s,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)))
1913
1914law pad15_correct:
1915  for +r: Nat
1916  for +remain: Nat
1917  for +index: U32
1918  for +s: T.State
1919  for +w0: U32
1920  for +w1: U32
1921  for +w2: U32
1922  for +w3: U32
1923  for +w4: U32
1924  for +w5: U32
1925  for +w6: U32
1926  for +w7: U32
1927  for +w8: U32
1928  for +w9: U32
1929  for +w10: U32
1930  for +w11: U32
1931  for +w12: U32
1932  for +w13: U32
1933  for +w14: U32
1934  for pair: Array<U32> & U32
1935  {K.pad15(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,18n,index,16,True{},remain,s,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1936
1937def pad15_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
1938  (a,w15) = pair
1939  pad16_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
1940
1941law pad14_correct:
1942  for +r: Nat
1943  for +remain: Nat
1944  for +index: U32
1945  for +s: T.State
1946  for +w0: U32
1947  for +w1: U32
1948  for +w2: U32
1949  for +w3: U32
1950  for +w4: U32
1951  for +w5: U32
1952  for +w6: U32
1953  for +w7: U32
1954  for +w8: U32
1955  for +w9: U32
1956  for +w10: U32
1957  for +w11: U32
1958  for +w12: U32
1959  for +w13: U32
1960  for pair: Array<U32> & U32
1961  {K.pad14(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,19n,index,15,True{},remain,s,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1962
1963def pad14_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
1964  (a,w14) = pair
1965  pad15_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
1966
1967law pad13_correct:
1968  for +r: Nat
1969  for +remain: Nat
1970  for +index: U32
1971  for +s: T.State
1972  for +w0: U32
1973  for +w1: U32
1974  for +w2: U32
1975  for +w3: U32
1976  for +w4: U32
1977  for +w5: U32
1978  for +w6: U32
1979  for +w7: U32
1980  for +w8: U32
1981  for +w9: U32
1982  for +w10: U32
1983  for +w11: U32
1984  for +w12: U32
1985  for pair: Array<U32> & U32
1986  {K.pad13(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,20n,index,14,True{},remain,s,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
1987
1988def pad13_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
1989  (a,w13) = pair
1990  pad14_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
1991
1992law pad12_correct:
1993  for +r: Nat
1994  for +remain: Nat
1995  for +index: U32
1996  for +s: T.State
1997  for +w0: U32
1998  for +w1: U32
1999  for +w2: U32
2000  for +w3: U32
2001  for +w4: U32
2002  for +w5: U32
2003  for +w6: U32
2004  for +w7: U32
2005  for +w8: U32
2006  for +w9: U32
2007  for +w10: U32
2008  for +w11: U32
2009  for pair: Array<U32> & U32
2010  {K.pad12(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,21n,index,13,True{},remain,s,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
2011
2012def pad12_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
2013  (a,w12) = pair
2014  pad13_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
2015
2016law pad11_correct:
2017  for +r: Nat
2018  for +remain: Nat
2019  for +index: U32
2020  for +s: T.State
2021  for +w0: U32
2022  for +w1: U32
2023  for +w2: U32
2024  for +w3: U32
2025  for +w4: U32
2026  for +w5: U32
2027  for +w6: U32
2028  for +w7: U32
2029  for +w8: U32
2030  for +w9: U32
2031  for +w10: U32
2032  for pair: Array<U32> & U32
2033  {K.pad11(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,22n,index,12,True{},remain,s,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
2034
2035def pad11_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
2036  (a,w11) = pair
2037  pad12_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
2038
2039law pad10_correct:
2040  for +r: Nat
2041  for +remain: Nat
2042  for +index: U32
2043  for +s: T.State
2044  for +w0: U32
2045  for +w1: U32
2046  for +w2: U32
2047  for +w3: U32
2048  for +w4: U32
2049  for +w5: U32
2050  for +w6: U32
2051  for +w7: U32
2052  for +w8: U32
2053  for +w9: U32
2054  for pair: Array<U32> & U32
2055  {K.pad10(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,23n,index,11,True{},remain,s,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
2056
2057def pad10_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
2058  (a,w10) = pair
2059  pad11_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
2060
2061law pad9_correct:
2062  for +r: Nat
2063  for +remain: Nat
2064  for +index: U32
2065  for +s: T.State
2066  for +w0: U32
2067  for +w1: U32
2068  for +w2: U32
2069  for +w3: U32
2070  for +w4: U32
2071  for +w5: U32
2072  for +w6: U32
2073  for +w7: U32
2074  for +w8: U32
2075  for pair: Array<U32> & U32
2076  {K.pad9(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,24n,index,10,True{},remain,s,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
2077
2078def pad9_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
2079  (a,w9) = pair
2080  pad10_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
2081
2082law pad8_correct:
2083  for +r: Nat
2084  for +remain: Nat
2085  for +index: U32
2086  for +s: T.State
2087  for +w0: U32
2088  for +w1: U32
2089  for +w2: U32
2090  for +w3: U32
2091  for +w4: U32
2092  for +w5: U32
2093  for +w6: U32
2094  for +w7: U32
2095  for pair: Array<U32> & U32
2096  {K.pad8(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,25n,index,9,True{},remain,s,[w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
2097
2098def pad8_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,pair):
2099  (a,w8) = pair
2100  pad9_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
2101
2102law pad7_correct:
2103  for +r: Nat
2104  for +remain: Nat
2105  for +index: U32
2106  for +s: T.State
2107  for +w0: U32
2108  for +w1: U32
2109  for +w2: U32
2110  for +w3: U32
2111  for +w4: U32
2112  for +w5: U32
2113  for +w6: U32
2114  for pair: Array<U32> & U32
2115  {K.pad7(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,26n,index,8,True{},remain,s,[w6,w5,w4,w3,w2,w1,w0],pair)) : T.State}
2116
2117def pad7_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,pair):
2118  (a,w7) = pair
2119  pad8_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
2120
2121law pad6_correct:
2122  for +r: Nat
2123  for +remain: Nat
2124  for +index: U32
2125  for +s: T.State
2126  for +w0: U32
2127  for +w1: U32
2128  for +w2: U32
2129  for +w3: U32
2130  for +w4: U32
2131  for +w5: U32
2132  for pair: Array<U32> & U32
2133  {K.pad6(r,remain,index,s,w0,w1,w2,w3,w4,w5,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,27n,index,7,True{},remain,s,[w5,w4,w3,w2,w1,w0],pair)) : T.State}
2134
2135def pad6_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,pair):
2136  (a,w6) = pair
2137  pad7_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
2138
2139law pad5_correct:
2140  for +r: Nat
2141  for +remain: Nat
2142  for +index: U32
2143  for +s: T.State
2144  for +w0: U32
2145  for +w1: U32
2146  for +w2: U32
2147  for +w3: U32
2148  for +w4: U32
2149  for pair: Array<U32> & U32
2150  {K.pad5(r,remain,index,s,w0,w1,w2,w3,w4,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,28n,index,6,True{},remain,s,[w4,w3,w2,w1,w0],pair)) : T.State}
2151
2152def pad5_correct(r,remain,index,s,w0,w1,w2,w3,w4,pair):
2153  (a,w5) = pair
2154  pad6_correct(r,remain,index,s,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
2155
2156law pad4_correct:
2157  for +r: Nat
2158  for +remain: Nat
2159  for +index: U32
2160  for +s: T.State
2161  for +w0: U32
2162  for +w1: U32
2163  for +w2: U32
2164  for +w3: U32
2165  for pair: Array<U32> & U32
2166  {K.pad4(r,remain,index,s,w0,w1,w2,w3,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,29n,index,5,True{},remain,s,[w3,w2,w1,w0],pair)) : T.State}
2167
2168def pad4_correct(r,remain,index,s,w0,w1,w2,w3,pair):
2169  (a,w4) = pair
2170  pad5_correct(r,remain,index,s,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
2171
2172law pad3_correct:
2173  for +r: Nat
2174  for +remain: Nat
2175  for +index: U32
2176  for +s: T.State
2177  for +w0: U32
2178  for +w1: U32
2179  for +w2: U32
2180  for pair: Array<U32> & U32
2181  {K.pad3(r,remain,index,s,w0,w1,w2,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,30n,index,4,True{},remain,s,[w2,w1,w0],pair)) : T.State}
2182
2183def pad3_correct(r,remain,index,s,w0,w1,w2,pair):
2184  (a,w3) = pair
2185  pad4_correct(r,remain,index,s,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
2186
2187law pad2_correct:
2188  for +r: Nat
2189  for +remain: Nat
2190  for +index: U32
2191  for +s: T.State
2192  for +w0: U32
2193  for +w1: U32
2194  for pair: Array<U32> & U32
2195  {K.pad2(r,remain,index,s,w0,w1,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,31n,index,3,True{},remain,s,[w1,w0],pair)) : T.State}
2196
2197def pad2_correct(r,remain,index,s,w0,w1,pair):
2198  (a,w2) = pair
2199  pad3_correct(r,remain,index,s,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
2200
2201law pad1_correct:
2202  for +r: Nat
2203  for +remain: Nat
2204  for +index: U32
2205  for +s: T.State
2206  for +w0: U32
2207  for pair: Array<U32> & U32
2208  {K.pad1(r,remain,index,s,w0,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,32n,index,2,True{},remain,s,[w0],pair)) : T.State}
2209
2210def pad1_correct(r,remain,index,s,w0,pair):
2211  (a,w1) = pair
2212  pad2_correct(r,remain,index,s,w0,w1,Array.get(U32,a,U32.add(index,2)))
2213
2214law pad0_correct:
2215  for +r: Nat
2216  for +remain: Nat
2217  for +index: U32
2218  for +s: T.State
2219  for pair: Array<U32> & U32
2220  {K.pad0(r,remain,index,s,pair) == Pair.snd(Array<U32>,T.State,R.gather(r,33n,index,1,True{},remain,s,[],pair)) : T.State}
2221
2222def pad0_correct(r,remain,index,s,pair):
2223  (a,w0) = pair
2224  pad1_correct(r,remain,index,s,w0,Array.get(U32,a,U32.add(index,1)))
2225
2226
2227law absorb_correct:
2228  for +r: Nat
2229  for a: Array<U32>
2230  for +index: U32
2231  for +s: T.State
2232  {K.absorb(r,a,index,s) == R.absorb(r,a,index,s) : Array<U32> & T.State}
2233
2234def absorb_correct(r,a,index,s):
2235  read0_correct(r,index,s,Array.get(U32,a,index))
2236
2237law finish_correct:
2238  for +r: Nat
2239  for a: Array<U32>
2240  for +index: U32
2241  for +remain: Nat
2242  for +s: T.State
2243  {K.finish(r,a,index,remain,s) == R.finish(r,a,index,remain,s) : T.State}
2244
2245def finish_correct(r,a,index,remain,s):
2246  pad0_correct(r,remain,index,s,Array.get(U32,a,index))
2247
2248law blocks_correct:
2249  for +r: Nat
2250  for +n: Nat
2251  for +index: U32
2252  for +remain: Nat
2253  for pair: Array<U32> & T.State
2254  {K.blocks(r,n,index,remain,pair) == R.blocks(r,n,index,remain,pair) : T.State}
2255
2256law blocks_step:
2257  for +r: Nat
2258  for +n: Nat
2259  for +index: U32
2260  for +remain: Nat
2261  for -a: Array<U32>
2262  for +s: T.State
2263  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
2264  for recurse: @pair: (Array<U32> & T.State) -> {K.blocks(r,n,U32.add(index,34),remain,pair) == R.blocks(r,n,U32.add(index,34),remain,pair) : T.State}
2265  {K.blocks(r,1n+n,index,remain,(a,s)) == R.blocks(r,1n+n,index,remain,(a,s)) : T.State}
2266
2267def blocks_step(r,n,index,remain,a,s,view,recurse):
2268  match view:
2269    case Tuple{+tree,pf}:
2270      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.blocks(r,1n+n,index,remain,(_,s)) == R.blocks(r,1n+n,index,remain,(_,s)) : T.State}
2271      Equal.trans(T.State,
2272        K.blocks(r,n,U32.add(index,34),remain,K.absorb(r,A.thaw(tree),index,s)),
2273        R.blocks(r,n,U32.add(index,34),remain,K.absorb(r,A.thaw(tree),index,s)),
2274        R.blocks(r,n,U32.add(index,34),remain,R.absorb(r,A.thaw(tree),index,s)),
2275        recurse(K.absorb(r,A.thaw(tree),index,s)),
2276        Equal.cong(Array<U32> & T.State,T.State,pair => R.blocks(r,n,U32.add(index,34),remain,pair),
2277          K.absorb(r,A.thaw(tree),index,s),R.absorb(r,A.thaw(tree),index,s),absorb_correct(r,A.thaw(tree),index,s)))
2278
2279def blocks_correct(r,n,index,remain,pair):
2280  match n pair:
2281    case 0n Tuple{a,s}: finish_correct(r,a,index,remain,s)
2282    case 1n+p Tuple{a,s}:
2283      blocks_step(r,p,index,remain,a,s,A.reify(a),pair => blocks_correct(r,p,U32.add(index,34),remain,pair))
2284
2285law unchecked_correct:
2286  for +r: Nat
2287  for a: Array<U32>
2288  for +length: Nat
2289  {K.unchecked(r,a,length) == R.unchecked(r,a,length) : T.State}
2290
2291def unchecked_correct(r,a,length):
2292  blocks_correct(r,Nat.div(length,136n),0,Nat.mod(length,136n),(a,P.initial()))
2293
2294law digest_correct:
2295  for +s: T.State
2296  {K.digest(s) == R.digest(s) : Array<U32>}
2297
2298def digest_correct(s):
2299  match s:
2300    case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
2301
2302law checked_true_reified:
2303  for +r: Nat
2304  for -a: Array<U32>
2305  for +length: Nat
2306  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
2307  {K.checked(r,True{},a,length) == R.checked(r,True{},a,length) : Maybe<&1,Array<U32>>}
2308
2309def checked_true_reified(r,a,length,view):
2310  match view:
2311    case Tuple{+tree,pf}:
2312      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.checked(r,True{},_,length) == R.checked(r,True{},_,length) : Maybe<&1,Array<U32>>}
2313      Equal.trans(Maybe<&1,Array<U32>>,
2314        Some{K.digest(K.unchecked(r,A.thaw(tree),length))},
2315        Some{K.digest(R.unchecked(r,A.thaw(tree),length))},
2316        Some{R.digest(R.unchecked(r,A.thaw(tree),length))},
2317        Equal.cong(T.State,Maybe<&1,Array<U32>>,s => Some{K.digest(s)},K.unchecked(r,A.thaw(tree),length),R.unchecked(r,A.thaw(tree),length),unchecked_correct(r,A.thaw(tree),length)),
2318        Equal.cong(Array<U32>,Maybe<&1,Array<U32>>,a => Some{a},K.digest(R.unchecked(r,A.thaw(tree),length)),R.digest(R.unchecked(r,A.thaw(tree),length)),digest_correct(R.unchecked(r,A.thaw(tree),length))))
2319
2320law checked_correct:
2321  for +r: Nat
2322  for +valid: Bool
2323  for a: Array<U32>
2324  for +length: Nat
2325  {K.checked(r,valid,a,length) == R.checked(r,valid,a,length) : Maybe<&1,Array<U32>>}
2326
2327def checked_correct(r,valid,a,length):
2328  match valid:
2329    case False{}: {==}
2330    case True{}: checked_true_reified(r,a,length,A.reify(a))
2331
2332law sized_correct:
2333  for +r: Nat
2334  for +length: Nat
2335  for pair: Array<U32> & U32
2336  {K.sized(r,length,pair) == R.sized(r,length,pair) : Maybe<&1,Array<U32>>}
2337
2338def sized_correct(r,length,pair):
2339  (a,capacity) = pair
2340  checked_correct(r,Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
2341
2342law hash_correct:
2343  for +r: Nat
2344  for a: Array<U32>
2345  for +length: Nat
2346  {K.keccak256_rounds(r,a,length) == R.keccak256_rounds(r,a,length) : Maybe<&1,Array<U32>>}
2347
2348def hash_correct(r,a,length):
2349  sized_correct(r,length,Array.size(U32,a))
2350
2351law ethereum_round_count:
2352  for a: Array<U32>
2353  for +length: Nat
2354  {K.keccak256(a,length) == K.keccak256_rounds(24n,a,length) : Maybe<&1,Array<U32>>}
2355
2356def ethereum_round_count(a,length): {==}
2357
2358law public_correct:
2359  for a: Array<U32>
2360  for +length: Nat
2361  {K.keccak256(a,length) == R.keccak256_rounds(24n,a,length) : Maybe<&1,Array<U32>>}
2362
2363def public_correct(a,length): hash_correct(24n,a,length)