proofs/crypto/hash/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 63 lines · 12 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as Hash
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as FIPS180
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as FIPS180_512
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as FIPS202
6
7# The clauses of src/crypto/hash.bend. Proved in proof.bend for every input.
8
9# Each one-shot function is its standard's executable specification.
10law Sha256.value:
11  for +bytes: List<&2, U32>
12  {Hash.sha256(bytes) == FIPS180.sha256_bytes(bytes) : List<&2, U32>}
13
14law Sha512.value:
15  for +bytes: List<&2, U32>
16  {Hash.sha512(bytes) == FIPS180_512.sha512_bytes(bytes) : List<&2, U32>}
17
18law Sha3_256.value:
19  for +bytes: List<&2, U32>
20  {Hash.sha3_256(bytes) == FIPS202.sha3_256(bytes) : List<&2, U32>}
21
22# Digest sizes: 32, 64 and 32 bytes.
23law Sha256.length:
24  for +bytes: List<&2, U32>
25  {List.length(&2, U32, Hash.sha256(bytes)) == 32n : Nat}
26
27law Sha512.length:
28  for +bytes: List<&2, U32>
29  {List.length(&2, U32, Hash.sha512(bytes)) == 64n : Nat}
30
31law Sha3_256.length:
32  for +bytes: List<&2, U32>
33  {List.length(&2, U32, Hash.sha3_256(bytes)) == 32n : Nat}
34
35# Incremental hashing equals one-shot hashing for every split of the input:
36# the chunks, in order, digest to the hash of their concatenation.
37law Incremental.sha256:
38  for +chunks: List<&2, List<&2, U32>>
39  {Hash.digest(Hash.update_all(Hash.new_sha256(), chunks)) == Hash.sha256(List.concat(&2, U32, chunks)) : List<&2, U32>}
40
41law Incremental.sha512:
42  for +chunks: List<&2, List<&2, U32>>
43  {Hash.digest(Hash.update_all(Hash.new_sha512(), chunks)) == Hash.sha512(List.concat(&2, U32, chunks)) : List<&2, U32>}
44
45law Incremental.sha3_256:
46  for +chunks: List<&2, List<&2, U32>>
47  {Hash.digest(Hash.update_all(Hash.new_sha3_256(), chunks)) == Hash.sha3_256(List.concat(&2, U32, chunks)) : List<&2, U32>}
48
49# The two-chunk case, spelled with update.
50law Split.sha256:
51  for +a: List<&2, U32>
52  for +b: List<&2, U32>
53  {Hash.digest(Hash.update(Hash.update(Hash.new_sha256(), a), b)) == Hash.sha256(List.append(&2, U32, a, b)) : List<&2, U32>}
54
55law Split.sha512:
56  for +a: List<&2, U32>
57  for +b: List<&2, U32>
58  {Hash.digest(Hash.update(Hash.update(Hash.new_sha512(), a), b)) == Hash.sha512(List.append(&2, U32, a, b)) : List<&2, U32>}
59
60law Split.sha3_256:
61  for +a: List<&2, U32>
62  for +b: List<&2, U32>
63  {Hash.digest(Hash.update(Hash.update(Hash.new_sha3_256(), a), b)) == Hash.sha3_256(List.append(&2, U32, a, b)) : List<&2, U32>}