proofs/kernel_read_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_read_witness.bend as Kernel_read_witness

6 imports

import Base
import ../kernel_gemm.bend as Gemm
import ../kernel_rows.bend as Rows
import ../kernel_tile.bend as Tile
import ../traversal_loop.bend as Loop
import ./storage_witness.bend as Witness

Types

type Looped source · line 10 · raw

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop -> Data

The k loop returns every owner it received. Index, context and the erased accumulators are whatever the steps produced.

Looped

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop -> @index:U32 -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Context -> @-accumulators:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.Rows<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @equation:{state == 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop{input, weights, bias, output, index, context, accumulators} : 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop} -> Looped<input, weights, bias, output, state>

Definitions

def after_input source · line 14 · raw

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+index:U32 -> @+context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Context -> @-accumulators:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.Rows<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-samples:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.Rows<F32> -> @+address:U32 -> @read:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, Array.get(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, address)> -> Looped<input, weights, bias, output, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.with_input(weights, bias, output, index, context, accumulators, samples, Array.get(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, address))>

Templates

template after_weights source · line 22 · raw

@-upper:Bool -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+index:U32 -> @+context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Context -> @+input_base:U32 -> @-accumulators:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.Rows<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+address:U32 -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @read:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights, Array.get(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights, address)> -> Looped<input, weights, bias, output, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.with_weights(upper, input, bias, output, index, context, input_base, accumulators, Array.get(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights, address))>

template step_at source · line 32 · raw

@-upper:Bool -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+index:U32 -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Context -> @-accumulators:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.Rows<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @+weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> Looped<input, weights, bias, output, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.step(upper, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop{input, weights, bias, output, index, context, accumulators})>

template step source · line 39 · raw

@-upper:Bool -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @+weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @evidence:Looped<input, weights, bias, output, state> -> Looped<input, weights, bias, output, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.step(upper, state)>

template run source · line 47 · raw

@-upper:Bool -> @count:Nat -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @+weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @evidence:Looped<input, weights, bias, output, state> -> Looped<input, weights, bias, output, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.step(upper), count, state)>