proofs/traversal_batch_refinement.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as Traversal_batch_refinement

A batch writes the mapped values of consecutive positions after reading all of them from the original tree. Inside the tree it is the ordered in-place map of the same positions: no step of that map reads a position an earlier step wrote. For every element type and every batch length.

11 imports

import Base
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ./traversal_array_refinement.bend as ArrayLaws
import ./traversal_map_readback.bend as MapReadback
import ./storage_tree_model.bend as Tree
import ./storage_shape.bend as Shape
import ./nat_to_u32_bounds.bend as Bounds
import ./nat_order.bend as Order
import ./natural_addition.bend as Addition
import ./nat_interval.bend as Interval

Templates

template batch source · line 17 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @count:Nat -> @+position:U32 -> @+context:Context -> @+source:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @target:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>

template ModelState source · line 24 · raw

@-Element:Data -> @-Context:Data -> Data

template last_step source · line 28 · raw

@-State:Data -> @-step:(@_:State -> State) -> @+count:Nat -> @+state:State -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(State, step, 1n+count, state) == step(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(State, step, count, state)) : State}

A loop's last step, for every state and count.

template state_after source · line 35 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @+count:Nat -> @+start:Nat -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(ModelState(Element, Context), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_array_refinement.model_map_step(Element, Context, map), count, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State{Unit{}, input, U32.from_nat(start), context}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State{Unit{}, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run_indexed(Element, Context, map, count, U32.from_nat(start), context, input), U32.from_nat(Nat.add(start, count)), context} : ModelState(Element, Context)}

The whole state after count steps of the model map.

template extended source · line 55 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @+done:Nat -> @+start:Nat -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run_indexed(Element, Context, map, 1n+done, U32.from_nat(start), context, input) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run_indexed(Element, Context, map, done, U32.from_nat(start), context, input), U32.from_nat(Nat.add(start, done)), map(context, U32.from_nat(Nat.add(start, done)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run_indexed(Element, Context, map, done, U32.from_nat(start), context, input), U32.from_nat(Nat.add(start, done))))) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>}

One more step of the model map writes the position after the ones it mapped.

template continued source · line 75 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @+remaining:Nat -> @+done:Nat -> @+start:Nat -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+depth:Nat -> @+capacity:U32 -> @+capacity_equal:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, input) == capacity : U32} -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_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, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run_indexed(Element, Context, map, done, U32.from_nat(start), context, input)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run_indexed(Element, Context, map, Nat.add(done, remaining), U32.from_nat(start), context, input) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>}

A batch that continues done steps of the map completes the map.

template mapped source · line 117 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @+count:Nat -> @+start:Nat -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+depth:Nat -> @+capacity:U32 -> @+capacity_equal:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, input) == capacity : U32} -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_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(start, count), U32.to_nat(capacity)) == True{} : Bool} -> {batch(Element, Context, map, count, U32.from_nat(start), context, input, input) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run_indexed(Element, Context, map, count, U32.from_nat(start), context, input) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>}

A batch from the original tree is the map of its positions.