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