TensorAccessCertificate.swept_sample: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as TensorAccessCertificate
Lines 342-354 of stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&start_line=342&end_line=354

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/traversal_loop.bend as Loop
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

def swept_sample(~Element: Data,~operation: Element -> Element -> Element,-input: Array<Element>,context: Access.SweepContext<Element>,position: U32,
  evidence: Witness.ArrayWitness<Element,input>) ->
  TraversalWitness.Sample<Array<Element>,Element,input,Access.read_swept(~Element,~operation,input,context,position)>:
  Access.SweepContext{+sweep,+pad} = context
  Access.Sweep{extent,step,+kernel,stride,padding,out_extent,origin} = sweep
  +position = position
  line_sample(~Element,input,
    Loop.run(~Traversal.State<&1,&2,Array<Element>,Element,Access.Line<Element>>,
      ~Traversal.fold_step(~Array<Element>,~Element,~Element,~Access.Line<Element>,~Access.read_line(~Element),~operation),
      U32.to_nat(kernel),Traversal.State{input,pad,0,Access.line_at(~Element,sweep,pad,position)}),
    TraversalWitness.fold_run(~Array<Element>,~Element,~Element,~Access.Line<Element>,~TraversalWitness.array_evidence(~Element),~Access.read_line(~Element),~operation,
      ~read_line_sample(~Element),U32.to_nat(kernel),input,Traversal.State{input,pad,0,Access.line_at(~Element,sweep,pad,position)},evidence,
      TraversalWitness.FoldEvidence{pad,0,Access.line_at(~Element,sweep,pad,position),{==}}))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=ArrayWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=line_sample
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=read_line_sample
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=FoldEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=Sample
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=array_evidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=fold_run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=Line
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=Sweep
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=SweepContext
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=line_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=read_line
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=read_swept
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=fold_step
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_loop.bend&name=run