def init_block_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/run.bend:28

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I
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/argon2/hash.bend as HS

28def init_block_eq(+hh: List<&2, U32>, +i: Nat, +l: Nat) -> {I.block_of(I.hprime(1024n, I.cat(hh, I.cat(I.le32(i), I.le32(l))))) == SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(i), SA.le32(l))))) : A.Block}:
29  +x = SA.cat(hh, SA.cat(SA.le32(i), SA.le32(l)))
30  Equal.trans(A.Block, I.block_of(I.hprime(1024n, x)), I.block_of(SA.hprime(1024n, x)), SA.block_of(SA.hprime(1024n, x)),
31    Equal.cong(List<&2, U32>, A.Block, z => I.block_of(z), I.hprime(1024n, x), SA.hprime(1024n, x), HS.hprime_eq(1024n, x)),
32    HS.block_of_eq(SA.hprime(1024n, x)))