proofs/storage_refinement.bend

stelliferous@0.0.2.0 · 497 lines · 39 definitions

1import Base
2import stelliferous@0.0.2.0/storage_buffer.bend as Storage
3import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
4import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
5import stelliferous@0.0.2.0/proofs/loop_projection.bend as Projection
6import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
7import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
8import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
9import stelliferous@0.0.2.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)