law digest_octets_length

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/proof.bend:17

import Base
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as State
import bend-collections@1.0.0.0/spec/crypto/sha.bend as FIPS

17law digest_octets_length:
18  for s: State.State
19  {List.length(&2, U32, FIPS.digest_octets(FIPS.digest(s))) == 32n : Nat}