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 import ./kernel_tile_refinement.bend as TileLaws 24 import ./loop_projection.bend as Projection 25 import ./bounded_u32_arithmetic.bend as Arithmetic 26 27 def 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 31 def cell(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+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 42 def 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 47 def 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 53 def identity_cell_at(+lane: Nat,+values: Tree.Tree,+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 68 def identity_cell_indexed(+lane: Nat,+values: Tree.Tree,+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 73 def identity_cell_equal(+left: Tree.Tree,+right: Tree.Tree,+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 85 def gathered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+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 & 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,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 & Tile.Tile8} 105 %Equal.sym(Array & 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 & Tile.Tile8} 107 %Equal.sym(Array & 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 & Tile.Tile8} 109 %Equal.sym(Array & 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 & Tile.Tile8} 111 %Equal.sym(Array & 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 & Tile.Tile8} 113 %Equal.sym(Array & 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 & Tile.Tile8} 115 %Equal.sym(Array & 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 & Tile.Tile8} 117 %Equal.sym(Array & 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 & Tile.Tile8} 119 {==} 120 121 # Eight ordered writes from position. 122 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: 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 132 def scattered(+values: Tree.Tree,+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}: 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,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} 151 %Equal.sym(Array,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} 153 %Equal.sym(Array,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} 155 %Equal.sym(Array,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} 157 %Equal.sym(Array,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} 159 %Equal.sym(Array,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} 161 %Equal.sym(Array,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} 163 StorageLaws.write(F32,w7,p7,h) 164 165 def cell_scattered(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+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}: 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. 179 def round(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+scratch: Tree.Tree,+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,~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,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,~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,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. 198 def 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}: 200 Traversal.State{Unit{},output,position,context} = state 201 {==} 202 203 def scalar(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree) -> 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}: 206 +initial = {Traversal.State{Unit{},values,position,context} : Batch.ModelState(~F32,~Context)} 207 %Equal.sym(Traversal.State<&2,&1,Unit,Array,Context>, 208 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}), 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} 212 output(~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial)) 213 214 def few(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+slot: U32,+context: Context,+values: Tree.Tree,+scratch: Tree.Tree) -> 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}: 217 scalar(~Context,~map,count,position,context,values) 218 219 # The position of the model map after k steps from start. 220 def 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 225 def 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 232 def 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 236 def 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 240 def 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. 248 def 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, 250 +count: Nat,-state: Cells.State,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 265 def 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. 281 def rounds_property(~Context: Data,~map: Context -> F32 -> F32,count: Nat) -> Type: 282 @+start: Nat -> @+slot: U32 -> @+context: Context -> @+values: Tree.Tree -> @+scratch: Tree.Tree -> 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} 288 289 def 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}, 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 313 def 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,Tile.Tile8,Context>, 320 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}), 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} 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} 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} 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 334 def rounds(~Context: Data,~map: Context -> F32 -> F32,count: Nat,+start: Nat,+slot: U32,+context: Context,+values: Tree.Tree,+scratch: Tree.Tree, 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}: 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. 343 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), 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}: 347 +position = U32.from_nat(start) 348 %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)), 349 scalar(~Context,~map,count,position,context,values)) : 350 {Lanes.map(~Context,~map,count,position,context,Tree.pack(F32,values)) == _ : Array} 351 %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))) : 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} 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. 357 def GatherRoundLaw(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & Tile.Tile8) -> Type: 358 @+context: Context -> @+a: F32 -> @+b: F32 -> @+c: F32 -> @+d: F32 -> @+e: F32 -> @+f: F32 -> @+g: F32 -> @read: Array & 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 & Tile.Tile8} 360 361 def transform7(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & 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) -> 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 & Tile.Tile8}: 363 (values,g) = read 364 lawful(context,a,b,c,d,e,f,g,Array.get(F32,values,(position + 1 : U32))) 365 366 def transform6(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & 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) -> 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 & 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 371 def transform5(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,+c: F32,+d: F32,read: Array & 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 & 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 376 def transform4(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,+c: F32,read: Array & 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 & 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 381 def transform3(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,+b: F32,read: Array & F32) -> 382 {after(context,Lanes.gather3(~Context,~initial,position,context,a,b,read)) == Lanes.gather3(~Context,~operation,position,context,a,b,read) : Array & 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 386 def transform2(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,+a: F32,read: Array & F32) -> 387 {after(context,Lanes.gather2(~Context,~initial,position,context,a,read)) == Lanes.gather2(~Context,~operation,position,context,a,read) : Array & 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 391 def transform1(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),+position: U32,+context: Context,read: Array & F32) -> 392 {after(context,Lanes.gather1(~Context,~initial,position,context,read)) == Lanes.gather1(~Context,~operation,position,context,read) : Array & 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 396 def gather_transform(~Context: Data,~initial: Context -> F32 -> F32,~operation: Context -> F32 -> F32,~after: Context -> (Array & Tile.Tile8) -> Array & Tile.Tile8,~lawful: GatherRoundLaw(~Context,~initial,~operation,~after),values: Array,+position: U32,+context: Context) -> 397 {after(context,Lanes.gather(~Context,~initial,values,position,context)) == Lanes.gather(~Context,~operation,values,position,context) : Array & 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. 401 def GatherLaw(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8) -> Type: 402 @values: Array -> @+position: U32 -> @+context: Context -> 403 {collect(values,position,context) == Lanes.gather(~Context,~operation,values,position,context) : Array & Tile.Tile8} 404 405 def collected_values(~Context: Data,~operation: Context -> F32 -> F32,+values: Tree.Tree,+position: U32,+context: Context) -> Tree.Tree: 406 Batch.batch(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~operation),8n,position,context,values,values) 407 408 def collected_state(~Context: Data,~operation: Context -> F32 -> F32,+values: Tree.Tree,+scratch: Tree.Tree,+position: U32,+slot: U32,+context: Context) -> Cells.State,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 413 def collected_step(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,+values: Tree.Tree,+scratch: Tree.Tree,+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 & Tile.Tile8}) -> 415 {Cells.step(~Array,~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,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 419 def WithProperty(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,count: Nat) -> Type: 420 @+values: Tree.Tree -> @+scratch: Tree.Tree -> @+position: U32 -> @+slot: U32 -> @+context: Context -> 421 {Lanes.rounds_with(~Array,~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} 423 424 def with_few(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & 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, 428 Lanes.rounds_with(~Array,~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,~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,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,~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 436 def with_more(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & 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,Tile.Tile8,Context>, 439 Cells.step(~Array,~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 & 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,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),rest,_) == 444 Lanes.rounds(~Context,~operation,rest,Cells.step(~Array,~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} 445 %Equal.sym(Cells.State,Tile.Tile8,Context>, 446 Cells.step(~Array,~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,~Context,~collect,~Lanes.scatter,~Lanes.finish(~Context,~operation),rest,collected_state(~Context,~operation,values,scratch,position,slot,context)) == Lanes.rounds(~Context,~operation,rest,_) : Array} 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 451 def with_rounds(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & 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 454 def with_packed(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,+values: Tree.Tree) -> 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}: 456 %StorageLaws.fresh(Tile.Tile8,6n,Tile.filled(0.0)) : 457 {Lanes.rounds_with(~Array,~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} 459 with_rounds(~Context,~operation,~collect,~lawful,count)(values,Tree.fresh(Tile.Tile8,6n,Tile.filled(0.0)),position,0,context) 460 461 def with_observed(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,-values: Array,observation: StorageLaws.Observation) -> 462 {Lanes.map_with(~Context,~operation,~collect,count,position,context,values) == Lanes.map(~Context,~operation,count,position,context,values) : Array}: 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} 465 with_packed(~Context,~operation,~collect,~lawful,count,position,context,tree) 466 467 def map_with(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,values: Array) -> 468 {Lanes.map_with(~Context,~operation,~collect,count,position,context,values) == Lanes.map(~Context,~operation,count,position,context,values) : Array}: 469 with_observed(~Context,~operation,~collect,~lawful,count,position,context,values,StorageLaws.observe(F32,values)) 470 471 def map_with_when(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,~lawful: GatherLaw(~Context,~operation,~collect),+covered: Bool,+count: Nat,+position: U32,+context: Context,values: Array) -> 472 {Lanes.map_with_when(~Context,~operation,~collect,covered,count,position,context,values) == Lanes.map_when(~Context,~operation,covered,count,position,context,values) : Array}: 473 match covered: 474 case False{}: {==} 475 case True{}: map_with(~Context,~operation,~collect,~lawful,count,position,context,values) 476 477 def 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 481 def 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) -> 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 & Tile.Tile8}: 483 (values,h) = read 484 Equal.cong(Tile.Tile8,Array & 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 487 def gather_tiles(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8,~lawful: TileLaw(~Context,~operation,~transform),values: Array,+position: U32,+context: Context) -> 488 {Lanes.gather_transformed(~Context,~transform,values,position,context) == Lanes.gather(~Context,~operation,values,position,context) : Array & Tile.Tile8}: 489 gather_transform(~Context,~Lanes.identity(~Context),~operation,~Lanes.transformed(~Context,~transform),~transformed_round(~Context,~operation,~transform,~lawful),values,position,context)