~/bend-docscommunity

proofs/traversal_array_refinement.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as Traversal_array_refinement

The same ownership-parameterized state is used by implementation and model. One read contract and one generic Array.set refinement cover every traversal.

10 imports
import Base
import ../kernel_block.bend as Block
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ./storage_tree_model.bend as Tree
import ./storage_refinement.bend as StorageLaws
import ./loop_projection.bend as Projection
import ./natural_addition.bend as Addition
import ./nat_to_u32_bounds.bend as Bounds
import ./nat_order.bend as Order

Templates

template represent source · line 14 · raw

@-Reader:Type -> @-Model:Data -> @-Element:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context>

template model_step source · line 19 · raw

@-Model:Data -> @-Element:Data -> @-Context:Data -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Element) -> @-destination:(@_:Context -> @_:U32 -> U32) -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context>

template step_refines_model source · line 25 · raw

@-Reader:Type -> @-Model:Data -> @-Element:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Element)) -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Element) -> @-destination:(@_:Context -> @_:U32 -> U32) -> @-read_matches:(@+reader:Model -> @+context:Context -> @+position:U32 -> {read(pack_reader(reader), context, position) == (pack_reader(reader), sample(reader, context, position)) : Pair(Reader, Element)}) -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.step(Reader, Element, Context, read, destination, represent(Reader, Model, Element, Context, pack_reader, state)) == represent(Reader, Model, Element, Context, pack_reader, model_step(Model, Element, Context, sample, destination, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context>}

template traversal_refines_model source · line 47 · raw

@-Reader:Type -> @-Model:Data -> @-Element:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Element)) -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Element) -> @-destination:(@_:Context -> @_:U32 -> U32) -> @-read_matches:(@+reader:Model -> @+context:Context -> @+position:U32 -> {read(pack_reader(reader), context, position) == (pack_reader(reader), sample(reader, context, position)) : Pair(Reader, Element)}) -> @+count:Nat -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.run(Reader, Element, Context, read, destination, count, represent(Reader, Model, Element, Context, pack_reader, state)) == represent(Reader, Model, Element, Context, pack_reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context>, model_step(Model, Element, Context, sample, destination), count, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context>}

template pack_tree source · line 62 · raw

@-Element:Data -> @tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> Array<Element>

template sample_offset source · line 65 · raw

@-Element:Data -> @tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets -> @position:U32 -> Element

template offset_read_refines_storage source · line 69 · raw

@-Element:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+context:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets -> @+position:U32 -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.source_offset(Element, pack_tree(Element, tree), context, position) == (pack_tree(Element, tree), sample_offset(Element, tree, context, position)) : Pair(Array<Element>, Element)}

template copy_traversal_refines_storage source · line 75 · raw

@-Element:Data -> @+count:Nat -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.run(Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.source_offset(Element), 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.destination_offset, count, represent(Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets, pack_tree(Element), state)) == represent(Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets, pack_tree(Element), 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets>, model_step(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets, sample_offset(Element), 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.destination_offset), count, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets>}

template represent_fold source · line 88 · raw

@-Reader:Type -> @-Model:Data -> @-Accumulator:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, Accumulator, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context>

The accumulator is an observation, independent of its numeric interpretation. In particular this theorem never rewrites or reassociates a floating sum.

template model_fold_step source · line 93 · raw

@-Model:Data -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Element) -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, Accumulator, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, Accumulator, Context>

template fold_step_refines_model source · line 99 · raw

@-Reader:Type -> @-Model:Data -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Element)) -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Element) -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @-read_matches:(@+reader:Model -> @+context:Context -> @+position:U32 -> {read(pack_reader(reader), context, position) == (pack_reader(reader), sample(reader, context, position)) : Pair(Reader, Element)}) -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, Accumulator, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.fold_step(Reader, Element, Accumulator, Context, read, combine, represent_fold(Reader, Model, Accumulator, Context, pack_reader, state)) == represent_fold(Reader, Model, Accumulator, Context, pack_reader, model_fold_step(Model, Element, Accumulator, Context, sample, combine, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context>}

template fold_refines_ordered_model source · line 118 · raw

@-Reader:Type -> @-Model:Data -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Element)) -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Element) -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @-read_matches:(@+reader:Model -> @+context:Context -> @+position:U32 -> {read(pack_reader(reader), context, position) == (pack_reader(reader), sample(reader, context, position)) : Pair(Reader, Element)}) -> @+count:Nat -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, Accumulator, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context>, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.fold_step(Reader, Element, Accumulator, Context, read, combine), count, represent_fold(Reader, Model, Accumulator, Context, pack_reader, state)) == represent_fold(Reader, Model, Accumulator, Context, pack_reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, Accumulator, Context>, model_fold_step(Model, Element, Accumulator, Context, sample, combine), count, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context>}

template represent_map source · line 135 · raw

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

In-place transforms retain one owner and use the same generic loop lifting.

template unindexed source · line 140 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @context:Context -> @position:U32 -> @value:Element -> Element

template model_map_step source · line 143 · raw

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

template map_step_refines_model source · line 149 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Unit, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_step(Element, Context, map, represent_map(Element, Context, state)) == represent_map(Element, Context, model_map_step(Element, Context, unindexed(Element, Context, map), state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context>}

template map_loop_refines_model source · line 165 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @+count:Nat -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Unit, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context>, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_step(Element, Context, map), count, represent_map(Element, Context, state)) == represent_map(Element, Context, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Unit, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context>, model_map_step(Element, Context, unindexed(Element, Context, map)), count, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context>}

