def pixel

stelliferous@0.0.2.0 · proofs/kernel_packing_read_witness.bend:24

import Base
import stelliferous@0.0.2.0/kernel_spatial_packing.bend as Packing
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

24def pixel(-input: Array<F32>,+row: U32,+column: U32,+channel: U32,+height: U32,+width: U32,evidence: family(input)) ->
25  TraversalWitness.Sample<Array<F32>,F32,input,Packing.pixel(input,row,column,channel,height,width)>:
26  +index = (channel + row * width + column : U32)
27  masked_read(input,U32.is_lt(row,height) && U32.is_lt(column,width),Array.get(F32,input,index),Witness.observed(F32,input,index,evidence))