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