proofs/crypto/sha3/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 16 lines · 2 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/sha3_256.bend as SHA3
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as FIPS
4
5# SHA3-256: the public API against the FIPS 202 specification
6# spec/crypto/sha3.bend (sponge on the specification's Keccak-p[1600, 24]).
7
8# The digest of every byte list is the specification's.
9law sha3_256_correct:
10  for +bytes: List<&2, U32>
11  {SHA3.sha3_256(bytes) == FIPS.sha3_256(bytes) : List<&2, U32>}
12
13# Every digest is 32 bytes.
14law sha3_256_length:
15  for +bytes: List<&2, U32>
16  {List.length(&2, U32, SHA3.sha3_256(bytes)) == 32n : Nat}