def offset_read

stelliferous@0.0.2.0 · proofs/traversal_witness.bend:78

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

78def offset_read(~Element: Data,-storage: Array<Element>,context: Traversal.Offsets,index: U32,
79  evidence: Witness.ArrayWitness<Element,storage>) ->
80  Sample<Array<Element>,Element,storage,Traversal.source_offset(~Element,storage,context,index)>:
81  Traversal.Offsets{source,destination} = context
82  array_sample(~Element,storage,Array.get(Element,storage,(source + index : U32)),Witness.observed(Element,storage,(source + index : U32),evidence))