def indexed_read

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:291

import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as TensorAccessCertificate

import Base
import stelliferous@0.0.2.0/tensor_access.bend as Access
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

291def indexed_read(~Element: Data,~operation: U32 -> Element -> Element,-storage: Array<Element>,context: Traversal.Offsets,index: U32,
292  evidence: Witness.ArrayWitness<Element,storage>) ->
293  TraversalWitness.Sample<Array<Element>,Element,storage,Access.read_indexed(~Element,~operation,storage,context,index)>:
294  +index = index
295  indexed_sample(~Element,~operation,storage,index,Traversal.source_offset(~Element,storage,context,index),
296    TraversalWitness.offset_read(~Element,storage,context,index,evidence))

Uses (9)

Used by (1)

stelliferous@0.0.2.0/proofs/tensor_access_certificate:indexed