def masked_read

stelliferous@0.0.2.0 · proofs/kernel_packing_read_witness.bend:18

import stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend as KernelPackingReadWitness

import Base
import stelliferous@0.0.2.0/kernel_spatial_packing.bend as Packing
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

18def masked_read(-input: Array<F32>,+inside: Bool,-result: Array<F32> & F32,observed: Witness.Read<F32,input,result>) ->
19  TraversalWitness.Sample<Array<F32>,F32,input,Packing.masked(inside,result)>:
20  Witness.Read{value,equation} = observed
21  %Equal.sym(Array<F32> & F32,result,(input,value),equation) : TraversalWitness.Sample<Array<F32>,F32,input,Packing.masked(inside,_)>
22  TraversalWitness.Sample{PackingSamples.masked(value,inside),{==}}

Uses (10)

Used by (1)

stelliferous@0.0.2.0/proofs/kernel_packing_read_witness:pixel