~/bend-docscommunity

CORRECTNESS.bend checks

raw source on the hub · import 0x3bdc0c9f5265bb49f7fc76b61f529f24/CORRECTNESS.bend as CORRECTNESS

8 imports
import Base
import ./buffer_proof.bend as BufferProof
import ./state.bend as State
import ./legacy_model.bend as SHA
import ./fips.bend as FIPS
import ./conformance.bend as Conformance
import ./packed_proof.bend as PackedProof
import ./LAWS.bend as Laws

Laws

law digest_octets_length provedsource · line 17 · raw

@s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {List.length(&2, U32, 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.digest_octets(0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.digest(s))) == 32n : Nat}