1	import Base
2	import ../../../../spec/crypto/sha.bend as F
3	import ../../../../src/crypto/sha/packed/buffer.bend as B
4	import ../../../../src/crypto/sha/packed/packed.bend as P
5	import ../../../../spec/crypto/sha/packed.bend as R
6	import ./packed_proof.bend as Proof
7	import ./packed_array_proof.bend as A
8	import ../../../../src/crypto/sha/state.bend as S
9	import ../../../../src/crypto/sha/packed/sha256.bend as SHA
10	
11	law 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	
16	def 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	
20	law digest_size:
21	  for s: S.State
22	  {Pair.snd(Array<U32>,U32,Array.size(U32,B.digest(s))) == 8 : U32}
23	
24	def digest_size(s):
25	  match s:
26	    case S.H{a,b,c,d,e,f,g,h}: {==}
27	
28	# Proof-only observation; never called by the buffer hashing API.
29	def 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	
34	law digest_words:
35	  for +s: S.State
36	  {words(B.digest(s)) == F.digest(s) : List<&2,U32>}
37	
38	def digest_words(s):
39	  match s:
40	    case S.H{a,b,c,d,e,f,g,h}: {==}
41	
42	# Full public-result observation against the independent packed specification.
43	def 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	
48	law observe_digest:
49	  for +r: Maybe<&2,S.State>
50	  {observe(B.result(r)) == R.digest_result(r) : Maybe<&2,List<&2,U32>>}
51	
52	def 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	
59	law 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	
65	def 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	
77	law 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	
82	def full_correct(a,length):
83	  full_reified(a,length,A.reify(a))