1 import Base 2 import ../../../../src/crypto/sha/packed/core.bend as Runtime 3 import ./legacy_model.bend as Legacy 4 import ./packed_array_proof.bend as A 5 import ../../../../src/crypto/sha/packed/packed.bend as P 6 import ../../../../spec/crypto/sha/packed.bend as R 7 import ./core_model.bend as C 8 import ../../../../spec/crypto/sha.bend as F 9 import ../../../../src/crypto/sha/state.bend as S 10 import ./conformance.bend as Conformance 11 12 law 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 33 def 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 36 law 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 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 & S.State} 57 58 def 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 & 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 62 law 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 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 & S.State} 82 83 def 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 87 law 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 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 & S.State} 106 107 def 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 111 law 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 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 & S.State} 129 130 def 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 134 law 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 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 & S.State} 151 152 def 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 156 law 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 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 & S.State} 172 173 def 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 177 law 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 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 & S.State} 192 193 def 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 197 law 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 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 & S.State} 211 212 def 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 216 law 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 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 & S.State} 229 230 def 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 234 law 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 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 & S.State} 246 247 def 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 251 law 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 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 & S.State} 262 263 def 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 267 law 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 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 & S.State} 277 278 def 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 282 law 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 290 {P.read4(extra,index,s,w0,w1,w2,pair) == R.gather(extra,12n,index,False{},0n,0n,s,[w2,w1,w0],pair) : Array & S.State} 291 292 def 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 296 law 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 303 {P.read3(extra,index,s,w0,w1,pair) == R.gather(extra,13n,index,False{},0n,0n,s,[w1,w0],pair) : Array & S.State} 304 305 def 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 309 law read2_correct: 310 for +extra: Nat 311 for +index: U32 312 for +s: S.State 313 for +w0: U32 314 for pair: Array & U32 315 {P.read2(extra,index,s,w0,pair) == R.gather(extra,14n,index,False{},0n,0n,s,[w0],pair) : Array & S.State} 316 317 def 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 321 law read1_correct: 322 for +extra: Nat 323 for +index: U32 324 for +s: S.State 325 for pair: Array & U32 326 {P.read1(extra,index,s,pair) == R.gather(extra,15n,index,False{},0n,0n,s,Nil{},pair) : Array & S.State} 327 328 def 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 332 law partial_correct: 333 for +w: U32 334 for +delta: Nat 335 {P.partial(w,delta) == R.partial(w,delta) : U32} 336 def partial_correct(w,delta): 337 match delta: 338 case 0n: {==} 339 case 1n: {==} 340 case 2n: {==} 341 case 3n: {==} 342 case 4n+p: {==} 343 344 law 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} 349 def pad_choose_correct(c,w,delta): 350 match c: 351 case GT{}: {==} 352 case EQ{}: {==} 353 case LT{}: partial_correct(w,delta) 354 355 law 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} 360 def pad_word_correct(w,pos,remain): 361 pad_choose_correct(Nat.cmp(pos,remain),w,Nat.sub(remain,pos)) 362 363 law 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} 370 def tail_word_correct(short,w,pos,remain,length): 371 match short: 372 case True{}: {==} 373 case False{}: pad_word_correct(w,pos,remain) 374 375 law 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 396 def 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 431 law 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 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 & S.State} 454 455 def 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 & 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 & 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 & 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 467 law 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 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 & S.State} 489 490 def 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 494 law 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 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 & S.State} 515 516 def 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 520 law 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 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 & S.State} 540 541 def 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 545 law 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 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 & S.State} 564 565 def 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 569 law 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 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 & S.State} 587 588 def 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 592 law 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 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 & S.State} 609 610 def 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 614 law 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 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 & S.State} 630 631 def 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 635 law 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 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 & S.State} 650 651 def 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 655 law 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 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 & S.State} 669 670 def 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 674 law 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 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 & S.State} 687 688 def 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 692 law 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 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 & S.State} 704 705 def 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 709 law 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 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 & S.State} 720 721 def 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 725 law 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 734 {P.pad3(extra,index,s,remain,total,w0,w1,pair) == R.gather(extra,13n,index,True{},remain,total,s,[w1,w0],pair) : Array & S.State} 735 736 def 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 740 law 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 748 {P.pad2(extra,index,s,remain,total,w0,pair) == R.gather(extra,14n,index,True{},remain,total,s,[w0],pair) : Array & S.State} 749 750 def 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 754 law 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 761 {P.pad1(extra,index,s,remain,total,pair) == R.gather(extra,15n,index,True{},remain,total,s,Nil{},pair) : Array & S.State} 762 763 def 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 767 law final_extra_correct: 768 for +extra: Nat 769 for +more: Bool 770 for +total: Nat 771 for pair: Array & S.State 772 {P.final_extra(extra,more,total,pair) == R.final_extra(extra,more,total,pair) : Array & S.State} 773 774 def 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 & 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 783 law 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 & S.State 790 {P.blocks(extra,n,index,remain,total,pair) == R.blocks(extra,n,index,remain,total,pair) : Array & S.State} 791 792 law blocks_zero_reified: 793 for +extra: Nat 794 for +index: U32 795 for +remain: Nat 796 for +total: Nat 797 for -a: Array 798 for +s: S.State 799 for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array}> 800 {P.blocks(extra,0n,index,remain,total,(a,s)) == R.blocks(extra,0n,index,remain,total,(a,s)) : Array & S.State} 801 802 def blocks_zero_reified(extra,index,remain,total,a,s,view): 803 match view: 804 case Tuple{+tree,pf}: 805 %Equal.sym(Array,a,A.thaw(tree),pf) : {P.blocks(extra,0n,index,remain,total,(_,s)) == R.blocks(extra,0n,index,remain,total,(_,s)) : Array & S.State} 806 Equal.trans(Array & 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 & S.State,Array & 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 816 law 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 823 for +s: S.State 824 for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array}> 825 for recurse: @pair: (Array & 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 & S.State} 826 {P.blocks(extra,1n+p,index,remain,total,(a,s)) == R.blocks(extra,1n+p,index,remain,total,(a,s)) : Array & S.State} 827 828 def blocks_step_reified(p,extra,index,remain,total,a,s,view,recurse): 829 match view: 830 case Tuple{+tree,pf}: 831 %Equal.sym(Array,a,A.thaw(tree),pf) : {P.blocks(extra,1n+p,index,remain,total,(_,s)) == R.blocks(extra,1n+p,index,remain,total,(_,s)) : Array & S.State} 832 Equal.trans(Array & 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 & S.State,Array & 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 842 def 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 850 law hash_unchecked_correct: 851 for a: Array 852 for +length: Nat 853 {P.hash_unchecked(a,length) == R.hash_unchecked(a,length) : S.State} 854 855 def hash_unchecked_correct(a,length): 856 Equal.cong(Array & 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 861 law checked_correct: 862 for +valid: Bool 863 for a: Array 864 for +length: Nat 865 {P.checked(valid,a,length) == R.checked(valid,a,length) : Maybe<&2,S.State>} 866 867 def 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 874 law sized_correct: 875 for +length: Nat 876 for pair: Array & U32 877 {P.sized(length,pair) == R.sized(length,pair) : Maybe<&2,S.State>} 878 879 def 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 883 law hash_correct: 884 for a: Array 885 for +length: Nat 886 {P.hash(a,length) == R.hash(a,length) : Maybe<&2,S.State>} 887 888 def hash_correct(a,length): 889 sized_correct(length,Array.size(U32,a)) 890 891 law 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 895 def 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 902 law sha256_correct: 903 for a: Array 904 for +length: Nat 905 {Legacy.sha256_packed(a,length) == R.sha256(a,length) : Maybe<&2,List<&2,U32>>} 906 907 law sha256_reified: 908 for -a: Array 909 for +length: Nat 910 for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array}> 911 {Legacy.sha256_packed(a,length) == R.sha256(a,length) : Maybe<&2,List<&2,U32>>} 912 def sha256_reified(a,length,view): 913 match view: 914 case Tuple{+tree,pf}: 915 %Equal.sym(Array,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 922 def sha256_correct(a,length): 923 sha256_reified(a,length,A.reify(a))