Measure-bounded memory-client while loops

The source is finite recursion in the existing Memory.Prog. Its cutoff depends only on the explicit initial input. A reached-state measure proves that the guard becomes false before the cutoff, so the native code can use a genuine Code.loop without computing or storing that cutoff. The native guard is an existing Cond on the faithfully encoded environment and mutable state; an arbitrary semantic predicate is not granted executable code by a body certificate.

Local work counts only executed iterations. Every native guard, body, register copy and control instruction is charged, including the initial/final false guard and iterations without queries. Rank and potential may inspect reached memory as proof data; they never secretly select the source program or its initial cutoff from unencoded memory.

Main definitions

• boundedWhile: an early-exit loop represented by an ordinary finite memory program.
• whileSafe, whileWork: reached body domains, nontruncation and local iteration charges.

Main results

• whileSafe_of_measure: invariant and decreasing rank establish the nontruncating domain.
• boundedWhile_stops: the returned source value has a false guard.
• while_charge_le_potential: a potential pays memory and local work and retains exit credit.
• Realizes.whileBounded: one native emitter before every runtime input and width.
• Realizes.whileMeasure: semantic invariant/rank conditions discharge the native entry domain.

def Cslib.WordRAM.Realization.boundedWhile {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (d : δ) : ℕ → σ → DataStructure.Memory.Prog σ

Finite source representation of a while loop. whileSafe excludes cutoff truncation.

def Cslib.WordRAM.Realization.whileSafe {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (safe : ℕ → δ × σ → DataStructure.Memory.State → Prop) (w : ℕ) (d : δ) : ℕ → σ → DataStructure.Memory.State → Prop

Only continuing states require the body domain. At the cutoff the guard must be false.

def Cslib.WordRAM.Realization.whileWork {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (work : δ × σ → DataStructure.Memory.State → ℕ) (d : δ) : ℕ → σ → DataStructure.Memory.State → ℕ

Local body work and one control unit for each executed iteration. The final guard is paid by the existing realization overhead, even when no body executes.

theorem Cslib.WordRAM.Realization.boundedWhile_of_not {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (d : δ) (n : ℕ) (a : σ) (hg : ¬guard d a) : boundedWhile guard body d n a = pure a

An initially false guard does not execute the body, independently of the ghost cutoff.

theorem Cslib.WordRAM.Realization.while_charge_succ {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (work : δ × σ → DataStructure.Memory.State → ℕ) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) (hg : guard d a) : memoryCost (boundedWhile guard body d (n + 1) a) s + whileWork guard body work d (n + 1) a s = memoryCost (body (d, a)) s + work (d, a) s + (memoryCost (boundedWhile guard body d n ((DataStructure.Memory.spec 0).clientResult s (body (d, a)))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) + whileWork guard body work d n ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a)))) + 1

Every real continuation splits its exact memory cost and local control charge.

theorem Cslib.WordRAM.Realization.whileSafe_of_measure {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (safe : ℕ → δ × σ → DataStructure.Memory.State → Prop) (w : ℕ) (d : δ) (I : σ → DataStructure.Memory.State → Prop) (rank : σ → DataStructure.Memory.State → ℕ) (hzero : ∀ (a : σ) (s : DataStructure.Memory.State), I a s → rank a s = 0 → ¬guard d a) (hstep : ∀ (a : σ) (s : DataStructure.Memory.State), I a s → guard d a → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (body (d, a))) → safe w (d, a) s ∧ I ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) ∧ rank ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) < rank a s) {n : ℕ} {a : σ} {s : DataStructure.Memory.State} (hi : I a s) (hr : rank a s ≤ n) (hv : (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (boundedWhile guard body d n a))) : whileSafe guard body safe w d n a s

An invariant supplies the genuine body domain and a strictly decreasing reached-state rank. The source cutoff is sufficient when it initially bounds that rank. No rank is executed.

theorem Cslib.WordRAM.Realization.boundedWhile_stops {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (safe : ℕ → δ × σ → DataStructure.Memory.State → Prop) (w : ℕ) (d : δ) {n : ℕ} {a : σ} {s : DataStructure.Memory.State} (hs : whileSafe guard body safe w d n a s) (hv : (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (boundedWhile guard body d n a))) : ¬guard d ((DataStructure.Memory.spec 0).clientResult s (boundedWhile guard body d n a))

The reached-state domain guarantees a false guard at the actual returned source value, not merely a value obtained by truncating an unfinished loop.

theorem Cslib.WordRAM.Realization.while_charge_le_potential {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (work : δ × σ → DataStructure.Memory.State → ℕ) (w : ℕ) (d : δ) (I : σ → DataStructure.Memory.State → Prop) (potential : σ → DataStructure.Memory.State → ℕ) (hstep : ∀ (a : σ) (s : DataStructure.Memory.State), I a s → guard d a → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (body (d, a))) → I ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) ∧ memoryCost (body (d, a)) s + work (d, a) s + 1 + potential ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) ≤ potential a s) {n : ℕ} {a : σ} {s : DataStructure.Memory.State} (hi : I a s) (hv : (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (boundedWhile guard body d n a))) : memoryCost (boundedWhile guard body d n a) s + whileWork guard body work d n a s + potential ((DataStructure.Memory.spec 0).clientResult s (boundedWhile guard body d n a)) ((DataStructure.Memory.spec 0).clientState s (boundedWhile guard body d n a)) ≤ potential a s

