def address

stelliferous@0.0.2.0 · proofs/kernel_packing_read_witness.bend:59

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

59def address(-input: Array<F32>,address: PackingSamples.PixelAddress,evidence: family(input)) ->
60  TraversalWitness.Sample<Array<F32>,F32,input,PackingSamples.read_pixel_address(input,address)>:
61  PackingSamples.PixelAddress{+index,inside} = address
62  masked(input,inside,Array.get(F32,input,index),Witness.observed(F32,input,index,evidence))