tensor_lanes.bend checks

raw source on the hub · import stelliferous@0.0.2.0/tensor_lanes.bend as Tensor_lanes

Owned FP32 input bundles use the same Cells/Lanes rounds as unary maps.

12 imports

import Base
import ./math_compare.bend as Compare
import ./storage_buffer.bend as Storage
import ./traversal_lanes.bend as Lanes
import ./traversal_cells.bend as Cells
import ./kernel_tile.bend as Tile
import ./tensor_operations.bend as Operations
import ./tensor_view.bend as Views
import ./tensor_access.bend as Access
import ./proofs/storage_certificate.bend as Certificate
import ./proofs/traversal_lanes_certificate.bend as LanesCertificate
import ./proofs/traversal_witness.bend as Witness

Types

type Binary source · line 36 · raw

Type

Binary

@left:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> Binary

type Selected source · line 81 · raw

Type

Selected

@mask:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @yes:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @no:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> Selected

Definitions

def identity source · line 15 · raw

@context:Unit -> @value:F32 -> F32

def read_result source · line 18 · raw

@length:Nat -> @result:Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, result)> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)

def read source · line 23 · raw

@buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @+position:U32 -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)

def write source · line 27 · raw

@buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @+position:U32 -> @+tile:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>

def pair_scatter source · line 49 · raw

@owners:Binary -> @position:U32 -> @tile:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> Binary

def pair_result source · line 53 · raw

@result:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>) -> Binary

def pair_buffers source · line 67 · raw

@owners:Binary -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>)

def select_tile source · line 84 · raw

@mask:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @yes:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @no:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8

def select_reads source · line 91 · raw

@mask:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> @yes:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> @no:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> Pair(Selected, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)

def select_gather source · line 97 · raw

@owners:Selected -> @position:U32 -> @context:Unit -> Pair(Selected, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)

def select_scatter source · line 102 · raw

@owners:Selected -> @position:U32 -> @tile:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> Selected

def select_joined source · line 106 · raw

@mask:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @joined:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>) -> Selected

def select_rejected source · line 110 · raw

@+count:Nat -> @+position:U32 -> @yes:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @result:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>) -> Selected

def select_chosen source · line 114 · raw

@+count:Nat -> @+position:U32 -> @no:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @result:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>) -> Selected

def select_finish source · line 121 · raw

@count:Nat -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Selected, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Unit> -> Selected

The final 0..7 values use the existing certified binary kernels. Only the tail makes three passes; full cells read all three inputs in one round.

def select_result source · line 127 · raw

@owners:Selected -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>

def select source · line 131 · raw

@count:Nat -> @mask:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @yes:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @no:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>

Templates

template combine_tile source · line 31 · raw

@-operation:(@_:F32 -> @_:F32 -> F32) -> @left:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8

template pair_reads source · line 39 · raw

@-operation:(@_:F32 -> @_:F32 -> F32) -> @left:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> @right:Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> Pair(Binary, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)

template pair_gather source · line 44 · raw

@-operation:(@_:F32 -> @_:F32 -> F32) -> @owners:Binary -> @position:U32 -> @context:Unit -> Pair(Binary, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)

template pair_finish source · line 58 · raw

@-operation:(@_:F32 -> @_:F32 -> F32) -> @count:Nat -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Binary, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Unit> -> Binary

The checked caller has already validated both views and owners.

template pair_map source · line 63 · raw

@-operation:(@_:F32 -> @_:F32 -> F32) -> @count:Nat -> @position:U32 -> @left:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> Binary

template pair_when source · line 71 · raw

@-operation:(@_:F32 -> @_:F32 -> F32) -> @fast:Bool -> @count:Nat -> @right_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @offset:U32 -> @left:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>)

template combine source · line 77 · raw

@-operation:(@_:F32 -> @_:F32 -> F32) -> @+count:Nat -> @+right_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @+offset:U32 -> @left:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>)