def read_line_sample

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:323

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

323# The one-axis window reduction: every sample is an element of the input or
324# the pad, so the sweep returns its input and writes only its output.
325def read_line_sample(~Element: Data,-input: Array<Element>,line: Access.Line<Element>,position: U32,
326  evidence: Witness.ArrayWitness<Element,input>) ->
327  TraversalWitness.Sample<Array<Element>,Element,input,Access.read_line(~Element,input,line,position)>:
328  Access.Line{+base,+first,+extent,+step,+padding,+pad} = line
329  +coordinate = (first + position - padding : U32)
330  window_read_sample(~Element,pad,U32.is_lt(coordinate,extent),input,(base + coordinate * step : U32),evidence)