def run

stelliferous@0.0.2.0 · proofs/kernel_weights_certificate.bend:52

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

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