def bounded_read

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:197

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

197def bounded_read(~Element: Data,+fallback: Element,+tree: Tree.Tree<Element>,+index: U32,+logical_length: U32) ->
198  {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,logical_length) ==
199    (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),
200      Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}:
201  %Equal.sym(Array<Element> & U32,Array.size(Element,Tree.pack(Element,tree)),(Tree.pack(Element,tree),Tree.capacity(Element,tree)),
202    size(Element,tree)) :
203    {Storage.read_sized(Element,fallback,index,logical_length,_) ==
204      (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),
205        Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}
206  guarded_read(~Element,fallback,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),tree,index)