def fips_len
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/mac/hmac.bend:19
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend as Hmac
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as FIPS
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/correctness.bend as ShaCorrect
19def fips_len(+bytes: List<&2, U32>) -> {List.length(&2, U32, FIPS.sha256_bytes(bytes)) == 32n : Nat}:
20 ShaCorrect.digest_octets_length(FIPS.blocks(FIPS.prepare(bytes, 48n), FIPS.constants())(FIPS.initial()))