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. 4 import Base 5 import ../traversal_lanes.bend as Lanes 6 import ../traversal_cells.bend as Cells 7 import ../traversal_array.bend as Traversal 8 import ../traversal_loop.bend as Loop 9 import ../kernel_tile.bend as Tile 10 import ./traversal_cells_refinement.bend as CellLaws 11 import ./traversal_batch_refinement.bend as Batch 12 import ./traversal_array_refinement.bend as ArrayLaws 13 import ./traversal_map_readback.bend as MapReadback 14 import ./storage_tree_model.bend as Tree 15 import ./storage_refinement.bend as StorageLaws 16 import ./storage_shape.bend as Shape 17 import ./nat_to_u32_bounds.bend as Bounds 18 import ./nat_order.bend as Order 19 import ./nat_division.bend as Division 20 import ./word_encoding.bend as WordEncoding 21 import ./word_arithmetic.bend as WordArithmetic 22 import ./word_power_of_two.bend as Power 23 24 # The tile a round gathers at position. 25 def cell(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+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 36 def gathered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+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 & 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,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 & Tile.Tile8} 56 %Equal.sym(Array & 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 & Tile.Tile8} 58 %Equal.sym(Array & 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 & Tile.Tile8} 60 %Equal.sym(Array & 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 & Tile.Tile8} 62 %Equal.sym(Array & 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 & Tile.Tile8} 64 %Equal.sym(Array & 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 & Tile.Tile8} 66 %Equal.sym(Array & 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 & Tile.Tile8} 68 %Equal.sym(Array & 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 & Tile.Tile8} 70 {==} 71 72 # Eight ordered writes from position. 73 def written(+values: Tree.Tree,+position: U32,a: F32,b: F32,c: F32,d: F32,e: F32,f: F32,g: F32,h: F32) -> Tree.Tree: 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 83 def scattered(+values: Tree.Tree,+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}: 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,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} 102 %Equal.sym(Array,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} 104 %Equal.sym(Array,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} 106 %Equal.sym(Array,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} 108 %Equal.sym(Array,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} 110 %Equal.sym(Array,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} 112 %Equal.sym(Array,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} 114 StorageLaws.write(F32,w7,p7,h) 115 116 def cell_scattered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+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}: 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 # One round maps eight positions. 130 def round(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+scratch: Tree.Tree,+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,~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,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,~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,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 # The scalar map from any position, on a packed tree. 149 def 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}: 151 Traversal.State{Unit{},output,position,context} = state 152 {==} 153 154 def scalar(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree) -> 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}: 157 +initial = {Traversal.State{Unit{},values,position,context} : Batch.ModelState(~F32,~Context)} 158 %Equal.sym(Traversal.State<&2,&1,Unit,Array,Context>, 159 Loop.run(~Traversal.State<&2,&1,Unit,Array,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} 163 output(~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial)) 164 165 def few(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+slot: U32,+context: Context,+values: Tree.Tree,+scratch: Tree.Tree) -> 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}: 168 scalar(~Context,~map,count,position,context,values) 169 170 # The position of the model map after k steps from start. 171 def 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 176 def 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 183 def 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 187 def 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 191 def 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 # The shared induction on eight-value rounds. The proposition may carry all 198 # owners and bounds, so binary and ternary instances need only local cases. 199 def 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, 201 +count: Nat,-state: Cells.State,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 216 def 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 # Every count: whole rounds, then the last positions one by one. 232 def rounds_property(~Context: Data,~map: Context -> F32 -> F32,count: Nat) -> Type: 233 @+start: Nat -> @+slot: U32 -> @+context: Context -> @+values: Tree.Tree -> @+scratch: Tree.Tree -> 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} 239 240 def 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}, 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 264 def 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,Tile.Tile8,Context>, 271 Cells.step(~Array,~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} 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} 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} 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 285 def rounds(~Context: Data,~map: Context -> F32 -> F32,count: Nat,+start: Nat,+slot: U32,+context: Context,+values: Tree.Tree,+scratch: Tree.Tree, 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}: 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 # The whole map from any position, with a fresh scratch array. 294 def map(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+start: Nat,+context: Context,+values: Tree.Tree,+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}: 298 +position = U32.from_nat(start) 299 %Equal.sym(Array,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} 302 %Equal.sym(Array,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} 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)