TraversalLanesRefinement.gathered: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement Lines 36-70 of stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&start_line=36&end_line=70 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_tree_model.bend as Tree import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws def gathered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+position: U32,+context: Context) -> {Lanes.gather(~Context,~map,Tree.pack(F32,values),position,context) == (Tree.pack(F32,values),cell(~Context,~map,values,position,context)) : Array & Tile.Tile8}: -owner = Tree.pack(F32,values) +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) +a = Tree.read(F32,values,position) +b = Tree.read(F32,values,p1) +c = Tree.read(F32,values,p2) +d = Tree.read(F32,values,p3) +e = Tree.read(F32,values,p4) +f = Tree.read(F32,values,p5) +g = Tree.read(F32,values,p6) +h = Tree.read(F32,values,p7) %Equal.sym(Array & F32,Array.get(F32,owner,position),(owner,a),StorageLaws.read(F32,values,position)) : {Lanes.gather1(~Context,~map,position,context,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} %Equal.sym(Array & F32,Array.get(F32,owner,p1),(owner,b),StorageLaws.read(F32,values,p1)) : {Lanes.gather2(~Context,~map,p1,context,a,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} %Equal.sym(Array & F32,Array.get(F32,owner,p2),(owner,c),StorageLaws.read(F32,values,p2)) : {Lanes.gather3(~Context,~map,p2,context,a,b,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} %Equal.sym(Array & F32,Array.get(F32,owner,p3),(owner,d),StorageLaws.read(F32,values,p3)) : {Lanes.gather4(~Context,~map,p3,context,a,b,c,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} %Equal.sym(Array & F32,Array.get(F32,owner,p4),(owner,e),StorageLaws.read(F32,values,p4)) : {Lanes.gather5(~Context,~map,p4,context,a,b,c,d,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} %Equal.sym(Array & F32,Array.get(F32,owner,p5),(owner,f),StorageLaws.read(F32,values,p5)) : {Lanes.gather6(~Context,~map,p5,context,a,b,c,d,e,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} %Equal.sym(Array & F32,Array.get(F32,owner,p6),(owner,g),StorageLaws.read(F32,values,p6)) : {Lanes.gather7(~Context,~map,p6,context,a,b,c,d,e,f,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} %Equal.sym(Array & F32,Array.get(F32,owner,p7),(owner,h),StorageLaws.read(F32,values,p7)) : {Lanes.gathered(~Context,~map,context,a,b,c,d,e,f,g,_) == (owner,cell(~Context,~map,values,position,context)) : Array & Tile.Tile8} {==} Uses (23): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma 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/proofs/storage_refinement.bend&name=read https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=read https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=cell https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather1 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather2 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather3 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather4 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather5 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather6 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather7 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gathered