def first

stelliferous@0.0.2.0 · proofs/kernel_packing_read_witness.bend:68

import Base
import stelliferous@0.0.2.0/kernel_packing_samples.bend as PackingSamples
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

68def first(-input: Array<F32>,+position: U32,+reduction: U32,+height: U32,+width: U32,+kernel: U32,+stride: U32,+padding: U32,+output_width: U32,evidence: family(input)) ->
69  TraversalWitness.Sample<Array<F32>,F32,input,PackingSamples.pixel(input,position,reduction,height,width,kernel,stride,padding,output_width)>:
70  +row = (position / output_width * stride + reduction / kernel % kernel - padding : U32)
71  +column = (position % output_width * stride + reduction % kernel - padding : U32)
72  +index = (reduction / (kernel * kernel) * height * width + row * width + column : U32)
73  masked(input,U32.is_lt(row,height) && U32.is_lt(column,width),Array.get(F32,input,index),Witness.observed(F32,input,index,evidence))