TraversalLanesRefinement.more_rounds: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement Lines 264-283 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=264&end_line=283 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_map_readback.bend as MapReadback import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree def more_rounds(~Context: Data,~map: Context -> F32 -> F32,+rest: Nat,previous: rounds_property(~Context,~map,rest)) -> rounds_property(~Context,~map,8n+rest): start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room => +position = U32.from_nat(start) +mapped = MapReadback.run(~F32,~Context,~map,8n,position,context,values) +next = Tree.write(Tile.Tile8,scratch,slot,cell(~Context,~map,values,position,context)) +turn = U32.and((slot + 1 : U32),63) %Equal.sym(Cells.State,Tile.Tile8,Context>, 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,mapped),Tree.pack(Tile.Tile8,next),(position + 8 : U32),turn,context}, 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))) : {Lanes.rounds(~Context,~map,rest,_) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,position,context,values)) : Array} %Equal.sym(U32,(position + 8 : U32),U32.from_nat(8n+start),after_round(start)) : {Lanes.rounds(~Context,~map,rest,Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),_,turn,context}) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,position,context,values)) : Array} %Equal.sym(U32,stepped(8n,start),U32.from_nat(8n+start),advanced(8n,start)) : {Lanes.rounds(~Context,~map,rest,Cells.State{Tree.pack(F32,mapped),Tree.pack(Tile.Tile8,next),U32.from_nat(8n+start),turn,context}) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,rest,_,context,mapped)) : Array} previous(8n+start,turn,context,mapped,next,depth,capacity, Equal.trans(U32,Tree.capacity(F32,mapped),Tree.capacity(F32,values),capacity,MapReadback.capacity(~F32,~Context,~map,8n,position,context,values),capacity_equal), MapReadback.balanced(~F32,~Context,~map,8n,position,context,values,depth,balanced),limit,capacity_ok,rest_room(start,rest,U32.to_nat(capacity),room)) Uses (30): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans 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=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.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/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_lanes_refinement.bend&name=advanced https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=after_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=rest_room https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=round https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=round_room https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=rounds_property https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=stepped https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=balanced https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=capacity 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=rounds https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=scatter