TraversalLanesWitness.scatter: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as TraversalLanesWitness
Lines 57-80 of stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend&start_line=57&end_line=80

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

def scatter(+depth: Nat,-values: Array<F32>,+position: U32,-tile: Tile.Tile8,witness: Witness.Witness(F32,depth,values)) ->
  Witness.Witness(F32,depth,Lanes.scatter(values,position,tile)):
  +p1 = (position + 1 : U32)
  +p2 = (p1 + 1 : U32)
  +p3 = (p2 + 1 : U32)
  +p4 = (p3 + 1 : U32)
  +p5 = (p4 + 1 : U32)
  +p6 = (p5 + 1 : U32)
  +p7 = (p6 + 1 : U32)
  -o1 = Array.set(F32,values,position,Tile.lane0(tile))
  -o2 = Array.set(F32,o1,p1,Tile.lane1(tile))
  -o3 = Array.set(F32,o2,p2,Tile.lane2(tile))
  -o4 = Array.set(F32,o3,p3,Tile.lane3(tile))
  -o5 = Array.set(F32,o4,p4,Tile.lane4(tile))
  -o6 = Array.set(F32,o5,p5,Tile.lane5(tile))
  -o7 = Array.set(F32,o6,p6,Tile.lane6(tile))
  witness = Witness.write(F32,depth,values,position,Tile.lane0(tile),witness)
  witness = Witness.write(F32,depth,o1,p1,Tile.lane1(tile),witness)
  witness = Witness.write(F32,depth,o2,p2,Tile.lane2(tile),witness)
  witness = Witness.write(F32,depth,o3,p3,Tile.lane3(tile),witness)
  witness = Witness.write(F32,depth,o4,p4,Tile.lane4(tile),witness)
  witness = Witness.write(F32,depth,o5,p5,Tile.lane5(tile),witness)
  witness = Witness.write(F32,depth,o6,p6,Tile.lane6(tile),witness)
  Witness.write(F32,depth,o7,p7,Tile.lane7(tile),witness)

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane0
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane1
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane2
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane3
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane4
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane5
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane6
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane7
  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/storage_witness.bend&name=write
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=scatter