def write

stelliferous@0.0.2.0 · proofs/kernel_gemm_certificate.bend:76

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

76def write(+depth: Nat,context: Gemm.Context,-accumulators: Rows.Rows<Tile.Tile8>,
77  -bias: Array<F32>,-output: Array<F32>,+bias_evidence: Witness.ArrayWitness<F32,bias>,balanced: Witness.Witness(F32,depth,output)) ->
78  Written<bias,depth,Gemm.write(context,accumulators,bias,output)>:
79  Gemm.Context{+row,+position,+rows,+columns,input_base,weight_base} = context
80  -a = Rows.first(~Tile.Tile8,accumulators)
81  -b = Rows.second(~Tile.Tile8,accumulators)
82  -c = Rows.third(~Tile.Tile8,accumulators)
83  -d = Rows.fourth(~Tile.Tile8,accumulators)
84  evidence = write_row(depth,U32.is_lt(row,rows),row,position,columns,a,bias,output,bias_evidence,balanced)
85  -owners = Gemm.write_row(U32.is_lt(row,rows),row,position,columns,a,(bias,output))
86  evidence = next(depth,U32.is_lt((row + 1 : U32),rows),(row + 1 : U32),position,columns,b,bias,owners,bias_evidence,evidence)
87  -owners = Gemm.write_row(U32.is_lt((row + 1 : U32),rows),(row + 1 : U32),position,columns,b,owners)
88  evidence = next(depth,U32.is_lt((row + 2 : U32),rows),(row + 2 : U32),position,columns,c,bias,owners,bias_evidence,evidence)
89  -owners = Gemm.write_row(U32.is_lt((row + 2 : U32),rows),(row + 2 : U32),position,columns,c,owners)
90  next(depth,U32.is_lt((row + 3 : U32),rows),(row + 3 : U32),position,columns,d,bias,owners,bias_evidence,evidence)