KernelGemmCertificate.write_bias: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend as KernelGemmCertificate
Lines 51-58 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=51&end_line=58

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

def write_bias(+depth: Nat,-bias: Array<F32>,-output: Array<F32>,+offset: U32,+row: U32,-accumulator: Tile.Tile8,+count: U32,
  read: Witness.Read<F32,bias,Array.get(F32,bias,row)>,evidence: Witness.Witness(F32,depth,output)) ->
  Written<bias,depth,Gemm.write_bias(output,offset,accumulator,count,Array.get(F32,bias,row))>:
  Witness.Read{value,equation} = read
  Written{Gemm.store_tail(count,output,offset,value,accumulator),
    %Equal.sym(Array<F32> & F32,Array.get(F32,bias,row),(bias,value),equation) :
      {Gemm.write_bias(output,offset,accumulator,count,_) == (bias,Gemm.store_tail(count,output,offset,value,accumulator)) : Array<F32> & Array<F32>}
    {==},store_tail(count,depth,output,offset,value,accumulator,evidence)}

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=Nat
  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=stelliferous@0.0.2.0/kernel_gemm.bend&name=store_tail
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=write_bias
  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=Written
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend&name=store_tail
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness