~/bend-docscommunity

proofs/kernel_packing_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend as Kernel_packing_witness

The packer hands back its input unchanged and keeps the witness of its output: every loop of kernel_spatial_packing preserves both.

9 imports
import Base
import ../traversal_loop.bend as Loop
import ../kernel_spatial_packing.bend as Packing
import ../kernel_packing_samples.bend as PackingSamples
import ../kernel_tile.bend as Tile
import ./storage_witness.bend as Witness
import ./traversal_witness.bend as TraversalWitness
import ./kernel_packing_read_witness.bend as PackingReadWitness
import ./kernel_tile_witness.bend as TileWitness

Types

type RowCursor source · line 13 · raw

Data

type RowEvidence source · line 20 · raw

@-input:Array<F32> -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> Data

type CrossingCursor source · line 120 · raw

Data

type CrossingEvidence source · line 127 · raw

@-input:Array<F32> -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Crossings -> Data

type TileCursor source · line 160 · raw

Data

type TileEvidence source · line 167 · raw

@-input:Array<F32> -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Tiled -> Data

Definitions

def restore_row source · line 16 · raw

@input:Array<F32> -> @output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @cursor:RowCursor -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles

def stored_row source · line 23 · raw

@output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @cursor:RowCursor -> @result:Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles

def store_row source · line 27 · raw

@+depth:Nat -> @-input:Array<F32> -> @-output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @cursor:RowCursor -> @-result:Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, output) -> @sample:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, result> -> RowEvidence<input, depth, stored_row(output, cursor, result)>

def after_columns source · line 60 · raw

@-depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.next_kernel_row(state)>

def after_kernel_rows source · line 90 · raw

@-depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.next_channel(state)>

def restore_crossing source · line 123 · raw

@input:Array<F32> -> @output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @cursor:CrossingCursor -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Crossings

def stored_crossing source · line 131 · raw

@output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @cursor:CrossingCursor -> @result:Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Crossings

def store_crossing source · line 135 · raw

@+depth:Nat -> @-input:Array<F32> -> @-output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @cursor:CrossingCursor -> @-result:Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, output) -> @sample:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, result> -> CrossingEvidence<input, depth, stored_crossing(output, cursor, result)>

def crossing source · line 143 · raw

@+depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Crossings -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:CrossingEvidence<input, depth, state> -> CrossingEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.crossing_step(state)>

def crossing_loop source · line 154 · raw

@+depth:Nat -> @count:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Crossings -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:CrossingEvidence<input, depth, state> -> CrossingEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Crossings, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.crossing_step, count, state)>

def restore_tiles source · line 163 · raw

@input:Array<F32> -> @output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @cursor:TileCursor -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Tiled

def after_row_tile source · line 170 · raw

@-depth:Nat -> @-input:Array<F32> -> @position:U32 -> @kernel:U32 -> @channels:Nat -> @inner:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @evidence:RowEvidence<input, depth, state> -> TileEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.after_row_tile(position, kernel, channels, inner, state)>

def after_crossing source · line 178 · raw

@-depth:Nat -> @-input:Array<F32> -> @channels:Nat -> @taps:Nat -> @inner:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Crossings -> @evidence:CrossingEvidence<input, depth, state> -> TileEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.after_crossing(channels, taps, inner, state)>

def tile source · line 186 · raw

@+depth:Nat -> @within:Bool -> @wraps:Bool -> @-input:Array<F32> -> @-output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+i:U32 -> @+position:U32 -> @+h:U32 -> @+w:U32 -> @+k:U32 -> @+s:U32 -> @+p:U32 -> @+ow:U32 -> @+channels:Nat -> @+taps:Nat -> @+inner:Nat -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, output) -> TileEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.tile(within, wraps, input, output, i, position, h, w, k, s, p, ow, channels, taps, inner)>

def tile_step source · line 203 · raw

@+depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Tiled -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:TileEvidence<input, depth, state> -> TileEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.tile_step(state)>

def tile_loop source · line 210 · raw

@+depth:Nat -> @count:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Tiled -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:TileEvidence<input, depth, state> -> TileEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Tiled, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.tile_step, count, state)>

def finish source · line 216 · raw

@-depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Tiled -> @evidence:TileEvidence<input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.finish(state)>

def pack source · line 224 · raw

@+depth:Nat -> @+count:Nat -> @+start:U32 -> @-input:Array<F32> -> @-output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+h:U32 -> @+w:U32 -> @+k:U32 -> @+s:U32 -> @+p:U32 -> @+ow:U32 -> @+inner:U32 -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, output) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.pack(count, start, input, output, h, w, k, s, p, ow, inner)>

Templates

template column source · line 35 · raw

@-block:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Block -> @-sampled:(@-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:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>) -> @+depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.column_step(block, state)>

template column_loop source · line 50 · raw

@-block:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Block -> @-sampled:(@-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:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>) -> @+depth:Nat -> @count:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.column_step(block), count, state)>

template kernel_row source · line 67 · raw

@-block:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Block -> @-sampled:(@-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:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>) -> @+depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.kernel_row_step(block, state)>

template kernel_row_loop source · line 80 · raw

@-block:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Block -> @-sampled:(@-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:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>) -> @+depth:Nat -> @count:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.kernel_row_step(block), count, state)>

template channel source · line 97 · raw

@-block:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Block -> @-sampled:(@-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:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>) -> @+depth:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.channel_step(block, state)>

template channel_loop source · line 110 · raw

@-block:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Block -> @-sampled:(@-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:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, block(input, row, column, channel, height, width, stride, next_row, offset, output_width, kernel_column, padding)>) -> @+depth:Nat -> @count:Nat -> @-input:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.family(input) -> @evidence:RowEvidence<input, depth, state> -> RowEvidence<input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.RowTiles, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.channel_step(block), count, state)>