1	# A flat live certificate: depth plus one equality word. Its equation identifies
2	# the owner with a balanced normalization of its proof-only tree observation.
3	# Proof trees occur only under equality rewrites and are erased from native code.
4	import Base
5	import ../traversal_array.bend as Traversal
6	import ./storage_tree_model.bend as Tree
7	import ./storage_witness.bend as Witness
8	
9	def first(-Element: Data,tree: Tree.Tree<Element>) -> Element:
10	  match tree:
11	    case Tree.Leaf{value}: value
12	    case Tree.Node{left,right}: first(Element,left)
13	
14	def left(-Element: Data,tree: Tree.Tree<Element>) -> Tree.Tree<Element>:
15	  match tree:
16	    case Tree.Leaf{value}: Tree.Leaf{value}
17	    case Tree.Node{left,right}: left
18	
19	def right(-Element: Data,tree: Tree.Tree<Element>) -> Tree.Tree<Element>:
20	  match tree:
21	    case Tree.Leaf{value}: Tree.Leaf{value}
22	    case Tree.Node{left,right}: right
23	
24	def normalized(-Element: Data,depth: Nat,+tree: Tree.Tree<Element>) -> Tree.Tree<Element>:
25	  match depth:
26	    case 0n: Tree.Leaf{first(Element,tree)}
27	    case 1n+ +rest:
28	      Tree.Node{normalized(Element,rest,left(Element,tree)),normalized(Element,rest,right(Element,tree))}
29	
30	def normalized_witness(-Element: Data,+depth: Nat,-tree: Tree.Tree<Element>) ->
31	  Witness.Witness(Element,depth,Tree.pack(Element,normalized(Element,depth,tree))):
32	  match depth:
33	    case 0n: Witness.Leaf{first(Element,tree),{==}}
34	    case 1n+ +rest:
35	      Witness.Node{Tree.pack(Element,normalized(Element,rest,left(Element,tree))),
36	        Tree.pack(Element,normalized(Element,rest,right(Element,tree))),{==},
37	        normalized_witness(Element,rest,left(Element,tree)),normalized_witness(Element,rest,right(Element,tree))}
38	
39	def restored(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness.Witness(Element,depth,storage)) ->
40	  {Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) == storage : Array<Element>}:
41	  match depth witness:
42	    case 0n Witness.Leaf{value,owner}:
43	      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) :
44	        {Tree.pack(Element,normalized(Element,0n,Tree.reflect(Element,_))) == _ : Array<Element>}
45	      {==}
46	    case 1n+ +rest Witness.Node{left,right,owner,left_balanced,right_balanced}:
47	      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) :
48	        {Tree.pack(Element,normalized(Element,1n+rest,Tree.reflect(Element,_))) == _ : Array<Element>}
49	      %restored(Element,rest,left,left_balanced) :
50	        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),
51	          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} == ANode{_,right} : Array<Element>}
52	      %restored(Element,rest,right,right_balanced) :
53	        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),
54	          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} ==
55	          ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),_} : Array<Element>}
56	      {==}
57	
58	type Certificate<-Element: Data,-storage: Array<Element>> is Data:
59	  Certificate{depth: Nat,equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}}
60	
61	def witness_at(-Element: Data,+depth: Nat,-storage: Array<Element>,
62	  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
63	  Witness.Witness(Element,depth,storage):
64	  %Equal.sym(Array<Element>,storage,Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))),equation) :
65	    Witness.Witness(Element,depth,_)
66	  normalized_witness(Element,depth,Tree.reflect(Element,storage))
67	
68	def witness(-Element: Data,-storage: Array<Element>,certificate: Certificate<Element,storage>) -> Witness.ArrayWitness<Element,storage>:
69	  Certificate{+depth,equation} = certificate
70	  %Equal.sym(Array<Element>,storage,Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))),equation) :
71	    Witness.ArrayWitness<Element,_>
72	  Witness.ArrayWitness{depth,normalized_witness(Element,depth,Tree.reflect(Element,storage))}
73	
74	def fresh_equation(-Element: Data,+depth: Nat,value: Element) ->
75	  {Array.new(Element,depth,value) == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}:
76	  %restored(Element,depth,Array.new(Element,depth,value),Witness.fresh(Element,depth,value)) :
77	    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}
78	  {==}
79	
80	def allocated(-Element: Data,+depth: Nat,value: Element) -> Certificate<Element,Array.new(Element,depth,value)>:
81	  Certificate{depth,fresh_equation(Element,depth,value)}
82	
83	def family(~Element: Data,-storage: Array<Element>) -> Data:
84	  Certificate<Element,storage>
85	
86	def written(~Element: Data,+depth: Nat,values: List<&2,Element>,+offset: U32,-storage: Array<Element>,
87	  evidence: Witness.Witness(Element,depth,storage)) -> Witness.Witness(Element,depth,Traversal.write_list(~Element,values,offset,storage)):
88	  match values:
89	    case []: evidence
90	    case head <> tail:
91	      written(~Element,depth,tail,(offset + 1 : U32),Array.set(Element,storage,offset,head),Witness.write(Element,depth,storage,offset,head,evidence))
92	
93	def written_equation(~Element: Data,+depth: Nat,values: List<&2,Element>,offset: U32,-storage: Array<Element>,
94	  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
95	  {Traversal.write_list(~Element,values,offset,storage) ==
96	    Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Traversal.write_list(~Element,values,offset,storage)))) : Array<Element>}:
97	  %restored(Element,depth,Traversal.write_list(~Element,values,offset,storage),
98	    written(~Element,depth,values,offset,storage,witness_at(Element,depth,storage,equation))) :
99	    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Traversal.write_list(~Element,values,offset,storage)))) : Array<Element>}
100	  {==}
101	
102	def write_list(~Element: Data,values: List<&2,Element>,offset: U32,-storage: Array<Element>,certificate: Certificate<Element,storage>) ->
103	  Certificate<Element,Traversal.write_list(~Element,values,offset,storage)>:
104	  Certificate{+depth,equation} = certificate
105	  Certificate{depth,written_equation(~Element,depth,values,offset,storage,equation)}
106	
107	def set_equation(~Element: Data,+depth: Nat,+index: U32,-value: Element,-storage: Array<Element>,
108	  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
109	  {Array.set(Element,storage,index,value) ==
110	    Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.set(Element,storage,index,value)))) : Array<Element>}:
111	  %restored(Element,depth,Array.set(Element,storage,index,value),
112	    Witness.write(Element,depth,storage,index,value,witness_at(Element,depth,storage,equation))) :
113	    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.set(Element,storage,index,value)))) : Array<Element>}
114	  {==}
115	
116	# One value written; the balance depth is unchanged whatever the value.
117	def set(~Element: Data,+index: U32,-value: Element,-storage: Array<Element>,certificate: Certificate<Element,storage>) ->
118	  Certificate<Element,Array.set(Element,storage,index,value)>:
119	  Certificate{+depth,equation} = certificate
120	  Certificate{depth,set_equation(~Element,depth,index,value,storage,equation)}
121	
122	# Transport a storage certificate across the read-only native array operation.
123	def retained(~Element: Data,+depth: Nat,-storage: Array<Element>,-value: Element,-result: Array<Element> & Element,
124	  +same: {(storage,value) == result : Array<Element> & Element},
125	  +equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
126	  Certificate<Element,Pair.fst(Array<Element>,Element,result)>:
127	  Certificate{depth,
128	    %Equal.cong(Array<Element> & Element,Array<Element>,pair => Pair.fst(Array<Element>,Element,pair),(storage,value),result,same) :
129	      {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,_))) : Array<Element>}
130	    equation}
131	
132	def read_owner(~Element: Data,-storage: Array<Element>,+index: U32,
133	  read: Witness.Read<Element,storage,Array.get(Element,storage,index)>) ->
134	  {storage == Pair.fst(Array<Element>,Element,Array.get(Element,storage,index)) : Array<Element>}:
135	  Witness.Read{value,+same} = read
136	  Equal.cong(Array<Element> & Element,Array<Element>,pair => Pair.fst(Array<Element>,Element,pair),(storage,value),Array.get(Element,storage,index),
137	    Equal.sym(Array<Element> & Element,Array.get(Element,storage,index),(storage,value),same))
138	
139	def read_equation(~Element: Data,+depth: Nat,-storage: Array<Element>,+index: U32,
140	  +equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>},
141	  read: Witness.Read<Element,storage,Array.get(Element,storage,index)>) ->
142	  {Pair.fst(Array<Element>,Element,Array.get(Element,storage,index)) == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Pair.fst(Array<Element>,Element,Array.get(Element,storage,index))))) : Array<Element>}:
143	  %read_owner(~Element,storage,index,read) :
144	    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,_))) : Array<Element>}
145	  equation
146	
147	def read_kept(~Element: Data,-storage: Array<Element>,+index: U32,certificate: Certificate<Element,storage>) ->
148	  Certificate<Element,Pair.fst(Array<Element>,Element,Array.get(Element,storage,index))>:
149	  Certificate{+depth,+equation} = certificate
150	  Certificate{depth,
151	    %read_owner(~Element,storage,index,Witness.observed(Element,storage,index,Witness.ArrayWitness{depth,witness_at(Element,depth,storage,equation)})) :
152	      {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,_))) : Array<Element>}
153	    equation}