proofs/crypto/blake/blake2s/compress.bend source
proofs/crypto/blake/blake2s/compress.bend on the hub · documented module
# Generated by tools/generators/blake2s_gen.py; do not edit.# The unrolled compression function refines the list-based RFC 7693 F.## The implementation runs ten explicit rounds. A proof-side model runs the# same round function r times, selecting the permuted words by round index;# for an abstract r both the model and the specification stay symbolic, so# every comparison below is between one round at most. The theorem is then# instantiated at r = 10, where the model coincides with the implementation.import Baseimport ../../../../src/crypto/blake/blake2s/types.bend as Timport ../../../../src/crypto/blake/blake2s/compress.bend as Cimport ../../../../spec/crypto/blake/blake2s.bend as R# The work vector as the RFC list v[0..15], one projection per entry, so# that the list has its shape even when the vector is abstract.def p0(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a0def p1(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a1def p2(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a2def p3(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a3def p4(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a4def p5(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a5def p6(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a6def p7(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a7def p8(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a8def p9(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a9def p10(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a10def p11(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a11def p12(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a12def p13(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a13def p14(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a14def p15(v: T.Vector) -> U32: match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a15def vec(+v: T.Vector) -> List<&2,U32>: [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)]# Model: round i of the implementation reads the words in SIGMA[i mod 10] order.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: match i: case 0n: C.round(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 1n: C.round(v,m14,m10,m4,m8,m9,m15,m13,m6,m1,m12,m0,m2,m11,m7,m5,m3) case 2n: C.round(v,m11,m8,m12,m0,m5,m2,m15,m13,m10,m14,m3,m6,m7,m1,m9,m4) case 3n: C.round(v,m7,m9,m3,m1,m13,m12,m11,m14,m2,m6,m5,m10,m4,m0,m15,m8) case 4n: C.round(v,m9,m0,m5,m7,m2,m4,m10,m15,m14,m1,m11,m12,m6,m8,m3,m13) case 5n: C.round(v,m2,m12,m6,m10,m0,m11,m8,m3,m4,m13,m7,m5,m15,m14,m1,m9) case 6n: C.round(v,m12,m5,m1,m15,m14,m13,m4,m10,m0,m7,m6,m3,m9,m2,m8,m11) case 7n: C.round(v,m13,m11,m7,m14,m12,m1,m3,m9,m5,m0,m15,m4,m8,m6,m2,m10) case 8n: C.round(v,m6,m15,m14,m9,m11,m3,m0,m8,m12,m2,m13,m7,m1,m4,m10,m5) case 9n: C.round(v,m10,m2,m8,m4,m7,m6,m1,m5,m15,m11,m9,m14,m3,m12,m13,m0) case 10n+p: round_at(p,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)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: match n: case 0n: v 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)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: 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))law round0_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round1_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round1_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round2_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round2_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round3_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round3_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round4_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round4_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round5_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round5_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round6_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round6_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round7_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round7_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round8_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round8_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round9_correct: for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round9_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law round_correct: for +i: Nat for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def round_correct(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match i: case 0n: round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 1n: round1_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 2n: round2_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 3n: round3_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 4n: round4_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 5n: round5_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 6n: round6_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 7n: round7_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 8n: round8_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 9n: round9_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) case 10n+p: round_correct(p,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)law rounds_correct: for +n: Nat for +i: Nat for +v: T.Vector for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 {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>}def rounds_correct(n,i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15): match n: case 0n: {==} case 1n+p: Equal.trans(List<&2,U32>, 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)), 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]), 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]), 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), 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)))def fin(h0: U32,h1: U32,h2: U32,h3: U32,h4: U32,h5: U32,h6: U32,h7: U32,+l: List<&2,U32>) -> T.State: 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))}law finish_correct: for +h0: U32 for +h1: U32 for +h2: U32 for +h3: U32 for +h4: U32 for +h5: U32 for +h6: U32 for +h7: U32 for +v: T.Vector {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}def finish_correct(h0,h1,h2,h3,h4,h5,h6,h7,v): match v: case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law init_correct: for +h0: U32 for +h1: U32 for +h2: U32 for +h3: U32 for +h4: U32 for +h5: U32 for +h6: U32 for +h7: U32 for +t0: U32 for +t1: U32 for +last: Bool {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>}def init_correct(h0,h1,h2,h3,h4,h5,h6,h7,t0,t1,last): match last: case True{}: {==} case False{}: {==}law model_correct: for +r: Nat for +h: T.State for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 for +t0: U32 for +t1: U32 for +last: Bool {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}def model_correct(r,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last): match h: case T.H{h0,h1,h2,h3,h4,h5,h6,h7}: Equal.trans(T.State, 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)), 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))), 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), 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)), Equal.trans(T.State, 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))), 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])), 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), 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)), 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))))# F as implemented (ten unrolled rounds) is F of the specification with r = 10.law compress_correct: for +h: T.State for +m0: U32 for +m1: U32 for +m2: U32 for +m3: U32 for +m4: U32 for +m5: U32 for +m6: U32 for +m7: U32 for +m8: U32 for +m9: U32 for +m10: U32 for +m11: U32 for +m12: U32 for +m13: U32 for +m14: U32 for +m15: U32 for +t0: U32 for +t1: U32 for +last: Bool {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}def compress_correct(h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last): 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), {==},model_correct(10n,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last))