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