KernelPackingReadWitness.first: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend as KernelPackingReadWitness
Lines 68-73 of stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend&start_line=68&end_line=73

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

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

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_packing_samples.bend&name=pixel
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend&name=family
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend&name=masked
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=observed
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=Sample