def channel

stelliferous@0.0.2.0 · proofs/kernel_gather_certificate.bend:9

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

9def channel(+depth: Nat,+channel: U32,+width: U32,+offset: U32,+positions: U32,+span: U32,-input: Array<F32>,-owners: Array<F32> & Array<F32>,
10  input_evidence: Witness.ArrayWitness<F32,input>,evidence: TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,owners>) ->
11  TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,Gather.gather_channel(channel,width,offset,positions,span,owners)>:
12  TraversalWitness.ResultEvidence{output,equation,balanced} = evidence
13  %Equal.sym(Array<F32> & Array<F32>,owners,(input,output),equation) :
14    TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,Gather.gather_channel(channel,width,offset,positions,span,_)>
15  +context = {Traversal.Offsets{(channel * span : U32),(channel * positions + offset : U32)} : Traversal.Offsets}
16  -state = {Traversal.State{input,output,0,context} : Traversal.State<&1,&1,Array<F32>,Array<F32>,Traversal.Offsets>}
17  TraversalWitness.finish(~Array<F32>,~F32,~Traversal.Offsets,input,depth,
18    Traversal.run(~Array<F32>,~F32,~Traversal.Offsets,~Traversal.source_offset(~F32),~Traversal.destination_offset,U32.to_nat(width),state),
19    TraversalWitness.run(~Array<F32>,~F32,~Traversal.Offsets,~TraversalWitness.array_evidence(~F32),~Traversal.source_offset(~F32),~Traversal.destination_offset,~TraversalWitness.offset_read(~F32),
20      depth,U32.to_nat(width),input,state,input_evidence,TraversalWitness.StateEvidence{output,0,context,{==},balanced}))