template model_update_step source · line 181 · raw

@-Model:Data -> @-Element:Data -> @-Sample:Data -> @-Context:Data -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Sample) -> @-combine:(@_:Element -> @_:Sample -> Element) -> @-destination:(@_:Context -> @_:U32 -> U32) -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context>

In-place binary updates use the current destination value in left position. This theorem models sequential writes, including modular/overlapping raw addresses. Valid view guards and non-overlap are separate obligations.

template update_step_refines_model source · line 188 · raw

@-Reader:Type -> @-Model:Data -> @-Element:Data -> @-Sample:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Sample)) -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Sample) -> @-combine:(@_:Element -> @_:Sample -> Element) -> @-destination:(@_:Context -> @_:U32 -> U32) -> @-read_matches:(@+reader:Model -> @+context:Context -> @+position:U32 -> {read(pack_reader(reader), context, position) == (pack_reader(reader), sample(reader, context, position)) : Pair(Reader, Sample)}) -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.update_step(Reader, Element, Sample, Context, read, combine, destination, represent(Reader, Model, Element, Context, pack_reader, state)) == represent(Reader, Model, Element, Context, pack_reader, model_update_step(Model, Element, Sample, Context, sample, combine, destination, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context>}

template update_refines_model source · line 219 · raw

@-Reader:Type -> @-Model:Data -> @-Element:Data -> @-Sample:Data -> @-Context:Data -> @-pack_reader:(@_:Model -> Reader) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Sample)) -> @-sample:(@_:Model -> @_:Context -> @_:U32 -> Sample) -> @-combine:(@_:Element -> @_:Sample -> Element) -> @-destination:(@_:Context -> @_:U32 -> U32) -> @-read_matches:(@+reader:Model -> @+context:Context -> @+position:U32 -> {read(pack_reader(reader), context, position) == (pack_reader(reader), sample(reader, context, position)) : Pair(Reader, Sample)}) -> @+count:Nat -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.update(Reader, Element, Sample, Context, read, combine, destination, count, represent(Reader, Model, Element, Context, pack_reader, state)) == represent(Reader, Model, Element, Context, pack_reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &2, Model, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, Context>, model_update_step(Model, Element, Sample, Context, sample, combine, destination), count, state)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context>}

template indexed_fold_refines_model source · line 237 · raw

@-Runtime:Type -> @-Model:Data -> @-Context:Data -> @-update:(@_:U32 -> @_:Context -> @_:Runtime -> Runtime) -> @-model_update:(@_:U32 -> @_:Context -> @_:Model -> Model) -> @-represent:(@_:Model -> Runtime) -> @-step_matches:(@+index:U32 -> @+context:Context -> @+state:Model -> {update(index, context, represent(state)) == represent(model_update(index, context, state)) : Runtime}) -> @+count:Nat -> @+index:U32 -> @+context:Context -> @+state:Model -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(Runtime, Context, update, count, index, context, represent(state)) == represent(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(Model, Context, model_update, count, index, context, state)) : Runtime}

template indexed_fold_change_context source · line 257 · raw

@-State:Data -> @-Outer:Data -> @-Inner:Data -> @-project:(@_:Outer -> Inner) -> @-outer_step:(@_:U32 -> @_:Outer -> @_:State -> State) -> @-inner_step:(@_:U32 -> @_:Inner -> @_:State -> State) -> @-same_step:(@+index:U32 -> @+context:Outer -> @+state:State -> {outer_step(index, context, state) == inner_step(index, project(context), state) : State}) -> @+count:Nat -> @+first:U32 -> @+context:Outer -> @+state:State -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(State, Outer, outer_step, count, first, context, state) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(State, Inner, inner_step, count, first, project(context), state) : State}

One bounded induction carries capacity, preserved sources and completed output values together. A strategy proves its local update obligation; it does not reimplement the whole output traversal proof.

template indexed_fold_preserves_invariant source · line 273 · raw

@-State:Data -> @-Context:Data -> @-limit:(@_:Context -> Nat) -> @-Invariant:(@_:Context -> @_:Nat -> @_:State -> Data) -> @-update:(@_:U32 -> @_:Context -> @_:State -> State) -> @-preserve:(@+context:Context -> @+index:Nat -> @+state:State -> @_:{Nat.is_lt(index, limit(context)) == True{} : Bool} -> @_:Invariant(context, index, state) -> Invariant(context, 1n+index, update(U32.from_nat(index), context, state))) -> @+count:Nat -> @+first:Nat -> @+context:Context -> @+state:State -> @+room:{Nat.is_le(Nat.add(first, count), limit(context)) == True{} : Bool} -> @evidence:Invariant(context, first, state) -> Invariant(context, Nat.add(first, count), 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(State, Context, update, count, U32.from_nat(first), context, state))

template indexed_fold_split source · line 297 · raw

@-Value:Type -> @-Context:Data -> @-update:(@_:U32 -> @_:Context -> @_:Value -> Value) -> @+first:Nat -> @+second:Nat -> @+start:Nat -> @+context:Context -> @-initial:Value -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(Value, Context, update, Nat.add(first, second), U32.from_nat(start), context, initial) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(Value, Context, update, second, U32.from_nat(Nat.add(start, first)), context, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(Value, Context, update, first, U32.from_nat(start), context, initial)) : Value}

Splitting a traversal preserves every state update in the same order. The boundary uses modular U32 conversion; no scalar/FP32-specific induction.