def scatter

stelliferous@0.0.2.0 · proofs/traversal_lanes_witness.bend:57

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

57def scatter(+depth: Nat,-values: Array<F32>,+position: U32,-tile: Tile.Tile8,witness: Witness.Witness(F32,depth,values)) ->
58  Witness.Witness(F32,depth,Lanes.scatter(values,position,tile)):
59  +p1 = (position + 1 : U32)
60  +p2 = (p1 + 1 : U32)
61  +p3 = (p2 + 1 : U32)
62  +p4 = (p3 + 1 : U32)
63  +p5 = (p4 + 1 : U32)
64  +p6 = (p5 + 1 : U32)
65  +p7 = (p6 + 1 : U32)
66  -o1 = Array.set(F32,values,position,Tile.lane0(tile))
67  -o2 = Array.set(F32,o1,p1,Tile.lane1(tile))
68  -o3 = Array.set(F32,o2,p2,Tile.lane2(tile))
69  -o4 = Array.set(F32,o3,p3,Tile.lane3(tile))
70  -o5 = Array.set(F32,o4,p4,Tile.lane4(tile))
71  -o6 = Array.set(F32,o5,p5,Tile.lane5(tile))
72  -o7 = Array.set(F32,o6,p6,Tile.lane6(tile))
73  witness = Witness.write(F32,depth,values,position,Tile.lane0(tile),witness)
74  witness = Witness.write(F32,depth,o1,p1,Tile.lane1(tile),witness)
75  witness = Witness.write(F32,depth,o2,p2,Tile.lane2(tile),witness)
76  witness = Witness.write(F32,depth,o3,p3,Tile.lane3(tile),witness)
77  witness = Witness.write(F32,depth,o4,p4,Tile.lane4(tile),witness)
78  witness = Witness.write(F32,depth,o5,p5,Tile.lane5(tile),witness)
79  witness = Witness.write(F32,depth,o6,p6,Tile.lane6(tile),witness)
80  Witness.write(F32,depth,o7,p7,Tile.lane7(tile),witness)