proofs/storage_witness.bend

stelliferous@0.0.2.0 · 222 lines · 26 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.2.0/proofs/storage_tree_model.bend as Tree
5import stelliferous@0.0.2.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 allocated(-Element: Data,+depth: Nat,value: Element) -> ArrayWitness<Element,Array.new(Element,depth,value)>:
196  ArrayWitness{depth,fresh(Element,depth,value)}
197
198def stored(-Element: Data,-storage: Array<Element>,+index: U32,-value: Element,evidence: ArrayWitness<Element,storage>) ->
199  ArrayWitness<Element,Array.set(Element,storage,index,value)>:
200  ArrayWitness{+depth,witness} = evidence
201  ArrayWitness{depth,write(Element,depth,storage,index,value,witness)}
202
203def observed(-Element: Data,-storage: Array<Element>,index: U32,evidence: ArrayWitness<Element,storage>) ->
204  Read<Element,storage,Array.get(Element,storage,index)>:
205  ArrayWitness{depth,witness} = evidence
206  read(Element,depth,storage,index,witness)
207
208# The native clone duplicates payload ownership, while its source observation
209# and balance depth are unchanged. This theorem is consumed only by rewrites.
210def clone(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
211  {Array.clone(Element,storage) == (storage,storage) : Array<Element> & Array<Element>}:
212  match depth witness:
213    case 0n Leaf{value,owner}:
214      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
215      {==}
216    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
217      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
218      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,left),(left,left),clone(Element,rest,left,left_balanced)) :
219        {Array.clone.node(Element,_,Array.clone(Element,right)) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
220      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,right),(right,right),clone(Element,rest,right,right_balanced)) :
221        {Array.clone.node(Element,(left,left),_) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
222      {==}