proofs/storage_witness.bend
stelliferous@0.0.3.0 · 214 lines · 0 definitions
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.
3import Base
4import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
5import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
6
7law Witness:
8 for -Element: Data
9 for depth: Nat
10 for storage: Array<Element>
11 Data
12
13type LeafWitness<-Element: Data,-storage: Array<Element>> is Data:
14 Leaf{-value: Element,owner: {storage == ALeaf{value} : Array<Element>}}
15
16type 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
20def Witness(Element,depth,storage):
21 match depth:
22 case 0n: LeafWitness<Element,storage>
23 case 1n+rest: NodeWitness<Element,rest,storage>
24
25def 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
35def 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
45def 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
54def 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
58def 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
70type 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
74def 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
84def 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.
96def 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
111def 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
124def 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
131def 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.
142type Read<-Element: Data,-storage: Array<Element>,-result: Array<Element> & Element> is Data:
143 Read{-value: Element,equation: {result == (storage,value) : Array<Element> & Element}}
144
145def 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
152def 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
159def 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
171def 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
184def 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.
192type ArrayWitness<-Element: Data,-storage: Array<Element>> is Data:
193 ArrayWitness{depth: Nat,witness: Witness(Element,depth,storage)}
194
195def 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.
202def 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 {==}