KernelWeightsCertificate.block: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend as KernelWeightsCertificate
Lines 17-29 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=17&end_line=29

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/proofs/kernel_weights_witness.bend as WeightsWitness
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 block(+depth: Nat,+block: U32,+layout: Weights.Layout,-input: Array<F32>,-owners: Array<F32> & Array<Tile.Tile8>,
  input_evidence: Witness.ArrayWitness<F32,input>,evidence: TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,owners>) ->
  TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,Weights.copy_block(block,layout,owners)>:
  Weights.Layout{+rows,+inner} = layout
  TraversalWitness.ResultEvidence{output,equation,output_evidence} = evidence
  %Equal.sym(Array<F32> & Array<Tile.Tile8>,owners,(input,output),equation) :
    TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,Weights.copy_block(block,Weights.Layout{rows,inner},_)>
  +context = {Weights.Context{rows,inner,(block * 8 : U32),(block * inner : U32)} : Weights.Context}
  -state = {Traversal.State{input,output,0,context} : Traversal.State<&1,&1,Array<F32>,Array<Tile.Tile8>,Weights.Context>}
  TraversalWitness.finish(~Array<F32>,~Tile.Tile8,~Weights.Context,input,depth,
    Traversal.run(~Array<F32>,~Tile.Tile8,~Weights.Context,~Weights.read,~Weights.destination,U32.to_nat(inner),state),
    TraversalWitness.run(~Array<F32>,~Tile.Tile8,~Weights.Context,~family,~Weights.read,~Weights.destination,~WeightsWitness.read,
      depth,U32.to_nat(inner),input,state,input_evidence,TraversalWitness.StateEvidence{output,0,context,{==},output_evidence}))

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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.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_weights.bend&name=Context
  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=destination
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_weights.bend&name=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend&name=family
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_weights_witness.bend&name=read
  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/traversal_witness.bend&name=ResultEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=StateEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=finish
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=run