TraversalBatchRefinement.continued: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as TraversalBatchRefinement Lines 74-114 of stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&start_line=74&end_line=114 import Base 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_to_u32_bounds.bend as Bounds import stelliferous@0.0.2.0/proofs/nat_order.bend as Order import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition import stelliferous@0.0.2.0/proofs/nat_interval.bend as Interval # A batch that continues done steps of the map completes the map. def continued(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+remaining: Nat,+done: Nat,+start: Nat,+context: Context,+input: Tree.Tree, +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input), +limit: {Nat.is_le(depth,31n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool}, +room: {Nat.is_le(Nat.add(Nat.add(start,done),remaining),U32.to_nat(capacity)) == True{} : Bool}) -> {batch(~Element,~Context,~map,remaining,U32.from_nat(Nat.add(start,done)),context,input,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input)) == MapReadback.run_indexed(~Element,~Context,~map,Nat.add(done,remaining),U32.from_nat(start),context,input) : Tree.Tree}: match remaining: case 0n: %Equal.sym(Nat,Nat.add(done,0n),done,Addition.zero_right(done)) : {MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input) == MapReadback.run_indexed(~Element,~Context,~map,_,U32.from_nat(start),context,input) : Tree.Tree} {==} case 1n+ +rest: +reached = Nat.add(start,done) +query = U32.from_nat(reached) +mapped = MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input) +inside = Order.room_index(reached,rest,U32.to_nat(capacity),room) +within = Bounds.strict_le(reached,U32.to_nat(capacity),inside) +unread = MapReadback.outside_indexed(~Element,~Context,~map,done,start,query,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,within, MapReadback.address_inside(reached,capacity,capacity_ok,inside), Interval.After{ %Equal.sym(Nat,U32.to_nat(query),reached,Bounds.roundtrip(reached,capacity,capacity_ok,within)) : {Nat.is_le(reached,_) == True{} : Bool} Order.reflexive(reached)}) %Equal.sym(Nat,Nat.add(done,1n+rest),1n+Nat.add(done,rest),Addition.successor_right(done,rest)) : {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,Tree.write(Element,mapped,query,map(context,query,Tree.read(Element,input,query)))) == MapReadback.run_indexed(~Element,~Context,~map,_,U32.from_nat(start),context,input) : Tree.Tree} %unread : {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,Tree.write(Element,mapped,query,map(context,query,_))) == MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree} %extended(~Element,~Context,~map,done,start,context,input) : {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,_) == MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree} %Equal.sym(U32,(query + 1 : U32),U32.from_nat(1n+reached),Bounds.add_one(query)) : {batch(~Element,~Context,~map,rest,_,context,input,MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input)) == MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree} %Addition.successor_right(start,done) : {batch(~Element,~Context,~map,rest,U32.from_nat(_),context,input,MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input)) == MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree} continued(~Element,~Context,~map,rest,1n+done,start,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok, %Equal.sym(Nat,Nat.add(start,1n+done),1n+reached,Addition.successor_right(start,done)) : {Nat.is_le(Nat.add(_,rest),U32.to_nat(capacity)) == True{} : Bool} Order.advance_room(reached,rest,U32.to_nat(capacity),room)) Uses (29): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym 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.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/proofs/nat_interval.bend&name=Outside https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=advance_room https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=reflexive https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=room_index https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=add_one https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=roundtrip https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=strict_le https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=successor_right https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=zero_right 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=read 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_batch_refinement.bend&name=batch https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&name=extended https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=address_inside https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=outside_indexed https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=run_indexed