proofs/storage_refinement.bend source

proofs/storage_refinement.bend on the hub · documented module

import Baseimport ../storage_buffer.bend as Storageimport ./storage_tree_model.bend as Treeimport ./storage_witness.bend as Witnessimport ./loop_projection.bend as Projectionimport ./bounded_u32_arithmetic.bend as Arithmeticimport ./word_encoding.bend as WordEncodingimport ./u32_comparison.bend as Comparisonimport ./u32_division.bend as U32Division# The tree model covers every native Array owner, including capacities larger# than its logical sequence. These equalities allocate no runtime conversion.def reflect_packed(-Element: Data,+tree: Tree.Tree<Element>) ->  {Tree.reflect(Element,Tree.pack(Element,tree)) == tree : Tree.Tree<Element>}:  match tree:    case Tree.Leaf{value}: {==}    case Tree.Node{+left,+right}:      %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,left)),left,reflect_packed(Element,left)) :        {Tree.Node{_,Tree.reflect(Element,Tree.pack(Element,right))} == Tree.Node{left,right} : Tree.Tree<Element>}      %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,right)),right,reflect_packed(Element,right)) :        {Tree.Node{left,_} == Tree.Node{left,right} : Tree.Tree<Element>}      {==}def pack_reflected(-Element: Data,storage: Array<Element>) ->  {Tree.pack(Element,Tree.reflect(Element,storage)) == storage : Array<Element>}:  match storage:    case ALeaf{value}: {==}    case ANode{left,right}:      %pack_reflected(Element,left) :        {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{_,right} : Array<Element>}      %pack_reflected(Element,right) :        {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>}      {==}law fresh:  for -T: Data  for +depth: Nat  for +value: T  {Array.new(T,depth,value) == Tree.pack(T,Tree.fresh(T,depth,value)) : Array<T>}law clone:  for -T: Data  for +tree: Tree.Tree<T>  {Array.clone(T,Tree.pack(T,tree)) == (Tree.pack(T,tree),Tree.pack(T,tree)) : Array<T> & Array<T>}law read:  for -T: Data  for +tree: Tree.Tree<T>  for +i: U32  {Array.get(T,Tree.pack(T,tree),i) == (Tree.pack(T,tree),Tree.read(T,tree,i)) : Array<T> & T}law write:  for -T: Data  for +tree: Tree.Tree<T>  for +i: U32  for +value: T  {Array.set(T,Tree.pack(T,tree),i,value) == Tree.pack(T,Tree.write(T,tree,i,value)) : Array<T>}def fresh(T,depth,value):  Witness.fresh_model(T,depth,value)def clone(T,tree):  match tree:    case Tree.Leaf{v}:      {==}    case Tree.Node{+l,+r}:      %Equal.sym(Array<T> & Array<T>,Array.clone(T,Tree.pack(T,l)),(Tree.pack(T,l),Tree.pack(T,l)),        clone(T,l)) : {Array.clone.node(T,_,Array.clone(T,Tree.pack(T,r))) == (Tree.pack(T,            Tree.Node{l,r}),Tree.pack(T,Tree.Node{l,r})) : Array<T> & Array<T>}      %Equal.sym(Array<T> & Array<T>,Array.clone(T,Tree.pack(T,r)),(Tree.pack(T,r),Tree.pack(T,r)),        clone(T,r)) : {Array.clone.node(T,(Tree.pack(T,l),Tree.pack(T,l)),_) == (Tree.pack(T,            Tree.Node{l,r}),Tree.pack(T,Tree.Node{l,r})) : Array<T> & Array<T>}      {==}law size:  for -T: Data  for +tree: Tree.Tree<T>  {Array.size(T,Tree.pack(T,tree)) == (Tree.pack(T,tree),Tree.capacity(T,tree)) : Array<T> & U32}def size(T,tree):  match tree:    case Tree.Leaf{v}:      {==}    case Tree.Node{+l,+r}:      %Equal.sym(Array<T> & U32,Array.size(T,Tree.pack(T,l)),(Tree.pack(T,l),Tree.capacity(T,l)),size(T,          l)) : {Array.size.node(T,Tree.pack(T,r),_) == (Tree.pack(T,Tree.Node{l,r}),U32.shl(Tree.capacity(T,              l))) : Array<T> & U32}      {==}# Base passes the branch z that the caller computed as i < n/2; each child# receives its own comparison against its half. The tree model picks the same# branch, so every lemma holds for any z and the recursion supplies its value.law get_node:  for -T: Data  for +l: Tree.Tree<T>  for +r: Tree.Tree<T>  for +n: U32  for +i: U32  for +z: Bool  for pl: {Array.get.go(T,Tree.pack(T,l),U32.shr(n),i,U32.is_lt(i,U32.shr(U32.shr(n)))) ==      (Tree.pack(T,l),Tree.fetch(T,l,U32.shr(n),i)) : Array<T> & T}  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)))) ==      (Tree.pack(T,r),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n)))) : Array<T> & T}  {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,        Tree.fetch(T,l,U32.shr(n),i),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n))))) : Array<T> & T}def get_node(T,l,r,n,i,z,pl,pr):  match z:    case True{}:      %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))))) ==          Array.swap.lo(T,Tree.pack(T,r),_) : Array<T> & T}      {==}    case False{}:      %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)),          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}      {==}law get_go:  for -T: Data  for +tree: Tree.Tree<T>  for +n: U32  for +i: U32  {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}def get_go(T,tree,n,i):  match tree:    case Tree.Leaf{v}:      {==}    case Tree.Node{+l,+r}:      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))))def read(T,tree,i):  %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,        Tree.pack(T,tree))) == _ : Array<T> & T}  %size(T,tree) : {Array.get.at(T,i,Array.size(T,Tree.pack(T,tree))) == Array.get.at(T,i,_) : Array<T> & T}  {==}law swap_node:  for -T: Data  for +l: Tree.Tree<T>  for +r: Tree.Tree<T>  for +n: U32  for +i: U32  for +v: T  for +z: Bool  for pl: {Array.swap.go(T,Tree.pack(T,l),U32.shr(n),i,v,U32.is_lt(i,U32.shr(U32.shr(n)))) ==      (Tree.pack(T,Tree.store(T,l,U32.shr(n),i,v)),Tree.fetch(T,l,U32.shr(n),i)) : Array<T> & T}  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)))) ==      (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}  {Array.swap.go(T,Tree.pack(T,Tree.Node{l,r}),n,i,v,z) == (Tree.pack(T,Bool.pick(Tree.Tree<T>,z,          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)})),        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}def swap_node(T,l,r,n,i,v,z,pl,pr):  match z:    case True{}:      %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))))) ==          Array.swap.lo(T,Tree.pack(T,r),_) : Array<T> & T}      {==}    case False{}:      %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,          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}      {==}law swap_go:  for -T: Data  for +tree: Tree.Tree<T>  for +n: U32  for +i: U32  for +v: T  {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)),      Tree.fetch(T,tree,n,i)) : Array<T> & T}def swap_go(T,tree,n,i,v):  match tree:    case Tree.Leaf{old}:      {==}    case Tree.Node{+l,+r}:      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))law swap:  for -T: Data  for +tree: Tree.Tree<T>  for +i: U32  for +v: T  {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}def swap(T,tree,i,v):  %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,        Tree.pack(T,tree))) == _ : Array<T> & T}  %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}  {==}def write(T,tree,i,value):  %Equal.sym(Array<T> & T,Array.swap(T,Tree.pack(T,tree),i,value),(Tree.pack(T,Tree.write(T,tree,i,value)),      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>}  {==}def guarded_read(~Element: Data,+fallback: Element,+valid: Bool,+tree: Tree.Tree<Element>,+index: U32) ->  {Storage.read_when(Element,fallback,valid,Tree.pack(Element,tree),index) ==    (Tree.pack(Element,tree),Bool.pick(Element,valid,Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}:  match valid:    case False{}: {==}    case True{}: read(Element,tree,index)def bounded_read(~Element: Data,+fallback: Element,+tree: Tree.Tree<Element>,+index: U32,+logical_length: U32) ->  {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,logical_length) ==    (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),      Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}:  %Equal.sym(Array<Element> & U32,Array.size(Element,Tree.pack(Element,tree)),(Tree.pack(Element,tree),Tree.capacity(Element,tree)),    size(Element,tree)) :    {Storage.read_sized(Element,fallback,index,logical_length,_) ==      (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),        Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}  guarded_read(~Element,fallback,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),tree,index)def bounded_read_is_get(~Element: Data,+fallback: Element,+tree: Tree.Tree<Element>,+index: U32,+logical_length: U32,  inside: {U32.is_lt(index,logical_length) == True{} : Bool},  room: {U32.is_le(logical_length,Tree.capacity(Element,tree)) == True{} : Bool}) ->  {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,logical_length) ==    Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}:  %Equal.sym(Array<Element> & U32,Array.size(Element,Tree.pack(Element,tree)),(Tree.pack(Element,tree),Tree.capacity(Element,tree)),    size(Element,tree)) :    {Storage.read_sized(Element,fallback,index,logical_length,_) == Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}  %Equal.sym(Bool,U32.is_lt(index,logical_length),True{},inside) :    {Storage.read_when(Element,fallback,_ && U32.is_le(logical_length,Tree.capacity(Element,tree)),Tree.pack(Element,tree),index) ==      Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}  %Equal.sym(Bool,U32.is_le(logical_length,Tree.capacity(Element,tree)),True{},room) :    {Storage.read_when(Element,fallback,_,Tree.pack(Element,tree),index) == Array.get(Element,Tree.pack(Element,tree),index) : Array<Element> & Element}  {==}# Sequence transfers preserve native modular addressing for every element type.# Logical bounds belong to callers, independently of this representation law.def write_sequence(~Element: Data,+values: List<&2,Element>,+offset: U32,+tree: Tree.Tree<Element>) ->  {Storage.write_list(Element,values,offset,Tree.pack(Element,tree)) ==    Tree.pack(Element,Tree.write_sequence(~Element,values,offset,tree)) : Array<Element>}:  match values:    case Nil{}: {==}    case +head <> +tail:      %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,tree),offset,head),        Tree.pack(Element,Tree.write(Element,tree,offset,head)),write(Element,tree,offset,head)) :        {Storage.write_list(Element,tail,(offset + 1 : U32),_) ==          Tree.pack(Element,Tree.write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head))) : Array<Element>}      write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head))def read_sequence(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>) ->  {Storage.read_list(Element,count,offset,Tree.pack(Element,tree)) ==    Tree.read_sequence(~Element,count,offset,tree) : List<&2,Element>}:  match count:    case 0n: {==}    case 1n+ +rest:      %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,tree),offset),        (Tree.pack(Element,tree),Tree.read(Element,tree,offset)),read(Element,tree,offset)) :        {Storage.bind_pair(Array<Element>,Element,List<&2,Element>,_,storage => value =>          value <> Storage.read_list(Element,rest,(offset + 1 : U32),storage)) ==          Tree.read(Element,tree,offset) <> Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree) : List<&2,Element>}      %read_sequence(~Element,rest,(offset + 1 : U32),tree) :        {Tree.read(Element,tree,offset) <> Storage.read_list(Element,rest,(offset + 1 : U32),Tree.pack(Element,tree)) ==          Tree.read(Element,tree,offset) <> _ : List<&2,Element>}      {==}def sequence_length(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>) ->  {List.length(&2,Element,Tree.read_sequence(~Element,count,offset,tree)) == count : Nat}:  match count:    case 0n: {==}    case 1n+ +rest:      %sequence_length(~Element,rest,(offset + 1 : U32),tree) :        {1n+List.length(&2,Element,Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree)) == 1n+_ : Nat}      {==}# An observed logical prefix has the actual stored element at every valid index.# Capacity need not equal count; address overflow remains explicitly modular.def sequence_element(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>,+index: Nat,  inside: {Nat.is_lt(index,count) == True{} : Bool}) ->  {List.get(&2,Element,Tree.read_sequence(~Element,count,offset,tree),index) ==    Some{Tree.read(Element,tree,(offset + U32.from_nat(index) : U32))} : Maybe<&2,Element>}:  match count index:    case 0n 0n:      Empty.absurd({None{} == Some{Tree.read(Element,tree,(offset + 0 : U32))} : Maybe<&2,Element>},WordEncoding.false_true(inside))    case 0n 1n+previous:      Empty.absurd({None{} == Some{Tree.read(Element,tree,(offset + U32.from_nat(1n+previous) : U32))} : Maybe<&2,Element>},WordEncoding.false_true(inside))    case 1n+rest 0n:      %Equal.sym(U32,(offset + 0 : U32),offset,Arithmetic.add_zero(offset)) :        {Some{Tree.read(Element,tree,offset)} == Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}      {==}    case 1n+ +rest 1n+ +previous:      %Equal.sym(U32,(offset + U32.from_nat(1n+previous) : U32),((offset + 1 : U32) + U32.from_nat(previous) : U32),        Projection.indexed_successor(offset,previous)) :        {List.get(&2,Element,Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree),previous) ==          Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}      sequence_element(~Element,rest,(offset + 1 : U32),tree,previous,inside)def sequence_missing(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>,+index: Nat,  outside: {Nat.is_lt(index,count) == False{} : Bool}) ->  {List.get(&2,Element,Tree.read_sequence(~Element,count,offset,tree),index) == None{} : Maybe<&2,Element>}:  match count index:    case 0n index: {==}    case 1n+rest 0n:      Empty.absurd({Some{Tree.read(Element,tree,offset)} == None{} : Maybe<&2,Element>},        WordEncoding.false_true(Equal.sym(Bool,True{},False{},outside)))    case 1n+rest 1n+previous:      sequence_missing(~Element,rest,(offset + 1 : U32),tree,previous,outside)def sequence_lookup_case(~Element: Data,+present: Bool,+length: U32,+tree: Tree.Tree<Element>,+index: U32,  order: {U32.is_lt(index,length) == present : Bool}) ->  {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==    Bool.pick(Maybe<&2,Element>,present,Some{Tree.read(Element,tree,index)},None{}) : Maybe<&2,Element>}:  match present:    case False{}:      sequence_missing(~Element,U32.to_nat(length),0,tree,U32.to_nat(index),        %Comparison.lt(index,length) : {_ == False{} : Bool}        order)    case True{}:      %Arithmetic.native_roundtrip(index) :        {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==          Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}      %Arithmetic.add_zero_left(U32.from_nat(U32.to_nat(index))) :        {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==          Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}      sequence_element(~Element,U32.to_nat(length),0,tree,U32.to_nat(index),        %Comparison.lt(index,length) : {_ == True{} : Bool}        order)def default_after_presence(~Element: Data,+fallback: Element,+present: Bool,+value: Element) ->  {Bool.pick(Element,present && True{},value,fallback) ==    Maybe.default(&2,Element,Bool.pick(Maybe<&2,Element>,present,Some{value},None{}),fallback) : Element}:  match present:    case False{}: {==}    case True{}: {==}def bounded_read_observation_case(~Element: Data,+fallback: Element,+present: Bool,+length: U32,+tree: Tree.Tree<Element>,+index: U32,  +order: {U32.is_lt(index,length) == present : Bool},room: {U32.is_le(length,Tree.capacity(Element,tree)) == True{} : Bool}) ->  {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length) ==    (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,      Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}:  %Equal.sym(Array<Element> & Element,Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length),    (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)),    bounded_read(~Element,fallback,tree,index,length)) :    {_ == (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,      Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}  %Equal.sym(Bool,U32.is_le(length,Tree.capacity(Element,tree)),True{},room) :    {(Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,length) && _,Tree.read(Element,tree,index),fallback)) ==      (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,        Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}  %Equal.sym(Bool,U32.is_lt(index,length),present,order) :    {(Tree.pack(Element,tree),Bool.pick(Element,_ && True{},Tree.read(Element,tree,index),fallback)) ==      (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,        Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}  %Equal.sym(Maybe<&2,Element>,List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),    Bool.pick(Maybe<&2,Element>,present,Some{Tree.read(Element,tree,index)},None{}),sequence_lookup_case(~Element,present,length,tree,index,order)) :    {(Tree.pack(Element,tree),Bool.pick(Element,present && True{},Tree.read(Element,tree,index),fallback)) ==      (Tree.pack(Element,tree),Maybe.default(&2,Element,_,fallback)) : Array<Element> & Element}  %default_after_presence(~Element,fallback,present,Tree.read(Element,tree,index)) :    {(Tree.pack(Element,tree),Bool.pick(Element,present && True{},Tree.read(Element,tree,index),fallback)) ==      (Tree.pack(Element,tree),_) : Array<Element> & Element}  {==}# Full logical-read contract, including out-of-range fallback. Only real# capacity is required; the logical length need not fill the allocation.def bounded_read_observation(~Element: Data,+fallback: Element,+length: U32,+tree: Tree.Tree<Element>,+index: U32,  room: {U32.is_le(length,Tree.capacity(Element,tree)) == True{} : Bool}) ->  {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length) ==    (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,      Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}:  bounded_read_observation_case(~Element,fallback,U32.is_lt(index,length),length,tree,index,{==},room)# A fact about an existing storage prefix, not another runtime container.# Both the allocator and an external Array owner must establish these fields.type SequenceEvidence<-Element: Data,-length: Nat,-values: List<&2,Element>> is Data:  SequenceEvidence{storage: Tree.Tree<Element>,    contents: {Tree.read_sequence(~Element,length,0,storage) == values : List<&2,Element>},    room: {Nat.is_le(length,U32.to_nat(Tree.capacity(Element,storage))) == True{} : Bool}}def sequence_storage(-Element: Data,-length: Nat,-values: List<&2,Element>,  evidence: SequenceEvidence<Element,length,values>) -> Tree.Tree<Element>:  SequenceEvidence{storage,contents,room} = evidence  storagedef sequence_owner(-Element: Data,-length: Nat,-values: List<&2,Element>,  evidence: SequenceEvidence<Element,length,values>) -> Array<Element>:  Tree.pack(Element,sequence_storage(Element,length,values,evidence))# The unchecked primitive is usable after the caller establishes its logical# index bound. This is independent of allocation shape and unused capacity.def stored_sequence_element(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,  +evidence: SequenceEvidence<Element,length,values>,+index: Nat,  inside: {Nat.is_lt(index,length) == True{} : Bool}) ->  {Tree.read(Element,sequence_storage(Element,length,values,evidence),U32.from_nat(index)) ==    Maybe.default(&2,Element,List.get(&2,Element,values,index),fallback) : Element}:  SequenceEvidence{+storage,+contents,room} = evidence  %contents :    {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,List.get(&2,Element,_,index),fallback) : Element}  %Equal.sym(Maybe<&2,Element>,List.get(&2,Element,Tree.read_sequence(~Element,length,0,storage),index),    Some{Tree.read(Element,storage,(0 + U32.from_nat(index) : U32))},sequence_element(~Element,length,0,storage,index,inside)) :    {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,_,fallback) : Element}  %Equal.sym(U32,(0 + U32.from_nat(index) : U32),U32.from_nat(index),Arithmetic.add_zero_left(U32.from_nat(index))) :    {Tree.read(Element,storage,U32.from_nat(index)) == Tree.read(Element,storage,_) : Element}  {==}def read_sequence_evidence(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,  +evidence: SequenceEvidence<Element,length,values>,+index: U32,+native_length: U32,  +length_exact: {U32.to_nat(native_length) == length : Nat}) ->  {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),index,native_length) ==    (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,U32.to_nat(index)),fallback)) : Array<Element> & Element}:  SequenceEvidence{+storage,+contents,room} = evidence  %contents :    {Storage.read_or(Element,fallback,Tree.pack(Element,storage),index,native_length) ==      (Tree.pack(Element,storage),Maybe.default(&2,Element,List.get(&2,Element,_,U32.to_nat(index)),fallback)) : Array<Element> & Element}  %length_exact :    {Storage.read_or(Element,fallback,Tree.pack(Element,storage),index,native_length) ==      (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}  bounded_read_observation(~Element,fallback,native_length,storage,index,    U32Division.nat_le_native(native_length,Tree.capacity(Element,storage),      %Equal.sym(Nat,U32.to_nat(native_length),length,length_exact) :        {Nat.is_le(_,U32.to_nat(Tree.capacity(Element,storage))) == True{} : Bool}      room))# The logical address conversion is separate from the physical owner.def read_encoded_sequence(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,  +evidence: SequenceEvidence<Element,length,values>,+address: U32,+index: Nat,+native_length: U32,  address_exact: {U32.to_nat(address) == index : Nat},length_exact: {U32.to_nat(native_length) == length : Nat}) ->  {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),address,native_length) ==    (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,index),fallback)) : Array<Element> & Element}:  %address_exact :    {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),address,native_length) ==      (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,_),fallback)) : Array<Element> & Element}  read_sequence_evidence(~Element,fallback,length,values,evidence,address,native_length,length_exact)# Used only in propositions to compare reads from different physical owners.def replace_read_owner(~Owner: Type,~Element: Data,owner: Owner,result: Owner & Element) -> Owner & Element:  (previous,value) = result  (owner,value)def equivalent_sequence_read(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,  +left: SequenceEvidence<Element,length,values>,+right: SequenceEvidence<Element,length,values>,  +index: U32,+native_length: U32,+length_exact: {U32.to_nat(native_length) == length : Nat}) ->  {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,left),index,native_length) ==    replace_read_owner(~Array<Element>,~Element,sequence_owner(Element,length,values,left),      Storage.read_or(Element,fallback,sequence_owner(Element,length,values,right),index,native_length)) : Array<Element> & Element}:  %Equal.sym(Array<Element> & Element,    Storage.read_or(Element,fallback,sequence_owner(Element,length,values,right),index,native_length),    (sequence_owner(Element,length,values,right),Maybe.default(&2,Element,List.get(&2,Element,values,U32.to_nat(index)),fallback)),    read_sequence_evidence(~Element,fallback,length,values,right,index,native_length,length_exact)) :    {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,left),index,native_length) ==      replace_read_owner(~Array<Element>,~Element,sequence_owner(Element,length,values,left),_) : Array<Element> & Element}  read_sequence_evidence(~Element,fallback,length,values,left,index,native_length,length_exact)# Reify an affine owner once for proof consumers that need both its Data model# and the relation. This helper is never imported by a numerical runtime path.type Observation<-Element: Data,-storage: Array<Element>> is Data:  Observation{tree: Tree.Tree<Element>,packed: {Tree.pack(Element,tree) == storage : Array<Element>},    reflected: {tree == Tree.reflect(Element,storage) : Tree.Tree<Element>}}def observed_node_equation(-Element: Data,-left: Array<Element>,-right: Array<Element>,+left_tree: Tree.Tree<Element>,+right_tree: Tree.Tree<Element>,  left_packed: {Tree.pack(Element,left_tree) == left : Array<Element>},right_packed: {Tree.pack(Element,right_tree) == right : Array<Element>}) ->  {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{left,right} : Array<Element>}:  %left_packed : {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{_,right} : Array<Element>}  %right_packed : {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{Tree.pack(Element,left_tree),_} : Array<Element>}  {==}def observed_node_reflection(-Element: Data,-left: Array<Element>,-right: Array<Element>,+left_tree: Tree.Tree<Element>,+right_tree: Tree.Tree<Element>,  left_reflected: {left_tree == Tree.reflect(Element,left) : Tree.Tree<Element>},  right_reflected: {right_tree == Tree.reflect(Element,right) : Tree.Tree<Element>}) ->  {Tree.Node{left_tree,right_tree} == Tree.reflect(Element,ANode{left,right}) : Tree.Tree<Element>}:  %left_reflected : {Tree.Node{left_tree,right_tree} == Tree.Node{_,Tree.reflect(Element,right)} : Tree.Tree<Element>}  %right_reflected : {Tree.Node{left_tree,right_tree} == Tree.Node{left_tree,_} : Tree.Tree<Element>}  {==}def observed_node(-Element: Data,-left: Array<Element>,-right: Array<Element>,  left_observation: Observation<Element,left>,right_observation: Observation<Element,right>) -> Observation<Element,ANode{left,right}>:  Observation{+left_tree,left_packed,left_reflected} = left_observation  Observation{+right_tree,right_packed,right_reflected} = right_observation  Observation{Tree.Node{left_tree,right_tree},observed_node_equation(Element,left,right,left_tree,right_tree,left_packed,right_packed),    observed_node_reflection(Element,left,right,left_tree,right_tree,left_reflected,right_reflected)}def observe(-Element: Data,storage: Array<Element>) -> Observation<Element,storage>:  match storage:    case ALeaf{+value}: Observation{Tree.Leaf{value},{==},{==}}    case ANode{left,right}: observed_node(Element,left,right,observe(Element,left),observe(Element,right))# Transport a concrete owner observation into a proposition checked on trees.# The proposition and canonical proof are proof-only; they are not loop inputs.def lift_observation(~Element: Data,~Context: Data,  ~Proposition: Context -> @-storage: Array<Element> -> @-tree: Tree.Tree<Element> -> Type,  +context: Context,-storage: Array<Element>,observation: Observation<Element,storage>,  canonical: @+tree: Tree.Tree<Element> -> Proposition(context,Tree.pack(Element,tree),tree)) ->  Proposition(context,storage,Tree.reflect(Element,storage)):  Observation{+tree,packed,reflected} = observation  %reflected : Proposition(context,storage,_)  %packed : Proposition(context,_,tree)  canonical(tree)def lift_pair_observation(~Element: Data,~Context: Data,  ~Proposition: Context -> @-input: Array<Element> -> @-output: Array<Element> ->    @-input_tree: Tree.Tree<Element> -> @-output_tree: Tree.Tree<Element> -> Type,  +context: Context,-input: Array<Element>,-output: Array<Element>,  input_observation: Observation<Element,input>,output_observation: Observation<Element,output>,  canonical: @+input_tree: Tree.Tree<Element> -> @+output_tree: Tree.Tree<Element> ->    Proposition(context,Tree.pack(Element,input_tree),Tree.pack(Element,output_tree),input_tree,output_tree)) ->  Proposition(context,input,output,Tree.reflect(Element,input),Tree.reflect(Element,output)):  Observation{+input_tree,input_packed,input_reflected} = input_observation  Observation{+output_tree,output_packed,output_reflected} = output_observation  %input_reflected : Proposition(context,input,output,_,Tree.reflect(Element,output))  %output_reflected : Proposition(context,input,output,input_tree,_)  %input_packed : Proposition(context,_,output,input_tree,output_tree)  %output_packed : Proposition(context,Tree.pack(Element,input_tree),_,input_tree,output_tree)  canonical(input_tree)(output_tree)