Native loop invariants with explicit proof state

An invariant may relate the native data to additional mathematical proof state, such as the represented worklist and emitted output. The decreasing measure then applies directly to that proof state. It need not be reconstructed by an additional machine program or a choice of representation from the native data alone.

Main results

• ExecWithin.loop_invariant_state: the native loop rule with explicit proof state and a natural decreasing measure, including all loop-control instructions in the bound.

This is an original extension of the existing native invariant/measure rule. The body premise is actual ExecWithin execution of the given native code, not a source execution or time oracle.

theorem Cslib.WordRAM.ExecWithin.loop_invariant_state {B : Basis} {r w T : ℕ} {σ : Type u_1} (I : σ → Data r → Prop) (μ : σ → ℕ) {cond : Cond r} {body : Code B r} (hbody : ∀ (s : σ) (x : Data r), I s x → cond.Holds x → ∃ (s' : σ) (y : Data r), ExecWithin w body x y T ∧ I s' y ∧ μ s' < μ s) {s : σ} {x : Data r} (hx : I s x) : ∃ (s' : σ) (y : Data r), ExecWithin w (Code.loop cond body) x y (μ s * (T + 2) + 2) ∧ I s' y ∧ ¬cond.Holds y

Native loop rule carrying explicit mathematical proof state. The body must execute the actual native code, preserve the relation and strictly decrease the proof-state measure.