StorageRefinement.bounded_read_observation: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
Lines 349-356 of stelliferous@0.0.2.0/proofs/storage_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&start_line=349&end_line=356

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

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

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  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_le
  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.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=bounded_read_observation_case
  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=capacity
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=read_sequence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_buffer.bend&name=read_or