The unary invariant rule for bounded loop approximants

A predicate I on heaps that the body preserves whenever the guard holds is an invariant of every approximant whileApprox guard body n: from a heap satisfying I, each outcome of the approximant satisfies I and falsifies the guard.

The rule needs no termination hypothesis. A run that exhausts its budget fails, and failure carries no value mass, so the postcondition holds vacuously on it; the judgment is partial correctness. Termination enters separately, through losslessness: at a budget where the approximant has mass one, the postcondition has probability one.

Main results

• pHoare_whileApprox — the invariant rule at every budget
• pHoare_whileApprox_conseq — the same with the postcondition weakened
• prEvent_whileApprox_eq_one — probability one under conditional losslessness
• prEvent_whileApprox_eq_one_of_isLossless — the unconditional variant

Base case

theorem CatCrypt.NonUniform.pHoare_whileApprox_zero (P : Unary.UPre) (Q : Unary.UPost Unit) (guard : Core.Heap → Bool) (body : Core.SPComp Unit) : Unary.pHoare P (whileApprox guard body 0) Q

The zero-budget approximant is SPComp.fail, which satisfies every judgment: its support contains no outcome.

The invariant rule

theorem CatCrypt.NonUniform.pHoare_whileApprox {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') (n : ℕ) : Unary.pHoare I (whileApprox guard body n) fun (x : Unit) (h' : Core.Heap) => I h' ∧ guard h' = false

Invariant rule for the bounded approximants. If body restores I from any heap satisfying I on which the guard holds, then from a heap satisfying I the approximant whileApprox guard body n ends in a heap satisfying I on which the guard is false, for every budget n.

theorem CatCrypt.NonUniform.pHoare_whileApprox_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) (n : ℕ) : Unary.pHoare I (whileApprox guard body n) Q

The invariant rule with the postcondition weakened: any Q implied by the invariant together with the guard being false.

Termination-gated probability

theorem CatCrypt.NonUniform.prEvent_whileApprox_eq_one {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') {n : ℕ} (hll : Unary.isLosslessIf I (whileApprox guard body n)) (h₀ : Core.Heap) (hI : I h₀) : (Unary.prEvent (whileApprox guard body n h₀) fun (x : Unit) (h' : Core.Heap) => I h' ∧ guard h' = false) = 1

At a budget where the approximant is lossless on heaps satisfying the invariant, the invariant together with the guard being false has probability one.

theorem CatCrypt.NonUniform.prEvent_whileApprox_eq_one_of_isLossless {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') {n : ℕ} (hll : Unary.isLossless (whileApprox guard body n)) (h₀ : Core.Heap) (hI : I h₀) : (Unary.prEvent (whileApprox guard body n h₀) fun (x : Unit) (h' : Core.Heap) => I h' ∧ guard h' = false) = 1

prEvent_whileApprox_eq_one under unconditional losslessness of the approximant.

theorem CatCrypt.NonUniform.prEvent_whileApprox_conseq_eq_one {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) {n : ℕ} (hll : Unary.isLosslessIf I (whileApprox guard body n)) (h₀ : Core.Heap) (hI : I h₀) : (Unary.prEvent (whileApprox guard body n h₀) fun (a : Unit) (h' : Core.Heap) => Q a h') = 1

The weakened form at probability one: a postcondition implied by the invariant and the guard being false holds with probability one at a budget where the approximant is lossless.