def write_bias

stelliferous@0.0.2.0 · proofs/kernel_gemm_certificate.bend:51

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

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