proofs/crypto/blake/blake2s/reads.bend

bend-collections-laws-crypto@1.0.0.0 · 945 lines · 48 definitions

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