def offset_read_refines_storage

stelliferous@0.0.2.0 · proofs/traversal_array_refinement.bend:69

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws

69def offset_read_refines_storage(~Element: Data,+tree: Tree.Tree<Element>,+context: Traversal.Offsets,+position: U32) ->
70  {Traversal.source_offset(~Element,pack_tree(~Element,tree),context,position) ==
71    (pack_tree(~Element,tree),sample_offset(~Element,tree,context,position)) : Array<Element> & Element}:
72  Traversal.Offsets{source,destination} = context
73  StorageLaws.read(Element,tree,(source + position : U32))