proofs/crypto/sha3/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 15 lines · 0 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as C
3import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/conformance.bend as Conformance
4import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/laws.bend as Laws
5
6# Gate for the SHA3-256 package: `bend proofs/crypto/sha3/proof.bend` prints
7# ALL PROOFS CHECK when every law of laws.bend holds. The conformance is
8# proved for every round count; SHA3-256 instantiates 24.
9
10def Laws.sha3_256_correct(bytes):
11  Conformance.keccak_correct(bytes, 24n)
12
13def Laws.sha3_256_length(bytes):
14  Conformance.digest_length(C.absorb(C.lanes(List.append(&2, U32, bytes,
15    C.suffix(List.length(&2, U32, bytes)))), 24n, C.zero()))