KernelGatherCertificate.channel: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend as KernelGatherCertificate
Lines 9-20 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=9&end_line=20

import Base
import stelliferous@0.0.2.0/kernel_gather.bend as Gather
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
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 channel(+depth: Nat,+channel: U32,+width: U32,+offset: U32,+positions: U32,+span: U32,-input: Array<F32>,-owners: Array<F32> & Array<F32>,
  input_evidence: Witness.ArrayWitness<F32,input>,evidence: TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,owners>) ->
  TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,Gather.gather_channel(channel,width,offset,positions,span,owners)>:
  TraversalWitness.ResultEvidence{output,equation,balanced} = evidence
  %Equal.sym(Array<F32> & Array<F32>,owners,(input,output),equation) :
    TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,Gather.gather_channel(channel,width,offset,positions,span,_)>
  +context = {Traversal.Offsets{(channel * span : U32),(channel * positions + offset : U32)} : Traversal.Offsets}
  -state = {Traversal.State{input,output,0,context} : Traversal.State<&1,&1,Array<F32>,Array<F32>,Traversal.Offsets>}
  TraversalWitness.finish(~Array<F32>,~F32,~Traversal.Offsets,input,depth,
    Traversal.run(~Array<F32>,~F32,~Traversal.Offsets,~Traversal.source_offset(~F32),~Traversal.destination_offset,U32.to_nat(width),state),
    TraversalWitness.run(~Array<F32>,~F32,~Traversal.Offsets,~TraversalWitness.array_evidence(~F32),~Traversal.source_offset(~F32),~Traversal.destination_offset,~TraversalWitness.offset_read(~F32),
      depth,U32.to_nat(width),input,state,input_evidence,TraversalWitness.StateEvidence{output,0,context,{==},balanced}))

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=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.add
  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_gather.bend&name=gather_channel
  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=array_evidence
  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=offset_read
  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=Offsets
  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=destination_offset
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=source_offset