proofs/traversal_map_readback.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as Traversal_map_readback

Pointwise semantics of the actual ordered in-place map traversal. A bounded cursor visits each address once, so later stores preserve earlier results.

14 imports

import Base
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ./traversal_array_refinement.bend as ArrayLaws
import ./storage_tree_model.bend as Tree
import ./storage_shape.bend as Shape
import ./storage_readback.bend as StorageReadback
import ./nat_to_u32_bounds.bend as Bounds
import ./nat_order.bend as Order
import ./natural_addition.bend as Addition
import ./u32_comparison.bend as Comparison
import ./nat_interval.bend as Interval
import ./nat_division.bend as Division
import ./word_encoding.bend as WordEncoding

Definitions

def address_inside source · line 44 · raw

@+position:Nat -> @+capacity:U32 -> @+capacity_ok:{U32.is_le(capacity, 2147483648) == True{} : Bool} -> @+inside:{Nat.is_lt(position, U32.to_nat(capacity)) == True{} : Bool} -> {U32.is_lt(U32.from_nat(position), capacity) == True{} : Bool}

Templates

template output source · line 18 · raw

@-Element:Data -> @-Context:Data -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Unit, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>

template run_indexed source · line 22 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @count:Nat -> @position:U32 -> @context:Context -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>

template capacity_indexed source · line 26 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @count:Nat -> @+position:U32 -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, run_indexed(Element, Context, operation, count, position, context, input)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, input) : U32}

template balanced_indexed source · line 36 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @count:Nat -> @+position:U32 -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+depth:Nat -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, run_indexed(Element, Context, operation, count, position, context, input))

template unchanged_full source · line 48 · raw

@-Element:Data -> @+depth:Nat -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+position:U32 -> @+query:U32 -> @+value:Element -> @+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} -> @position_inside:{U32.is_lt(position, capacity) == True{} : Bool} -> @query_inside:{U32.is_lt(query, capacity) == True{} : Bool} -> @different:{U32.is_eq(position, query) == False{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, input, position, value), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, input, query) : Element}

template outside_indexed source · line 56 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @count:Nat -> @+position:Nat -> @+query:U32 -> @+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(position, count), U32.to_nat(capacity)) == True{} : Bool} -> @+query_inside:{U32.is_lt(query, capacity) == True{} : Bool} -> @+separate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/nat_interval.Outside<position, count, U32.to_nat(query)> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, run_indexed(Element, Context, operation, count, U32.from_nat(position), context, input), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, input, query) : Element}

template inside_indexed source · line 82 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:U32 -> @_:Element -> Element) -> @count:Nat -> @+position:Nat -> @index: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(position, count), U32.to_nat(capacity)) == True{} : Bool} -> @+selected:{Nat.is_lt(index, count) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, run_indexed(Element, Context, operation, count, U32.from_nat(position), context, input), U32.from_nat(Nat.add(position, index))) == operation(context, U32.from_nat(Nat.add(position, index)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, input, U32.from_nat(Nat.add(position, index)))) : Element}

template run source · line 132 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:Element -> Element) -> @count:Nat -> @position:U32 -> @context:Context -> @input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>

Unary maps use the same indexed induction with an unused position.

template capacity source · line 135 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:Element -> Element) -> @count:Nat -> @+position:U32 -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, run(Element, Context, operation, count, position, context, input)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, input) : U32}

template balanced source · line 139 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:Element -> Element) -> @count:Nat -> @+position:U32 -> @+context:Context -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+depth:Nat -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, input) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, run(Element, Context, operation, count, position, context, input))

template outside source · line 143 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:Element -> Element) -> @count:Nat -> @+position:Nat -> @+query:U32 -> @+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, 30n) == True{} : Bool} -> @+capacity_ok:{U32.is_le(capacity, 2147483648) == True{} : Bool} -> @+room:{Nat.is_le(Nat.add(position, count), U32.to_nat(capacity)) == True{} : Bool} -> @+query_inside:{U32.is_lt(query, capacity) == True{} : Bool} -> @+separate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/nat_interval.Outside<position, count, U32.to_nat(query)> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, run(Element, Context, operation, count, U32.from_nat(position), context, input), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, input, query) : Element}

template inside source · line 150 · raw

@-Element:Data -> @-Context:Data -> @-operation:(@_:Context -> @_:Element -> Element) -> @count:Nat -> @+position:Nat -> @index: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, 30n) == True{} : Bool} -> @+capacity_ok:{U32.is_le(capacity, 2147483648) == True{} : Bool} -> @+room:{Nat.is_le(Nat.add(position, count), U32.to_nat(capacity)) == True{} : Bool} -> @+selected:{Nat.is_lt(index, count) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, run(Element, Context, operation, count, U32.from_nat(position), context, input), U32.from_nat(Nat.add(position, index))) == operation(context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, input, U32.from_nat(Nat.add(position, index)))) : Element}

template unchanged source · line 158 · raw

@-Element:Data -> @+depth:Nat -> @+input:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+position:U32 -> @+query:U32 -> @+value:Element -> @+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, 30n) == True{} : Bool} -> @position_inside:{U32.is_lt(position, capacity) == True{} : Bool} -> @query_inside:{U32.is_lt(query, capacity) == True{} : Bool} -> @different:{U32.is_eq(position, query) == False{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, input, position, value), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, input, query) : Element}