proofs/crypto/hash/proof.bend
bend-collections-laws-crypto@1.0.0.0 · 87 lines · 1 definition
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S256
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend as C256
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as SHA256
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C512
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as C3
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as Hash
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend as SC
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/laws.bend as SL
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/correctness.bend as SCorr
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend as S512
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/conformance.bend as S3
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/lists.bend as L
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend as I
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/laws.bend as Laws
16
17
18
19
20def Laws.Sha256.value(bytes):
21 SL.sha256_bytes_correct(bytes)
22
23def Laws.Sha512.value(bytes):
24 S512.sha512_correct(bytes)
25
26def Laws.Sha3_256.value(bytes):
27 S3.keccak_correct(bytes, 24n)
28
29def Laws.Sha256.length(bytes):
30 SL.sha256_bytes_length(bytes)
31
32def Laws.Sha512.length(bytes):
33 S512.digest_length(C512.blocks(C512.lanes(List.append(&2, U32, bytes,
34 C512.suffix(List.length(&2, U32, bytes)))), 64n, C512.round_constants(), C512.initial()))
35
36def Laws.Sha3_256.length(bytes):
37 S3.digest_length(C3.absorb(C3.lanes(List.append(&2, U32, bytes,
38 C3.suffix(List.length(&2, U32, bytes)))), 24n, C3.zero()))
39
40
41
42law oneshot256:
43 for +m: List<&2, U32>
44 {Hash.sha256(m) == SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
45 C256.suffix(List.length(&2, U32, m))), 48n, C256.round_constants(), C256.initial()))) : List<&2, U32>}
46
47def oneshot256(m):
48 %L.add_zero(List.length(&2, U32, m)) :
49 {Hash.sha256(m) == SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
50 C256.suffix(_)), 48n, C256.round_constants(), C256.initial()))) : List<&2, U32>}
51 Equal.cong(S256.State, List<&2, U32>, t => SHA256.digest_bytes(C256.digest(t)),
52 C256.stream(m, 0n, 48n, C256.initial()),
53 C256.block_bytes(List.append(&2, U32, m, C256.suffix(Nat.add(List.length(&2, U32, m), 0n))),
54 48n, C256.round_constants(), C256.initial()),
55 SC.stream_correct(m, 0n, 48n, C256.initial()))
56
57def Laws.Incremental.sha256(chunks):
58 +m = List.concat(&2, U32, chunks)
59 Equal.trans(List<&2, U32>,
60 Hash.digest(Hash.update_all(Hash.new_sha256(), chunks)),
61 SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
62 C256.suffix(List.length(&2, U32, m))), 48n, C256.round_constants(), C256.initial()))),
63 Hash.sha256(m),
64 I.incremental256(chunks),
65 Equal.sym(List<&2, U32>, Hash.sha256(m), SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
66 C256.suffix(List.length(&2, U32, m))), 48n, C256.round_constants(), C256.initial()))), oneshot256(m)))
67
68def Laws.Incremental.sha512(chunks):
69 I.incremental512(chunks)
70
71def Laws.Incremental.sha3_256(chunks):
72 I.incremental3(chunks)
73
74def Laws.Split.sha256(a, b):
75 %L.append_nil(b) :
76 {Hash.digest(Hash.update(Hash.update(Hash.new_sha256(), a), b)) == Hash.sha256(List.append(&2, U32, a, _)) : List<&2, U32>}
77 Laws.Incremental.sha256([a, b])
78
79def Laws.Split.sha512(a, b):
80 %L.append_nil(b) :
81 {Hash.digest(Hash.update(Hash.update(Hash.new_sha512(), a), b)) == Hash.sha512(List.append(&2, U32, a, _)) : List<&2, U32>}
82 Laws.Incremental.sha512([a, b])
83
84def Laws.Split.sha3_256(a, b):
85 %L.append_nil(b) :
86 {Hash.digest(Hash.update(Hash.update(Hash.new_sha3_256(), a), b)) == Hash.sha3_256(List.append(&2, U32, a, _)) : List<&2, U32>}
87 Laws.Incremental.sha3_256([a, b])