def finished

stelliferous@0.0.2.0 · proofs/kernel_gemm_certificate.bend:103

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_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/kernel_read_witness.bend as ReadWitness

103# The final step stores into the owners the loop returned unchanged.
104def finished(+depth: Nat,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,-state: Gemm.Loop,
105  +bias_evidence: Witness.ArrayWitness<F32,bias>,balanced: Witness.Witness(F32,depth,output),
106  evidence: ReadWitness.Looped<input,weights,bias,output,state>) -> Evidence<input,weights,bias,depth,Gemm.finish(state)>:
107  ReadWitness.Looped{index,context,accumulators,equation} = evidence
108  %Equal.sym(Gemm.Loop,state,Gemm.Loop{input,weights,bias,output,index,context,accumulators},equation) :
109    Evidence<input,weights,bias,depth,Gemm.finish(_)>
110  after_write(input,weights,bias,depth,Gemm.write(context,accumulators,bias,output),
111    write(depth,context,accumulators,bias,output,bias_evidence,balanced))