proofs/crypto/sha/laws.bend

bend-collections@1.0.0.0 · 24 lines · 5 definitions

1import Base
2import bend-collections@1.0.0.0/src/crypto/sha/sha256.bend as SHA
3import bend-collections@1.0.0.0/spec/crypto/sha.bend as FIPS
4
5# These claims mention the actual public API and the complete independent spec.
6# There are no arbitrary preprocessing functions, tables, or correctness premises.
7law constants_correct:
8  {SHA.constants() == FIPS.constants() : List<&2, U32>}
9
10law sha256_correct:
11  for +bytes: List<&2, U32>
12  {SHA.sha256(bytes) == FIPS.sha256(bytes) : List<&2, U32>}
13
14law digest_bytes_correct:
15  for +ws: List<&2, U32>
16  {SHA.digest_bytes(ws) == FIPS.digest_octets(ws) : List<&2, U32>}
17
18law sha256_bytes_correct:
19  for +bytes: List<&2, U32>
20  {SHA.sha256_bytes(bytes) == FIPS.sha256_bytes(bytes) : List<&2, U32>}
21
22law sha256_bytes_length:
23  for +bytes: List<&2, U32>
24  {List.length(&2, U32, SHA.sha256_bytes(bytes)) == 32n : Nat}