def guarded_read

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:190

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

190def guarded_read(~Element: Data,+fallback: Element,+valid: Bool,+tree: Tree.Tree<Element>,+index: U32) ->
191  {Storage.read_when(Element,fallback,valid,Tree.pack(Element,tree),index) ==
192    (Tree.pack(Element,tree),Bool.pick(Element,valid,Tree.read(Element,tree,index),fallback)) : Array<Element> & Element}:
193  match valid:
194    case False{}: {==}
195    case True{}: read(Element,tree,index)