~/bend-docscommunity

proofs/crypto/sha/correctness.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/correctness.bend as Correctness

6 imports
import Base
import ../../../src/crypto/sha/state.bend as State
import ../../../src/crypto/sha/sha256.bend as SHA
import ../../../spec/crypto/sha.bend as FIPS
import ./conformance.bend as Conformance
import ./laws.bend as Laws

Laws

law digest_octets_length provedsource · line 15 · raw

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