proofs/crypto/sha/packed/buffer_proof.bend
bend-collections-laws-crypto@1.0.0.0 · 83 lines · 8 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as F
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/buffer.bend as B
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/packed.bend as P
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha/packed.bend as R
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/packed_proof.bend as Proof
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/packed_array_proof.bend as A
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/sha256.bend as SHA
10
11law correct:
12 for a: Array<U32>
13 for +length: Nat
14 {SHA.sha256(a,length) == B.result(R.hash(a,length)) : Maybe<&1,Array<U32>>}
15
16def correct(a,length):
17 Equal.cong(Maybe<&2,S.State>,Maybe<&1,Array<U32>>,r => B.result(r),
18 P.hash(a,length),R.hash(a,length),Proof.hash_correct(a,length))
19
20law digest_size:
21 for s: S.State
22 {Pair.snd(Array<U32>,U32,Array.size(U32,B.digest(s))) == 8 : U32}
23
24def digest_size(s):
25 match s:
26 case S.H{a,b,c,d,e,f,g,h}: {==}
27
28
29def words(a: Array<U32>) -> List<&2,U32>:
30 match a:
31 case ALeaf{x}: [x]
32 case ANode{l,r}: List.append(&2,U32,words(l),words(r))
33
34law digest_words:
35 for +s: S.State
36 {words(B.digest(s)) == F.digest(s) : List<&2,U32>}
37
38def digest_words(s):
39 match s:
40 case S.H{a,b,c,d,e,f,g,h}: {==}
41
42
43def observe(r: Maybe<&1,Array<U32>>) -> Maybe<&2,List<&2,U32>>:
44 match r:
45 case None{}: None{}
46 case Some{a}: Some{words(a)}
47
48law observe_digest:
49 for +r: Maybe<&2,S.State>
50 {observe(B.result(r)) == R.digest_result(r) : Maybe<&2,List<&2,U32>>}
51
52def observe_digest(r):
53 match r:
54 case None{}: {==}
55 case Some{s}:
56 Equal.cong(List<&2,U32>,Maybe<&2,List<&2,U32>>,ws => Some{ws},
57 words(B.digest(s)),F.digest(s),digest_words(s))
58
59law full_reified:
60 for -a: Array<U32>
61 for +length: Nat
62 for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
63 {observe(SHA.sha256(a,length)) == R.sha256(a,length) : Maybe<&2,List<&2,U32>>}
64
65def full_reified(a,length,view):
66 match view:
67 case Tuple{+tree,pf}:
68 %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {observe(SHA.sha256(_,length)) == R.sha256(_,length) : Maybe<&2,List<&2,U32>>}
69 Equal.trans(Maybe<&2,List<&2,U32>>,
70 observe(SHA.sha256(A.thaw(tree),length)),
71 observe(B.result(R.hash(A.thaw(tree),length))),
72 R.sha256(A.thaw(tree),length),
73 Equal.cong(Maybe<&1,Array<U32>>,Maybe<&2,List<&2,U32>>,r => observe(r),
74 SHA.sha256(A.thaw(tree),length),B.result(R.hash(A.thaw(tree),length)),correct(A.thaw(tree),length)),
75 observe_digest(R.hash(A.thaw(tree),length)))
76
77law full_correct:
78 for a: Array<U32>
79 for +length: Nat
80 {observe(SHA.sha256(a,length)) == R.sha256(a,length) : Maybe<&2,List<&2,U32>>}
81
82def full_correct(a,length):
83 full_reified(a,length,A.reify(a))