def swept_sample

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:342

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

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