TraversalLanesRefinement.scattered: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement Lines 83-114 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=83&end_line=114 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 scattered(+values: Tree.Tree,+position: U32,+a: F32,+b: F32,+c: F32,+d: F32,+e: F32,+f: F32,+g: F32,+h: F32) -> {Lanes.scatter(Tree.pack(F32,values),position,Tile.Tile{a,b,c,d,e,f,g,h}) == Tree.pack(F32,written(values,position,a,b,c,d,e,f,g,h)) : Array}: +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) +w1 = Tree.write(F32,values,position,a) +w2 = Tree.write(F32,w1,p1,b) +w3 = Tree.write(F32,w2,p2,c) +w4 = Tree.write(F32,w3,p3,d) +w5 = Tree.write(F32,w4,p4,e) +w6 = Tree.write(F32,w5,p5,f) +w7 = Tree.write(F32,w6,p6,g) +w8 = Tree.write(F32,w7,p7,h) %Equal.sym(Array,Array.set(F32,Tree.pack(F32,values),position,a),Tree.pack(F32,w1),StorageLaws.write(F32,values,position,a)) : {Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,_,p1,b),p2,c),p3,d),p4,e),p5,f),p6,g),p7,h) == Tree.pack(F32,w8) : Array} %Equal.sym(Array,Array.set(F32,Tree.pack(F32,w1),p1,b),Tree.pack(F32,w2),StorageLaws.write(F32,w1,p1,b)) : {Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,_,p2,c),p3,d),p4,e),p5,f),p6,g),p7,h) == Tree.pack(F32,w8) : Array} %Equal.sym(Array,Array.set(F32,Tree.pack(F32,w2),p2,c),Tree.pack(F32,w3),StorageLaws.write(F32,w2,p2,c)) : {Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,_,p3,d),p4,e),p5,f),p6,g),p7,h) == Tree.pack(F32,w8) : Array} %Equal.sym(Array,Array.set(F32,Tree.pack(F32,w3),p3,d),Tree.pack(F32,w4),StorageLaws.write(F32,w3,p3,d)) : {Array.set(F32,Array.set(F32,Array.set(F32,Array.set(F32,_,p4,e),p5,f),p6,g),p7,h) == Tree.pack(F32,w8) : Array} %Equal.sym(Array,Array.set(F32,Tree.pack(F32,w4),p4,e),Tree.pack(F32,w5),StorageLaws.write(F32,w4,p4,e)) : {Array.set(F32,Array.set(F32,Array.set(F32,_,p5,f),p6,g),p7,h) == Tree.pack(F32,w8) : Array} %Equal.sym(Array,Array.set(F32,Tree.pack(F32,w5),p5,f),Tree.pack(F32,w6),StorageLaws.write(F32,w5,p5,f)) : {Array.set(F32,Array.set(F32,_,p6,g),p7,h) == Tree.pack(F32,w8) : Array} %Equal.sym(Array,Array.set(F32,Tree.pack(F32,w6),p6,g),Tree.pack(F32,w7),StorageLaws.write(F32,w6,p6,g)) : {Array.set(F32,_,p7,h) == Tree.pack(F32,w8) : Array} StorageLaws.write(F32,w7,p7,h) Uses (13): 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=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=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=write 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=write https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=written https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=scatter