1 # Generated by tools/generators/blake2s_gen.py; do not edit. 2 # The unrolled compression function refines the list-based RFC 7693 F. 3 # 4 # The implementation runs ten explicit rounds. A proof-side model runs the 5 # same round function r times, selecting the permuted words by round index; 6 # for an abstract r both the model and the specification stay symbolic, so 7 # every comparison below is between one round at most. The theorem is then 8 # instantiated at r = 10, where the model coincides with the implementation. 9 import Base 10 import ../../../../src/crypto/blake/blake2s/types.bend as T 11 import ../../../../src/crypto/blake/blake2s/compress.bend as C 12 import ../../../../spec/crypto/blake/blake2s.bend as R 13 14 # The work vector as the RFC list v[0..15], one projection per entry, so 15 # that the list has its shape even when the vector is abstract. 16 def p0(v: T.Vector) -> U32: 17 match v: 18 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a0 19 20 def p1(v: T.Vector) -> U32: 21 match v: 22 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a1 23 24 def p2(v: T.Vector) -> U32: 25 match v: 26 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a2 27 28 def p3(v: T.Vector) -> U32: 29 match v: 30 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a3 31 32 def p4(v: T.Vector) -> U32: 33 match v: 34 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a4 35 36 def p5(v: T.Vector) -> U32: 37 match v: 38 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a5 39 40 def p6(v: T.Vector) -> U32: 41 match v: 42 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a6 43 44 def p7(v: T.Vector) -> U32: 45 match v: 46 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a7 47 48 def p8(v: T.Vector) -> U32: 49 match v: 50 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a8 51 52 def p9(v: T.Vector) -> U32: 53 match v: 54 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a9 55 56 def p10(v: T.Vector) -> U32: 57 match v: 58 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a10 59 60 def p11(v: T.Vector) -> U32: 61 match v: 62 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a11 63 64 def p12(v: T.Vector) -> U32: 65 match v: 66 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a12 67 68 def p13(v: T.Vector) -> U32: 69 match v: 70 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a13 71 72 def p14(v: T.Vector) -> U32: 73 match v: 74 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a14 75 76 def p15(v: T.Vector) -> U32: 77 match v: 78 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a15 79 80 def vec(+v: T.Vector) -> List<&2,U32>: 81 [p0(v),p1(v),p2(v),p3(v),p4(v),p5(v),p6(v),p7(v),p8(v),p9(v),p10(v),p11(v),p12(v),p13(v),p14(v),p15(v)] 82 83 # Model: round i of the implementation reads the words in SIGMA[i mod 10] order. 84 def round_at(i: Nat, v: T.Vector,+m0: U32,+m1: U32,+m2: U32,+m3: U32,+m4: U32,+m5: U32,+m6: U32,+m7: U32,+m8: U32,+m9: U32,+m10: U32,+m11: U32,+m12: U32,+m13: U32,+m14: U32,+m15: U32) -> T.Vector: 85 match i: 86 case 0n: C.round(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 87 case 1n: C.round(v,m14,m10,m4,m8,m9,m15,m13,m6,m1,m12,m0,m2,m11,m7,m5,m3) 88 case 2n: C.round(v,m11,m8,m12,m0,m5,m2,m15,m13,m10,m14,m3,m6,m7,m1,m9,m4) 89 case 3n: C.round(v,m7,m9,m3,m1,m13,m12,m11,m14,m2,m6,m5,m10,m4,m0,m15,m8) 90 case 4n: C.round(v,m9,m0,m5,m7,m2,m4,m10,m15,m14,m1,m11,m12,m6,m8,m3,m13) 91 case 5n: C.round(v,m2,m12,m6,m10,m0,m11,m8,m3,m4,m13,m7,m5,m15,m14,m1,m9) 92 case 6n: C.round(v,m12,m5,m1,m15,m14,m13,m4,m10,m0,m7,m6,m3,m9,m2,m8,m11) 93 case 7n: C.round(v,m13,m11,m7,m14,m12,m1,m3,m9,m5,m0,m15,m4,m8,m6,m2,m10) 94 case 8n: C.round(v,m6,m15,m14,m9,m11,m3,m0,m8,m12,m2,m13,m7,m1,m4,m10,m5) 95 case 9n: C.round(v,m10,m2,m8,m4,m7,m6,m1,m5,m15,m11,m9,m14,m3,m12,m13,m0) 96 case 10n+p: round_at(p,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 97 98 def rounds(n: Nat, +i: Nat, v: T.Vector,+m0: U32,+m1: U32,+m2: U32,+m3: U32,+m4: U32,+m5: U32,+m6: U32,+m7: U32,+m8: U32,+m9: U32,+m10: U32,+m11: U32,+m12: U32,+m13: U32,+m14: U32,+m15: U32) -> T.Vector: 99 match n: 100 case 0n: v 101 case 1n+p: rounds(p,1n+i,round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 102 103 def model(+r: Nat, +h: T.State,+m0: U32,+m1: U32,+m2: U32,+m3: U32,+m4: U32,+m5: U32,+m6: U32,+m7: U32,+m8: U32,+m9: U32,+m10: U32,+m11: U32,+m12: U32,+m13: U32,+m14: U32,+m15: U32,t0: U32,t1: U32,last: Bool) -> T.State: 104 C.finish(h,rounds(r,0n,C.init(h,t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) 105 106 law round0_correct: 107 for +v: T.Vector 108 for +m0: U32 109 for +m1: U32 110 for +m2: U32 111 for +m3: U32 112 for +m4: U32 113 for +m5: U32 114 for +m6: U32 115 for +m7: U32 116 for +m8: U32 117 for +m9: U32 118 for +m10: U32 119 for +m11: U32 120 for +m12: U32 121 for +m13: U32 122 for +m14: U32 123 for +m15: U32 124 {vec(round_at(0n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(0n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 125 126 def round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 127 match v: 128 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 129 130 law round1_correct: 131 for +v: T.Vector 132 for +m0: U32 133 for +m1: U32 134 for +m2: U32 135 for +m3: U32 136 for +m4: U32 137 for +m5: U32 138 for +m6: U32 139 for +m7: U32 140 for +m8: U32 141 for +m9: U32 142 for +m10: U32 143 for +m11: U32 144 for +m12: U32 145 for +m13: U32 146 for +m14: U32 147 for +m15: U32 148 {vec(round_at(1n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(1n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 149 150 def round1_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 151 match v: 152 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 153 154 law round2_correct: 155 for +v: T.Vector 156 for +m0: U32 157 for +m1: U32 158 for +m2: U32 159 for +m3: U32 160 for +m4: U32 161 for +m5: U32 162 for +m6: U32 163 for +m7: U32 164 for +m8: U32 165 for +m9: U32 166 for +m10: U32 167 for +m11: U32 168 for +m12: U32 169 for +m13: U32 170 for +m14: U32 171 for +m15: U32 172 {vec(round_at(2n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(2n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 173 174 def round2_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 175 match v: 176 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 177 178 law round3_correct: 179 for +v: T.Vector 180 for +m0: U32 181 for +m1: U32 182 for +m2: U32 183 for +m3: U32 184 for +m4: U32 185 for +m5: U32 186 for +m6: U32 187 for +m7: U32 188 for +m8: U32 189 for +m9: U32 190 for +m10: U32 191 for +m11: U32 192 for +m12: U32 193 for +m13: U32 194 for +m14: U32 195 for +m15: U32 196 {vec(round_at(3n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(3n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 197 198 def round3_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 199 match v: 200 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 201 202 law round4_correct: 203 for +v: T.Vector 204 for +m0: U32 205 for +m1: U32 206 for +m2: U32 207 for +m3: U32 208 for +m4: U32 209 for +m5: U32 210 for +m6: U32 211 for +m7: U32 212 for +m8: U32 213 for +m9: U32 214 for +m10: U32 215 for +m11: U32 216 for +m12: U32 217 for +m13: U32 218 for +m14: U32 219 for +m15: U32 220 {vec(round_at(4n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(4n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 221 222 def round4_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 223 match v: 224 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 225 226 law round5_correct: 227 for +v: T.Vector 228 for +m0: U32 229 for +m1: U32 230 for +m2: U32 231 for +m3: U32 232 for +m4: U32 233 for +m5: U32 234 for +m6: U32 235 for +m7: U32 236 for +m8: U32 237 for +m9: U32 238 for +m10: U32 239 for +m11: U32 240 for +m12: U32 241 for +m13: U32 242 for +m14: U32 243 for +m15: U32 244 {vec(round_at(5n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(5n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 245 246 def round5_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 247 match v: 248 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 249 250 law round6_correct: 251 for +v: T.Vector 252 for +m0: U32 253 for +m1: U32 254 for +m2: U32 255 for +m3: U32 256 for +m4: U32 257 for +m5: U32 258 for +m6: U32 259 for +m7: U32 260 for +m8: U32 261 for +m9: U32 262 for +m10: U32 263 for +m11: U32 264 for +m12: U32 265 for +m13: U32 266 for +m14: U32 267 for +m15: U32 268 {vec(round_at(6n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(6n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 269 270 def round6_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 271 match v: 272 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 273 274 law round7_correct: 275 for +v: T.Vector 276 for +m0: U32 277 for +m1: U32 278 for +m2: U32 279 for +m3: U32 280 for +m4: U32 281 for +m5: U32 282 for +m6: U32 283 for +m7: U32 284 for +m8: U32 285 for +m9: U32 286 for +m10: U32 287 for +m11: U32 288 for +m12: U32 289 for +m13: U32 290 for +m14: U32 291 for +m15: U32 292 {vec(round_at(7n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(7n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 293 294 def round7_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 295 match v: 296 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 297 298 law round8_correct: 299 for +v: T.Vector 300 for +m0: U32 301 for +m1: U32 302 for +m2: U32 303 for +m3: U32 304 for +m4: U32 305 for +m5: U32 306 for +m6: U32 307 for +m7: U32 308 for +m8: U32 309 for +m9: U32 310 for +m10: U32 311 for +m11: U32 312 for +m12: U32 313 for +m13: U32 314 for +m14: U32 315 for +m15: U32 316 {vec(round_at(8n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(8n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 317 318 def round8_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 319 match v: 320 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 321 322 law round9_correct: 323 for +v: T.Vector 324 for +m0: U32 325 for +m1: U32 326 for +m2: U32 327 for +m3: U32 328 for +m4: U32 329 for +m5: U32 330 for +m6: U32 331 for +m7: U32 332 for +m8: U32 333 for +m9: U32 334 for +m10: U32 335 for +m11: U32 336 for +m12: U32 337 for +m13: U32 338 for +m14: U32 339 for +m15: U32 340 {vec(round_at(9n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(9n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 341 342 def round9_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 343 match v: 344 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 345 346 law round_correct: 347 for +i: Nat 348 for +v: T.Vector 349 for +m0: U32 350 for +m1: U32 351 for +m2: U32 352 for +m3: U32 353 for +m4: U32 354 for +m5: U32 355 for +m6: U32 356 for +m7: U32 357 for +m8: U32 358 for +m9: U32 359 for +m10: U32 360 for +m11: U32 361 for +m12: U32 362 for +m13: U32 363 for +m14: U32 364 for +m15: U32 365 {vec(round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(i),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 366 367 def round_correct(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 368 match i: 369 case 0n: round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 370 case 1n: round1_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 371 case 2n: round2_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 372 case 3n: round3_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 373 case 4n: round4_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 374 case 5n: round5_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 375 case 6n: round6_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 376 case 7n: round7_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 377 case 8n: round8_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 378 case 9n: round9_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 379 case 10n+p: round_correct(p,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) 380 381 law rounds_correct: 382 for +n: Nat 383 for +i: Nat 384 for +v: T.Vector 385 for +m0: U32 386 for +m1: U32 387 for +m2: U32 388 for +m3: U32 389 for +m4: U32 390 for +m5: U32 391 for +m6: U32 392 for +m7: U32 393 for +m8: U32 394 for +m9: U32 395 for +m10: U32 396 for +m11: U32 397 for +m12: U32 398 for +m13: U32 399 for +m14: U32 400 for +m15: U32 401 {vec(rounds(n,i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.rounds(n,i,vec(v),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>} 402 403 def rounds_correct(n,i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): 404 match n: 405 case 0n: {==} 406 case 1n+p: 407 Equal.trans(List<&2,U32>, 408 vec(rounds(p,1n+i,round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)), 409 R.rounds(p,1n+i,vec(round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]), 410 R.rounds(p,1n+i,R.round(vec(v),R.sigma(i),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]), 411 rounds_correct(p,1n+i,round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15), 412 Equal.cong(List<&2,U32>,List<&2,U32>,x => R.rounds(p,1n+i,x,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),vec(round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),R.round(vec(v),R.sigma(i),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),round_correct(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))) 413 414 def fin(h0: U32,h1: U32,h2: U32,h3: U32,h4: U32,h5: U32,h6: U32,h7: U32,+l: List<&2,U32>) -> T.State: 415 T.H{U32.xor(U32.xor(h0,R.get(l,0n)),R.get(l,8n)),U32.xor(U32.xor(h1,R.get(l,1n)),R.get(l,9n)),U32.xor(U32.xor(h2,R.get(l,2n)),R.get(l,10n)),U32.xor(U32.xor(h3,R.get(l,3n)),R.get(l,11n)),U32.xor(U32.xor(h4,R.get(l,4n)),R.get(l,12n)),U32.xor(U32.xor(h5,R.get(l,5n)),R.get(l,13n)),U32.xor(U32.xor(h6,R.get(l,6n)),R.get(l,14n)),U32.xor(U32.xor(h7,R.get(l,7n)),R.get(l,15n))} 416 417 law finish_correct: 418 for +h0: U32 419 for +h1: U32 420 for +h2: U32 421 for +h3: U32 422 for +h4: U32 423 for +h5: U32 424 for +h6: U32 425 for +h7: U32 426 for +v: T.Vector 427 {C.finish(T.H{h0,h1,h2,h3,h4,h5,h6,h7},v) == fin(h0,h1,h2,h3,h4,h5,h6,h7,vec(v)) : T.State} 428 429 def finish_correct(h0,h1,h2,h3,h4,h5,h6,h7,v): 430 match v: 431 case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==} 432 433 law init_correct: 434 for +h0: U32 435 for +h1: U32 436 for +h2: U32 437 for +h3: U32 438 for +h4: U32 439 for +h5: U32 440 for +h6: U32 441 for +h7: U32 442 for +t0: U32 443 for +t1: U32 444 for +last: Bool 445 {vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)) == R.invert(last,[h0,h1,h2,h3,h4,h5,h6,h7,1779033703,3144134277,1013904242,2773480762,U32.xor(1359893119,t0),U32.xor(2600822924,t1),528734635,1541459225]) : List<&2,U32>} 446 447 def init_correct(h0,h1,h2,h3,h4,h5,h6,h7,t0,t1,last): 448 match last: 449 case True{}: {==} 450 case False{}: {==} 451 452 law model_correct: 453 for +r: Nat 454 for +h: T.State 455 for +m0: U32 456 for +m1: U32 457 for +m2: U32 458 for +m3: U32 459 for +m4: U32 460 for +m5: U32 461 for +m6: U32 462 for +m7: U32 463 for +m8: U32 464 for +m9: U32 465 for +m10: U32 466 for +m11: U32 467 for +m12: U32 468 for +m13: U32 469 for +m14: U32 470 for +m15: U32 471 for +t0: U32 472 for +t1: U32 473 for +last: Bool 474 {model(r,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last) == R.compress(r,h,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last) : T.State} 475 476 def model_correct(r,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last): 477 match h: 478 case T.H{h0,h1,h2,h3,h4,h5,h6,h7}: 479 Equal.trans(T.State, 480 C.finish(T.H{h0,h1,h2,h3,h4,h5,h6,h7},rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)), 481 fin(h0,h1,h2,h3,h4,h5,h6,h7,vec(rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))), 482 R.compress(r,T.H{h0,h1,h2,h3,h4,h5,h6,h7},[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last), 483 finish_correct(h0,h1,h2,h3,h4,h5,h6,h7,rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)), 484 Equal.trans(T.State, 485 fin(h0,h1,h2,h3,h4,h5,h6,h7,vec(rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))), 486 fin(h0,h1,h2,h3,h4,h5,h6,h7,R.rounds(r,0n,vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15])), 487 R.compress(r,T.H{h0,h1,h2,h3,h4,h5,h6,h7},[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last), 488 Equal.cong(List<&2,U32>,T.State,l => fin(h0,h1,h2,h3,h4,h5,h6,h7,l),vec(rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),R.rounds(r,0n,vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),rounds_correct(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)), 489 Equal.cong(List<&2,U32>,T.State,l => fin(h0,h1,h2,h3,h4,h5,h6,h7,R.rounds(r,0n,l,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15])),vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)),R.invert(last,[h0,h1,h2,h3,h4,h5,h6,h7,1779033703,3144134277,1013904242,2773480762,U32.xor(1359893119,t0),U32.xor(2600822924,t1),528734635,1541459225]),init_correct(h0,h1,h2,h3,h4,h5,h6,h7,t0,t1,last)))) 490 491 # F as implemented (ten unrolled rounds) is F of the specification with r = 10. 492 law compress_correct: 493 for +h: T.State 494 for +m0: U32 495 for +m1: U32 496 for +m2: U32 497 for +m3: U32 498 for +m4: U32 499 for +m5: U32 500 for +m6: U32 501 for +m7: U32 502 for +m8: U32 503 for +m9: U32 504 for +m10: U32 505 for +m11: U32 506 for +m12: U32 507 for +m13: U32 508 for +m14: U32 509 for +m15: U32 510 for +t0: U32 511 for +t1: U32 512 for +last: Bool 513 {C.compress(h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last) == R.compress(10n,h,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last) : T.State} 514 515 def compress_correct(h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last): 516 Equal.trans(T.State,C.compress(h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last),model(10n,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last),R.compress(10n,h,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last), 517 {==},model_correct(10n,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last))