The pRHL rule for the unbounded loop

rHoare_whileLoop relates whileLoop guard₁ body₁ to whileLoop guard₂ body₂ under the hypotheses of the fixed-budget rule rHoare_whileApprox: a relational invariant I that makes the two guards agree, and two bodies that preserve I from any I-related pair of heaps at which the guards hold.

The judgment at a fixed budget only produces a coupling of the two approximants at that budget, and couplings at different budgets need not be comparable. The rule at the loop is proved by building one non-decreasing family of couplings loopJoint and taking its limit: a chosen coupling bodyJoint of the two bodies is threaded through the recursion on the budget, so the coupling at budget n is a restriction of the coupling at budget n + 1.

Main definitions

• loopJoint guard₁ bj n h₁ h₂ — the joint distribution of the lockstep run of the two loops for at most n iterations, with bj coupling one execution of the two bodies
• bodyJoint hbody h₁ h₂ — a coupling of the two bodies chosen from the body judgment
• loopJointLim hbody h₁ h₂ — the limit of loopJoint guard₁ (bodyJoint hbody) over the budget

Main results

• loopJoint_mono — the family is non-decreasing in the budget
• loopJoint_bind_fst, loopJoint_bind_snd — the two marginals of the family at budget n are the two approximants at budget n
• loopJoint_support — every coupled pair at any budget satisfies I with both guards false
• rHoare_whileLoop — the synchronous invariant rule at the unbounded loop

Support of a bind

theorem CatCrypt.NonUniform.exists_ne_zero_of_bind_apply_ne_zero {α : Type u_1} {β : Type u_2} {d : Prob.SDistr α} {f : α → Prob.SDistr β} {b : β} (hne : (d.bind f) (some b) ≠ 0) : ∃ (a : α), d (some a) ≠ 0 ∧ (f a) (some b) ≠ 0

A value of nonzero weight under a bind comes from a value of nonzero weight under the bound distribution.

The joint distribution of a budgeted lockstep run

noncomputable def CatCrypt.NonUniform.loopJoint (guard₁ : Core.Heap → Bool) (bj : Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)) : ℕ → Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)

The joint distribution of the lockstep run of two loops at budget n: while the left guard holds, bj couples one execution of the two bodies and the remaining budget is spent from the two resulting heaps.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.NonUniform.loopJoint guard₁ bj 0 x✝¹ x✝ = CatCrypt.Prob.SDistr.fail

@[simp]

theorem CatCrypt.NonUniform.loopJoint_zero (guard₁ : Core.Heap → Bool) (bj : Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)) (h₁ h₂ : Core.Heap) : loopJoint guard₁ bj 0 h₁ h₂ = Prob.SDistr.fail

theorem CatCrypt.NonUniform.loopJoint_succ (guard₁ : Core.Heap → Bool) (bj : Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)) (n : ℕ) (h₁ h₂ : Core.Heap) : loopJoint guard₁ bj (n + 1) h₁ h₂ = if guard₁ h₁ = true then (bj h₁ h₂).bind fun (pq : (Unit × Core.Heap) × Unit × Core.Heap) => loopJoint guard₁ bj n pq.1.2 pq.2.2 else Prob.SDistr.pure (((), h₁), (), h₂)

theorem CatCrypt.NonUniform.loopJoint_succ_of_guard {guard₁ : Core.Heap → Bool} (bj : Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)) {h₁ : Core.Heap} (hg : guard₁ h₁ = true) (n : ℕ) (h₂ : Core.Heap) : loopJoint guard₁ bj (n + 1) h₁ h₂ = (bj h₁ h₂).bind fun (pq : (Unit × Core.Heap) × Unit × Core.Heap) => loopJoint guard₁ bj n pq.1.2 pq.2.2

theorem CatCrypt.NonUniform.loopJoint_succ_of_not_guard {guard₁ : Core.Heap → Bool} (bj : Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)) {h₁ : Core.Heap} (hg : guard₁ h₁ = false) (n : ℕ) (h₂ : Core.Heap) : loopJoint guard₁ bj (n + 1) h₁ h₂ = Prob.SDistr.pure (((), h₁), (), h₂)

The family is non-decreasing in the budget

theorem CatCrypt.NonUniform.loopJoint_apply_le_succ (guard₁ : Core.Heap → Bool) (bj : Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)) (n : ℕ) (h₁ h₂ : Core.Heap) (x : (Unit × Core.Heap) × Unit × Core.Heap) : (loopJoint guard₁ bj n h₁ h₂) (some x) ≤ (loopJoint guard₁ bj (n + 1) h₁ h₂) (some x)

Raising the budget by one does not decrease the weight of a coupled pair.

theorem CatCrypt.NonUniform.loopJoint_mono (guard₁ : Core.Heap → Bool) (bj : Core.Heap → Core.Heap → Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)) (h₁ h₂ : Core.Heap) : MonoSeq fun (n : ℕ) => loopJoint guard₁ bj n h₁ h₂

The weight of a coupled pair is non-decreasing in the budget.

A chosen coupling of the two bodies

theorem CatCrypt.NonUniform.exists_bodyJoint {guard₁ guard₂ : Core.Heap → Bool} {body₁ body₂ : Core.SPComp Unit} {I : Relational.RPre} (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₂) (h₁ h₂ : Core.Heap) : ∃ (d : Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)), I h₁ h₂ → guard₁ h₁ = true → guard₂ h₂ = true → (∀ (p : Unit × Core.Heap), (d.bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.1) (some p) = (body₁ h₁) (some p)) ∧ (∀ (p : Unit × Core.Heap), (d.bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.2) (some p) = (body₂ h₂) (some p)) ∧ ∀ (p q : Unit × Core.Heap), d (some (p, q)) ≠ 0 → I p.2 q.2

