KernelWeightsCertificate.run: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend as KernelWeightsCertificate
Lines 52-59 of stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend&start_line=52&end_line=59

import Base
import stelliferous@0.0.2.0/kernel_weights.bend as Weights
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/storage_allocation.bend as Allocation
import stelliferous@0.0.2.0/tensor.bend as Tensors
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

def run(+rows: U32,+inner: U32,-input: Array<F32>,evidence: Witness.ArrayWitness<F32,input>) ->
  Witness.Witness(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.run(rows,inner,input)):
  +blocks = ((rows + 7) / 8 : U32)
  +depth = Tensors.depth_for((blocks * inner : U32))
  +layout = {Weights.Layout{rows,inner} : Weights.Layout}
  -output = Allocation.array(~Tile.Tile8,depth,Tile.filled(0.0))
  finish(depth,input,Traversal.indexed_fold(~(Array<F32> & Array<Tile.Tile8>),~Weights.Layout,~Weights.copy_block,U32.to_nat(blocks),0,layout,(input,output)),
    traverse(depth,U32.to_nat(blocks),0,layout,input,(input,output),evidence,TraversalWitness.ResultEvidence{output,{==},allocated(depth)}))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  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=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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/kernel_tile.bend&name=filled
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_weights.bend&name=Layout
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_weights.bend&name=copy_block
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_weights.bend&name=run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend&name=allocated
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend&name=finish
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend&name=traverse
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=ArrayWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=ResultEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_allocation.bend&name=array
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor.bend&name=depth_for
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=indexed_fold