proofs/kernel_gemm_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend as Kernel_gemm_certificate

Shape evidence follows the real readers and writers. Only the final flat certificate is live; witness traversals occur beneath erased rewrites.

11 imports

import Base
import ../kernel_gemm.bend as Gemm
import ../kernel_rows.bend as Rows
import ../kernel_tile.bend as Tile
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ./storage_witness.bend as Witness
import ./storage_certificate.bend as Certificate
import ./storage_tree_model.bend as Tree
import ./loop_projection.bend as Projection
import ./kernel_read_witness.bend as ReadWitness

Types

type Written source · line 48 · raw

@-bias:Array<F32> -> @-depth:Nat -> @-result:Pair(Array<F32>, Array<F32>) -> Data

Written

@-bias:Array<F32> -> @-depth:Nat -> @-result:Pair(Array<F32>, Array<F32>) -> @-output:Array<F32> -> @equation:{result == (bias, output) : Pair(Array<F32>, Array<F32>)} -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> Written<bias, depth, result>

type Evidence source · line 92 · raw

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> Data

Evidence

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> @-output:Array<F32> -> @equation:{state == 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers{input, weights, bias, output} : 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers} -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> Evidence<input, weights, bias, depth, state>

type Kept source · line 206 · raw

@-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> Data

Kept

@-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.kept_input(state)> -> @weights:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.kept_weights(state)> -> @bias:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.kept_bias(state)> -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.result(state)> -> Kept<state>

Definitions

def store_lane source · line 15 · raw

@+depth:Nat -> @inside:Bool -> @-output:Array<F32> -> @+offset:U32 -> @-value:F32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.store_lane(inside, output, offset, value))

def store_tail source · line 21 · raw

@+count:U32 -> @+depth:Nat -> @-output:Array<F32> -> @+offset:U32 -> @-bias:F32 -> @-accumulator:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.store_tail(count, output, offset, bias, accumulator))

def write_bias source · line 51 · raw

@+depth:Nat -> @-bias:Array<F32> -> @-output:Array<F32> -> @+offset:U32 -> @+row:U32 -> @-accumulator:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @+count:U32 -> @read:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, bias, Array.get(F32, bias, row)> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> Written<bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.write_bias(output, offset, accumulator, count, Array.get(F32, bias, row))>

def write_row source · line 60 · raw

@+depth:Nat -> @valid:Bool -> @+row:U32 -> @+position:U32 -> @+columns:U32 -> @-accumulator:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @-bias:Array<F32> -> @-output:Array<F32> -> @bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> Written<bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.write_row(valid, row, position, columns, accumulator, (bias, output))>

def next source · line 68 · raw

@+depth:Nat -> @valid:Bool -> @row:U32 -> @position:U32 -> @columns:U32 -> @-accumulator:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @-bias:Array<F32> -> @-owners:Pair(Array<F32>, Array<F32>) -> @bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @evidence:Written<bias, depth, owners> -> Written<bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.write_row(valid, row, position, columns, accumulator, owners)>

def write source · line 76 · raw

@+depth:Nat -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Context -> @-accumulators:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.Rows<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> Written<bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.write(context, accumulators, bias, output)>

def after_write source · line 95 · raw

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-depth:Nat -> @-written:Pair(Array<F32>, Array<F32>) -> @evidence:Written<bias, depth, written> -> Evidence<input, weights, bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.after_write(input, weights, written)>

def finished source · line 104 · raw

@+depth:Nat -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop -> @+bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_read_witness.Looped<input, weights, bias, output, state> -> Evidence<input, weights, bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.finish(state)>

The final step stores into the owners the loop returned unchanged.

def reduce source · line 124 · raw

@upper:Bool -> @+depth:Nat -> @+count:Nat -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+context:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Context -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @+weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @+bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> Evidence<input, weights, bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.reduce(upper, count, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop{input, weights, bias, output, 0, context, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.filled(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.filled(0.0))})>

def execute source · line 136 · raw

@+depth:Nat -> @job:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Job -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @+weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @+bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @evidence:Evidence<input, weights, bias, depth, state> -> Evidence<input, weights, bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.execute(job, state)>

def traverse source · line 145 · raw

@+depth:Nat -> @count:Nat -> @+index:U32 -> @+layout:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Layout -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @+weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @+bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @evidence:Evidence<input, weights, bias, depth, state> -> Evidence<input, weights, bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Layout, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.step_job, count, index, layout, state)>

def finish source · line 155 · raw

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> @evidence:Evidence<input, weights, bias, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.result(state))

def run source · line 161 · raw

@+depth:Nat -> @+rows:U32 -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+columns:U32 -> @+inner:U32 -> @+start:U32 -> @+output_columns:U32 -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.run_at(rows, input, weights, bias, output, columns, inner, start, output_columns))

def equation source · line 170 · raw

@+depth:Nat -> @+rows:U32 -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+columns:U32 -> @+inner:U32 -> @+start:U32 -> @+output_columns:U32 -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @weight_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @bias_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, bias> -> @balanced:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(F32, output))) : Array<F32>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.run_at(rows, input, weights, bias, output, columns, inner, start, output_columns) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.run_at(rows, input, weights, bias, output, columns, inner, start, output_columns)))) : Array<F32>}

def certificate source · line 181 · raw

@rows:U32 -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @columns:U32 -> @inner:U32 -> @start:U32 -> @output_columns:U32 -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @weight_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @bias_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, bias> -> @output_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, output> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.run_at(rows, input, weights, bias, output, columns, inner, start, output_columns)>

def kept_state source · line 188 · raw

@-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers -> @evidence:Evidence<input, weights, bias, depth, state> -> {state == 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers{input, weights, bias, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.result(state)} : 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers}

The fold gives back the three buffers it only reads, next to the output of run.

def kept_equation source · line 195 · raw

@+depth:Nat -> @+rows:U32 -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+columns:U32 -> @+inner:U32 -> @+start:U32 -> @+output_columns:U32 -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @weight_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.run_keeping(rows, input, weights, bias, output, columns, inner, start, output_columns) == 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers{input, weights, bias, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.run_at(rows, input, weights, bias, output, columns, inner, start, output_columns)} : 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers}

def kept source · line 211 · raw

@+rows:U32 -> @-input:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-weights:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @-bias:Array<F32> -> @-output:Array<F32> -> @+columns:U32 -> @+inner:U32 -> @+start:U32 -> @+output_columns:U32 -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input> -> @weight_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, weights> -> @bias_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, bias> -> @output_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, output> -> Kept<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.run_keeping(rows, input, weights, bias, output, columns, inner, start, output_columns)>

The certificates of the read-only buffers are the ones that came in.

Templates

template reduced source · line 113 · raw

@-upper:Bool -> @+depth:Nat -> @+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> -> @+bias_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, bias> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_read_witness.Looped<input, weights, bias, output, state> -> Evidence<input, weights, bias, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run_then(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Loop, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.Buffers, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.step(upper), 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.finish, count, state)>