The body judgment supplies, at every pair of heaps, a distribution that is a coupling of the two bodies supported in the invariant whenever the invariant holds and both guards are true.

noncomputable def CatCrypt.NonUniform.bodyJoint {guard₁ guard₂ : Core.Heap → Bool} {body₁ body₂ : Core.SPComp Unit} {I : Relational.RPre} (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₂) (h₁ h₂ : Core.Heap) : Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)

A coupling of the two bodies chosen from the body judgment.

Equations

• CatCrypt.NonUniform.bodyJoint hbody h₁ h₂ = ⋯.choose

theorem CatCrypt.NonUniform.bodyJoint_spec {guard₁ guard₂ : Core.Heap → Bool} {body₁ body₂ : Core.SPComp Unit} {I : Relational.RPre} (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₂) {h₁ h₂ : Core.Heap} (hI : I h₁ h₂) (hg₁ : guard₁ h₁ = true) (hg₂ : guard₂ h₂ = true) : (∀ (p : Unit × Core.Heap), ((bodyJoint hbody h₁ h₂).bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.1) (some p) = (body₁ h₁) (some p)) ∧ (∀ (p : Unit × Core.Heap), ((bodyJoint hbody h₁ h₂).bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.2) (some p) = (body₂ h₂) (some p)) ∧ ∀ (p q : Unit × Core.Heap), (bodyJoint hbody h₁ h₂) (some (p, q)) ≠ 0 → I p.2 q.2

At a pair of heaps satisfying the invariant with both guards true, the chosen distribution has the two bodies as marginals and is supported in the invariant.

The marginals of the family

theorem CatCrypt.NonUniform.loopJoint_bind_fst {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 : ℕ) (h₁ h₂ : Core.Heap) : I h₁ h₂ → ((loopJoint guard₁ (bodyJoint hbody) n h₁ h₂).bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.1) = whileApprox guard₁ body₁ n h₁

The left marginal of the coupling at budget n is the left approximant at budget n.

theorem CatCrypt.NonUniform.loopJoint_bind_snd {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 : ℕ) (h₁ h₂ : Core.Heap) : I h₁ h₂ → ((loopJoint guard₁ (bodyJoint hbody) n h₁ h₂).bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.2) = whileApprox guard₂ body₂ n h₂

The right marginal of the coupling at budget n is the right approximant at budget n.

The support of the family

theorem CatCrypt.NonUniform.loopJoint_support {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 : ℕ) (h₁ h₂ : Core.Heap) : I h₁ h₂ → ∀ (p q : Unit × Core.Heap), (loopJoint guard₁ (bodyJoint hbody) n h₁ h₂) (some (p, q)) ≠ 0 → I p.2 q.2 ∧ guard₁ p.2 = false ∧ guard₂ q.2 = false

Every pair coupled at any budget satisfies the invariant with both guards false.

The limit of the family

noncomputable def CatCrypt.NonUniform.loopJointLim {guard₁ guard₂ : Core.Heap → Bool} {body₁ body₂ : Core.SPComp Unit} {I : Relational.RPre} (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₂) (h₁ h₂ : Core.Heap) : Prob.SDistr ((Unit × Core.Heap) × Unit × Core.Heap)

The limit over the budget of the couplings of the two loops.

Equations

• CatCrypt.NonUniform.loopJointLim hbody h₁ h₂ = CatCrypt.NonUniform.mlim (fun (n : ℕ) => CatCrypt.NonUniform.loopJoint guard₁ (CatCrypt.NonUniform.bodyJoint hbody) n h₁ h₂) ⋯

theorem CatCrypt.NonUniform.exists_loopJoint_ne_zero {guard₁ guard₂ : Core.Heap → Bool} {body₁ body₂ : Core.SPComp Unit} {I : Relational.RPre} {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₂} {h₁ h₂ : Core.Heap} {x : (Unit × Core.Heap) × Unit × Core.Heap} (hne : (loopJointLim hbody h₁ h₂) (some x) ≠ 0) : ∃ (n : ℕ), (loopJoint guard₁ (bodyJoint hbody) n h₁ h₂) (some x) ≠ 0

A pair coupled in the limit is coupled at some budget.

theorem CatCrypt.NonUniform.loopJointLim_bind_fst {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₂) {h₁ h₂ : Core.Heap} (hI : I h₁ h₂) (p : Unit × Core.Heap) : ((loopJointLim hbody h₁ h₂).bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.1) (some p) = (whileLoop guard₁ body₁ h₁) (some p)

The left marginal of the limit is the left loop.

theorem CatCrypt.NonUniform.loopJointLim_bind_snd {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₂) {h₁ h₂ : Core.Heap} (hI : I h₁ h₂) (p : Unit × Core.Heap) : ((loopJointLim hbody h₁ h₂).bind fun (q : (Unit × Core.Heap) × Unit × Core.Heap) => Prob.SDistr.pure q.2) (some p) = (whileLoop guard₂ body₂ h₂) (some p)

The right marginal of the limit is the right loop.

The rule

theorem CatCrypt.NonUniform.rHoare_whileLoop {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₂) : Relational.rHoare I (whileLoop guard₁ body₁) (whileLoop guard₂ body₂) 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 unbounded loop.

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 the two loops are related by I together with both guards being false.

theorem CatCrypt.NonUniform.rHoare_whileLoop_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₂) : Relational.rHoare I (whileLoop guard body) (whileLoop guard body) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => I h₁ h₂ ∧ guard h₁ = false ∧ guard h₂ = false

The rule with one guard and one body on both sides.