tensor_operations.bend checks

raw source on the hub · import stelliferous@0.0.2.0/tensor_operations.bend as Tensor_operations

Checked operations preserve all owners and their balanced-storage certificates. Element functions enter hot loops only as direct templates.

12 imports

import Base
import ./storage_buffer.bend as Storage
import ./tensor_shape.bend as Shapes
import ./tensor_view.bend as Views
import ./traversal_array.bend as Traversal
import ./tensor_access.bend as Access
import ./proofs/storage_certificate.bend as Certificate
import ./proofs/traversal_certificate.bend as TraversalCertificate
import ./proofs/traversal_witness.bend as TraversalWitness
import ./proofs/tensor_access_certificate.bend as AccessCertificate
import ./traversal_lanes.bend as Lanes
import ./proofs/traversal_lanes_certificate.bend as LanesCertificate

Types

type Outcome source · line 16 · raw

@-Value:Type -> Type

Accepted

@-Value:Type -> @value:Value -> Outcome<Value>

Rejected

@-Value:Type -> @value:Value -> Outcome<Value>

Definitions

def valid_buffer source · line 20 · raw

@+length:Nat -> @capacity:U32 -> @view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> Bool

def holds source · line 167 · raw

@count:Maybe<&2, U32> -> @+length:Nat -> @capacity:U32 -> Bool

def small source · line 183 · raw

@value:U32 -> Bool

def pool_geometry source · line 187 · raw

@+pool:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Pool -> Bool

The window geometry is exact and every sample address stays in U32.

def sweep_geometry source · line 210 · raw

@+sweep:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Sweep -> Bool

The window geometry of a whole axis is exact and every sample address stays in U32.

def sweep_input source · line 216 · raw

@+sweep:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Sweep -> @+outer:U32 -> Maybe<&2, U32>

def sweep_output source · line 220 · raw

@+sweep:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Sweep -> @+outer:U32 -> Maybe<&2, U32>

Templates

template pair_buffers source · line 23 · raw

@-Element:Data -> @input_length:Nat -> @output_length:Nat -> @result:Pair(Array<Element>, Array<Element>) -> @certificates:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_certificate.Certificates<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.family(Element), result> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)

template copy_when source · line 30 · raw

@-Element:Data -> @valid:Bool -> @count:Maybe<&2, U32> -> @+source:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @target:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template copy source · line 43 · raw

@-Element:Data -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+source:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+target:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template scatter_when source · line 56 · raw

@-Element:Data -> @valid:Bool -> @count:Maybe<&2, U32> -> @source:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @+target:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

output[address of element i of target] = input[offset of source + i]: a contiguous source written through a strided target view, in row-major order.

template scatter source · line 68 · raw

@-Element:Data -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+source:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+target:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template combine_buffers source · line 79 · raw

@-Element:Data -> @left_length:Nat -> @right_length:Nat -> @result:Pair(Array<Element>, Array<Element>) -> @certificates:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_certificate.Certificates<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.family(Element), result> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)

template combine_kernel source · line 85 · raw

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

template combine_when_with source · line 94 · raw

@-Element:Data -> @-kernel:(@+count:Nat -> @+right_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @+offset:U32 -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)) -> @valid:Bool -> @count:Maybe<&2, U32> -> @right_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @target:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @left:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template combine_with source · line 103 · raw

@-Element:Data -> @-kernel:(@+count:Nat -> @+right_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @+offset:U32 -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)) -> @left:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+left_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+right_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template combine source · line 115 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @left:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+left_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @right:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+right_view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template mapped source · line 122 · raw

@-Element:Data -> @-operation:(@_:Element -> Element) -> @+count:Nat -> @+position:U32 -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>

A mapper is the ordered map of count values from position on a certified Buffer. mapped applies the operation to one value at a time.

template lanes source · line 130 · raw

@-Context:Data -> @-operation:(@_:Context -> @_:F32 -> F32) -> @+count:Nat -> @+position:U32 -> @+context:Context -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<F32>

The same map with the values of each round of eight computed together: an operation written with FP32 arithmetic alone then compiles to vector code. The certificate's depth decides whether the array holds the positions.

template mapped_lanes source · line 135 · raw

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

template apply_context_when source · line 138 · raw

@-Element:Data -> @-Context:Data -> @-mapper:(@+count:Nat -> @+position:U32 -> @+context:Context -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>) -> @context:Context -> @valid:Bool -> @count:Maybe<&2, U32> -> @view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>>

template apply_context source · line 146 · raw

@-Element:Data -> @-Context:Data -> @-mapper:(@+count:Nat -> @+position:U32 -> @+context:Context -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>) -> @context:Context -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> Outcome<0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>>

template without_context source · line 153 · raw

@-Element:Data -> @-mapper:(@+count:Nat -> @+position:U32 -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>) -> @+count:Nat -> @+position:U32 -> @+context:Unit -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>

A mapper without a context, as the Unit-context case.

template apply_indexed_when source · line 156 · raw

@-Element:Data -> @-operation:(@_:U32 -> @_:Element -> Element) -> @valid:Bool -> @count:Maybe<&2, U32> -> @+view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template apply_indexed source · line 173 · raw

@-Element:Data -> @-operation:(@_:U32 -> @_:Element -> Element) -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

Writes f(index, element) for a contiguous input view into output[0..count).

template swept source · line 195 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+count:Nat -> @+context:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.SweepContext<Element> -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)

The unchecked sweep of two owners; the callers establish its bounds.

template sweep_when source · line 203 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @valid:Bool -> @count:Maybe<&2, U32> -> @+context:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.SweepContext<Element> -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template sweep source · line 225 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+pad:Element -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+sweep:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Sweep -> @+outer:U32 -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

Windows along one axis of outer contiguous blocks; see Access.Sweep.

template pool_finished source · line 236 · raw

@-Element:Data -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @result:Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

The input and the output of a pool around its column-swept planes.

template pool_rows source · line 242 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+pad:Element -> @result:Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)> -> @+rows:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Sweep -> @+channels:U32 -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template pool_lines source · line 248 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+pad:Element -> @lines:Maybe<&2, U32> -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+pool:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Pool -> @+channels:U32 -> @middle:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

template pool source · line 259 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+pad:Element -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+pool:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Pool -> @+channels:U32 -> @middle:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>)>

Windows over the last two axes of channels contiguous planes: a sweep along the columns of every row into middle, [channels,height,out_width], then a sweep along the rows into output. Each sweep checks its own geometry and counts.

template reduce_buffer source · line 264 · raw

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

template reduce_when source · line 269 · raw

@-Element:Data -> @-Accumulator:Data -> @-operation:(@_:Accumulator -> @_:Element -> Accumulator) -> @valid:Bool -> @count:Maybe<&2, U32> -> @+view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @initial:Accumulator -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, Accumulator)>

template reduce source · line 281 · raw

@-Element:Data -> @-Accumulator:Data -> @-operation:(@_:Accumulator -> @_:Element -> Accumulator) -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @initial:Accumulator -> Outcome<Pair(0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>, Accumulator)>