def hash_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/hash.bend:79

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend as IB
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as IH
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as SBL
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/blocks.bend as BB

79def hash_eq(+nn: Nat, +bs: List<&2, U32>) -> {IH.hash(nn, bs) == SA.hash(nn, bs) : List<&2, U32>}:
80  +ll = List.length(&2, U32, bs)
81  +n = Nat.div(Nat.sub(ll, 1n), 128n)
82  +rem = Nat.sub(ll, Nat.mul(n, 128n))
83  +f = U32.from_nat(nn)
84  Equal.trans(List<&2, U32>, List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (IH.pack(bs), IH.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn), SA.hash(nn, bs),
85    Equal.trans(List<&2, U32>, List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (IH.pack(bs), IH.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), IH.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn),
86      Equal.cong(Array<U32>, List<&2, U32>, z => List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (z, IH.initial(f)))), nn), IH.pack(bs), SA.pack(bs), pack_eq(bs)),
87      Equal.cong(T.Chain, List<&2, U32>, z => List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), z))), nn), IH.initial(f), SA.initial(f), initial_eq(f))),
88    Equal.trans(List<&2, U32>, List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn), SA.hash(nn, bs),
89      Equal.cong(T.Chain, List<&2, U32>, z => List.take(&2, U32, IH.chain_bytes(z), nn), IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f))), SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f))), BB.blocks_correct(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))),
90      Equal.cong(List<&2, U32>, List<&2, U32>, z => List.take(&2, U32, z, nn), IH.chain_bytes(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), SA.chain_bytes(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), chain_bytes_eq(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))))))