def kept

stelliferous@0.0.2.0 · proofs/kernel_gemm_certificate.bend:210

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

210# The certificates of the read-only buffers are the ones that came in.
211def 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,
212  input_certificate: Certificate.Certificate<Tile.Tile8,input>,weight_certificate: Certificate.Certificate<Tile.Tile8,weights>,bias_certificate: Certificate.Certificate<F32,bias>,
213  output_certificate: Certificate.Certificate<F32,output>) -> Kept<Gemm.run_keeping(rows,input,weights,bias,output,columns,inner,start,output_columns)>:
214  Certificate.Certificate{+input_depth,+input_equation} = input_certificate
215  Certificate.Certificate{+weight_depth,+weight_equation} = weight_certificate
216  Certificate.Certificate{+bias_depth,+bias_equation} = bias_certificate
217  Certificate.Certificate{+depth,+balanced} = output_certificate
218  -state = Gemm.run_keeping(rows,input,weights,bias,output,columns,inner,start,output_columns)
219  -result = Gemm.run_at(rows,input,weights,bias,output,columns,inner,start,output_columns)
220  +owners = kept_equation(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,
221    Certificate.witness(Tile.Tile8,input,Certificate.Certificate{input_depth,input_equation}),Certificate.witness(Tile.Tile8,weights,Certificate.Certificate{weight_depth,weight_equation}),
222    Certificate.witness(F32,bias,Certificate.Certificate{bias_depth,bias_equation}),Certificate.witness_at(F32,depth,output,balanced))
223  Kept{
224    Certificate.Certificate{input_depth,
225      %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
226        {Gemm.kept_input(_) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,input_depth,Tree.reflect(Tile.Tile8,Gemm.kept_input(_)))) : Array<Tile.Tile8>}
227      input_equation},
228    Certificate.Certificate{weight_depth,
229      %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
230        {Gemm.kept_weights(_) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,weight_depth,Tree.reflect(Tile.Tile8,Gemm.kept_weights(_)))) : Array<Tile.Tile8>}
231      weight_equation},
232    Certificate.Certificate{bias_depth,
233      %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
234        {Gemm.kept_bias(_) == Tree.pack(F32,Certificate.normalized(F32,bias_depth,Tree.reflect(F32,Gemm.kept_bias(_)))) : Array<F32>}
235      bias_equation},
236    Certificate.Certificate{depth,equation(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,Certificate.Certificate{input_depth,input_equation},
237      Certificate.Certificate{weight_depth,weight_equation},Certificate.Certificate{bias_depth,bias_equation},balanced)}}