KernelReadWitness.after_input: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_read_witness.bend as KernelReadWitness
Lines 14-20 of stelliferous@0.0.2.0/proofs/kernel_read_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_read_witness.bend&start_line=14&end_line=20

import Base
import stelliferous@0.0.2.0/kernel_gemm.bend as Gemm
import stelliferous@0.0.2.0/kernel_rows.bend as Rows
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

def after_input(-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,+index: U32,+context: Gemm.Context,
  -accumulators: Rows.Rows<Tile.Tile8>,-samples: Rows.Rows<F32>,+address: U32,read: Witness.Read<Tile.Tile8,input,Array.get(Tile.Tile8,input,address)>) ->
  Looped<input,weights,bias,output,Gemm.with_input(weights,bias,output,index,context,accumulators,samples,Array.get(Tile.Tile8,input,address))>:
  Witness.Read{value,equation} = read
  %Equal.sym(Array<Tile.Tile8> & Tile.Tile8,Array.get(Tile.Tile8,input,address),(input,value),equation) :
    Looped<input,weights,bias,output,Gemm.with_input(weights,bias,output,index,context,accumulators,samples,_)>
  Looped{(index + 1 : U32),context,Gemm.update(accumulators,value,samples),{==}}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=Context
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=update
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=with_input
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_rows.bend&name=Rows
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_read_witness.bend&name=Looped
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Read