1	# Structural proof data indexed by an erased affine owner. Runtime owners carry
2	# flat certificates; this tree is used only by proofs, never by numerical loops.
3	import Base
4	import ./storage_tree_model.bend as Tree
5	import ./storage_shape.bend as Shape
6	
7	law Witness:
8	  for -Element: Data
9	  for depth: Nat
10	  for storage: Array<Element>
11	  Data
12	
13	type LeafWitness<-Element: Data,-storage: Array<Element>> is Data:
14	  Leaf{-value: Element,owner: {storage == ALeaf{value} : Array<Element>}}
15	
16	type NodeWitness<-Element: Data,-depth: Nat,-storage: Array<Element>> is Data:
17	  Node{-left: Array<Element>,-right: Array<Element>,owner: {storage == ANode{left,right} : Array<Element>},
18	    left_balanced: Witness(Element,depth,left),right_balanced: Witness(Element,depth,right)}
19	
20	def Witness(Element,depth,storage):
21	  match depth:
22	    case 0n: LeafWitness<Element,storage>
23	    case 1n+rest: NodeWitness<Element,rest,storage>
24	
25	def balanced(-Element: Data,depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
26	  Shape.Balanced(Element,depth,Tree.reflect(Element,storage)):
27	  match depth witness:
28	    case 0n Leaf{value,owner}:
29	      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : Shape.Balanced(Element,0n,Tree.reflect(Element,_))
30	      Unit{}
31	    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
32	      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : Shape.Balanced(Element,1n+rest,Tree.reflect(Element,_))
33	      Shape.Both{balanced(Element,rest,left,left_balanced),balanced(Element,rest,right,right_balanced)}
34	
35	def from_shape(-Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,balanced: Shape.Balanced(Element,depth,tree)) ->
36	  Witness(Element,depth,Tree.pack(Element,tree)):
37	  match depth tree:
38	    case 0n Tree.Leaf{value}: Leaf{value,{==}}
39	    case 0n Tree.Node{left,right}: match balanced:
40	    case 1n+rest Tree.Leaf{value}: match balanced:
41	    case 1n+ +rest Tree.Node{+left,+right}:
42	      Shape.Both{left_balanced,right_balanced} = balanced
43	      Node{Tree.pack(Element,left),Tree.pack(Element,right),{==},from_shape(Element,rest,left,left_balanced),from_shape(Element,rest,right,right_balanced)}
44	
45	def fresh_model(-Element: Data,+depth: Nat,+value: Element) ->
46	  {Array.new(Element,depth,value) == Tree.pack(Element,Tree.fresh(Element,depth,value)) : Array<Element>}:
47	  match depth:
48	    case 0n: {==}
49	    case 1n+ +rest:
50	      %fresh_model(Element,rest,value) : {Array.new(Element,1n+rest,value) == ANode{_,Tree.pack(Element,Tree.fresh(Element,rest,value))} : Array<Element>}
51	      %fresh_model(Element,rest,value) : {Array.new(Element,1n+rest,value) == ANode{Array.new(Element,rest,value),_} : Array<Element>}
52	      {==}
53	
54	def fresh(-Element: Data,+depth: Nat,+value: Element) -> Witness(Element,depth,Array.new(Element,depth,value)):
55	  %Equal.sym(Array<Element>,Array.new(Element,depth,value),Tree.pack(Element,Tree.fresh(Element,depth,value)),fresh_model(Element,depth,value)) : Witness(Element,depth,_)
56	  from_shape(Element,depth,Tree.fresh(Element,depth,value),Shape.fresh(Element,depth,value))
57	
58	def size(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
59	  {Array.size(Element,storage) == (storage,U32.shln(1,depth)) : Array<Element> & U32}:
60	  match depth witness:
61	    case 0n Leaf{value,owner}:
62	      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : {Array.size(Element,_) == (_,U32.shln(1,0n)) : Array<Element> & U32}
63	      {==}
64	    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
65	      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : {Array.size(Element,_) == (_,U32.shln(1,1n+rest)) : Array<Element> & U32}
66	      %size(Element,rest,left,left_balanced) :
67	        {Array.size.node(Element,right,Array.size(Element,left)) == Array.size.node(Element,right,_) : Array<Element> & U32}
68	      {==}
69	
70	type Swapped<-Element: Data,-depth: Nat,-result: Array<Element> & Element> is Data:
71	  Swapped{-storage: Array<Element>,-previous: Element,
72	    equation: {result == (storage,previous) : Array<Element> & Element},balanced: Witness(Element,depth,storage)}
73	
74	def swap_left(-Element: Data,-depth: Nat,-right: Array<Element>,-result: Array<Element> & Element,
75	  swapped: Swapped<Element,depth,result>,right_balanced: Witness(Element,depth,right)) ->
76	  Swapped<Element,1n+depth,Array.swap.lo(Element,right,result)>:
77	  match swapped:
78	    case Swapped{storage,previous,equation,left_balanced}:
79	      Swapped{ANode{storage,right},previous,
80	        Equal.cong(Array<Element> & Element,Array<Element> & Element,
81	          pair => Array.swap.lo(Element,right,pair),result,(storage,previous),equation),
82	        Node{storage,right,{==},left_balanced,right_balanced}}
83	
84	def swap_right(-Element: Data,-depth: Nat,-left: Array<Element>,-result: Array<Element> & Element,
85	  left_balanced: Witness(Element,depth,left),swapped: Swapped<Element,depth,result>) ->
86	  Swapped<Element,1n+depth,Array.swap.hi(Element,left,result)>:
87	  match swapped:
88	    case Swapped{storage,previous,equation,right_balanced}:
89	      Swapped{ANode{left,storage},previous,
90	        Equal.cong(Array<Element> & Element,Array<Element> & Element,
91	          pair => Array.swap.hi(Element,left,pair),result,(storage,previous),equation),
92	        Node{left,storage,{==},left_balanced,right_balanced}}
93	
94	# Base passes the branch z (i < n/2) computed by its caller; any z is covered
95	# here, and each child receives the comparison against its own half.
96	def swap_choose(-Element: Data,-depth: Nat,-left: Array<Element>,-right: Array<Element>,
97	  +capacity: U32,+index: U32,-value: Element,choose_left: Bool,
98	  left_balanced: Witness(Element,depth,left),right_balanced: Witness(Element,depth,right),
99	  left_result: Swapped<Element,depth,Array.swap.go(Element,left,U32.shr(capacity),index,value,U32.is_lt(index,U32.shr(U32.shr(capacity))))>,
100	  right_result: Swapped<Element,depth,Array.swap.go(Element,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),value,
101	    U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity))))>) ->
102	  Swapped<Element,1n+depth,Array.swap.go(Element,ANode{left,right},capacity,index,value,choose_left)>:
103	  match choose_left:
104	    case True{}:
105	      swap_left(Element,depth,right,Array.swap.go(Element,left,U32.shr(capacity),index,value,U32.is_lt(index,U32.shr(U32.shr(capacity)))),
106	        left_result,right_balanced)
107	    case False{}:
108	      swap_right(Element,depth,left,Array.swap.go(Element,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),value,
109	        U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity)))),left_balanced,right_result)
110	
111	def swap(-Element: Data,+depth: Nat,-storage: Array<Element>,+capacity: U32,+index: U32,-value: Element,choose_left: Bool,
112	  witness: Witness(Element,depth,storage)) -> Swapped<Element,depth,Array.swap.go(Element,storage,capacity,index,value,choose_left)>:
113	  match depth witness:
114	    case 0n Leaf{previous,owner}:
115	      %Equal.sym(Array<Element>,storage,ALeaf{previous},owner) : Swapped<Element,0n,Array.swap.go(Element,_,capacity,index,value,choose_left)>
116	      Swapped{ALeaf{value},previous,{==},Leaf{value,{==}}}
117	    case 1n+ +rest Node{left,right,owner,+left_balanced,+right_balanced}:
118	      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : Swapped<Element,1n+rest,Array.swap.go(Element,_,capacity,index,value,choose_left)>
119	      swap_choose(Element,rest,left,right,capacity,index,value,choose_left,left_balanced,right_balanced,
120	        swap(Element,rest,left,U32.shr(capacity),index,value,U32.is_lt(index,U32.shr(U32.shr(capacity))),left_balanced),
121	        swap(Element,rest,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),value,
122	          U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity))),right_balanced))
123	
124	def finish(-Element: Data,-depth: Nat,-result: Array<Element> & Element,swapped: Swapped<Element,depth,result>) ->
125	  Witness(Element,depth,Array.set.fin(Element,result)):
126	  match swapped:
127	    case Swapped{storage,previous,equation,witness}:
128	      %Equal.sym(Array<Element> & Element,result,(storage,previous),equation) : Witness(Element,depth,Array.set.fin(Element,_))
129	      witness
130	
131	def write(-Element: Data,+depth: Nat,-storage: Array<Element>,+index: U32,-value: Element,
132	  +witness: Witness(Element,depth,storage)) -> Witness(Element,depth,Array.set(Element,storage,index,value)):
133	  %Equal.sym(Array<Element> & U32,Array.size(Element,storage),(storage,U32.shln(1,depth)),size(Element,depth,storage,witness)) :
134	    Witness(Element,depth,Array.set.fin(Element,Array.swap.at(Element,index,value,_)))
135	  +start = U32.and(index,U32.sub(U32.shln(1,depth),1))
136	  +choose_left = U32.is_lt(start,U32.shr(U32.shln(1,depth)))
137	  finish(Element,depth,Array.swap.go(Element,storage,U32.shln(1,depth),start,value,choose_left),
138	    swap(Element,depth,storage,U32.shln(1,depth),start,value,choose_left,witness))
139	
140	# Reading returns precisely the original affine owner. The observed element is
141	# an erased index of this proof; no runtime sample is copied into evidence.
142	type Read<-Element: Data,-storage: Array<Element>,-result: Array<Element> & Element> is Data:
143	  Read{-value: Element,equation: {result == (storage,value) : Array<Element> & Element}}
144	
145	def read_left(-Element: Data,-left: Array<Element>,-right: Array<Element>,-result: Array<Element> & Element,
146	  read: Read<Element,left,result>) -> Read<Element,ANode{left,right},Array.swap.lo(Element,right,result)>:
147	  match read:
148	    case Read{value,equation}:
149	      Read{value,Equal.cong(Array<Element> & Element,Array<Element> & Element,
150	        pair => Array.swap.lo(Element,right,pair),result,(left,value),equation)}
151	
152	def read_right(-Element: Data,-left: Array<Element>,-right: Array<Element>,-result: Array<Element> & Element,
153	  read: Read<Element,right,result>) -> Read<Element,ANode{left,right},Array.swap.hi(Element,left,result)>:
154	  match read:
155	    case Read{value,equation}:
156	      Read{value,Equal.cong(Array<Element> & Element,Array<Element> & Element,
157	        pair => Array.swap.hi(Element,left,pair),result,(right,value),equation)}
158	
159	def read_choose(-Element: Data,-left: Array<Element>,-right: Array<Element>,+capacity: U32,+index: U32,choose_left: Bool,
160	  left_read: Read<Element,left,Array.get.go(Element,left,U32.shr(capacity),index,U32.is_lt(index,U32.shr(U32.shr(capacity))))>,
161	  right_read: Read<Element,right,Array.get.go(Element,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),
162	    U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity))))>) ->
163	  Read<Element,ANode{left,right},Array.get.go(Element,ANode{left,right},capacity,index,choose_left)>:
164	  match choose_left:
165	    case True{}:
166	      read_left(Element,left,right,Array.get.go(Element,left,U32.shr(capacity),index,U32.is_lt(index,U32.shr(U32.shr(capacity)))),left_read)
167	    case False{}:
168	      read_right(Element,left,right,Array.get.go(Element,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),
169	        U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity)))),right_read)
170	
171	def read_tree(-Element: Data,+depth: Nat,-storage: Array<Element>,+capacity: U32,+index: U32,choose_left: Bool,
172	  witness: Witness(Element,depth,storage)) -> Read<Element,storage,Array.get.go(Element,storage,capacity,index,choose_left)>:
173	  match depth witness:
174	    case 0n Leaf{value,owner}:
175	      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : Read<Element,_,Array.get.go(Element,_,capacity,index,choose_left)>
176	      Read{value,{==}}
177	    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
178	      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : Read<Element,_,Array.get.go(Element,_,capacity,index,choose_left)>
179	      read_choose(Element,left,right,capacity,index,choose_left,
180	        read_tree(Element,rest,left,U32.shr(capacity),index,U32.is_lt(index,U32.shr(U32.shr(capacity))),left_balanced),
181	        read_tree(Element,rest,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),
182	          U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity))),right_balanced))
183	
184	def read(-Element: Data,+depth: Nat,-storage: Array<Element>,+index: U32,+witness: Witness(Element,depth,storage)) ->
185	  Read<Element,storage,Array.get(Element,storage,index)>:
186	  %Equal.sym(Array<Element> & U32,Array.size(Element,storage),(storage,U32.shln(1,depth)),size(Element,depth,storage,witness)) :
187	    Read<Element,storage,Array.get.at(Element,index,_)>
188	  +start = U32.and(index,U32.sub(U32.shln(1,depth),1))
189	  read_tree(Element,depth,storage,U32.shln(1,depth),start,U32.is_lt(start,U32.shr(U32.shln(1,depth))),witness)
190	
191	# Existential depth travels with proof data, not numerical storage.
192	type ArrayWitness<-Element: Data,-storage: Array<Element>> is Data:
193	  ArrayWitness{depth: Nat,witness: Witness(Element,depth,storage)}
194	
195	def observed(-Element: Data,-storage: Array<Element>,index: U32,evidence: ArrayWitness<Element,storage>) ->
196	  Read<Element,storage,Array.get(Element,storage,index)>:
197	  ArrayWitness{depth,witness} = evidence
198	  read(Element,depth,storage,index,witness)
199	
200	# The native clone duplicates payload ownership, while its source observation
201	# and balance depth are unchanged. This theorem is consumed only by rewrites.
202	def clone(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
203	  {Array.clone(Element,storage) == (storage,storage) : Array<Element> & Array<Element>}:
204	  match depth witness:
205	    case 0n Leaf{value,owner}:
206	      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
207	      {==}
208	    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
209	      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
210	      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,left),(left,left),clone(Element,rest,left,left_balanced)) :
211	        {Array.clone.node(Element,_,Array.clone(Element,right)) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
212	      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,right),(right,right),clone(Element,rest,right,right_balanced)) :
213	        {Array.clone.node(Element,(left,left),_) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
214	      {==}