pRHL rules for bounded loop approximants

rHoare Φ c₁ c₂ Ψ holds when the output sub-distributions of c₁ and c₂, run from any Φ-related pair of heaps, admit a coupling supported in Ψ. This file gives the rules relating whileApprox guard₁ body₁ n to whileApprox guard₂ body₂ n at a fixed budget n.

A relational invariant I that forces the two guards to agree, together with bodies that preserve I while the guards hold, relates the two approximants at every budget. The two sides run in lockstep: the same n on both sides. A Coupling matches its two marginals exactly, so the failure mass carried by a joint sub-distribution is shared by both sides; at equal budgets the two approximants do lose the same mass, which is what makes the lockstep statement couplable.

Main results

• rHoare_fail_fail — a coupling of two failed computations, on any pre- and postcondition
• rHoare_whileApprox_zero — the budget-0 case, where both approximants are SPComp.fail
• rHoare_whileApprox_step — one synchronous iteration at budget n + 1, given the judgment for the bodies and the judgment at budget n
• rHoare_whileApprox — the synchronous invariant rule at every budget
• rHoare_whileApprox_same — the specialization to one guard and one body

Failure against failure

theorem CatCrypt.NonUniform.rHoare_fail_fail {α : Type u_1} {β : Type u_2} {Φ : Relational.RPre} {Ψ : Relational.RPost α β} : Relational.rHoare Φ Core.SPComp.fail Core.SPComp.fail Ψ

Two failed computations are related by any postcondition: the zero sub-distribution is a coupling of SPComp.fail with itself, and its support is empty.

The approximants at a fixed budget

theorem CatCrypt.NonUniform.rHoare_whileApprox_zero (guard₁ guard₂ : Core.Heap → Bool) (body₁ body₂ : Core.SPComp Unit) (Φ : Relational.RPre) (Ψ : Relational.RPost Unit Unit) : Relational.rHoare Φ (whileApprox guard₁ body₁ 0) (whileApprox guard₂ body₂ 0) Ψ

At budget 0 both approximants are SPComp.fail, so any pre- and postcondition relate them.

theorem CatCrypt.NonUniform.rHoare_whileApprox_step {guard₁ guard₂ : Core.Heap → Bool} {body₁ body₂ : Core.SPComp Unit} {I : Relational.RPre} {Ψ : Relational.RPost Unit Unit} {n : ℕ} (hbody : Relational.rHoare (fun (h₁ h₂ : Core.Heap) => I h₁ h₂ ∧ guard₁ h₁ = true ∧ guard₂ h₂ = true) body₁ body₂ fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => I h₁ h₂) (hrec : Relational.rHoare I (whileApprox guard₁ body₁ n) (whileApprox guard₂ body₂ n) Ψ) : Relational.rHoare (fun (h₁ h₂ : Core.Heap) => I h₁ h₂ ∧ guard₁ h₁ = true ∧ guard₂ h₂ = true) (whileApprox guard₁ body₁ (n + 1)) (whileApprox guard₂ body₂ (n + 1)) Ψ

One synchronous iteration. From a pair of heaps satisfying I with both guards true, a judgment for the two bodies and a judgment for the two approximants at budget n give the judgment at budget n + 1.

theorem CatCrypt.NonUniform.rHoare_whileApprox {guard₁ guard₂ : Core.Heap → Bool} {body₁ body₂ : Core.SPComp Unit} {I : Relational.RPre} (hguard : ∀ (h₁ h₂ : Core.Heap), I h₁ h₂ → guard₁ h₁ = guard₂ h₂) (hbody : Relational.rHoare (fun (h₁ h₂ : Core.Heap) => I h₁ h₂ ∧ guard₁ h₁ = true ∧ guard₂ h₂ = true) body₁ body₂ fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => I h₁ h₂) (n : ℕ) : Relational.rHoare I (whileApprox guard₁ body₁ n) (whileApprox guard₂ body₂ n) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => I h₁ h₂ ∧ guard₁ h₁ = false ∧ guard₂ h₂ = false

The synchronous invariant rule for the bounded approximants.

If the relational invariant I forces the two guards to agree, and the two bodies preserve I from any I-related pair of heaps at which the guards hold, then at every budget n the two approximants are related by I together with both guards being false.

theorem CatCrypt.NonUniform.rHoare_whileApprox_same {guard : Core.Heap → Bool} {body : Core.SPComp Unit} {I : Relational.RPre} (hguard : ∀ (h₁ h₂ : Core.Heap), I h₁ h₂ → guard h₁ = guard h₂) (hbody : Relational.rHoare (fun (h₁ h₂ : Core.Heap) => I h₁ h₂ ∧ guard h₁ = true ∧ guard h₂ = true) body body fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => I h₁ h₂) (n : ℕ) : Relational.rHoare I (whileApprox guard body n) (whileApprox guard body n) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => I h₁ h₂ ∧ guard h₁ = false ∧ guard h₂ = false

The synchronous rule with one guard and one body on both sides: the invariant only has to make the guard agree on the two heaps.