KernelGatherCertificate.block: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend as KernelGatherCertificate
Lines 37-42 of stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend&start_line=37&end_line=42

import Base
import stelliferous@0.0.2.0/kernel_gather.bend as Gather
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

def block(+depth: Nat,+count: U32,+offset: U32,+positions: U32,+span: U32,-input: Array<F32>,-output: Array<F32>,
  input_evidence: Witness.ArrayWitness<F32,input>,balanced: Witness.Witness(F32,depth,output)) ->
  Witness.Witness(F32,depth,Gather.gather_block(count,offset,positions,span,input,output)):
  +width = Gather.gather_width(offset,positions,span)
  finish(depth,input,Gather.gather_channels(U32.to_nat(count),0,width,offset,positions,span,(input,output)),
    channels(depth,U32.to_nat(count),0,width,offset,positions,span,input,(input,output),input_evidence,TraversalWitness.ResultEvidence{output,{==},balanced}))

Uses (14):
  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=Nat
  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.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gather.bend&name=gather_block
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gather.bend&name=gather_channels
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gather.bend&name=gather_width
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend&name=channels
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend&name=finish
  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