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