KernelGemmBuffer.kept: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/kernel_gemm_buffer.bend as KernelGemmBuffer
Lines 24-28 of stelliferous@0.0.2.0/kernel_gemm_buffer.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/kernel_gemm_buffer.bend&start_line=24&end_line=28

import Base
import stelliferous@0.0.2.0/kernel_gemm.bend as Gemm
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend as GemmCertificate

def kept(state: Gemm.Buffers,input_length: Nat,weight_length: Nat,bias_length: Nat,length: Nat,certificates: GemmCertificate.Kept<state>) -> Kept:
  Gemm.Buffers{input,weights,bias,output} = state
  GemmCertificate.Kept{input_certificate,weight_certificate,bias_certificate,certificate} = certificates
  Kept{Storage.Buffer{input,input_length,input_certificate},Storage.Buffer{weights,weight_length,weight_certificate},
    Storage.Buffer{bias,bias_length,bias_certificate},Storage.Buffer{output,length,certificate}}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=Buffers
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm_buffer.bend&name=Kept
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend&name=Kept
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_buffer.bend&name=Buffer