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 definitions

• iterationSum: sum a state-dependent charge along a fixed semantic transition.

Main results

• ExecWithin.loop_potential_state: variable charged work paid by an explicit ghost potential.
• 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.
• ExecWithin.loop_invariant_state_additive: same-code bounds with additive control overhead.
• ExecWithin.loop_invariant_state_charged: bounded native loops carrying explicit semantic proof state and charging state-dependent body work plus one control unit per iteration.

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_potential_state {B : Basis} {r w : ℕ} {σ : 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) (t : ℕ), ExecWithin w body x y t ∧ I s' y ∧ t + 2 + μ s' ≤ μ s) {s : σ} {x : Data r} (hx : I s x) : ∃ (s' : σ) (y : Data r), ExecWithin w (Code.loop cond body) x y (μ s + 2) ∧ I s' y ∧ ¬cond.Holds y

Native loop rule with an explicit proof-state potential. Each actual body execution and its two loop-control instructions must be paid by the potential decrease. Semantic successor states and body charges may depend on the reached native state.

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.

def Cslib.WordRAM.iterationSum {σ : Type u_1} (next : σ → σ) (charge : σ → ℕ) : ℕ → σ → ℕ

Sum a state-dependent charge along a fixed semantic transition.

theorem Cslib.WordRAM.ExecWithin.loop_invariant_state_additive {σ : Type u_1} {B : Basis} {r : ℕ} {cond : Cond r} {code : Code B r} {w C D : ℕ} (I : ℕ → σ → Data r → Prop) (next : σ → σ) (charge : σ → ℕ) (hexit : ∀ (s : σ) (x : Data r), I 0 s x → ¬cond.Holds x) (hbody : ∀ (n : ℕ) (s : σ) (x : Data r), I (n + 1) s x → cond.Holds x ∧ ∃ (y : Data r), ExecWithin w code x y (C * (charge s + 1) + D) ∧ I n (next s) y) {n : ℕ} {s : σ} {x : Data r} (hx : I n s x) : ∃ (y : Data r), ExecWithin w (Code.loop cond code) x y (C * iterationSum next charge n s + (C + D + 2) * n + 2) ∧ I 0 (next^[n] s) y

Charge each body at its actual proof state and pay native loop control additively. The code, register bank and exchange constants are fixed before fuel; no query is required.

theorem Cslib.WordRAM.ExecWithin.loop_invariant_state_charged {σ : Type u_1} {B : Basis} {r : ℕ} {cond : Cond r} {code : Code B r} {w C D : ℕ} (I : ℕ → σ → Data r → Prop) (next : σ → σ) (charge : σ → ℕ) (hexit : ∀ (s : σ) (x : Data r), I 0 s x → ¬cond.Holds x) (hbody : ∀ (n : ℕ) (s : σ) (x : Data r), I (n + 1) s x → cond.Holds x ∧ ∃ (y : Data r), ExecWithin w code x y (C * (charge s + 1) + D) ∧ I n (next s) y) {n : ℕ} {s : σ} {x : Data r} (hx : I n s x) : ∃ (y : Data r), ExecWithin w (Code.loop cond code) x y ((C + D + 2) * (iterationSum next charge n s + n + 1)) ∧ I 0 (next^[n] s) y

A bounded native loop may charge variable body work and one unit per iteration without issuing a memory query. Its body, register bank and exchange constants are fixed before fuel. The remaining-fuel relation also carries arbitrary semantic proof state.