def bounded_read_observation

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:349

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

349# Full logical-read contract, including out-of-range fallback. Only real
350# capacity is required; the logical length need not fill the allocation.
351def bounded_read_observation(~Element: Data,+fallback: Element,+length: U32,+tree: Tree.Tree<Element>,+index: U32,
352  room: {U32.is_le(length,Tree.capacity(Element,tree)) == True{} : Bool}) ->
353  {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length) ==
354    (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element,
355      Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array<Element> & Element}:
356  bounded_read_observation_case(~Element,fallback,U32.is_lt(index,length),length,tree,index,{==},room)