~/bend-docscommunity

proofs/crypto/sha/packed/proof.bend fails

raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/proof.bend as Proof

8 imports
import Base
import ./buffer_proof.bend as BufferProof
import ../../../../src/crypto/sha/state.bend as State
import ./legacy_model.bend as SHA
import ../../../../spec/crypto/sha.bend as FIPS
import ./conformance.bend as Conformance
import ./packed_proof.bend as PackedProof
import ./laws.bend as Laws

Laws

law digest_octets_length unverifiedits file does not pass the checker (fails)source · line 17 · raw

@s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> {List.length(&2, U32, 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.digest_octets(0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.digest(s))) == 32n : Nat}