1	import Base
2	import ../../../../src/crypto/blake/blake3/types.bend as T
3	import ../../../../src/crypto/blake/blake3/blake3.bend as K
4	import ../../../../spec/lib/common.bend as SC
5	import ../../../../spec/crypto/blake/blake3.bend as S
6	import ./array.bend as A
7	import ./compress.bend as P
8	import ./loop.bend as LP
9	
10	# BLAKE3 public API theorem: for every packed input array and every
11	# byte_length, the implementation's blake3 equals the specification's
12	# (spec/crypto/blake/blake3.bend), including the rejection of lengths
13	# past 4 * capacity. No axioms, no holes.
14	#
15	# The chain: compress.bend (the unrolled compression function is the list
16	# specification's), read.bend (block reads and the final-block mask),
17	# chunk.bend (chunk loops), tree.bend (the subtree stack computes the
18	# specification's tree), loop.bend (the chunk loop runs the stack over the
19	# specification's chunk list), and here the root, the digest and the API.
20	
21	law root_correct:
22	  for +o: T.Out
23	  {K.root_cv(o) == S.root(o) : T.CV}
24	
25	def root_correct(o):
26	  match o:
27	    case T.Out{+c,+b,+t,+len,+flags}: P.compress_correct(c,b,t,len,U32.or(flags,8))
28	
29	law unchecked_view:
30	  for -a: Array<U32>
31	  for +length: Nat
32	  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
33	  {K.unchecked(a,length) == S.hash(a,length) : T.CV}
34	
35	def unchecked_view(a,length,view):
36	  match view:
37	    case Tuple{+tree,pf}:
38	      +n = Nat.div(Nat.sub(length,1n),1024n)
39	      +last = Nat.sub(length,Nat.mul(n,1024n))
40	      +cs = S.chunks(n,0,0,last,S.chunk_at(n,0,0,last,A.thaw(tree)))
41	      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.unchecked(_,length) == S.hash(_,length) : T.CV}
42	      Equal.trans(T.CV,
43	        K.root_cv(K.chunks(n,0,0,last,(A.thaw(tree),K.StkNil{}))),
44	        K.root_cv(LP.run(K.StkNil{},cs)),
45	        S.root(S.tree(SC.length(T.Out,cs),cs)),
46	        Equal.cong(T.Out,T.CV,o => K.root_cv(o),K.chunks(n,0,0,last,(A.thaw(tree),K.StkNil{})),LP.run(K.StkNil{},cs),LP.fuse(n,0,0,last,A.thaw(tree),K.StkNil{})),
47	        Equal.trans(T.CV,
48	          K.root_cv(LP.run(K.StkNil{},cs)),
49	          K.root_cv(S.tree(SC.length(T.Out,cs),cs)),
50	          S.root(S.tree(SC.length(T.Out,cs),cs)),
51	          Equal.cong(T.Out,T.CV,o => K.root_cv(o),LP.run(K.StkNil{},cs),S.tree(SC.length(T.Out,cs),cs),LP.run_chunks(n,0,0,last,S.chunk_at(n,0,0,last,A.thaw(tree)))),
52	          root_correct(S.tree(SC.length(T.Out,cs),cs))))
53	
54	law digest_correct:
55	  for +c: T.CV
56	  {K.digest(c) == S.digest(c) : Array<U32>}
57	
58	def digest_correct(c):
59	  match c:
60	    case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}: {==}
61	
62	law checked_view:
63	  for -a: Array<U32>
64	  for +length: Nat
65	  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
66	  {K.checked(True{},a,length) == S.checked(True{},a,length) : Maybe<&1,Array<U32>>}
67	
68	def checked_view(a,length,view):
69	  match view:
70	    case Tuple{+tree,pf}:
71	      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.checked(True{},_,length) == S.checked(True{},_,length) : Maybe<&1,Array<U32>>}
72	      Equal.trans(Maybe<&1,Array<U32>>,
73	        Some{K.digest(K.unchecked(A.thaw(tree),length))},
74	        Some{K.digest(S.hash(A.thaw(tree),length))},
75	        Some{S.digest(S.hash(A.thaw(tree),length))},
76	        Equal.cong(T.CV,Maybe<&1,Array<U32>>,c => Some{K.digest(c)},K.unchecked(A.thaw(tree),length),S.hash(A.thaw(tree),length),unchecked_view(A.thaw(tree),length,A.reify(A.thaw(tree)))),
77	        Equal.cong(Array<U32>,Maybe<&1,Array<U32>>,d => Some{d},K.digest(S.hash(A.thaw(tree),length)),S.digest(S.hash(A.thaw(tree),length)),digest_correct(S.hash(A.thaw(tree),length))))
78	
79	law checked_correct:
80	  for +valid: Bool
81	  for a: Array<U32>
82	  for +length: Nat
83	  {K.checked(valid,a,length) == S.checked(valid,a,length) : Maybe<&1,Array<U32>>}
84	
85	def checked_correct(valid,a,length):
86	  match valid:
87	    case False{}: {==}
88	    case True{}: checked_view(a,length,A.reify(a))
89	
90	law sized_correct:
91	  for +length: Nat
92	  for pair: Array<U32> & U32
93	  {K.sized(length,pair) == S.sized(length,pair) : Maybe<&1,Array<U32>>}
94	
95	def sized_correct(length,pair):
96	  (a,capacity) = pair
97	  checked_correct(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
98	
99	# The public API: for every packed word array and every byte length.
100	law blake3_correct:
101	  for words: Array<U32>
102	  for +byte_length: Nat
103	  {K.blake3(words,byte_length) == S.blake3(words,byte_length) : Maybe<&1,Array<U32>>}
104	
105	def blake3_correct(words,byte_length):
106	  sized_correct(byte_length,Array.size(U32,words))
107	
108	# Rejection: a length past 4 * capacity gives None.
109	law blake3_rejects:
110	  for a: Array<U32>
111	  for +n: Nat
112	  for +capacity: U32
113	  for invalid: {Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))) == False{} : Bool}
114	  {K.sized(n,(a,capacity)) == None{} : Maybe<&1,Array<U32>>}
115	
116	def blake3_rejects(a,n,capacity,invalid):
117	  Equal.cong(Bool,Maybe<&1,Array<U32>>,b => K.checked(b,a,n),Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))),False{},invalid)
118	
119	# The digest is eight words.
120	law digest_size:
121	  for +c: T.CV
122	  {Pair.snd(Array<U32>,U32,Array.size(U32,K.digest(c))) == 8 : U32}
123	
124	def digest_size(c):
125	  match c:
126	    case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}: {==}