While loops with semantic guards and absorbed work

boundedWhile accepts any decidable guard, so a source states its guard in its own terms: 0 < r, a ≠ 0, i < n. Realizes.whileBounded certifies the loop whose guard is a native comparison of the encoded words. The congruence lemmas below move a loop, its domain and its charge between pointwise equivalent guards and between environments at which the loop's guard and body agree, so a certificate for the native guard transfers to the source's guard. The realize tactic does this transfer itself.

whileWork_le bounds the local work of a loop whose body costs at most K by cutoff * (K + 1); with a logarithmic cutoff this gives a sift its logarithmic local work through Realizes.consequence. When every body begins with a memory query, that query pays the iteration's control unit (whileWork_zero_le), and Realizes.while₀ is the while rule with local work 0, the shape realize composes.

Main results

• boundedWhile_congr, whileSafe_imp, whileSafe_congr, whileWork_congr: congruence in the guard, the body and the environment.
• whileWork_le: the local work is at most cutoff * (K + 1).
• whileWork_zero_le: a loop whose body begins with a query pays its control from memory.
• Realizes.while₀: the native while rule with absorbed local work.

Congruence

theorem Cslib.WordRAM.Realization.boundedWhile_congr {δ δ' σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (guard' : δ' → σ → Prop) [(d : δ') → (a : σ) → Decidable (guard' d a)] {body : δ × σ → DataStructure.Memory.Prog σ} {body' : δ' × σ → DataStructure.Memory.Prog σ} {d : δ} {d' : δ'} (hguard : ∀ (a : σ), guard d a ↔ guard' d' a) (hbody : ∀ (a : σ), body (d, a) = body' (d', a)) (n : ℕ) (a : σ) : boundedWhile guard body d n a = boundedWhile guard' body' d' n a

Loops whose guards and bodies agree at their environments are equal, whatever the guards' decidability instances.

theorem Cslib.WordRAM.Realization.whileSafe_imp {δ δ' σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (guard' : δ' → σ → Prop) [(d : δ') → (a : σ) → Decidable (guard' d a)] {body : δ × σ → DataStructure.Memory.Prog σ} {body' : δ' × σ → DataStructure.Memory.Prog σ} {d : δ} {d' : δ'} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {safe' : ℕ → δ' × σ → DataStructure.Memory.State → Prop} {w : ℕ} (hguard : ∀ (a : σ), guard d a ↔ guard' d' a) (hbody : ∀ (a : σ), body (d, a) = body' (d', a)) (hsafe : ∀ (a : σ) (s : DataStructure.Memory.State), guard d a → safe w (d, a) s → safe' w (d', a) s) {n : ℕ} {a : σ} {s : DataStructure.Memory.State} (h : whileSafe guard body safe w d n a s) : whileSafe guard' body' safe' w d' n a s

The reached-state domain transfers along agreeing guards and bodies and a weaker body domain. The body domains are compared only where the guard holds, as only there is a body run.

theorem Cslib.WordRAM.Realization.whileSafe_congr {δ δ' σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (guard' : δ' → σ → Prop) [(d : δ') → (a : σ) → Decidable (guard' d a)] {body : δ × σ → DataStructure.Memory.Prog σ} {body' : δ' × σ → DataStructure.Memory.Prog σ} {d : δ} {d' : δ'} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {safe' : ℕ → δ' × σ → DataStructure.Memory.State → Prop} {w : ℕ} (hguard : ∀ (a : σ), guard d a ↔ guard' d' a) (hbody : ∀ (a : σ), body (d, a) = body' (d', a)) (hsafe : ∀ (a : σ) (s : DataStructure.Memory.State), guard d a → (safe w (d, a) s ↔ safe' w (d', a) s)) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : whileSafe guard body safe w d n a s ↔ whileSafe guard' body' safe' w d' n a s

The reached-state domain is invariant under agreeing guards, bodies and body domains.

theorem Cslib.WordRAM.Realization.whileWork_congr {δ δ' σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (guard' : δ' → σ → Prop) [(d : δ') → (a : σ) → Decidable (guard' d a)] {body : δ × σ → DataStructure.Memory.Prog σ} {body' : δ' × σ → DataStructure.Memory.Prog σ} {d : δ} {d' : δ'} {work : δ × σ → DataStructure.Memory.State → ℕ} {work' : δ' × σ → DataStructure.Memory.State → ℕ} (hguard : ∀ (a : σ), guard d a ↔ guard' d' a) (hbody : ∀ (a : σ), body (d, a) = body' (d', a)) (hwork : ∀ (a : σ) (s : DataStructure.Memory.State), work (d, a) s = work' (d', a) s) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : whileWork guard body work d n a s = whileWork guard' body' work' d' n a s

The local work is invariant under agreeing guards, bodies and body charges.

Work envelopes

theorem Cslib.WordRAM.Realization.whileWork_le {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) {work : δ × σ → DataStructure.Memory.State → ℕ} {K : ℕ} (hK : ∀ (x : δ × σ) (s : DataStructure.Memory.State), work x s ≤ K) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : whileWork guard body work d n a s ≤ n * (K + 1)

With body work at most K, a loop with cutoff n has local work at most n * (K + 1).

theorem Cslib.WordRAM.Realization.whileWork_zero_le {δ σ : Type} (guard : δ → σ → Prop) [(d : δ) → (a : σ) → Decidable (guard d a)] (body : δ × σ → DataStructure.Memory.Prog σ) (hquery : ∀ (x : δ × σ) (s : DataStructure.Memory.State), 1 ≤ memoryCost (body x) s) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : whileWork guard body (fun (x : δ × σ) (x_1 : DataStructure.Memory.State) => 0) d n a s ≤ memoryCost (boundedWhile guard body d n a) s

When every body issues a query, the loop's control work is at most its memory charge.

The absorbed rule

theorem Cslib.WordRAM.Realization.Realizes.while₀ {δ σ : Type} {B : Basis} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) (cond : Cond (k + l)) (cutoff : δ × σ → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} (h : Realizes B body (appendWords input output) output safe fun (x : δ × σ) (x_1 : DataStructure.Memory.State) => 0) (hquery : ∀ (x : δ × σ) (s : DataStructure.Memory.State), 1 ≤ memoryCost (body x) 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) => whileSafe (fun (d : δ) (a : σ) => test cond ((appendWords input output) (d, a))) body safe w d (cutoff (d, a)) a s) fun (x : δ × σ) (x_1 : DataStructure.Memory.State) => 0

A while loop whose body begins with a query has local work 0: each executed iteration's control unit is paid by that query's memory charge. The guard is the native comparison cond of the encoded environment and state; the cutoff is a ghost bound, never computed.