~/bend-docscommunity

proofs/loop_projection.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/loop_projection.bend as Loop_projection

One induction for every state representation, output index and step count.

4 imports
import Base
import ./bounded_u32_arithmetic.bend as Arithmetic
import ./word_arithmetic.bend as WordArithmetic
import ../traversal_loop.bend as Loop

Types

type Measured source · line 54 · raw

@-State:Data -> Data

Definitions

def add_work source · line 57 · raw

@-State:Data -> @work:Nat -> @tail:Measured<State> -> Measured<State>

def indexed_successor source · line 86 · raw

@+position:U32 -> @+offset:Nat -> {U32.add(position, U32.from_nat(1n+offset)) == U32.add(U32.add(position, 1), U32.from_nat(offset)) : U32}

def add_counted_stride source · line 92 · raw

@+position:U32 -> @+stride:Nat -> @+count:Nat -> {U32.add(U32.add(position, U32.from_nat(stride)), U32.from_nat(Nat.mul(count, stride))) == U32.add(position, U32.from_nat(Nat.mul(1n+count, stride))) : U32}

Templates

template iterate source · line 7 · raw

@-State:Data -> @-step:(@_:State -> State) -> @count:Nat -> @state:State -> State

template iteration_refines_model source · line 12 · raw

@-RuntimeState:Type -> @-ModelState:Data -> @-runtime_step:(@_:RuntimeState -> RuntimeState) -> @-model_step:(@_:ModelState -> ModelState) -> @-represent:(@_:ModelState -> RuntimeState) -> @-step_matches:(@+state:ModelState -> {runtime_step(represent(state)) == represent(model_step(state)) : RuntimeState}) -> @+count:Nat -> @+state:ModelState -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(RuntimeState, runtime_step, count, represent(state)) == represent(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(ModelState, model_step, count, state)) : RuntimeState}

A single commuting step lifts to every count. RuntimeState may own arrays; only the model is duplicated in the proof. No runtime array is cloned.

template preserves_observation source · line 27 · raw

@-State:Data -> @-Observation:Data -> @-step:(@_:State -> State) -> @-observe:(@_:State -> Observation) -> @-preserved:(@+state:State -> {observe(step(state)) == observe(state) : Observation}) -> @+count:Nat -> @+state:State -> {observe(iterate(State, step, count, state)) == observe(state) : Observation}

A read-only observation is preserved for every number of iterations.

template iteration_matches_denotation source · line 38 · raw

@-Observation:Data -> @-State:Data -> @-Index:Data -> @-step:(@_:State -> State) -> @-project:(@_:Index -> @_:State -> Observation) -> @-denote:(@_:Index -> @_:Nat -> @_:State -> Observation) -> @-at_zero:(@+index:Index -> @+state:State -> {project(index, state) == denote(index, 0n, state) : Observation}) -> @-after_step:(@+index:Index -> @+count:Nat -> @+state:State -> {denote(index, count, step(state)) == denote(index, 1n+count, state) : Observation}) -> @+count:Nat -> @+index:Index -> @+state:State -> {project(index, iterate(State, step, count, state)) == denote(index, count, state) : Observation}

template measured_iteration source · line 61 · raw

@-State:Data -> @-step:(@_:State -> State) -> @-cost:(@_:State -> Nat) -> @count:Nat -> @+state:State -> Measured<State>

template iteration_result_and_work source · line 68 · raw

@-State:Data -> @-step:(@_:State -> State) -> @-cost:(@_:State -> Nat) -> @-width:Nat -> @-cost_per_step:(@+state:State -> {cost(state) == width : Nat}) -> @+count:Nat -> @+state:State -> {measured_iteration(State, step, cost, count, state) == Measured{iterate(State, step, count, state), Nat.mul(count, width)} : Measured<State>}

Concrete adapters must establish cost_per_step; it is not a heap-cost claim.

template counter_progress source · line 101 · raw

@-State:Data -> @-step:(@_:State -> State) -> @-position:(@_:State -> U32) -> @-stride:Nat -> @-advances:(@+state:State -> {position(step(state)) == U32.add(position(state), U32.from_nat(stride)) : U32}) -> @+count:Nat -> @+state:State -> {position(iterate(State, step, count, state)) == U32.add(position(state), U32.from_nat(Nat.mul(count, stride))) : U32}

template run_then_finishes source · line 113 · raw

@-State:Type -> @-Result:Type -> @-step:(@_:State -> State) -> @-finish:(@_:State -> Result) -> @count:Nat -> @-state:State -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run_then(State, Result, step, finish, count, state) == finish(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(State, step, count, state)) : Result}

The final step is applied once, to the state the loop ends in.