def fetch_preserved

stelliferous@0.0.2.0 · proofs/storage_readback.bend:94

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
import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Power
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

94def fetch_preserved(~Element: Data,+depth: Nat,tree: Tree.Tree<Element>,+index: U32,+query: U32,+value: Element,
95  balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,31n) == True{} : Bool},
96  +index_inside: {U32.is_lt(index,Address.capacity(depth)) == True{} : Bool},+query_inside: {U32.is_lt(query,Address.capacity(depth)) == True{} : Bool},
97  +different: {U32.is_eq(index,query) == False{} : Bool}) ->
98  {Tree.fetch(Element,Tree.store(Element,tree,Address.capacity(depth),index,value),Address.capacity(depth),query) == Tree.fetch(Element,tree,Address.capacity(depth),query) : Element}:
99  match depth tree:
100    case 0n Tree.Leaf{old}:
101      Empty.absurd({value == old : Element},Address.unequal_words(index,query,different,Address.equal_values(index,query,
102        Equal.trans(Nat,U32.to_nat(index),0n,U32.to_nat(query),Equal.sym(Nat,0n,U32.to_nat(index),Address.below_one_value(index,index_inside)),Address.below_one_value(query,query_inside)))))
103    case 0n Tree.Node{left,right}: match balanced:
104    case 1n+rest Tree.Leaf{old}: match balanced:
105    case 1n+ +rest Tree.Node{+left,+right}:
106      Shape.Both{+left_balanced,+right_balanced} = balanced
107      +half_equal = Power.native_half_power(rest,Bounds.predecessor_strict(rest,31n,limit))
108      other_node(~Element,left,right,Address.capacity(1n+rest),index,query,value,U32.is_lt(index,U32.shr(Address.capacity(1n+rest))),U32.is_lt(query,U32.shr(Address.capacity(1n+rest))),{==},{==},
109        in_left => query_left =>
110          %Equal.sym(U32,U32.shr(Address.capacity(1n+rest)),Address.capacity(rest),half_equal) :
111            {Tree.fetch(Element,Tree.store(Element,left,_,index,value),_,query) == Tree.fetch(Element,left,_,query) : Element}
112          fetch_preserved(~Element,rest,left,index,query,value,left_balanced,Address.child_limit_full(rest,limit),
113            %half_equal : {U32.is_lt(index,_) == True{} : Bool} in_left,
114            %half_equal : {U32.is_lt(query,_) == True{} : Bool} query_left,different),
115        in_right => query_right =>
116          %Equal.sym(U32,U32.shr(Address.capacity(1n+rest)),Address.capacity(rest),half_equal) :
117            {Tree.fetch(Element,Tree.store(Element,right,_,(index - _ : U32),value),_,(query - _ : U32)) == Tree.fetch(Element,right,_,(query - _ : U32)) : Element}
118          fetch_preserved(~Element,rest,right,(index - Address.capacity(rest) : U32),(query - Address.capacity(rest) : U32),value,right_balanced,Address.child_limit_full(rest,limit),
119            Address.right_stays_in_child_full(rest,index,limit,index_inside,%half_equal : {U32.is_lt(index,_) == False{} : Bool} in_right),
120            Address.right_stays_in_child_full(rest,query,limit,query_inside,%half_equal : {U32.is_lt(query,_) == False{} : Bool} query_right),Address.subtract_distinct(index,query,Address.capacity(rest),different)))