def scattered

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:83

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

83def scattered(+values: Tree.Tree<F32>,+position: U32,+a: F32,+b: F32,+c: F32,+d: F32,+e: F32,+f: F32,+g: F32,+h: F32) ->
84  {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<F32>}:
85  +p1 = (position + 1 : U32)
86  +p2 = (p1 + 1 : U32)
87  +p3 = (p2 + 1 : U32)
88  +p4 = (p3 + 1 : U32)
89  +p5 = (p4 + 1 : U32)
90  +p6 = (p5 + 1 : U32)
91  +p7 = (p6 + 1 : U32)
92  +w1 = Tree.write(F32,values,position,a)
93  +w2 = Tree.write(F32,w1,p1,b)
94  +w3 = Tree.write(F32,w2,p2,c)
95  +w4 = Tree.write(F32,w3,p3,d)
96  +w5 = Tree.write(F32,w4,p4,e)
97  +w6 = Tree.write(F32,w5,p5,f)
98  +w7 = Tree.write(F32,w6,p6,g)
99  +w8 = Tree.write(F32,w7,p7,h)
100  %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,values),position,a),Tree.pack(F32,w1),StorageLaws.write(F32,values,position,a)) :
101    {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<F32>}
102  %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w1),p1,b),Tree.pack(F32,w2),StorageLaws.write(F32,w1,p1,b)) :
103    {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<F32>}
104  %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w2),p2,c),Tree.pack(F32,w3),StorageLaws.write(F32,w2,p2,c)) :
105    {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<F32>}
106  %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w3),p3,d),Tree.pack(F32,w4),StorageLaws.write(F32,w3,p3,d)) :
107    {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<F32>}
108  %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w4),p4,e),Tree.pack(F32,w5),StorageLaws.write(F32,w4,p4,e)) :
109    {Array.set(F32,Array.set(F32,Array.set(F32,_,p5,f),p6,g),p7,h) == Tree.pack(F32,w8) : Array<F32>}
110  %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w5),p5,f),Tree.pack(F32,w6),StorageLaws.write(F32,w5,p5,f)) :
111    {Array.set(F32,Array.set(F32,_,p6,g),p7,h) == Tree.pack(F32,w8) : Array<F32>}
112  %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w6),p6,g),Tree.pack(F32,w7),StorageLaws.write(F32,w6,p6,g)) :
113    {Array.set(F32,_,p7,h) == Tree.pack(F32,w8) : Array<F32>}
114  StorageLaws.write(F32,w7,p7,h)