def hprime_eq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/hash.bend:116
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as Hash
import Base
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
116
117def hprime_eq(+tl: Nat, +a: List<&2, U32>) -> {I.hprime(tl, a) == SA.hprime(tl, a) : List<&2, U32>}:
118 hp_pick_eq(tl, SA.cat(SA.le32(tl), a), Nat.is_le(tl, 64n))