proofs/storage_certificate.bend
stelliferous@0.0.3.0 · 153 lines · 0 definitions
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.
4import Base
5import stelliferous@0.0.3.0/traversal_array.bend as Traversal
6import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
7import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
8
9def 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
14def 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
19def 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
24def 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
30def 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
39def 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
58type 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
61def 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
68def 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
74def 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
80def allocated(-Element: Data,+depth: Nat,value: Element) -> Certificate<Element,Array.new(Element,depth,value)>:
81 Certificate{depth,fresh_equation(Element,depth,value)}
82
83def family(~Element: Data,-storage: Array<Element>) -> Data:
84 Certificate<Element,storage>
85
86def 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
93def 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
102def 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
107def 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.
117def 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.
123def 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
132def 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
139def 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
147def 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}