TraversalLanesRefinement.round: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement Lines 129-146 of stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&start_line=129&end_line=146 import Base import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes import stelliferous@0.0.2.0/traversal_cells.bend as Cells import stelliferous@0.0.2.0/kernel_tile.bend as Tile import stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend as CellLaws import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as Batch import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as ArrayLaws import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as MapReadback import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape import stelliferous@0.0.2.0/proofs/nat_order.bend as Order # One round maps eight positions. def round(~Context: Data,~map: Context -> F32 -> F32,+values: Tree.Tree,+scratch: Tree.Tree,+start: Nat,+slot: U32,+context: Context, +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(F32,values) == capacity : U32},+balanced: Shape.Balanced(F32,depth,values), +limit: {Nat.is_le(depth,30n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool}, +room: {Nat.is_le(Nat.add(start,8n),U32.to_nat(capacity)) == True{} : Bool}) -> {Cells.step(~Array,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8, Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) == Cells.State{Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n,U32.from_nat(start),context,values)), 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), U32.and((slot + 1 : U32),63),context} : Cells.State,Tile.Tile8,Context>}: +position = U32.from_nat(start) %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) : {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}) == Cells.State{Tree.pack(F32,_),Tree.pack(Tile.Tile8,Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~map,values,position,context))),(position + 8 : U32), U32.and((slot + 1 : U32),63),context} : Cells.State,Tile.Tile8,Context>} CellLaws.round(~F32,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,values,scratch,position,slot,context, cell(~Context,~map,values,position,context),Batch.batch(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map),8n,position,context,values,values), gathered(~Context,~map,values,position,context),cell_scattered(~Context,~map,values,position,context)) Uses (31): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=successor https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=capacity https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=write https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=unindexed https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&name=batch https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&name=mapped https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=round https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=cell https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=cell_scattered https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=gathered https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=run https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=State https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=step https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=scatter