The charged source cost telescopes while preserving the remaining exit potential. This can pay query-free iterations because local work and control are included in every step.

theorem Cslib.WordRAM.Realization.Realizes.whileBounded {δ σ : Type} {k l : ℕ} {B : Basis} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) (cond : Cond (k + l)) (cutoff : δ × σ → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : Realizes B body (appendWords input output) output safe work) : Realizes B (fun (x : δ × σ) => match x with | (d, a) => boundedWhile (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body d (cutoff (d, a)) a) (appendWords input output) output (fun (w : ℕ) (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => whileSafe (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body safe w d (cutoff (d, a)) a s) fun (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => whileWork (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body work d (cutoff (d, a)) a s

One native while emitter genuinely exits on the existing encoded condition. The pure source cutoff depends only on explicit initial input and is not computed or stored by this emitter. The domain excludes truncation; every executed guard/body/copy/control and final exit is charged.

theorem Cslib.WordRAM.Realization.Realizes.whileMeasure {δ σ : Type} {k l : ℕ} {B : Basis} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) (cond : Cond (k + l)) (cutoff : δ × σ → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : Realizes B body (appendWords input output) output safe work) (I : ℕ → δ → σ → DataStructure.Memory.State → Prop) (rank : δ → σ → DataStructure.Memory.State → ℕ) (hzero : ∀ (w : ℕ) (d : δ) (a : σ) (s : DataStructure.Memory.State), I w d a s → rank d a s = 0 → ¬test cond ((appendWords input output) (d, a))) (hstep : ∀ (w : ℕ) (d : δ) (a : σ) (s : DataStructure.Memory.State), I w d a s → test cond ((appendWords input output) (d, a)) → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (body (d, a))) → safe w (d, a) s ∧ I w d ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) ∧ rank d ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) < rank d a s) : Realizes B (fun (x : δ × σ) => match x with | (d, a) => boundedWhile (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body d (cutoff (d, a)) a) (appendWords input output) output (fun (w : ℕ) (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => I w d a s ∧ rank d a s ≤ cutoff (d, a)) fun (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => whileWork (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body work d (cutoff (d, a)) a s

Semantic invariants and a decreasing rank establish the native while's complete reached-state domain. The rank/cutoff comparison is proof data; the emitted code still tests only cond.

theorem Cslib.WordRAM.Realization.RealizesBounded.whileBounded {δ σ : Type} {k l : ℕ} {B : Basis} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) (cond : Cond (k + l)) (cutoff : δ × σ → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : RealizesBounded B body (appendWords input output) output safe work) : RealizesBounded B (fun (x : δ × σ) => match x with | (d, a) => boundedWhile (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body d (cutoff (d, a)) a) (appendWords input output) output (fun (w : ℕ) (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => whileSafe (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body safe w d (cutoff (d, a)) a s) fun (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => whileWork (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body work d (cutoff (d, a)) a s

Frontier-bounded native while realization.

theorem Cslib.WordRAM.Realization.RealizesBounded.whileMeasure {δ σ : Type} {k l : ℕ} {B : Basis} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) (cond : Cond (k + l)) (cutoff : δ × σ → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : RealizesBounded B body (appendWords input output) output safe work) (I : ℕ → δ → σ → DataStructure.Memory.State → Prop) (rank : δ → σ → DataStructure.Memory.State → ℕ) (hzero : ∀ (w : ℕ) (d : δ) (a : σ) (s : DataStructure.Memory.State), I w d a s → rank d a s = 0 → ¬test cond ((appendWords input output) (d, a))) (hstep : ∀ (w : ℕ) (d : δ) (a : σ) (s : DataStructure.Memory.State), I w d a s → test cond ((appendWords input output) (d, a)) → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (body (d, a))) → safe w (d, a) s ∧ I w d ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) ∧ rank d ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) < rank d a s) : RealizesBounded B (fun (x : δ × σ) => match x with | (d, a) => boundedWhile (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body d (cutoff (d, a)) a) (appendWords input output) output (fun (w : ℕ) (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => I w d a s ∧ rank d a s ≤ cutoff (d, a)) fun (x : δ × σ) (s : DataStructure.Memory.State) => match x with | (d, a) => whileWork (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body work d (cutoff (d, a)) a s

Measure-bounded frontier-bounded while realization.