def unchanged_full

stelliferous@0.0.2.0 · proofs/traversal_map_readback.bend:48

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_readback.bend as StorageReadback

48def unchanged_full(~Element: Data,+depth: Nat,+input: Tree.Tree<Element>,+position: U32,+query: U32,+value: Element,+capacity: U32,
49  +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},balanced: Shape.Balanced(Element,depth,input),limit: {Nat.is_le(depth,31n) == True{} : Bool},
50  position_inside: {U32.is_lt(position,capacity) == True{} : Bool},query_inside: {U32.is_lt(query,capacity) == True{} : Bool},different: {U32.is_eq(position,query) == False{} : Bool}) ->
51  {Tree.read(Element,Tree.write(Element,input,position,value),query) == Tree.read(Element,input,query) : Element}:
52  StorageReadback.read_preserved_full(~Element,depth,input,position,query,value,balanced,limit,
53    %Equal.sym(U32,Tree.capacity(Element,input),capacity,capacity_equal) : {U32.is_lt(position,_) == True{} : Bool} position_inside,
54    %Equal.sym(U32,Tree.capacity(Element,input),capacity,capacity_equal) : {U32.is_lt(query,_) == True{} : Bool} query_inside,different)