def cell_scattered

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:116

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as Batch
import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as ArrayLaws
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

116def cell_scattered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+position: U32,+context: Context) ->
117  {Lanes.scatter(Tree.pack(F32,values),position,cell(~Context,~map,values,position,context)) ==
118    Tree.pack(F32,Batch.batch(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map),8n,position,context,values,values)) : Array<F32>}:
119  +p1 = (position + 1 : U32)
120  +p2 = (p1 + 1 : U32)
121  +p3 = (p2 + 1 : U32)
122  +p4 = (p3 + 1 : U32)
123  +p5 = (p4 + 1 : U32)
124  +p6 = (p5 + 1 : U32)
125  +p7 = (p6 + 1 : U32)
126  scattered(values,position,map(context,Tree.read(F32,values,position)),map(context,Tree.read(F32,values,p1)),map(context,Tree.read(F32,values,p2)),map(context,Tree.read(F32,values,p3)),
127    map(context,Tree.read(F32,values,p4)),map(context,Tree.read(F32,values,p5)),map(context,Tree.read(F32,values,p6)),map(context,Tree.read(F32,values,p7)))