proofs/storage_refinement.bend
stelliferous@0.0.3.0 · 497 lines · 0 definitions
1import Base
2import stelliferous@0.0.3.0/storage_buffer.bend as Storage
3import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
4import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
5import stelliferous@0.0.3.0/proofs/loop_projection.bend as Projection
6import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
7import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
8import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
9import stelliferous@0.0.3.0/proofs/u32_division.bend as U32Division
10
11# The tree model covers every native Array owner, including capacities larger
12# than its logical sequence. These equalities allocate no runtime conversion.
13def reflect_packed(-Element: Data,+tree: Tree.Tree<Element>) ->
14 {Tree.reflect(Element,Tree.pack(Element,tree)) == tree : Tree.Tree<Element>}:
15 match tree:
16 case Tree.Leaf{value}: {==}
17 case Tree.Node{+left,+right}:
18 %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,left)),left,reflect_packed(Element,left)) :
19 {Tree.Node{_,Tree.reflect(Element,Tree.pack(Element,right))} == Tree.Node{left,right} : Tree.Tree<Element>}
20 %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,right)),right,reflect_packed(Element,right)) :
21 {Tree.Node{left,_} == Tree.Node{left,right} : Tree.Tree<Element>}
22 {==}
23
24def pack_reflected(-Element: Data,storage: Array<Element>) ->
25 {Tree.pack(Element,Tree.reflect(Element,storage)) == storage : Array<Element>}:
26 match storage:
27 case ALeaf{value}: {==}
28 case ANode{left,right}:
29 %pack_reflected(Element,left) :
30 {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{_,right} : Array<Element>}
31 %pack_reflected(Element,right) :
32 {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{Tree.pack(Element,Tree.reflect(Element,left)),_} : Array<Element>}
33 {==}
34
35law fresh:
36 for -T: Data
37 for +depth: Nat
38 for +value: T
39 {Array.new(T,depth,value) == Tree.pack(T,Tree.fresh(T,depth,value)) : Array<T>}
40law clone:
41 for -T: Data
42 for +tree: Tree.Tree<T>
43 {Array.clone(T,Tree.pack(T,tree)) == (Tree.pack(T,tree),Tree.pack(T,tree)) : Array<T> & Array<T>}
44law read:
45 for -T: Data
46 for +tree: Tree.Tree<T>
47 for +i: U32
48 {Array.get(T,Tree.pack(T,tree),i) == (Tree.pack(T,tree),Tree.read(T,tree,i)) : Array<T> & T}
49law write:
50 for -T: Data
51 for +tree: Tree.Tree<T>
52 for +i: U32
53 for +value: T
54 {Array.set(T,Tree.pack(T,tree),i,value) == Tree.pack(T,Tree.write(T,tree,i,value)) : Array<T>}
55
56def fresh(T,depth,value):
57 Witness.fresh_model(T,depth,value)
58
59def clone(T,tree):
60 match tree:
61 case Tree.Leaf{v}:
62 {==}
63 case Tree.Node{+l,+r}:
64 %Equal.sym(Array<T> & Array<T>,Array.clone(T,Tree.pack(T,l)),(Tree.pack(T,l),Tree.pack(T,l)),
65 clone(T,l)) : {Array.clone.node(T,_,Array.clone(T,Tree.pack(T,r))) == (Tree.pack(T,
66 Tree.Node{l,r}),Tree.pack(T,Tree.Node{l,r})) : Array<T> & Array<T>}
67 %Equal.sym(Array<T> & Array<T>,Array.clone(T,Tree.pack(T,r)),(Tree.pack(T,r),Tree.pack(T,r)),
68 clone(T,r)) : {Array.clone.node(T,(Tree.pack(T,l),Tree.pack(T,l)),_) == (Tree.pack(T,
69 Tree.Node{l,r}),Tree.pack(T,Tree.Node{l,r})) : Array<T> & Array<T>}
70 {==}
71
72law size:
73 for -T: Data
74 for +tree: Tree.Tree<T>
75 {Array.size(T,Tree.pack(T,tree)) == (Tree.pack(T,tree),Tree.capacity(T,tree)) : Array<T> & U32}
76def size(T,tree):
77 match tree:
78 case Tree.Leaf{v}:
79 {==}
80 case Tree.Node{+l,+r}:
81 %Equal.sym(Array<T> & U32,Array.size(T,Tree.pack(T,l)),(Tree.pack(T,l),Tree.capacity(T,l)),size(T,
82 l)) : {Array.size.node(T,Tree.pack(T,r),_) == (Tree.pack(T,Tree.Node{l,r}),U32.shl(Tree.capacity(T,
83 l))) : Array<T> & U32}
84 {==}
85
86# Base passes the branch z that the caller computed as i < n/2; each child
87# receives its own comparison against its half. The tree model picks the same
88# branch, so every lemma holds for any z and the recursion supplies its value.
89law get_node:
90 for -T: Data
91 for +l: Tree.Tree<T>
92 for +r: Tree.Tree<T>
93 for +n: U32
94 for +i: U32
95 for +z: Bool
96 for pl: {Array.get.go(T,Tree.pack(T,l),U32.shr(n),i,U32.is_lt(i,U32.shr(U32.shr(n)))) ==
97 (Tree.pack(T,l),Tree.fetch(T,l,U32.shr(n),i)) : Array<T> & T}
98 for pr: {Array.get.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)),U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n)))) ==
99 (Tree.pack(T,r),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n)))) : Array<T> & T}
100 {Array.get.go(T,Tree.pack(T,Tree.Node{l,r}),n,i,z) == (Tree.pack(T,Tree.Node{l,r}),Bool.pick(T,z,
101 Tree.fetch(T,l,U32.shr(n),i),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n))))) : Array<T> & T}
102def get_node(T,l,r,n,i,z,pl,pr):
103 match z:
104 case True{}:
105 %pl : {Array.swap.lo(T,Tree.pack(T,r),Array.get.go(T,Tree.pack(T,l),U32.shr(n),i,U32.is_lt(i,U32.shr(U32.shr(n))))) ==
106 Array.swap.lo(T,Tree.pack(T,r),_) : Array<T> & T}
107 {==}
108 case False{}:
109 %pr : {Array.swap.hi(T,Tree.pack(T,l),Array.get.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)),
110 U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n))))) == Array.swap.hi(T,Tree.pack(T,l),_) : Array<T> & T}
111 {==}
112
113law get_go:
114 for -T: Data
115 for +tree: Tree.Tree<T>
116 for +n: U32
117 for +i: U32
118 {Array.get.go(T,Tree.pack(T,tree),n,i,U32.is_lt(i,U32.shr(n))) == (Tree.pack(T,tree),Tree.fetch(T,tree,n,i)) : Array<T> & T}
119def get_go(T,tree,n,i):
120 match tree:
121 case Tree.Leaf{v}:
122 {==}
123 case Tree.Node{+l,+r}:
124 get_node(T,l,r,n,i,U32.is_lt(i,U32.shr(n)),get_go(T,l,U32.shr(n),i),get_go(T,r,U32.shr(n),U32.sub(i,U32.shr(n))))
125
126def read(T,tree,i):
127 %get_go(T,tree,Tree.capacity(T,tree),U32.and(i,U32.sub(Tree.capacity(T,tree),1))) : {Array.get.at(T,i,Array.size(T,
128 Tree.pack(T,tree))) == _ : Array<T> & T}
129 %size(T,tree) : {Array.get.at(T,i,Array.size(T,Tree.pack(T,tree))) == Array.get.at(T,i,_) : Array<T> & T}
130 {==}
131
132law swap_node:
133 for -T: Data
134 for +l: Tree.Tree<T>
135 for +r: Tree.Tree<T>
136 for +n: U32
137 for +i: U32
138 for +v: T
139 for +z: Bool
140 for pl: {Array.swap.go(T,Tree.pack(T,l),U32.shr(n),i,v,U32.is_lt(i,U32.shr(U32.shr(n)))) ==
141 (Tree.pack(T,Tree.store(T,l,U32.shr(n),i,v)),Tree.fetch(T,l,U32.shr(n),i)) : Array<T> & T}
142 for pr: {Array.swap.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)),v,U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n)))) ==
143 (Tree.pack(T,Tree.store(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v)),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n)))) : Array<T> & T}
144 {Array.swap.go(T,Tree.pack(T,Tree.Node{l,r}),n,i,v,z) == (Tree.pack(T,Bool.pick(Tree.Tree<T>,z,
145 Tree.Node{Tree.store(T,l,U32.shr(n),i,v),r},Tree.Node{l,Tree.store(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v)})),
146 Bool.pick(T,z,Tree.fetch(T,l,U32.shr(n),i),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n))))) : Array<T> & T}
147def swap_node(T,l,r,n,i,v,z,pl,pr):
148 match z:
149 case True{}:
150 %pl : {Array.swap.lo(T,Tree.pack(T,r),Array.swap.go(T,Tree.pack(T,l),U32.shr(n),i,v,U32.is_lt(i,U32.shr(U32.shr(n))))) ==
151 Array.swap.lo(T,Tree.pack(T,r),_) : Array<T> & T}
152 {==}
153 case False{}:
154 %pr : {Array.swap.hi(T,Tree.pack(T,l),Array.swap.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)),v,
155 U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n))))) == Array.swap.hi(T,Tree.pack(T,l),_) : Array<T> & T}
156 {==}
157
158law swap_go:
159 for -T: Data
160 for +tree: Tree.Tree<T>
161 for +n: U32
162 for +i: U32
163 for +v: T
164 {Array.swap.go(T,Tree.pack(T,tree),n,i,v,U32.is_lt(i,U32.shr(n))) == (Tree.pack(T,Tree.store(T,tree,n,i,v)),
165 Tree.fetch(T,tree,n,i)) : Array<T> & T}
166def swap_go(T,tree,n,i,v):
167 match tree:
168 case Tree.Leaf{old}:
169 {==}
170 case Tree.Node{+l,+r}:
171 swap_node(T,l,r,n,i,v,U32.is_lt(i,U32.shr(n)),swap_go(T,l,U32.shr(n),i,v),swap_go(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v))
172
173law swap:
174 for -T: Data
175 for +tree: Tree.Tree<T>
176 for +i: U32
177 for +v: T
178 {Array.swap(T,Tree.pack(T,tree),i,v) == (Tree.pack(T,Tree.write(T,tree,i,v)),Tree.read(T,tree,i)) : Array<T> & T}
179def swap(T,tree,i,v):
180 %swap_go(T,tree,Tree.capacity(T,tree),U32.and(i,U32.sub(Tree.capacity(T,tree),1)),v) : {Array.swap.at(T,i,v,Array.size(T,
181 Tree.pack(T,tree))) == _ : Array<T> & T}
182 %size(T,tree) : {Array.swap.at(T,i,v,Array.size(T,Tree.pack(T,tree))) == Array.swap.at(T,i,v,_) : Array<T> & T}
183 {==}
184
185def write(T,tree,i,value):
186 %Equal.sym(Array<T> & T,Array.swap(T,Tree.pack(T,tree),i,value),(Tree.pack(T,Tree.write(T,tree,i,value)),
187 Tree.read(T,tree,i)),swap(T,tree,i,value)) : {Array.set.fin(T,_) == Tree.pack(T,Tree.write(T,tree,i,value)) : Array<T>}
188 {==}
189
190def guarded_read(~Element: Data,+fallback: Element,+valid: Bool,+tree: Tree.Tree<Element>,+index: U32) ->
191 {Storage.read_when(Element,fallback,valid,Tree.pack(Element,tree),index) ==
192 (Tree.pack(Element,tree),Bool.pick(Element,valid,Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}:
193 match valid:
194 case False{}: {==}
195 case True{}: read(Element,tree,index)
196
197def bounded_read(~Element: Data,+fallback: Element,+tree: Tree.Tree<Element>,+index: U32,+logical_length: U32) ->
198 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,logical_length) ==
199 (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),
200 Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}:
201 %Equal.sym(Array<Element> & U32,Array.size(Element,Tree.pack(Element,tree)),(Tree.pack(Element,tree),Tree.capacity(Element,tree)),
202 size(Element,tree)) :
203 {Storage.read_sized(Element,fallback,index,logical_length,_) ==
204 (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),
205 Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}
206 guarded_read(~Element,fallback,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),tree,index)
207
208def bounded_read_is_get(~Element: Data,+fallback: Element,+tree: Tree.Tree<Element>,+index: U32,+logical_length: U32,
209 inside: {U32.is_lt(index,logical_length) == True{} : Bool},
210 room: {U32.is_le(logical_length,Tree.capacity(Element,tree)) == True{} : Bool}) ->
211 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,logical_length) ==
212 Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}:
213 %Equal.sym(Array<Element> & U32,Array.size(Element,Tree.pack(Element,tree)),(Tree.pack(Element,tree),Tree.capacity(Element,tree)),
214 size(Element,tree)) :
215 {Storage.read_sized(Element,fallback,index,logical_length,_) == Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}
216 %Equal.sym(Bool,U32.is_lt(index,logical_length),True{},inside) :
217 {Storage.read_when(Element,fallback,_ && U32.is_le(logical_length,Tree.capacity(Element,tree)),Tree.pack(Element,tree),index) ==
218 Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}
219 %Equal.sym(Bool,U32.is_le(logical_length,Tree.capacity(Element,tree)),True{},room) :
220 {Storage.read_when(Element,fallback,_,Tree.pack(Element,tree),index) == Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}
221 {==}
222
223# Sequence transfers preserve native modular addressing for every element type.
224# Logical bounds belong to callers, independently of this representation law.
225def write_sequence(~Element: Data,+values: List<&2,Element>,+offset: U32,+tree: Tree.Tree<Element>) ->
226 {Storage.write_list(Element,values,offset,Tree.pack(Element,tree)) ==
227 Tree.pack(Element,Tree.write_sequence(~Element,values,offset,tree)) : Array<Element>}:
228 match values:
229 case Nil{}: {==}
230 case +head <> +tail:
231 %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,tree),offset,head),
232 Tree.pack(Element,Tree.write(Element,tree,offset,head)),write(Element,tree,offset,head)) :
233 {Storage.write_list(Element,tail,(offset + 1 : U32),_) ==
234 Tree.pack(Element,Tree.write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head))) : Array<Element>}
235 write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head))
236
237def read_sequence(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>) ->
238 {Storage.read_list(Element,count,offset,Tree.pack(Element,tree)) ==
239 Tree.read_sequence(~Element,count,offset,tree) : List<&2,Element>}:
240 match count:
241 case 0n: {==}
242 case 1n+ +rest:
243 %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,tree),offset),
244 (Tree.pack(Element,tree),Tree.read(Element,tree,offset)),read(Element,tree,offset)) :
245 {Storage.bind_pair(Array<Element>,Element,List<&2,Element>,_,storage => value =>
246 value <> Storage.read_list(Element,rest,(offset + 1 : U32),storage)) ==
247 Tree.read(Element,tree,offset) <> Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree) : List<&2,Element>}
248 %read_sequence(~Element,rest,(offset + 1 : U32),tree) :
249 {Tree.read(Element,tree,offset) <> Storage.read_list(Element,rest,(offset + 1 : U32),Tree.pack(Element,tree)) ==
250 Tree.read(Element,tree,offset) <> _ : List<&2,Element>}
251 {==}
252
253def sequence_length(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>) ->
254 {List.length(&2,Element,Tree.read_sequence(~Element,count,offset,tree)) == count : Nat}:
255 match count:
256 case 0n: {==}
257 case 1n+ +rest:
258 %sequence_length(~Element,rest,(offset + 1 : U32),tree) :
259 {1n+List.length(&2,Element,Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree)) == 1n+_ : Nat}
260 {==}
261
262# An observed logical prefix has the actual stored element at every valid index.
263# Capacity need not equal count; address overflow remains explicitly modular.
264def sequence_element(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>,+index: Nat,
265 inside: {Nat.is_lt(index,count) == True{} : Bool}) ->
266 {List.get(&2,Element,Tree.read_sequence(~Element,count,offset,tree),index) ==
267 Some{Tree.read(Element,tree,(offset + U32.from_nat(index) : U32))} : Maybe<&2,Element>}:
268 match count index:
269 case 0n 0n:
270 Empty.absurd({None{} == Some{Tree.read(Element,tree,(offset + 0 : U32))} : Maybe<&2,Element>},WordEncoding.false_true(inside))
271 case 0n 1n+previous:
272 Empty.absurd({None{} == Some{Tree.read(Element,tree,(offset + U32.from_nat(1n+previous) : U32))} : Maybe<&2,Element>},WordEncoding.false_true(inside))
273 case 1n+rest 0n:
274 %Equal.sym(U32,(offset + 0 : U32),offset,Arithmetic.add_zero(offset)) :
275 {Some{Tree.read(Element,tree,offset)} == Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}
276 {==}
277 case 1n+ +rest 1n+ +previous:
278 %Equal.sym(U32,(offset + U32.from_nat(1n+previous) : U32),((offset + 1 : U32) + U32.from_nat(previous) : U32),
279 Projection.indexed_successor(offset,previous)) :
280 {List.get(&2,Element,Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree),previous) ==
281 Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}
282 sequence_element(~Element,rest,(offset + 1 : U32),tree,previous,inside)
283
284def sequence_missing(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>,+index: Nat,
285 outside: {Nat.is_lt(index,count) == False{} : Bool}) ->
286 {List.get(&2,Element,Tree.read_sequence(~Element,count,offset,tree),index) == None{} : Maybe<&2,Element>}:
287 match count index:
288 case 0n index: {==}
289 case 1n+rest 0n:
290 Empty.absurd({Some{Tree.read(Element,tree,offset)} == None{} : Maybe<&2,Element>},
291 WordEncoding.false_true(Equal.sym(Bool,True{},False{},outside)))
292 case 1n+rest 1n+previous:
293 sequence_missing(~Element,rest,(offset + 1 : U32),tree,previous,outside)
294
295def sequence_lookup_case(~Element: Data,+present: Bool,+length: U32,+tree: Tree.Tree<Element>,+index: U32,
296 order: {U32.is_lt(index,length) == present : Bool}) ->
297 {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==
298 Bool.pick(Maybe<&2,Element>,present,Some{Tree.read(Element,tree,index)},None{}) : Maybe<&2,Element>}:
299 match present:
300 case False{}:
301 sequence_missing(~Element,U32.to_nat(length),0,tree,U32.to_nat(index),
302 %Comparison.lt(index,length) : {_ == False{} : Bool}
303 order)
304 case True{}:
305 %Arithmetic.native_roundtrip(index) :
306 {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==
307 Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}
308 %Arithmetic.add_zero_left(U32.from_nat(U32.to_nat(index))) :
309 {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==
310 Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}
311 sequence_element(~Element,U32.to_nat(length),0,tree,U32.to_nat(index),
312 %Comparison.lt(index,length) : {_ == True{} : Bool}
313 order)
314
315def default_after_presence(~Element: Data,+fallback: Element,+present: Bool,+value: Element) ->
316 {Bool.pick(Element,present && True{},value,fallback) ==
317 Maybe.default(&2,Element,Bool.pick(Maybe<&2,Element>,present,Some{value},None{}),fallback) : Element}:
318 match present:
319 case False{}: {==}
320 case True{}: {==}
321
322def bounded_read_observation_case(~Element: Data,+fallback: Element,+present: Bool,+length: U32,+tree: Tree.Tree<Element>,+index: U32,
323 +order: {U32.is_lt(index,length) == present : Bool},room: {U32.is_le(length,Tree.capacity(Element,tree)) == True{} : Bool}) ->
324 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length) ==
325 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,
326 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}:
327 %Equal.sym(Array<Element> & Element,Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length),
328 (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,length) && U32.is_le(length,Tree.capacity(Element,tree)),Tree.read(Element,tree,index),fallback)),
329 bounded_read(~Element,fallback,tree,index,length)) :
330 {_ == (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,
331 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}
332 %Equal.sym(Bool,U32.is_le(length,Tree.capacity(Element,tree)),True{},room) :
333 {(Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,length) && _,Tree.read(Element,tree,index),fallback)) ==
334 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,
335 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}
336 %Equal.sym(Bool,U32.is_lt(index,length),present,order) :
337 {(Tree.pack(Element,tree),Bool.pick(Element,_ && True{},Tree.read(Element,tree,index),fallback)) ==
338 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,
339 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}
340 %Equal.sym(Maybe<&2,Element>,List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),
341 Bool.pick(Maybe<&2,Element>,present,Some{Tree.read(Element,tree,index)},None{}),sequence_lookup_case(~Element,present,length,tree,index,order)) :
342 {(Tree.pack(Element,tree),Bool.pick(Element,present && True{},Tree.read(Element,tree,index),fallback)) ==
343 (Tree.pack(Element,tree),Maybe.default(&2,Element,_,fallback)) : Array<Element> & Element}
344 %default_after_presence(~Element,fallback,present,Tree.read(Element,tree,index)) :
345 {(Tree.pack(Element,tree),Bool.pick(Element,present && True{},Tree.read(Element,tree,index),fallback)) ==
346 (Tree.pack(Element,tree),_) : Array<Element> & Element}
347 {==}
348
349# Full logical-read contract, including out-of-range fallback. Only real
350# capacity is required; the logical length need not fill the allocation.
351def bounded_read_observation(~Element: Data,+fallback: Element,+length: U32,+tree: Tree.Tree<Element>,+index: U32,
352 room: {U32.is_le(length,Tree.capacity(Element,tree)) == True{} : Bool}) ->
353 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length) ==
354 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,
355 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}:
356 bounded_read_observation_case(~Element,fallback,U32.is_lt(index,length),length,tree,index,{==},room)
357
358# A fact about an existing storage prefix, not another runtime container.
359# Both the allocator and an external Array owner must establish these fields.
360type SequenceEvidence<-Element: Data,-length: Nat,-values: List<&2,Element>> is Data:
361 SequenceEvidence{storage: Tree.Tree<Element>,
362 contents: {Tree.read_sequence(~Element,length,0,storage) == values : List<&2,Element>},
363 room: {Nat.is_le(length,U32.to_nat(Tree.capacity(Element,storage))) == True{} : Bool}}
364
365def sequence_storage(-Element: Data,-length: Nat,-values: List<&2,Element>,
366 evidence: SequenceEvidence<Element,length,values>) -> Tree.Tree<Element>:
367 SequenceEvidence{storage,contents,room} = evidence
368 storage
369
370def sequence_owner(-Element: Data,-length: Nat,-values: List<&2,Element>,
371 evidence: SequenceEvidence<Element,length,values>) -> Array<Element>:
372 Tree.pack(Element,sequence_storage(Element,length,values,evidence))
373
374# The unchecked primitive is usable after the caller establishes its logical
375# index bound. This is independent of allocation shape and unused capacity.
376def stored_sequence_element(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,
377 +evidence: SequenceEvidence<Element,length,values>,+index: Nat,
378 inside: {Nat.is_lt(index,length) == True{} : Bool}) ->
379 {Tree.read(Element,sequence_storage(Element,length,values,evidence),U32.from_nat(index)) ==
380 Maybe.default(&2,Element,List.get(&2,Element,values,index),fallback) : Element}:
381 SequenceEvidence{+storage,+contents,room} = evidence
382 %contents :
383 {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,List.get(&2,Element,_,index),fallback) : Element}
384 %Equal.sym(Maybe<&2,Element>,List.get(&2,Element,Tree.read_sequence(~Element,length,0,storage),index),
385 Some{Tree.read(Element,storage,(0 + U32.from_nat(index) : U32))},sequence_element(~Element,length,0,storage,index,inside)) :
386 {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,_,fallback) : Element}
387 %Equal.sym(U32,(0 + U32.from_nat(index) : U32),U32.from_nat(index),Arithmetic.add_zero_left(U32.from_nat(index))) :
388 {Tree.read(Element,storage,U32.from_nat(index)) == Tree.read(Element,storage,_) : Element}
389 {==}
390
391def read_sequence_evidence(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,
392 +evidence: SequenceEvidence<Element,length,values>,+index: U32,+native_length: U32,
393 +length_exact: {U32.to_nat(native_length) == length : Nat}) ->
394 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),index,native_length) ==
395 (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,U32.to_nat(index)),fallback)) : Array<Element> & Element}:
396 SequenceEvidence{+storage,+contents,room} = evidence
397 %contents :
398 {Storage.read_or(Element,fallback,Tree.pack(Element,storage),index,native_length) ==
399 (Tree.pack(Element,storage),Maybe.default(&2,Element,List.get(&2,Element,_,U32.to_nat(index)),fallback)) : Array<Element> & Element}
400 %length_exact :
401 {Storage.read_or(Element,fallback,Tree.pack(Element,storage),index,native_length) ==
402 (Tree.pack(Element,storage),Maybe.default(&2,Element,List.get(&2,Element,Tree.read_sequence(~Element,_,0,storage),U32.to_nat(index)),fallback)) : Array<Element> & Element}
403 bounded_read_observation(~Element,fallback,native_length,storage,index,
404 U32Division.nat_le_native(native_length,Tree.capacity(Element,storage),
405 %Equal.sym(Nat,U32.to_nat(native_length),length,length_exact) :
406 {Nat.is_le(_,U32.to_nat(Tree.capacity(Element,storage))) == True{} : Bool}
407 room))
408
409# The logical address conversion is separate from the physical owner.
410def read_encoded_sequence(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,
411 +evidence: SequenceEvidence<Element,length,values>,+address: U32,+index: Nat,+native_length: U32,
412 address_exact: {U32.to_nat(address) == index : Nat},length_exact: {U32.to_nat(native_length) == length : Nat}) ->
413 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),address,native_length) ==
414 (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,index),fallback)) : Array<Element> & Element}:
415 %address_exact :
416 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),address,native_length) ==
417 (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,_),fallback)) : Array<Element> & Element}
418 read_sequence_evidence(~Element,fallback,length,values,evidence,address,native_length,length_exact)
419
420# Used only in propositions to compare reads from different physical owners.
421def replace_read_owner(~Owner: Type,~Element: Data,owner: Owner,result: Owner & Element) -> Owner & Element:
422 (previous,value) = result
423 (owner,value)
424
425def equivalent_sequence_read(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,
426 +left: SequenceEvidence<Element,length,values>,+right: SequenceEvidence<Element,length,values>,
427 +index: U32,+native_length: U32,+length_exact: {U32.to_nat(native_length) == length : Nat}) ->
428 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,left),index,native_length) ==
429 replace_read_owner(~Array<Element>,~Element,sequence_owner(Element,length,values,left),
430 Storage.read_or(Element,fallback,sequence_owner(Element,length,values,right),index,native_length)) : Array<Element> & Element}:
431 %Equal.sym(Array<Element> & Element,
432 Storage.read_or(Element,fallback,sequence_owner(Element,length,values,right),index,native_length),
433 (sequence_owner(Element,length,values,right),Maybe.default(&2,Element,List.get(&2,Element,values,U32.to_nat(index)),fallback)),
434 read_sequence_evidence(~Element,fallback,length,values,right,index,native_length,length_exact)) :
435 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,left),index,native_length) ==
436 replace_read_owner(~Array<Element>,~Element,sequence_owner(Element,length,values,left),_) : Array<Element> & Element}
437 read_sequence_evidence(~Element,fallback,length,values,left,index,native_length,length_exact)
438
439# Reify an affine owner once for proof consumers that need both its Data model
440# and the relation. This helper is never imported by a numerical runtime path.
441type Observation<-Element: Data,-storage: Array<Element>> is Data:
442 Observation{tree: Tree.Tree<Element>,packed: {Tree.pack(Element,tree) == storage : Array<Element>},
443 reflected: {tree == Tree.reflect(Element,storage) : Tree.Tree<Element>}}
444
445def observed_node_equation(-Element: Data,-left: Array<Element>,-right: Array<Element>,+left_tree: Tree.Tree<Element>,+right_tree: Tree.Tree<Element>,
446 left_packed: {Tree.pack(Element,left_tree) == left : Array<Element>},right_packed: {Tree.pack(Element,right_tree) == right : Array<Element>}) ->
447 {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{left,right} : Array<Element>}:
448 %left_packed : {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{_,right} : Array<Element>}
449 %right_packed : {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{Tree.pack(Element,left_tree),_} : Array<Element>}
450 {==}
451
452def observed_node_reflection(-Element: Data,-left: Array<Element>,-right: Array<Element>,+left_tree: Tree.Tree<Element>,+right_tree: Tree.Tree<Element>,
453 left_reflected: {left_tree == Tree.reflect(Element,left) : Tree.Tree<Element>},
454 right_reflected: {right_tree == Tree.reflect(Element,right) : Tree.Tree<Element>}) ->
455 {Tree.Node{left_tree,right_tree} == Tree.reflect(Element,ANode{left,right}) : Tree.Tree<Element>}:
456 %left_reflected : {Tree.Node{left_tree,right_tree} == Tree.Node{_,Tree.reflect(Element,right)} : Tree.Tree<Element>}
457 %right_reflected : {Tree.Node{left_tree,right_tree} == Tree.Node{left_tree,_} : Tree.Tree<Element>}
458 {==}
459
460def observed_node(-Element: Data,-left: Array<Element>,-right: Array<Element>,
461 left_observation: Observation<Element,left>,right_observation: Observation<Element,right>) -> Observation<Element,ANode{left,right}>:
462 Observation{+left_tree,left_packed,left_reflected} = left_observation
463 Observation{+right_tree,right_packed,right_reflected} = right_observation
464 Observation{Tree.Node{left_tree,right_tree},observed_node_equation(Element,left,right,left_tree,right_tree,left_packed,right_packed),
465 observed_node_reflection(Element,left,right,left_tree,right_tree,left_reflected,right_reflected)}
466def observe(-Element: Data,storage: Array<Element>) -> Observation<Element,storage>:
467 match storage:
468 case ALeaf{+value}: Observation{Tree.Leaf{value},{==},{==}}
469 case ANode{left,right}: observed_node(Element,left,right,observe(Element,left),observe(Element,right))
470
471# Transport a concrete owner observation into a proposition checked on trees.
472# The proposition and canonical proof are proof-only; they are not loop inputs.
473def lift_observation(~Element: Data,~Context: Data,
474 ~Proposition: Context -> @-storage: Array<Element> -> @-tree: Tree.Tree<Element> -> Type,
475 +context: Context,-storage: Array<Element>,observation: Observation<Element,storage>,
476 canonical: @+tree: Tree.Tree<Element> -> Proposition(context,Tree.pack(Element,tree),tree)) ->
477 Proposition(context,storage,Tree.reflect(Element,storage)):
478 Observation{+tree,packed,reflected} = observation
479 %reflected : Proposition(context,storage,_)
480 %packed : Proposition(context,_,tree)
481 canonical(tree)
482
483def lift_pair_observation(~Element: Data,~Context: Data,
484 ~Proposition: Context -> @-input: Array<Element> -> @-output: Array<Element> ->
485 @-input_tree: Tree.Tree<Element> -> @-output_tree: Tree.Tree<Element> -> Type,
486 +context: Context,-input: Array<Element>,-output: Array<Element>,
487 input_observation: Observation<Element,input>,output_observation: Observation<Element,output>,
488 canonical: @+input_tree: Tree.Tree<Element> -> @+output_tree: Tree.Tree<Element> ->
489 Proposition(context,Tree.pack(Element,input_tree),Tree.pack(Element,output_tree),input_tree,output_tree)) ->
490 Proposition(context,input,output,Tree.reflect(Element,input),Tree.reflect(Element,output)):
491 Observation{+input_tree,input_packed,input_reflected} = input_observation
492 Observation{+output_tree,output_packed,output_reflected} = output_observation
493 %input_reflected : Proposition(context,input,output,_,Tree.reflect(Element,output))
494 %output_reflected : Proposition(context,input,output,input_tree,_)
495 %input_packed : Proposition(context,_,output,input_tree,output_tree)
496 %output_packed : Proposition(context,Tree.pack(Element,input_tree),_,input_tree,output_tree)
497 canonical(input_tree)(output_tree)