law digest_octets_length

bend-collections@1.0.0.0 · proofs/crypto/sha/correctness.bend:15

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

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