StorageReadback.fetch_preserved: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/storage_readback.bend as StorageReadback Lines 94-120 of stelliferous@0.0.2.0/proofs/storage_readback.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_readback.bend&start_line=94&end_line=120 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 def fetch_preserved(~Element: Data,+depth: Nat,tree: Tree.Tree,+index: U32,+query: U32,+value: Element, balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,31n) == True{} : Bool}, +index_inside: {U32.is_lt(index,Address.capacity(depth)) == True{} : Bool},+query_inside: {U32.is_lt(query,Address.capacity(depth)) == True{} : Bool}, +different: {U32.is_eq(index,query) == False{} : Bool}) -> {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}: match depth tree: case 0n Tree.Leaf{old}: Empty.absurd({value == old : Element},Address.unequal_words(index,query,different,Address.equal_values(index,query, 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))))) case 0n Tree.Node{left,right}: match balanced: case 1n+rest Tree.Leaf{old}: match balanced: case 1n+ +rest Tree.Node{+left,+right}: Shape.Both{+left_balanced,+right_balanced} = balanced +half_equal = Power.native_half_power(rest,Bounds.predecessor_strict(rest,31n,limit)) 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))),{==},{==}, in_left => query_left => %Equal.sym(U32,U32.shr(Address.capacity(1n+rest)),Address.capacity(rest),half_equal) : {Tree.fetch(Element,Tree.store(Element,left,_,index,value),_,query) == Tree.fetch(Element,left,_,query) : Element} fetch_preserved(~Element,rest,left,index,query,value,left_balanced,Address.child_limit_full(rest,limit), %half_equal : {U32.is_lt(index,_) == True{} : Bool} in_left, %half_equal : {U32.is_lt(query,_) == True{} : Bool} query_left,different), in_right => query_right => %Equal.sym(U32,U32.shr(Address.capacity(1n+rest)),Address.capacity(rest),half_equal) : {Tree.fetch(Element,Tree.store(Element,right,_,(index - _ : U32),value),_,(query - _ : U32)) == Tree.fetch(Element,right,_,(query - _ : U32)) : Element} fetch_preserved(~Element,rest,right,(index - Address.capacity(rest) : U32),(query - Address.capacity(rest) : U32),value,right_balanced,Address.child_limit_full(rest,limit), Address.right_stays_in_child_full(rest,index,limit,index_inside,%half_equal : {U32.is_lt(index,_) == False{} : Bool} in_right), 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))) Uses (27): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=predecessor_strict https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=below_one_value https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=capacity https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=child_limit_full https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=equal_values https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=right_stays_in_child_full https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=subtract_distinct https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=unequal_words https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_readback.bend&name=other_node https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Both https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=fetch https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=store https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=native_half_power