def read_preserved_full

stelliferous@0.0.2.0 · proofs/storage_readback.bend:131

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as Address

131def read_preserved_full(~Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,+index: U32,+query: U32,+value: Element,
132  +balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,31n) == True{} : Bool},
133  +index_inside: {U32.is_lt(index,Tree.capacity(Element,tree)) == True{} : Bool},+query_inside: {U32.is_lt(query,Tree.capacity(Element,tree)) == True{} : Bool},
134  different: {U32.is_eq(index,query) == False{} : Bool}) ->
135  {Tree.read(Element,Tree.write(Element,tree,index,value),query) == Tree.read(Element,tree,query) : Element}:
136  +capacity = Tree.capacity(Element,tree)
137  +capacity_equal = Shape.capacity(Element,depth,tree,balanced)
138  %Equal.sym(U32,Tree.capacity(Element,Tree.write(Element,tree,index,value)),capacity,write_capacity(~Element,tree,index,value)) :
139    {Tree.fetch(Element,Tree.write(Element,tree,index,value),_,U32.and(query,U32.sub(_,1))) == Tree.read(Element,tree,query) : Element}
140  %Equal.sym(U32,U32.and(index,U32.sub(capacity,1)),index,no_wrap(~Element,depth,tree,index,balanced,index_inside)) :
141    {Tree.fetch(Element,Tree.store(Element,tree,capacity,_,value),capacity,U32.and(query,U32.sub(capacity,1))) == Tree.read(Element,tree,query) : Element}
142  %Equal.sym(U32,U32.and(query,U32.sub(capacity,1)),query,no_wrap(~Element,depth,tree,query,balanced,query_inside)) :
143    {Tree.fetch(Element,Tree.store(Element,tree,capacity,index,value),capacity,_) == Tree.fetch(Element,tree,capacity,_) : Element}
144  %Equal.sym(U32,capacity,Address.capacity(depth),capacity_equal) :
145    {Tree.fetch(Element,Tree.store(Element,tree,_,index,value),_,query) == Tree.fetch(Element,tree,_,query) : Element}
146  fetch_preserved(~Element,depth,tree,index,query,value,balanced,limit,
147    %capacity_equal : {U32.is_lt(index,_) == True{} : Bool} index_inside,
148    %capacity_equal : {U32.is_lt(query,_) == True{} : Bool} query_inside,different)