The unbounded loop

whileLoop guard body runs body while guard holds of the current heap, with no bound on the number of iterations. It is the limit of whileApprox: the mass it assigns to a heap is the probability of reaching that heap and leaving the loop after any finite number of iterations, and the failure mass is the probability of running forever.

The pHL rule transports from the approximants because pHoare constrains the support: a heap in the support of the limit is in the support of some approximant, and the invariant rule holds at every budget.

noncomputable def CatCrypt.NonUniform.whileLoop (guard : Core.Heap → Bool) (body : Core.SPComp Unit) : Core.SPComp Unit

while guard do body, as the limit of its bounded approximants.

Equations

• CatCrypt.NonUniform.whileLoop guard body h = CatCrypt.NonUniform.mlim (fun (n : ℕ) => CatCrypt.NonUniform.whileApprox guard body n h) ⋯

@[simp]

theorem CatCrypt.NonUniform.whileLoop_apply_some (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) (p : Unit × Core.Heap) : (whileLoop guard body h) (some p) = ⨆ (n : ℕ), (whileApprox guard body n h) (some p)

theorem CatCrypt.NonUniform.exists_whileApprox_ne_zero {guard : Core.Heap → Bool} {body : Core.SPComp Unit} {h : Core.Heap} {p : Unit × Core.Heap} (hp : (whileLoop guard body h) (some p) ≠ 0) : ∃ (n : ℕ), (whileApprox guard body n h) (some p) ≠ 0

An outcome of the loop is an outcome of some approximant: a supremum over the budgets is nonzero only if one of them is.

theorem CatCrypt.NonUniform.pHoare_whileLoop {guard : Core.Heap → Bool} {body : Core.SPComp Unit} {I : Core.Heap → Prop} (hbody : Unary.pHoare (fun (h : Core.Heap) => I h ∧ guard h = true) body fun (x : Unit) (h' : Core.Heap) => I h') : Unary.pHoare I (whileLoop guard body) fun (x : Unit) (h' : Core.Heap) => I h' ∧ guard h' = false

The pHL rule for the unbounded loop. If the body preserves the invariant while the guard holds, then every outcome of the loop satisfies the invariant with the guard false.

This is partial correctness: the mass on which the loop runs forever is failure mass, which carries no outcome and so satisfies the postcondition vacuously.

theorem CatCrypt.NonUniform.pHoare_whileLoop_conseq {guard : Core.Heap → Bool} {body : Core.SPComp Unit} {I : Core.Heap → Prop} {Q : Unary.UPost Unit} (hbody : Unary.pHoare (fun (h : Core.Heap) => I h ∧ guard h = true) body fun (x : Unit) (h' : Core.Heap) => I h') (hQ : ∀ (h : Core.Heap), I h → guard h = false → Q () h) : Unary.pHoare I (whileLoop guard body) Q

The consequence form of the loop rule.