proofs/traversal_lanes_refinement.bend
stelliferous@0.0.2.0 · 305 lines · 21 definitions
1
2
3
4import Base
5import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
6import stelliferous@0.0.2.0/traversal_cells.bend as Cells
7import stelliferous@0.0.2.0/traversal_array.bend as Traversal
8import stelliferous@0.0.2.0/traversal_loop.bend as Loop
9import stelliferous@0.0.2.0/kernel_tile.bend as Tile
10import stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend as CellLaws
11import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as Batch
12import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as ArrayLaws
13import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as MapReadback
14import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
15import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
16import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
17import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
18import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
19import stelliferous@0.0.2.0/proofs/nat_division.bend as Division
20import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
21import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
22import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Power
23
24
25def cell(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+position: U32,+context: Context) -> Tile.Tile8:
26 +p1 = (position + 1 : U32)
27 +p2 = (p1 + 1 : U32)
28 +p3 = (p2 + 1 : U32)
29 +p4 = (p3 + 1 : U32)
30 +p5 = (p4 + 1 : U32)
31 +p6 = (p5 + 1 : U32)
32 +p7 = (p6 + 1 : U32)
33 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)),
34 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))}
35
36def gathered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+position: U32,+context: Context) ->
37 {Lanes.gather(~Context,~map,Tree.pack(F32,values),position,context) == (Tree.pack(F32,values),cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}:
38 -owner = Tree.pack(F32,values)
39 +p1 = (position + 1 : U32)
40 +p2 = (p1 + 1 : U32)
41 +p3 = (p2 + 1 : U32)
42 +p4 = (p3 + 1 : U32)
43 +p5 = (p4 + 1 : U32)
44 +p6 = (p5 + 1 : U32)
45 +p7 = (p6 + 1 : U32)
46 +a = Tree.read(F32,values,position)
47 +b = Tree.read(F32,values,p1)
48 +c = Tree.read(F32,values,p2)
49 +d = Tree.read(F32,values,p3)
50 +e = Tree.read(F32,values,p4)
51 +f = Tree.read(F32,values,p5)
52 +g = Tree.read(F32,values,p6)
53 +h = Tree.read(F32,values,p7)
54 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,position),(owner,a),StorageLaws.read(F32,values,position)) :
55 {Lanes.gather1(~Context,~map,position,context,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
56 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p1),(owner,b),StorageLaws.read(F32,values,p1)) :
57 {Lanes.gather2(~Context,~map,p1,context,a,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
58 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p2),(owner,c),StorageLaws.read(F32,values,p2)) :
59 {Lanes.gather3(~Context,~map,p2,context,a,b,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
60 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p3),(owner,d),StorageLaws.read(F32,values,p3)) :
61 {Lanes.gather4(~Context,~map,p3,context,a,b,c,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
62 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p4),(owner,e),StorageLaws.read(F32,values,p4)) :
63 {Lanes.gather5(~Context,~map,p4,context,a,b,c,d,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
64 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p5),(owner,f),StorageLaws.read(F32,values,p5)) :
65 {Lanes.gather6(~Context,~map,p5,context,a,b,c,d,e,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
66 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p6),(owner,g),StorageLaws.read(F32,values,p6)) :
67 {Lanes.gather7(~Context,~map,p6,context,a,b,c,d,e,f,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
68 %Equal.sym(Array<F32> & F32,Array.get(F32,owner,p7),(owner,h),StorageLaws.read(F32,values,p7)) :
69 {Lanes.gathered(~Context,~map,context,a,b,c,d,e,f,g,_) == (owner,cell(~Context,~map,values,position,context)) : Array<F32> & Tile.Tile8}
70 {==}
71
72
73def 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>:
74 +p1 = (position + 1 : U32)
75 +p2 = (p1 + 1 : U32)
76 +p3 = (p2 + 1 : U32)
77 +p4 = (p3 + 1 : U32)
78 +p5 = (p4 + 1 : U32)
79 +p6 = (p5 + 1 : U32)
80 +p7 = (p6 + 1 : U32)
81 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)
82
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)
115
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)))
128
129
130def round(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>,+start: Nat,+slot: U32,+context: Context,
131 +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(F32,values) == capacity : U32},+balanced: Shape.Balanced(F32,depth,values),
132 +limit: {Nat.is_le(depth,30n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
133 +room: {Nat.is_le(Nat.add(start,8n),U32.to_nat(capacity)) == True{} : Bool}) ->
134 {Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,
135 Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
136 Cells.State{Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n,U32.from_nat(start),context,values)),
137 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),
138 U32.and((slot + 1 : U32),63),context} : Cells.State<Array<F32>,Tile.Tile8,Context>}:
139 +position = U32.from_nat(start)
140 %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) :
141 {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}) ==
142 Cells.State{Tree.pack(F32,_),Tree.pack(Tile.Tile8,Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~map,values,position,context))),(position + 8 : U32),
143 U32.and((slot + 1 : U32),63),context} : Cells.State<Array<F32>,Tile.Tile8,Context>}
144 CellLaws.round(~F32,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,values,scratch,position,slot,context,
145 cell(~Context,~map,values,position,context),Batch.batch(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map),8n,position,context,values,values),
146 gathered(~Context,~map,values,position,context),cell_scattered(~Context,~map,values,position,context))
147
148
149def output(~Context: Data,+state: Batch.ModelState(~F32,~Context)) ->
150 {Traversal.mapped_output(~F32,~Context,ArrayLaws.represent_map(~F32,~Context,state)) == Tree.pack(F32,MapReadback.output(~F32,~Context,state)) : Array<F32>}:
151 Traversal.State{Unit{},output,position,context} = state
152 {==}
153
154def scalar(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree<F32>) ->
155 {Traversal.map_in_place(~F32,~Context,~map,count,position,context,Tree.pack(F32,values)) ==
156 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}:
157 +initial = {Traversal.State{Unit{},values,position,context} : Batch.ModelState(~F32,~Context)}
158 %Equal.sym(Traversal.State<&2,&1,Unit,Array<F32>,Context>,
159 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}),
160 ArrayLaws.represent_map(~F32,~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial)),
161 ArrayLaws.map_loop_refines_model(~F32,~Context,~map,count,initial)) :
162 {Traversal.mapped_output(~F32,~Context,_) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}
163 output(~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial))
164
165def few(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+slot: U32,+context: Context,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>) ->
166 {Lanes.finish(~Context,~map,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),position,slot,context}) ==
167 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}:
168 scalar(~Context,~map,count,position,context,values)
169
170
171def stepped(steps: Nat,start: Nat) -> U32:
172 match steps:
173 case 0n: U32.from_nat(start)
174 case 1n+rest: (stepped(rest,start) + 1 : U32)
175
176def advanced(+steps: Nat,+start: Nat) -> {stepped(steps,start) == U32.from_nat(Nat.add(steps,start)) : U32}:
177 match steps:
178 case 0n: {==}
179 case 1n+ +rest:
180 %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}
181 Bounds.add_one(U32.from_nat(Nat.add(rest,start)))
182
183def after_round(+start: Nat) -> {(U32.from_nat(start) + 8 : U32) == U32.from_nat(8n+start) : U32}:
184 %Order.commutative(start,8n) : {(U32.from_nat(start) + 8 : U32) == U32.from_nat(_) : U32}
185 WordArithmetic.native_add(start,8n)
186
187def round_room(+start: Nat,+rest: Nat,+capacity: Nat,room: {Nat.is_le(Nat.add(start,8n+rest),capacity) == True{} : Bool}) ->
188 {Nat.is_le(Nat.add(start,8n),capacity) == True{} : Bool}:
189 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)
190
191def rest_room(+start: Nat,+rest: Nat,+capacity: Nat,room: {Nat.is_le(Nat.add(start,8n+rest),capacity) == True{} : Bool}) ->
192 {Nat.is_le(Nat.add(8n+start,rest),capacity) == True{} : Bool}:
193 Order.advance_room(7n+start,rest,capacity,Order.advance_room(6n+start,1n+rest,capacity,Order.advance_room(5n+start,2n+rest,capacity,
194 Order.advance_room(4n+start,3n+rest,capacity,Order.advance_room(3n+start,4n+rest,capacity,Order.advance_room(2n+start,5n+rest,capacity,
195 Order.advance_room(1n+start,6n+rest,capacity,Order.advance_room(start,7n+rest,capacity,room))))))))
196
197
198
199def finish_small(~Owner: Type,~Context: Data,~gather: Owner -> U32 -> Context -> Owner & Tile.Tile8,
200 ~scatter: Owner -> U32 -> Tile.Tile8 -> Owner,~finish: Nat -> Cells.State<Owner,Tile.Tile8,Context> -> Owner,
201 +count: Nat,-state: Cells.State<Owner,Tile.Tile8,Context>,small: {Nat.is_lt(count,8n) == True{} : Bool}) ->
202 {Lanes.rounds_with(~Owner,~Context,~gather,~scatter,~finish,count,state) == finish(count,state) : Owner}:
203 match count:
204 case 0n: {==}
205 case 1n: {==}
206 case 2n: {==}
207 case 3n: {==}
208 case 4n: {==}
209 case 5n: {==}
210 case 6n: {==}
211 case 7n: {==}
212 case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
213 Empty.absurd({Lanes.rounds_with(~Owner,~Context,~gather,~scatter,~finish,8n+rest,state) == finish(8n+rest,state) : Owner},
214 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)))
215
216def by_rounds(~Property: Nat -> Type,
217 ~few: @+count: Nat -> {Nat.is_lt(count,8n) == True{} : Bool} -> Property(count),
218 ~more: @+rest: Nat -> Property(rest) -> Property(8n+rest),count: Nat) -> Property(count):
219 match count:
220 case 0n: few(0n,{==})
221 case 1n: few(1n,{==})
222 case 2n: few(2n,{==})
223 case 3n: few(3n,{==})
224 case 4n: few(4n,{==})
225 case 5n: few(5n,{==})
226 case 6n: few(6n,{==})
227 case 7n: few(7n,{==})
228 case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
229 more(rest,by_rounds(~Property,~few,~more,rest))
230
231
232def rounds_property(~Context: Data,~map: Context -> F32 -> F32,count: Nat) -> Type:
233 @+start: Nat -> @+slot: U32 -> @+context: Context -> @+values: Tree.Tree<F32> -> @+scratch: Tree.Tree<Tile.Tile8> ->
234 @+depth: Nat -> @+capacity: U32 -> @+capacity_equal: {Tree.capacity(F32,values) == capacity : U32} -> @+balanced: Shape.Balanced(F32,depth,values) ->
235 @+limit: {Nat.is_le(depth,30n) == True{} : Bool} -> @+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool} ->
236 @+room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool} ->
237 {Lanes.rounds(~Context,~map,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
238 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,U32.from_nat(start),context,values)) : Array<F32>}
239
240def few_rounds(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,small: {Nat.is_lt(count,8n) == True{} : Bool}) -> rounds_property(~Context,~map,count):
241 match count:
242 case 0n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
243 few(~Context,~map,0n,U32.from_nat(start),slot,context,values,scratch)
244 case 1n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
245 few(~Context,~map,1n,U32.from_nat(start),slot,context,values,scratch)
246 case 2n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
247 few(~Context,~map,2n,U32.from_nat(start),slot,context,values,scratch)
248 case 3n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
249 few(~Context,~map,3n,U32.from_nat(start),slot,context,values,scratch)
250 case 4n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
251 few(~Context,~map,4n,U32.from_nat(start),slot,context,values,scratch)
252 case 5n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
253 few(~Context,~map,5n,U32.from_nat(start),slot,context,values,scratch)
254 case 6n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
255 few(~Context,~map,6n,U32.from_nat(start),slot,context,values,scratch)
256 case 7n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
257 few(~Context,~map,7n,U32.from_nat(start),slot,context,values,scratch)
258 case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
259 start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
260 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}) ==
261 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,U32.from_nat(start),context,values)) : Array<F32>},
262 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)))
263
264def more_rounds(~Context: Data,~map: Context -> F32 -> F32,+rest: Nat,previous: rounds_property(~Context,~map,rest)) -> rounds_property(~Context,~map,8n+rest):
265 start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
266 +position = U32.from_nat(start)
267 +mapped = MapReadback.run(~F32,~Context,~map,8n,position,context,values)
268 +next = Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~map,values,position,context))
269 +turn = U32.and((slot + 1 : U32),63)
270 %Equal.sym(Cells.State<Array<F32>,Tile.Tile8,Context>,
271 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}),
272 Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),(position + 8 : U32),turn,context},
273 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))) :
274 {Lanes.rounds(~Context,~map,rest,_) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,position,context,values)) : Array<F32>}
275 %Equal.sym(U32,(position + 8 : U32),U32.from_nat(8n+start),after_round(start)) :
276 {Lanes.rounds(~Context,~map,rest,Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),_,turn,context}) ==
277 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,position,context,values)) : Array<F32>}
278 %Equal.sym(U32,stepped(8n,start),U32.from_nat(8n+start),advanced(8n,start)) :
279 {Lanes.rounds(~Context,~map,rest,Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),U32.from_nat(8n+start),turn,context}) ==
280 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,rest,_,context,mapped)) : Array<F32>}
281 previous(8n+start,turn,context,mapped,next,depth,capacity,
282 Equal.trans(U32,Tree.capacity(F32,mapped),Tree.capacity(F32,values),capacity,MapReadback.capacity(~F32,~Context,~map,8n,position,context,values),capacity_equal),
283 MapReadback.balanced(~F32,~Context,~map,8n,position,context,values,depth,balanced),limit,capacity_ok,rest_room(start,rest,U32.to_nat(capacity),room))
284
285def rounds(~Context: Data,~map: Context -> F32 -> F32,count: Nat,+start: Nat,+slot: U32,+context: Context,+values: Tree.Tree<F32>,+scratch: Tree.Tree<Tile.Tile8>,
286 +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(F32,values) == capacity : U32},+balanced: Shape.Balanced(F32,depth,values),
287 +limit: {Nat.is_le(depth,30n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
288 +room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool}) ->
289 {Lanes.rounds(~Context,~map,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
290 Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,U32.from_nat(start),context,values)) : Array<F32>}:
291 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)
292
293
294def 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),
295 +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}) ->
296 {Lanes.map(~Context,~map,count,U32.from_nat(start),context,Tree.pack(F32,values)) ==
297 Traversal.map_in_place(~F32,~Context,~map,count,U32.from_nat(start),context,Tree.pack(F32,values)) : Array<F32>}:
298 +position = U32.from_nat(start)
299 %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)),
300 scalar(~Context,~map,count,position,context,values)) :
301 {Lanes.map(~Context,~map,count,position,context,Tree.pack(F32,values)) == _ : Array<F32>}
302 %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))) :
303 {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>}
304 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,
305 Power.native_power_bound(depth,Order.successor(depth,30n,limit)),room)