KernelGemmCertificate.kept: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend as KernelGemmCertificate
Lines 210-237 of stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend&start_line=210&end_line=237

import Base
import stelliferous@0.0.2.0/kernel_gemm.bend as Gemm
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

# The certificates of the read-only buffers are the ones that came in.
def kept(+rows: U32,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,+columns: U32,+inner: U32,+start: U32,+output_columns: U32,
  input_certificate: Certificate.Certificate<Tile.Tile8,input>,weight_certificate: Certificate.Certificate<Tile.Tile8,weights>,bias_certificate: Certificate.Certificate<F32,bias>,
  output_certificate: Certificate.Certificate<F32,output>) -> Kept<Gemm.run_keeping(rows,input,weights,bias,output,columns,inner,start,output_columns)>:
  Certificate.Certificate{+input_depth,+input_equation} = input_certificate
  Certificate.Certificate{+weight_depth,+weight_equation} = weight_certificate
  Certificate.Certificate{+bias_depth,+bias_equation} = bias_certificate
  Certificate.Certificate{+depth,+balanced} = output_certificate
  -state = Gemm.run_keeping(rows,input,weights,bias,output,columns,inner,start,output_columns)
  -result = Gemm.run_at(rows,input,weights,bias,output,columns,inner,start,output_columns)
  +owners = kept_equation(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,
    Certificate.witness(Tile.Tile8,input,Certificate.Certificate{input_depth,input_equation}),Certificate.witness(Tile.Tile8,weights,Certificate.Certificate{weight_depth,weight_equation}),
    Certificate.witness(F32,bias,Certificate.Certificate{bias_depth,bias_equation}),Certificate.witness_at(F32,depth,output,balanced))
  Kept{
    Certificate.Certificate{input_depth,
      %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
        {Gemm.kept_input(_) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,input_depth,Tree.reflect(Tile.Tile8,Gemm.kept_input(_)))) : Array<Tile.Tile8>}
      input_equation},
    Certificate.Certificate{weight_depth,
      %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
        {Gemm.kept_weights(_) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,weight_depth,Tree.reflect(Tile.Tile8,Gemm.kept_weights(_)))) : Array<Tile.Tile8>}
      weight_equation},
    Certificate.Certificate{bias_depth,
      %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
        {Gemm.kept_bias(_) == Tree.pack(F32,Certificate.normalized(F32,bias_depth,Tree.reflect(F32,Gemm.kept_bias(_)))) : Array<F32>}
      bias_equation},
    Certificate.Certificate{depth,equation(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,Certificate.Certificate{input_depth,input_equation},
      Certificate.Certificate{weight_depth,weight_equation},Certificate.Certificate{bias_depth,bias_equation},balanced)}}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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=U32
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=Buffers
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=kept_bias
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=kept_input
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=kept_weights
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=run_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=run_keeping
  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_gemm_certificate.bend&name=Kept
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend&name=equation
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend&name=kept_equation
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=Certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=normalized
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=witness_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=reflect