law hash_correct

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

import Base
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/argon2/argon2.bend as SA

43# BLAKE2b with an nn-byte digest, H' and H0 (sections 3.2, 3.3).
44law hash_correct:
45  for +nn: Nat
46  for +bs: List<&2, U32>
47  {IH.hash(nn, bs) == SA.hash(nn, bs) : List<&2, U32>}