~/bend-docscommunity

proofs/kernel_packing_read_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend as Kernel_packing_read_witness

7 imports
import Base
import ../kernel_spatial_packing.bend as Packing
import ../kernel_packing_samples.bend as PackingSamples
import ./storage_witness.bend as Witness
import ./traversal_witness.bend as TraversalWitness
import ../kernel_tile.bend as Tile
import ./kernel_tile_witness.bend as TileWitness

Definitions

def family source · line 9 · raw

@-input:Array<F32> -> Data

def masked source · line 12 · raw

@-input:Array<F32> -> @+inside:Bool -> @-result:Pair(Array<F32>, F32) -> @observed:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, input, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_samples.mask_pixel(inside, result)>

def masked_read source · line 18 · raw

@-input:Array<F32> -> @+inside:Bool -> @-result:Pair(Array<F32>, F32) -> @observed:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, input, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.masked(inside, result)>

def pixel source · line 24 · raw

@-input:Array<F32> -> @+row:U32 -> @+column:U32 -> @+channel:U32 -> @+height:U32 -> @+width:U32 -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.pixel(input, row, column, channel, height, width)>

def row_read source · line 29 · raw

@-input:Array<F32> -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.PixelBlock -> @index:Nat -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.read_block_pixel(input, context, index)>

def row_block source · line 34 · raw

@-input:Array<F32> -> @+row:U32 -> @+column:U32 -> @+channel:U32 -> @+height:U32 -> @+width:U32 -> @+stride:U32 -> @+next_row:U32 -> @+offset:U32 -> @+output_width:U32 -> @+kernel_column:U32 -> @+padding:U32 -> @+evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>

def wrap_pixel source · line 39 · raw

@same:Bool -> @-input:Array<F32> -> @+row:U32 -> @+column:U32 -> @+channel:U32 -> @+height:U32 -> @+width:U32 -> @+stride:U32 -> @+next_row:U32 -> @+offset:U32 -> @+output_width:U32 -> @+kernel_column:U32 -> @+padding:U32 -> @+lane:U32 -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.wrap_pixel(same, input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding, lane)>

def wrap_lane source · line 45 · raw

@-input:Array<F32> -> @+row:U32 -> @+column:U32 -> @+channel:U32 -> @+height:U32 -> @+width:U32 -> @+stride:U32 -> @+next_row:U32 -> @+offset:U32 -> @+output_width:U32 -> @+kernel_column:U32 -> @+padding:U32 -> @+lane:U32 -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.wrap_lane(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding, lane)>

def wrap_read source · line 49 · raw

@-input:Array<F32> -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.WrapBlock -> @index:Nat -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.read_wrap_pixel(input, context, index)>

def wrap_block source · line 54 · raw

@-input:Array<F32> -> @+row:U32 -> @+column:U32 -> @+channel:U32 -> @+height:U32 -> @+width:U32 -> @+stride:U32 -> @+next_row:U32 -> @+offset:U32 -> @+output_width:U32 -> @+kernel_column:U32 -> @+padding:U32 -> @+evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.wrap_block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>

def address source · line 59 · raw

@-input:Array<F32> -> @address:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_samples.PixelAddress -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_samples.read_pixel_address(input, address)>

def crossing_read source · line 64 · raw

@-input:Array<F32> -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_samples.PixelBlock -> @index:Nat -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_samples.read_block_pixel(input, context, index)>

def first source · line 68 · raw

@-input:Array<F32> -> @+position:U32 -> @+reduction:U32 -> @+height:U32 -> @+width:U32 -> @+kernel:U32 -> @+stride:U32 -> @+padding:U32 -> @+output_width:U32 -> @evidence:family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, F32, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_samples.pixel(input, position, reduction, height, width, kernel, stride, padding, output_width)>