def gather

stelliferous@0.0.2.0 · proofs/traversal_lanes_witness.bend:44

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

44def gather(~Context: Data,~map: Context -> F32 -> F32,+depth: Nat,-values: Array<F32>,+position: U32,+context: Context,
45  +witness: Witness.Witness(F32,depth,values)) -> Gathered<values,Lanes.gather(~Context,~map,values,position,context)>:
46  +p1 = (position + 1 : U32)
47  +p2 = (p1 + 1 : U32)
48  +p3 = (p2 + 1 : U32)
49  +p4 = (p3 + 1 : U32)
50  +p5 = (p4 + 1 : U32)
51  +p6 = (p5 + 1 : U32)
52  +p7 = (p6 + 1 : U32)
53  gathered(~Context,~map,values,position,context,Witness.read(F32,depth,values,position,witness),Witness.read(F32,depth,values,p1,witness),
54    Witness.read(F32,depth,values,p2,witness),Witness.read(F32,depth,values,p3,witness),Witness.read(F32,depth,values,p4,witness),
55    Witness.read(F32,depth,values,p5,witness),Witness.read(F32,depth,values,p6,witness),Witness.read(F32,depth,values,p7,witness))