def read

stelliferous@0.0.2.0 · proofs/tensor_indexed_certificate.bend:21

import Base
import stelliferous@0.0.2.0/tensor_indexed.bend as Indexed
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

21def read(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element,
22  -input: Array<Element>,context: Context,position: U32,evidence: Witness.ArrayWitness<Element,input>) ->
23  TraversalWitness.Sample<Array<Element>,Element,input,Indexed.read(~Element,~Context,~index,~operation,input,context,position)>:
24  +position = position
25  sample(~Element,~Context,~index,~operation,input,context,position,Array.get(Element,input,position),
26    TraversalWitness.array_sample(~Element,input,Array.get(Element,input,position),Witness.observed(Element,input,position,evidence)))