proofs/crypto/sha/correctness.bend
bend-collections@1.0.0.0 · 41 lines · 1 definition
1import Base
2import bend-collections@1.0.0.0/src/crypto/sha/state.bend as State
3import bend-collections@1.0.0.0/src/crypto/sha/sha256.bend as SHA
4import bend-collections@1.0.0.0/spec/crypto/sha.bend as FIPS
5import bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend as Conformance
6import bend-collections@1.0.0.0/proofs/crypto/sha/laws.bend as Laws
7
8
9def Laws.constants_correct():
10 {==}
11
12def Laws.sha256_correct(bytes):
13 Conformance.sha256_correct(bytes)
14
15law digest_octets_length:
16 for s: State.State
17 {List.length(&2, U32, FIPS.digest_octets(FIPS.digest(s))) == 32n : Nat}
18
19def digest_octets_length(s):
20 match s:
21 case State.H{a, b, c, d, e, f, g, h}:
22 {==}
23
24def Laws.digest_bytes_correct(ws):
25 match ws:
26 case Nil{}:
27 {==}
28 case w <> tail:
29 %Laws.digest_bytes_correct(tail) :
30 {SHA.digest_bytes(w <> tail) == List.append(&2, U32, FIPS.word_octets(w), _) : List<&2, U32>}
31 {==}
32
33def Laws.sha256_bytes_correct(bytes):
34 %Laws.sha256_correct(bytes) :
35 {SHA.sha256_bytes(bytes) == FIPS.digest_octets(_) : List<&2, U32>}
36 Laws.digest_bytes_correct(SHA.sha256(bytes))
37
38def Laws.sha256_bytes_length(bytes):
39 %Equal.sym(List<&2, U32>, SHA.sha256_bytes(bytes), FIPS.sha256_bytes(bytes), Laws.sha256_bytes_correct(bytes)) :
40 {List.length(&2, U32, _) == 32n : Nat}
41 digest_octets_length(FIPS.blocks(FIPS.prepare(bytes, 48n), FIPS.constants())(FIPS.initial()))