proofs/traversal_lanes_refinement.bend
stelliferous@0.0.3.0 · 489 lines · 0 definitions
1# Lanes.map is Traversal.map_in_place: on a balanced array that holds its
2# count positions, the rounds through tiles and the ordered scalar map leave
3# the same array.
4import Base
5import stelliferous@0.0.3.0/traversal_lanes.bend as Lanes
6import stelliferous@0.0.3.0/traversal_cells.bend as Cells
7import stelliferous@0.0.3.0/traversal_array.bend as Traversal
8import stelliferous@0.0.3.0/traversal_loop.bend as Loop
9import stelliferous@0.0.3.0/kernel_tile.bend as Tile
10import stelliferous@0.0.3.0/proofs/traversal_cells_refinement.bend as CellLaws
11import stelliferous@0.0.3.0/proofs/traversal_batch_refinement.bend as Batch
12import stelliferous@0.0.3.0/proofs/traversal_array_refinement.bend as ArrayLaws
13import stelliferous@0.0.3.0/proofs/traversal_map_readback.bend as MapReadback
14import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
15import stelliferous@0.0.3.0/proofs/storage_refinement.bend as StorageLaws
16import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
17import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
18import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
19import stelliferous@0.0.3.0/proofs/nat_division.bend as Division
20import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
21import stelliferous@0.0.3.0/proofs/word_arithmetic.bend as WordArithmetic
22import stelliferous@0.0.3.0/proofs/word_power_of_two.bend as Power
23import stelliferous@0.0.3.0/proofs/kernel_tile_refinement.bend as TileLaws
24import stelliferous@0.0.3.0/proofs/loop_projection.bend as Projection
25import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
26
27def tile_values(values: Tile.Tile8) -> List<&2,F32>:
28 Tile.Tile{a,b,c,d,e,f,g,h} = values
29 [a,b,c,d,e,f,g,h]
30
31def cell(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+position: U32,+context: Context) -> Tile.Tile8:
32 +p1 = (position + 1 : U32)
33 +p2 = (p1 + 1 : U32)
34 +p3 = (p2 + 1 : U32)
35 +p4 = (p3 + 1 : U32)
36 +p5 = (p4 + 1 : U32)
37 +p6 = (p5 + 1 : U32)
38 +p7 = (p6 + 1 : U32)
39 Tile.Tile{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)),
40 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))}
41
42def position_after(count: Nat,position: U32) -> U32:
43 match count:
44 case 0n: position
45 case 1n+rest: position_after(rest,(position + 1 : U32))
46
47def position_after_matches(+count: Nat,+position: U32) -> {position_after(count,position) == (position + U32.from_nat(count) : U32) : U32}:
48 match count:
49 case 0n: Equal.sym(U32,(position + 0 : U32),position,Arithmetic.add_zero(position))
50 case 1n+ +rest:
51 Equal.trans(U32,position_after(rest,(position + 1 : U32)),((position + 1 : U32) + U32.from_nat(rest) : U32),(position + U32.from_nat(1n+rest) : U32),position_after_matches(rest,(position + 1 : U32)),Equal.sym(U32,(position + U32.from_nat(1n+rest) : U32),((position + 1 : U32) + U32.from_nat(rest) : U32),Projection.indexed_successor(position,rest)))
52
53def identity_cell_at(+lane: Nat,+values: Tree.Tree<F32>,+position: U32,within: {Nat.is_lt(lane,8n) == True{} : Bool}) ->
54 {TileLaws.select_lane(lane,cell(~Unit,~(context => value => value),values,position,Unit{})) == Tree.read(F32,values,position_after(lane,position)) : F32}:
55 match lane:
56 case 0n: {==}
57 case 1n: {==}
58 case 2n: {==}
59 case 3n: {==}
60 case 4n: {==}
61 case 5n: {==}
62 case 6n: {==}
63 case 7n: {==}
64 case 8n+ +rest:
65 Empty.absurd({TileLaws.select_lane(lane,cell(~Unit,~(context => value => value),values,position,Unit{})) == Tree.read(F32,values,position_after(lane,position)) : F32},
66 WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(rest,0n),True{},Equal.sym(Bool,Nat.is_lt(rest,0n),False{},Division.lt_zero(rest)),within)))
67
68def identity_cell_indexed(+lane: Nat,+values: Tree.Tree<F32>,+position: U32,within: {Nat.is_lt(lane,8n) == True{} : Bool}) ->
69 {TileLaws.select_lane(lane,cell(~Unit,~(context => value => value),values,position,Unit{})) == Tree.read(F32,values,(position + U32.from_nat(lane) : U32)) : F32}:
70 %position_after_matches(lane,position) : {TileLaws.select_lane(lane,cell(~Unit,~(context => value => value),values,position,Unit{})) == Tree.read(F32,values,_) : F32}
71 identity_cell_at(lane,values,position,within)
72
73def identity_cell_equal(+left: Tree.Tree<F32>,+right: Tree.Tree<F32>,+position: U32,
74 e0: {Tree.read(F32,left,position_after(0n,position)) == Tree.read(F32,right,position_after(0n,position)) : F32},
75 e1: {Tree.read(F32,left,position_after(1n,position)) == Tree.read(F32,right,position_after(1n,position)) : F32},
76 e2: {Tree.read(F32,left,position_after(2n,position)) == Tree.read(F32,right,position_after(2n,position)) : F32},
77 e3: {Tree.read(F32,left,position_after(3n,position)) == Tree.read(F32,right,position_after(3n,position)) : F32},
78 e4: {Tree.read(F32,left,position_after(4n,position)) == Tree.read(F32,right,position_after(4n,position)) : F32},
79 e5: {Tree.read(F32,left,position_after(5n,position)) == Tree.read(F32,right,position_after(5n,position)) : F32},
80 e6: {Tree.read(F32,left,position_after(6n,position)) == Tree.read(F32,right,position_after(6n,position)) : F32},
81 e7: {Tree.read(F32,left,position_after(7n,position)) == Tree.read(F32,right,position_after(7n,position)) : F32}) ->
82 {cell(~Unit,~(context => value => value),left,position,Unit{}) == cell(~Unit,~(context => value => value),right,position,Unit{}) : Tile.Tile8}:
83 TileLaws.tiles_equal(cell(~Unit,~(context => value => value),left,position,Unit{}),cell(~Unit,~(context => value => value),right,position,Unit{}),e0,e1,e2,e3,e4,e5,e6,e7)
84
85def gathered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+position: U32,+context: Context) ->
86 {Lanes.gather(~Context,~map,Tree.pack(F32,values),position,context) == (Tree.pack(F32,values),cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}:
87 -owner = Tree.pack(F32,values)
88 +p1 = (position + 1 : U32)
89 +p2 = (p1 + 1 : U32)
90 +p3 = (p2 + 1 : U32)
91 +p4 = (p3 + 1 : U32)
92 +p5 = (p4 + 1 : U32)
93 +p6 = (p5 + 1 : U32)
94 +p7 = (p6 + 1 : U32)
95 +a = Tree.read(F32,values,position)
96 +b = Tree.read(F32,values,p1)
97 +c = Tree.read(F32,values,p2)
98 +d = Tree.read(F32,values,p3)
99 +e = Tree.read(F32,values,p4)
100 +f = Tree.read(F32,values,p5)
101 +g = Tree.read(F32,values,p6)
102 +h = Tree.read(F32,values,p7)
103 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,position),(owner,a),StorageLaws.read(F32,values,position)) :
104 {Lanes.gather1(~Context,~map,position,context,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
105 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p1),(owner,b),StorageLaws.read(F32,values,p1)) :
106 {Lanes.gather2(~Context,~map,p1,context,a,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
107 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p2),(owner,c),StorageLaws.read(F32,values,p2)) :
108 {Lanes.gather3(~Context,~map,p2,context,a,b,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
109 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p3),(owner,d),StorageLaws.read(F32,values,p3)) :
110 {Lanes.gather4(~Context,~map,p3,context,a,b,c,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
111 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p4),(owner,e),StorageLaws.read(F32,values,p4)) :
112 {Lanes.gather5(~Context,~map,p4,context,a,b,c,d,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
113 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p5),(owner,f),StorageLaws.read(F32,values,p5)) :
114 {Lanes.gather6(~Context,~map,p5,context,a,b,c,d,e,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
115 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p6),(owner,g),StorageLaws.read(F32,values,p6)) :
116 {Lanes.gather7(~Context,~map,p6,context,a,b,c,d,e,f,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
117 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p7),(owner,h),StorageLaws.read(F32,values,p7)) :
118 {Lanes.gathered(~Context,~map,context,a,b,c,d,e,f,g,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
119 {==}
120
121# Eight ordered writes from position.
122def written(+values: Tree.Tree<F32>,+position: U32,a: F32,b: F32,c: F32,d: F32,e: F32,f: F32,g: F32,h: F32) -> Tree.Tree<F32>:
123 +p1 = (position + 1 : U32)
124 +p2 = (p1 + 1 : U32)
125 +p3 = (p2 + 1 : U32)
126 +p4 = (p3 + 1 : U32)
127 +p5 = (p4 + 1 : U32)
128 +p6 = (p5 + 1 : U32)
129 +p7 = (p6 + 1 : U32)
130 Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,values,position,a),p1,b),p2,c),p3,d),p4,e),p5,f),p6,g),p7,h)
131
132def scattered(+values: Tree.Tree<F32>,+position: U32,+a: F32,+b: F32,+c: F32,+d: F32,+e: F32,+f: F32,+g: F32,+h: F32) ->
133 {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>}:
134 +p1 = (position + 1 : U32)
135 +p2 = (p1 + 1 : U32)
136 +p3 = (p2 + 1 : U32)
137 +p4 = (p3 + 1 : U32)
138 +p5 = (p4 + 1 : U32)
139 +p6 = (p5 + 1 : U32)
140 +p7 = (p6 + 1 : U32)
141 +w1 = Tree.write(F32,values,position,a)
142 +w2 = Tree.write(F32,w1,p1,b)
143 +w3 = Tree.write(F32,w2,p2,c)
144 +w4 = Tree.write(F32,w3,p3,d)
145 +w5 = Tree.write(F32,w4,p4,e)
146 +w6 = Tree.write(F32,w5,p5,f)
147 +w7 = Tree.write(F32,w6,p6,g)
148 +w8 = Tree.write(F32,w7,p7,h)
149 %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,values),position,a),Tree.pack(F32,w1),StorageLaws.write(F32,values,position,a)) :
150 {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>}
151 %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w1),p1,b),Tree.pack(F32,w2),StorageLaws.write(F32,w1,p1,b)) :
152 {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>}
153 %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w2),p2,c),Tree.pack(F32,w3),StorageLaws.write(F32,w2,p2,c)) :
154 {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>}
155 %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w3),p3,d),Tree.pack(F32,w4),StorageLaws.write(F32,w3,p3,d)) :
156 {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>}
157 %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w4),p4,e),Tree.pack(F32,w5),StorageLaws.write(F32,w4,p4,e)) :
158 {Array.set(F32,Array.set(F32,Array.set(F32,_,p5,f),p6,g),p7,h) == Tree.pack(F32,w8) : Array<F32>}
159 %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w5),p5,f),Tree.pack(F32,w6),StorageLaws.write(F32,w5,p5,f)) :
160 {Array.set(F32,Array.set(F32,_,p6,g),p7,h) == Tree.pack(F32,w8) : Array<F32>}
161 %Equal.sym(Array<F32>,Array.set(F32,Tree.pack(F32,w6),p6,g),Tree.pack(F32,w7),StorageLaws.write(F32,w6,p6,g)) :
162 {Array.set(F32,_,p7,h) == Tree.pack(F32,w8) : Array<F32>}
163 StorageLaws.write(F32,w7,p7,h)
164
165def cell_scattered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+position: U32,+context: Context) ->
166 {Lanes.scatter(Tree.pack(F32,values),position,cell(~Context,~map,values,position,context)) ==
167 Tree.pack(F32,Batch.batch(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map),8n,position,context,values,values)) : Array<F32>}:
168 +p1 = (position + 1 : U32)
169 +p2 = (p1 + 1 : U32)
170 +p3 = (p2 + 1 : U32)
171 +p4 = (p3 + 1 : U32)
172 +p5 = (p4 + 1 : U32)
173 +p6 = (p5 + 1 : U32)
174 +p7 = (p6 + 1 : U32)
175 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)),
176 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)))
177
178# One round maps eight positions.
179def round(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>,+start: Nat,+slot: U32,+context: Context,
180 +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(F32,values) == capacity : U32},+balanced: Shape.Balanced(F32,depth,values),
181 +limit: {Nat.is_le(depth,30n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
182 +room: {Nat.is_le(Nat.add(start,8n),U32.to_nat(capacity)) == True{} : Bool}) ->
183 {Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,
184 Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
185 Cells.State{Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n,U32.from_nat(start),context,values)),
186 Tree.pack(Tile.Tile8,Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~map,values,U32.from_nat(start),context))),(U32.from_nat(start) + 8 : U32),
187 U32.and((slot + 1 : U32),63),context} : Cells.State<Array<F32>,Tile.Tile8,Context>}:
188 +position = U32.from_nat(start)
189 %Batch.mapped(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map),8n,start,context,values,depth,capacity,capacity_equal,balanced,Order.successor(depth,30n,limit),capacity_ok,room) :
190 {Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}) ==
191 Cells.State{Tree.pack(F32,_),Tree.pack(Tile.Tile8,Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~map,values,position,context))),(position + 8 : U32),
192 U32.and((slot + 1 : U32),63),context} : Cells.State<Array<F32>,Tile.Tile8,Context>}
193 CellLaws.round(~F32,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,values,scratch,position,slot,context,
194 cell(~Context,~map,values,position,context),Batch.batch(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map),8n,position,context,values,values),
195 gathered(~Context,~map,values,position,context),cell_scattered(~Context,~map,values,position,context))
196
197# The scalar map from any position, on a packed tree.
198def output(~Context: Data,+state: Batch.ModelState(~F32,~Context)) ->
199 {Traversal.mapped_output(~F32,~Context,ArrayLaws.represent_map(~F32,~Context,state)) == Tree.pack(F32,MapReadback.output(~F32,~Context,state)) : Array<F32>}:
200 Traversal.State{Unit{},output,position,context} = state
201 {==}
202
203def scalar(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree<F32>) ->
204 {Traversal.map_in_place(~F32,~Context,~map,count,position,context,Tree.pack(F32,values)) ==
205 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}:
206 +initial = {Traversal.State{Unit{},values,position,context} : Batch.ModelState(~F32,~Context)}
207 %Equal.sym(Traversal.State<&2,&1,Unit,Array<F32>,Context>,
208 Loop.run(~Traversal.State<&2,&1,Unit,Array<F32>,Context>,~Traversal.map_step(~F32,~Context,~map),count,Traversal.State{Unit{},Tree.pack(F32,values),position,context}),
209 ArrayLaws.represent_map(~F32,~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial)),
210 ArrayLaws.map_loop_refines_model(~F32,~Context,~map,count,initial)) :
211 {Traversal.mapped_output(~F32,~Context,_) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}
212 output(~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial))
213
214def few(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+slot: U32,+context: Context,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>) ->
215 {Lanes.finish(~Context,~map,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}) ==
216 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}:
217 scalar(~Context,~map,count,position,context,values)
218
219# The position of the model map after k steps from start.
220def stepped(steps: Nat,start: Nat) -> U32:
221 match steps:
222 case 0n: U32.from_nat(start)
223 case 1n+rest: (stepped(rest,start) + 1 : U32)
224
225def advanced(+steps: Nat,+start: Nat) -> {stepped(steps,start) == U32.from_nat(Nat.add(steps,start)) : U32}:
226 match steps:
227 case 0n: {==}
228 case 1n+ +rest:
229 %Equal.sym(U32,stepped(rest,start),U32.from_nat(Nat.add(rest,start)),advanced(rest,start)) : {(_ + 1 : U32) == U32.from_nat(1n+Nat.add(rest,start)) : U32}
230 Bounds.add_one(U32.from_nat(Nat.add(rest,start)))
231
232def after_round(+start: Nat) -> {(U32.from_nat(start) + 8 : U32) == U32.from_nat(8n+start) : U32}:
233 %Order.commutative(start,8n) : {(U32.from_nat(start) + 8 : U32) == U32.from_nat(_) : U32}
234 WordArithmetic.native_add(start,8n)
235
236def round_room(+start: Nat,+rest: Nat,+capacity: Nat,room: {Nat.is_le(Nat.add(start,8n+rest),capacity) == True{} : Bool}) ->
237 {Nat.is_le(Nat.add(start,8n),capacity) == True{} : Bool}:
238 Order.transitive(Nat.add(start,8n),Nat.add(start,8n+rest),capacity,Order.offset_le(start,8n,8n+rest,Order.le_add(8n,rest)),room)
239
240def rest_room(+start: Nat,+rest: Nat,+capacity: Nat,room: {Nat.is_le(Nat.add(start,8n+rest),capacity) == True{} : Bool}) ->
241 {Nat.is_le(Nat.add(8n+start,rest),capacity) == True{} : Bool}:
242 Order.advance_room(7n+start,rest,capacity,Order.advance_room(6n+start,1n+rest,capacity,Order.advance_room(5n+start,2n+rest,capacity,
243 Order.advance_room(4n+start,3n+rest,capacity,Order.advance_room(3n+start,4n+rest,capacity,Order.advance_room(2n+start,5n+rest,capacity,
244 Order.advance_room(1n+start,6n+rest,capacity,Order.advance_room(start,7n+rest,capacity,room))))))))
245
246# The shared induction on eight-value rounds. The proposition may carry all
247# owners and bounds, so binary and ternary instances need only local cases.
248def finish_small(~Owner: Type,~Context: Data,~gather: Owner -> U32 -> Context -> Owner & Tile.Tile8,
249 ~scatter: Owner -> U32 -> Tile.Tile8 -> Owner,~finish: Nat -> Cells.State<Owner,Tile.Tile8,Context> -> Owner,
250 +count: Nat,-state: Cells.State<Owner,Tile.Tile8,Context>,small: {Nat.is_lt(count,8n) == True{} : Bool}) ->
251 {Lanes.rounds_with(~Owner,~Context,~gather,~scatter,~finish,count,state) == finish(count,state) : Owner}:
252 match count:
253 case 0n: {==}
254 case 1n: {==}
255 case 2n: {==}
256 case 3n: {==}
257 case 4n: {==}
258 case 5n: {==}
259 case 6n: {==}
260 case 7n: {==}
261 case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
262 Empty.absurd({Lanes.rounds_with(~Owner,~Context,~gather,~scatter,~finish,8n+rest,state) == finish(8n+rest,state) : Owner},
263 WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(rest,0n),True{},Equal.sym(Bool,Nat.is_lt(rest,0n),False{},Division.lt_zero(rest)),small)))
264
265def by_rounds(~Property: Nat -> Type,
266 ~few: @+count: Nat -> {Nat.is_lt(count,8n) == True{} : Bool} -> Property(count),
267 ~more: @+rest: Nat -> Property(rest) -> Property(8n+rest),count: Nat) -> Property(count):
268 match count:
269 case 0n: few(0n,{==})
270 case 1n: few(1n,{==})
271 case 2n: few(2n,{==})
272 case 3n: few(3n,{==})
273 case 4n: few(4n,{==})
274 case 5n: few(5n,{==})
275 case 6n: few(6n,{==})
276 case 7n: few(7n,{==})
277 case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
278 more(rest,by_rounds(~Property,~few,~more,rest))
279
280# Every count: whole rounds, then the last positions one by one.
281def rounds_property(~Context: Data,~map: Context -> F32 -> F32,count: Nat) -> Type:
282 @+start: Nat -> @+slot: U32 -> @+context: Context -> @+values: Tree.Tree<F32> -> @+scratch: Tree.Tree<Tile.Tile8> ->
283 @+depth: Nat -> @+capacity: U32 -> @+capacity_equal: {Tree.capacity(F32,values) == capacity : U32} -> @+balanced: Shape.Balanced(F32,depth,values) ->
284 @+limit: {Nat.is_le(depth,30n) == True{} : Bool} -> @+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool} ->
285 @+room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool} ->
286 {Lanes.rounds(~Context,~map,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
287 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,U32.from_nat(start),context,values)) : Array<F32>}
288
289def few_rounds(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,small: {Nat.is_lt(count,8n) == True{} : Bool}) -> rounds_property(~Context,~map,count):
290 match count:
291 case 0n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
292 few(~Context,~map,0n,U32.from_nat(start),slot,context,values,scratch)
293 case 1n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
294 few(~Context,~map,1n,U32.from_nat(start),slot,context,values,scratch)
295 case 2n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
296 few(~Context,~map,2n,U32.from_nat(start),slot,context,values,scratch)
297 case 3n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
298 few(~Context,~map,3n,U32.from_nat(start),slot,context,values,scratch)
299 case 4n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
300 few(~Context,~map,4n,U32.from_nat(start),slot,context,values,scratch)
301 case 5n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
302 few(~Context,~map,5n,U32.from_nat(start),slot,context,values,scratch)
303 case 6n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
304 few(~Context,~map,6n,U32.from_nat(start),slot,context,values,scratch)
305 case 7n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
306 few(~Context,~map,7n,U32.from_nat(start),slot,context,values,scratch)
307 case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
308 start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
309 Empty.absurd({Lanes.rounds(~Context,~map,8n+rest,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
310 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,U32.from_nat(start),context,values)) : Array<F32>},
311 WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(rest,0n),True{},Equal.sym(Bool,Nat.is_lt(rest,0n),False{},Division.lt_zero(rest)),small)))
312
313def more_rounds(~Context: Data,~map: Context -> F32 -> F32,+rest: Nat,previous: rounds_property(~Context,~map,rest)) -> rounds_property(~Context,~map,8n+rest):
314 start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
315 +position = U32.from_nat(start)
316 +mapped = MapReadback.run(~F32,~Context,~map,8n,position,context,values)
317 +next = Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~map,values,position,context))
318 +turn = U32.and((slot + 1 : U32),63)
319 %Equal.sym(Cells.State<Array<F32>,Tile.Tile8,Context>,
320 Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),
321 Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),(position + 8 : U32),turn,context},
322 round(~Context,~map,values,scratch,start,slot,context,depth,capacity,capacity_equal,balanced,limit,capacity_ok,round_room(start,rest,U32.to_nat(capacity),room))) :
323 {Lanes.rounds(~Context,~map,rest,_) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,position,context,values)) : Array<F32>}
324 %Equal.sym(U32,(position + 8 : U32),U32.from_nat(8n+start),after_round(start)) :
325 {Lanes.rounds(~Context,~map,rest,Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),_,turn,context}) ==
326 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,position,context,values)) : Array<F32>}
327 %Equal.sym(U32,stepped(8n,start),U32.from_nat(8n+start),advanced(8n,start)) :
328 {Lanes.rounds(~Context,~map,rest,Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),U32.from_nat(8n+start),turn,context}) ==
329 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,rest,_,context,mapped)) : Array<F32>}
330 previous(8n+start,turn,context,mapped,next,depth,capacity,
331 Equal.trans(U32,Tree.capacity(F32,mapped),Tree.capacity(F32,values),capacity,MapReadback.capacity(~F32,~Context,~map,8n,position,context,values),capacity_equal),
332 MapReadback.balanced(~F32,~Context,~map,8n,position,context,values,depth,balanced),limit,capacity_ok,rest_room(start,rest,U32.to_nat(capacity),room))
333
334def rounds(~Context: Data,~map: Context -> F32 -> F32,count: Nat,+start: Nat,+slot: U32,+context: Context,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>,
335 +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(F32,values) == capacity : U32},+balanced: Shape.Balanced(F32,depth,values),
336 +limit: {Nat.is_le(depth,30n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
337 +room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool}) ->
338 {Lanes.rounds(~Context,~map,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
339 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,U32.from_nat(start),context,values)) : Array<F32>}:
340 by_rounds(~rounds_property(~Context,~map),~few_rounds(~Context,~map),~more_rounds(~Context,~map),count)(start,slot,context,values,scratch,depth,capacity,capacity_equal,balanced,limit,capacity_ok,room)
341
342# The whole map from any position, with a fresh scratch array.
343def map(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+start: Nat,+context: Context,+values: Tree.Tree<F32>,+depth: Nat,+balanced: Shape.Balanced(F32,depth,values),
344 +limit: {Nat.is_le(depth,30n) == True{} : Bool},+room: {Nat.is_le(Nat.add(start,count),U32.to_nat(U32.shln(1,depth))) == True{} : Bool}) ->
345 {Lanes.map(~Context,~map,count,U32.from_nat(start),context,Tree.pack(F32,values)) ==
346 Traversal.map_in_place(~F32,~Context,~map,count,U32.from_nat(start),context,Tree.pack(F32,values)) : Array<F32>}:
347 +position = U32.from_nat(start)
348 %Equal.sym(Array<F32>,Traversal.map_in_place(~F32,~Context,~map,count,position,context,Tree.pack(F32,values)),Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)),
349 scalar(~Context,~map,count,position,context,values)) :
350 {Lanes.map(~Context,~map,count,position,context,Tree.pack(F32,values)) == _ : Array<F32>}
351 %Equal.sym(Array<Tile.Tile8>,Array.new(Tile.Tile8,6n,Tile.filled(0.0)),Tree.pack(Tile.Tile8,Tree.fresh(Tile.Tile8,6n,Tile.filled(0.0))),StorageLaws.fresh(Tile.Tile8,6n,Tile.filled(0.0))) :
352 {Lanes.rounds(~Context,~map,count,Cells.State{Tree.pack(F32,values),_,position,0,context}) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}
353 rounds(~Context,~map,count,start,0,context,values,Tree.fresh(Tile.Tile8,6n,Tile.filled(0.0)),depth,U32.shln(1,depth),Shape.capacity(F32,depth,values,balanced),balanced,limit,
354 Power.native_power_bound(depth,Order.successor(depth,30n,limit)),room)
355
356# A change after gathering is determined by one eight-value leaf equation.
357def GatherRoundLaw(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8) -> Type:
358 @+context: Context -> @+a: F32 -> @+b: F32 -> @+c: F32 -> @+d: F32 -> @+e: F32 -> @+f: F32 -> @+g: F32 -> @read: Array<F32> & F32 ->
359 {after(context,Lanes.gathered(~Context,~initial,context,a,b,c,d,e,f,g,read)) == Lanes.gathered(~Context,~operation,context,a,b,c,d,e,f,g,read) : Array<F32> & Tile.Tile8}
360
361def transform7(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,+c: F32,+d: F32,+e: F32,+f: F32,read: Array<F32> & F32) ->
362 {after(context,Lanes.gather7(~Context,~initial,position,context,a,b,c,d,e,f,read)) == Lanes.gather7(~Context,~operation,position,context,a,b,c,d,e,f,read) : Array<F32> & Tile.Tile8}:
363 (values,g) = read
364 lawful(context,a,b,c,d,e,f,g,Array.get(F32,values,(position + 1 : U32)))
365
366def transform6(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,+c: F32,+d: F32,+e: F32,read: Array<F32> & F32) ->
367 {after(context,Lanes.gather6(~Context,~initial,position,context,a,b,c,d,e,read)) == Lanes.gather6(~Context,~operation,position,context,a,b,c,d,e,read) : Array<F32> & Tile.Tile8}:
368 (values,f) = read
369 transform7(~Context,~initial,~operation,~after,~lawful,(position + 1 : U32),context,a,b,c,d,e,f,Array.get(F32,values,(position + 1 : U32)))
370
371def transform5(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,+c: F32,+d: F32,read: Array<F32> & F32) ->
372 {after(context,Lanes.gather5(~Context,~initial,position,context,a,b,c,d,read)) == Lanes.gather5(~Context,~operation,position,context,a,b,c,d,read) : Array<F32> & Tile.Tile8}:
373 (values,e) = read
374 transform6(~Context,~initial,~operation,~after,~lawful,(position + 1 : U32),context,a,b,c,d,e,Array.get(F32,values,(position + 1 : U32)))
375
376def transform4(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,+c: F32,read: Array<F32> & F32) ->
377 {after(context,Lanes.gather4(~Context,~initial,position,context,a,b,c,read)) == Lanes.gather4(~Context,~operation,position,context,a,b,c,read) : Array<F32> & Tile.Tile8}:
378 (values,d) = read
379 transform5(~Context,~initial,~operation,~after,~lawful,(position + 1 : U32),context,a,b,c,d,Array.get(F32,values,(position + 1 : U32)))
380
381def transform3(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,read: Array<F32> & F32) ->
382 {after(context,Lanes.gather3(~Context,~initial,position,context,a,b,read)) == Lanes.gather3(~Context,~operation,position,context,a,b,read) : Array<F32> & Tile.Tile8}:
383 (values,c) = read
384 transform4(~Context,~initial,~operation,~after,~lawful,(position + 1 : U32),context,a,b,c,Array.get(F32,values,(position + 1 : U32)))
385
386def transform2(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,read: Array<F32> & F32) ->
387 {after(context,Lanes.gather2(~Context,~initial,position,context,a,read)) == Lanes.gather2(~Context,~operation,position,context,a,read) : Array<F32> & Tile.Tile8}:
388 (values,b) = read
389 transform3(~Context,~initial,~operation,~after,~lawful,(position + 1 : U32),context,a,b,Array.get(F32,values,(position + 1 : U32)))
390
391def transform1(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,read: Array<F32> & F32) ->
392 {after(context,Lanes.gather1(~Context,~initial,position,context,read)) == Lanes.gather1(~Context,~operation,position,context,read) : Array<F32> & Tile.Tile8}:
393 (values,a) = read
394 transform2(~Context,~initial,~operation,~after,~lawful,(position + 1 : U32),context,a,Array.get(F32,values,(position + 1 : U32)))
395
396def gather_transform(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array<F32> & Tile.Tile8) -> Array<F32> & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),values: Array<F32>,+position: U32,+context: Context) ->
397 {after(context,Lanes.gather(~Context,~initial,values,position,context)) == Lanes.gather(~Context,~operation,values,position,context) : Array<F32> & Tile.Tile8}:
398 transform1(~Context,~initial,~operation,~after,~lawful,position,context,Array.get(F32,values,position))
399
400# A gather equal to the scalar gather may use any internal arithmetic stages.
401def GatherLaw(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8) -> Type:
402 @values: Array<F32> -> @+position: U32 -> @+context: Context ->
403 {collect(values,position,context) == Lanes.gather(~Context,~operation,values,position,context) : Array<F32> & Tile.Tile8}
404
405def collected_values(~Context: Data,~operation: Context -> F32 -> F32,+values: Tree.Tree<F32>,+position: U32,+context: Context) -> Tree.Tree<F32>:
406 Batch.batch(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~operation),8n,position,context,values,values)
407
408def collected_state(~Context: Data,~operation: Context -> F32 -> F32,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>,+position: U32,+slot: U32,+context: Context) -> Cells.State<Array<F32>,Tile.Tile8,Context>:
409 Cells.State{Tree.pack(F32,collected_values(~Context,~operation,values,position,context)),
410 Tree.pack(Tile.Tile8,Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~operation,values,position,context))),
411 (position + 8 : U32),U32.and((slot + 1 : U32),63),context}
412
413def collected_step(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>,+position: U32,+slot: U32,+context: Context,
414 gathered: {collect(Tree.pack(F32,values),position,context) == (Tree.pack(F32,values),cell(~Context,~operation,values,position,context)) : Array<F32> & Tile.Tile8}) ->
415 {Cells.step(~Array<F32>,~Tile.Tile8,~Context,~collect,~Lanes.scatter,~8,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}) == collected_state(~Context,~operation,values,scratch,position,slot,context) : Cells.State<Array<F32>,Tile.Tile8,Context>}:
416 CellLaws.round(~F32,~Tile.Tile8,~Context,~collect,~Lanes.scatter,~8,values,scratch,position,slot,context,
417 cell(~Context,~operation,values,position,context),collected_values(~Context,~operation,values,position,context),gathered,cell_scattered(~Context,~operation,values,position,context))
418
419def WithProperty(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,count: Nat) -> Type:
420 @+values: Tree.Tree<F32> -> @+scratch: Tree.Tree<Tile.Tile8> -> @+position: U32 -> @+slot: U32 -> @+context: Context ->
421 {Lanes.rounds_with(~Array<F32>,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}) ==
422 Lanes.rounds(~Context,~operation,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}) : Array<F32>}
423
424def with_few(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,+count: Nat,small: {Nat.is_lt(count,8n) == True{} : Bool}) -> WithProperty(~Context,~operation,~collect,count):
425 +small = small
426 values => scratch => position => slot => context =>
427 Equal.trans(Array<F32>,
428 Lanes.rounds_with(~Array<F32>,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),
429 Lanes.finish(~Context,~operation,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),
430 Lanes.rounds(~Context,~operation,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),
431 finish_small(~Array<F32>,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context},small),
432 Equal.sym(Array<F32>,Lanes.rounds(~Context,~operation,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),
433 Lanes.finish(~Context,~operation,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),
434 finish_small(~Array<F32>,~Context,~Lanes.gather(~Context,~operation),~Lanes.scatter,~Lanes.finish(~Context,~operation),count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context},small)))
435
436def with_more(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+rest: Nat,remaining: WithProperty(~Context,~operation,~collect,rest)) -> WithProperty(~Context,~operation,~collect,8n+rest):
437 values => scratch => position => slot => context =>
438 %Equal.sym(Cells.State<Array<F32>,Tile.Tile8,Context>,
439 Cells.step(~Array<F32>,~Tile.Tile8,~Context,~collect,~Lanes.scatter,~8,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),collected_state(~Context,~operation,values,scratch,position,slot,context),
440 collected_step(~Context,~operation,~collect,values,scratch,position,slot,context,
441 Equal.trans(Array<F32> & Tile.Tile8,collect(Tree.pack(F32,values),position,context),Lanes.gather(~Context,~operation,Tree.pack(F32,values),position,context),
442 (Tree.pack(F32,values),cell(~Context,~operation,values,position,context)),lawful(Tree.pack(F32,values),position,context),gathered(~Context,~operation,values,position,context)))) :
443 {Lanes.rounds_with(~Array<F32>,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),rest,_) ==
444 Lanes.rounds(~Context,~operation,rest,Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~operation),~Lanes.scatter,~8,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context})) : Array<F32>}
445 %Equal.sym(Cells.State<Array<F32>,Tile.Tile8,Context>,
446 Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~operation),~Lanes.scatter,~8,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}),collected_state(~Context,~operation,values,scratch,position,slot,context),
447 collected_step(~Context,~operation,~Lanes.gather(~Context,~operation),values,scratch,position,slot,context,gathered(~Context,~operation,values,position,context))) :
448 {Lanes.rounds_with(~Array<F32>,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),rest,collected_state(~Context,~operation,values,scratch,position,slot,context)) == Lanes.rounds(~Context,~operation,rest,_) : Array<F32>}
449 remaining(collected_values(~Context,~operation,values,position,context),Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~operation,values,position,context)),(position + 8 : U32),U32.and((slot + 1 : U32),63),context)
450
451def with_rounds(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),count: Nat) -> WithProperty(~Context,~operation,~collect,count):
452 by_rounds(~WithProperty(~Context,~operation,~collect),~with_few(~Context,~operation,~collect),~with_more(~Context,~operation,~collect,~lawful),count)
453
454def with_packed(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,+values: Tree.Tree<F32>) ->
455 {Lanes.map_with(~Context,~operation,~collect,count,position,context,Tree.pack(F32,values)) == Lanes.map(~Context,~operation,count,position,context,Tree.pack(F32,values)) : Array<F32>}:
456 %StorageLaws.fresh(Tile.Tile8,6n,Tile.filled(0.0)) :
457 {Lanes.rounds_with(~Array<F32>,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),count,Cells.State{Tree.pack(F32,values),_,position,0,context}) ==
458 Lanes.rounds(~Context,~operation,count,Cells.State{Tree.pack(F32,values),_,position,0,context}) : Array<F32>}
459 with_rounds(~Context,~operation,~collect,~lawful,count)(values,Tree.fresh(Tile.Tile8,6n,Tile.filled(0.0)),position,0,context)
460
461def with_observed(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,-values: Array<F32>,observation: StorageLaws.Observation<F32,values>) ->
462 {Lanes.map_with(~Context,~operation,~collect,count,position,context,values) == Lanes.map(~Context,~operation,count,position,context,values) : Array<F32>}:
463 StorageLaws.Observation{+tree,packed,reflected} = observation
464 %packed : {Lanes.map_with(~Context,~operation,~collect,count,position,context,_) == Lanes.map(~Context,~operation,count,position,context,_) : Array<F32>}
465 with_packed(~Context,~operation,~collect,~lawful,count,position,context,tree)
466
467def map_with(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,values: Array<F32>) ->
468 {Lanes.map_with(~Context,~operation,~collect,count,position,context,values) == Lanes.map(~Context,~operation,count,position,context,values) : Array<F32>}:
469 with_observed(~Context,~operation,~collect,~lawful,count,position,context,values,StorageLaws.observe(F32,values))
470
471def map_with_when(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+covered: Bool,+count: Nat,+position: U32,+context: Context,values: Array<F32>) ->
472 {Lanes.map_with_when(~Context,~operation,~collect,covered,count,position,context,values) == Lanes.map_when(~Context,~operation,covered,count,position,context,values) : Array<F32>}:
473 match covered:
474 case False{}: {==}
475 case True{}: map_with(~Context,~operation,~collect,~lawful,count,position,context,values)
476
477def TileLaw(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8) -> Type:
478 @+context: Context -> @+a: F32 -> @+b: F32 -> @+c: F32 -> @+d: F32 -> @+e: F32 -> @+f: F32 -> @+g: F32 -> @+h: F32 ->
479 {transform(context,Tile.Tile{a,b,c,d,e,f,g,h}) == Tile.Tile{operation(context,a),operation(context,b),operation(context,c),operation(context,d),operation(context,e),operation(context,f),operation(context,g),operation(context,h)} : Tile.Tile8}
480
481def transformed_round(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8,~lawful: TileLaw(~Context,~operation,~transform),+context: Context,+a: F32,+b: F32,+c: F32,+d: F32,+e: F32,+f: F32,+g: F32,read: Array<F32> & F32) ->
482 {Lanes.transformed(~Context,~transform,context,Lanes.gathered(~Context,~Lanes.identity(~Context),context,a,b,c,d,e,f,g,read)) == Lanes.gathered(~Context,~operation,context,a,b,c,d,e,f,g,read) : Array<F32> & Tile.Tile8}:
483 (values,h) = read
484 Equal.cong(Tile.Tile8,Array<F32> & Tile.Tile8,tile => (values,tile),transform(context,Tile.Tile{a,b,c,d,e,f,g,h}),
485 Tile.Tile{operation(context,a),operation(context,b),operation(context,c),operation(context,d),operation(context,e),operation(context,f),operation(context,g),operation(context,h)},lawful(context,a,b,c,d,e,f,g,h))
486
487def gather_tiles(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8,~lawful: TileLaw(~Context,~operation,~transform),values: Array<F32>,+position: U32,+context: Context) ->
488 {Lanes.gather_transformed(~Context,~transform,values,position,context) == Lanes.gather(~Context,~operation,values,position,context) : Array<F32> & Tile.Tile8}:
489 gather_transform(~Context,~Lanes.identity(~Context),~operation,~Lanes.transformed(~Context,~transform),~transformed_round(~Context,~operation,~transform,~lawful),values,position,context)