proofs/crypto/sha3/conformance.bend source
proofs/crypto/sha3/conformance.bend on the hub · documented module
# Generated by tools/generators/sha3_gen.py; do not edit by hand.import Baseimport ../../../src/crypto/keccak/types.bend as Timport ../../../src/crypto/keccak/permutation.bend as Pimport ../../../src/crypto/sha3/core.bend as Cimport ../../../spec/crypto/sha3.bend as Fimport ../../../spec/crypto/keccak/permutation.bend as Kimport ../keccak/permutation.bend as KP# src/crypto/sha3/core.bend refines spec/crypto/sha3.bend: the block XOR is# equal after opening every lane, the permutation is the Keccak package's# proved one (KP.rounds_correct, for every round count), and the absorbing,# the parsing, the padding and the squeeze follow by induction or unfolding.# The round count stays a variable until the end (24 is never unfolded).law inject_correct: for +s: T.State for +l0: T.Lane for +l1: T.Lane for +l2: T.Lane for +l3: T.Lane for +l4: T.Lane for +l5: T.Lane for +l6: T.Lane for +l7: T.Lane for +l8: T.Lane for +l9: T.Lane for +l10: T.Lane for +l11: T.Lane for +l12: T.Lane for +l13: T.Lane for +l14: T.Lane for +l15: T.Lane for +l16: T.Lane {C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16) == F.of_lanes(F.xor_lanes(F.to_lanes(s), [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16])) : T.State}def inject_correct(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16): match s l0 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 l11 l12 l13 l14 l15 l16: case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}} T.W{u0, v0} T.W{u1, v1} T.W{u2, v2} T.W{u3, v3} T.W{u4, v4} T.W{u5, v5} T.W{u6, v6} T.W{u7, v7} T.W{u8, v8} T.W{u9, v9} T.W{u10, v10} T.W{u11, v11} T.W{u12, v12} T.W{u13, v13} T.W{u14, v14} T.W{u15, v15} T.W{u16, v16}: {==}law absorb_correct: for +ls: List<&2, T.Lane> for +rounds: Nat for +s: T.State {C.absorb(ls, rounds, s) == F.absorb(ls, rounds, s) : T.State}def absorb_correct(ls, rounds, s): match ls: case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest: +x = F.of_lanes(F.xor_lanes(F.to_lanes(s), [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16])) %inject_correct(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16) : {C.absorb(l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest, rounds, s) == F.absorb(rest, rounds, K.rounds(rounds, 0n, _)) : T.State} %KP.rounds_correct(rounds, 0n, C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16)) : {C.absorb(l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest, rounds, s) == F.absorb(rest, rounds, _) : T.State} absorb_correct(rest, rounds, P.rounds(rounds, 0n, C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16))) case Nil{}: {==} case l0 <> Nil{}: {==} case l0 <> l1 <> Nil{}: {==} case l0 <> l1 <> l2 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> Nil{}: {==} case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> Nil{}: {==}law lanes_correct: for +bytes: List<&2, U32> {C.lanes(bytes) == F.lanes(bytes) : List<&2, T.Lane>}def lanes_correct(bytes): match bytes: case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest: %lanes_correct(rest) : {C.lanes(b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest) == T.W{F.le32(b0, b1, b2, b3), F.le32(b4, b5, b6, b7)} <> _ : List<&2, T.Lane>} {==} case Nil{}: {==} case b0 <> Nil{}: {==} case b0 <> b1 <> Nil{}: {==} case b0 <> b1 <> b2 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> b4 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> Nil{}: {==} case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> Nil{}: {==}law tail_correct: for +q: Nat {C.tail(q) == F.padding_bytes(q) : List<&2, U32>}def tail_correct(q): match q: case 0n: {==} case 1n: {==} case 2n+k: {==}law suffix_correct: for +n: Nat {C.suffix(n) == F.padding(n) : List<&2, U32>}def suffix_correct(n): tail_correct(Nat.sub(136n, Nat.mod(n, 136n)))law digest_correct: for +s: T.State {C.digest_bytes(s) == F.squeeze(s) : List<&2, U32>}def digest_correct(s): match s: case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}}: {==}law digest_length: for +s: T.State {List.length(&2, U32, C.digest_bytes(s)) == 32n : Nat}def digest_length(s): match s: case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}}: {==}law keccak_correct: for +bytes: List<&2, U32> for +rounds: Nat {C.keccak(bytes, rounds) == F.keccak(bytes, rounds) : List<&2, U32>}def keccak_correct(bytes, rounds): +n = List.length(&2, U32, bytes) %suffix_correct(n) : {C.keccak(bytes, rounds) == F.squeeze(F.absorb(F.lanes(List.append(&2, U32, bytes, _)), rounds, F.initial())) : List<&2, U32>} +padded = List.append(&2, U32, bytes, C.suffix(n)) %lanes_correct(padded) : {C.keccak(bytes, rounds) == F.squeeze(F.absorb(_, rounds, F.initial())) : List<&2, U32>} %absorb_correct(C.lanes(padded), rounds, C.zero()) : {C.keccak(bytes, rounds) == F.squeeze(_) : List<&2, U32>} digest_correct(C.absorb(C.lanes(padded), rounds, C.zero()))