proofs/crypto/sha512/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 26 lines · 3 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/sha512.bend as SHA
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as FIPS
5import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/words.bend as Words
7
8# SHA-512: the public API against the complete, independent FIPS 180-4
9# specification spec/crypto/sha512.bend. No test vector, table or premise.
10
11# The digest of every byte list is the specification's.
12law sha512_correct:
13  for +bytes: List<&2, U32>
14  {SHA.sha512(bytes) == FIPS.sha512_bytes(bytes) : List<&2, U32>}
15
16# Every digest is 64 bytes.
17law sha512_length:
18  for +bytes: List<&2, U32>
19  {List.length(&2, U32, SHA.sha512(bytes)) == 64n : Nat}
20
21# The specification's word addition is addition modulo 2^64 (FIPS 180-4
22# section 3.2), with W{hi, lo} read as lo + 2^32 hi.
23law spec_add_mod:
24  for +a: T.Lane
25  for +b: T.Lane
26  {Words.value(FIPS.add(a, b)) == C.low(64n, Nat.add(Words.value(a), Words.value(b))) : Nat}