Constant-cost counting loops

An indexed semantic invariant describes the state after each completed iteration. The native counter increases by exactly one, and the limit register keeps the fixed endpoint. The rule derives the counter bounds, decreasing rank and final index from these facts; clients still prove execution of the actual body, including its word fits and memory semantics.

Main results

• ExecWithin.loop_count: count from the current index to N with a body allowance T, charging (N - index) * (T + 2) + 2, including both loop-control instructions per iteration and the final test/exit. No one-past-end word-fit premise is required.
• prefix_write_step: advance a written-prefix and outside-prefix memory invariant across a single store at d + j.

This is an original specialization of ExecWithin.loop_invariant.

theorem Cslib.WordRAM.ExecWithin.loop_count {B : Basis} {r w N T : ℕ} {index limit : Fin r} {body : Code B r} (P : ℕ → Data r → Prop) (hlimit : ∀ (y : Data r), P (y.regs index) y → y.regs limit = N) (hbody : ∀ (y : Data r), P (y.regs index) y → y.regs index < N → ∃ (z : Data r), ExecWithin w body y z T ∧ P (y.regs index + 1) z ∧ z.regs index = y.regs index + 1) {x : Data r} (hle : x.regs index ≤ N) (hx : P (x.regs index) x) : ∃ (y : Data r), ExecWithin w (Code.loop (Cond.lt index limit) body) x y ((N - x.regs index) * (T + 2) + 2) ∧ P N y ∧ y.regs index = N

Execute a native counting loop with an indexed semantic invariant. The invariant supplies the unchanged limit register. Each body execution advances the counter by exactly one and establishes the next semantic state. The bound excludes setup and the final program halt.

theorem Cslib.WordRAM.prefix_write_step {α : Type u_1} {m₀ m z : ℕ → α} {d j : ℕ} {e : ℕ → α} (hm : ∀ i < j, m (d + i) = e i) (hf : ∀ (a : ℕ), ¬(d ≤ a ∧ a < d + j) → m a = m₀ a) (hz : z = Function.update m (d + j) (e j)) : (∀ i < j + 1, z (d + i) = e i) ∧ ∀ (a : ℕ), ¬(d ≤ a ∧ a < d + (j + 1)) → z a = m₀ a

Advance a loop's written-prefix and outside-prefix memory invariants across a single store at d + j.