Order theory of the bounded loop approximants

The mass whileApprox guard body n h assigns to a value is non-decreasing in the budget n, the mass it assigns to failure is non-increasing, and the value mass is bounded by 1 at every budget. Together these make the pointwise supremum over n a well-defined sub-probability assignment, which is what a limit construction for while guard do body consumes.

Main results

• SDistr.bind_apply_mono — bind is monotone in its continuation, pointwise at a fixed outcome
• whileApprox_apply_le_succ, whileApprox_apply_mono, monotone_whileApprox_apply — the value mass is non-decreasing in the budget
• whileApprox_apply_none_succ_le, whileApprox_apply_none_antitone — the failure mass is non-increasing in the budget
• whileApprox_apply_le_one, tsum_whileApprox_apply_le_one — the value mass is bounded by 1 at every budget
• iSup_whileApprox_apply_le_one, tsum_iSup_whileApprox_apply_le_one — the same bounds for the pointwise supremum over budgets

Unfolding at a fixed outcome

theorem CatCrypt.NonUniform.whileApprox_succ_bind_of_guard {guard : Core.Heap → Bool} {body : Core.SPComp Unit} {h : Core.Heap} (hg : guard h = true) (n : ℕ) : whileApprox guard body (n + 1) h = (body h).bind fun (q : Unit × Core.Heap) => whileApprox guard body n q.2

The guarded step of an approximant as an SDistr bind: the body is run once and the remaining budget is spent from the resulting heap.

@[simp]

theorem CatCrypt.NonUniform.whileApprox_zero_apply_some (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) (p : Unit × Core.Heap) : (whileApprox guard body 0 h) (some p) = 0

@[simp]

theorem CatCrypt.NonUniform.whileApprox_zero_apply_none (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) : (whileApprox guard body 0 h) none = 1

The value mass is non-decreasing in the budget

theorem CatCrypt.NonUniform.whileApprox_apply_le_succ (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (n : ℕ) (h : Core.Heap) (p : Unit × Core.Heap) : (whileApprox guard body n h) (some p) ≤ (whileApprox guard body (n + 1) h) (some p)

Raising the budget by one does not decrease the mass at a value: a run that has not yet left the loop contributes no mass at the smaller budget.

theorem CatCrypt.NonUniform.whileApprox_apply_mono (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) (n m : ℕ) : n ≤ m → ∀ (p : Unit × Core.Heap), (whileApprox guard body n h) (some p) ≤ (whileApprox guard body m h) (some p)

The mass at a value is non-decreasing in the budget.

theorem CatCrypt.NonUniform.monotone_whileApprox_apply (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) (p : Unit × Core.Heap) : Monotone fun (n : ℕ) => (whileApprox guard body n h) (some p)

The mass at a value, as a function of the budget, is monotone.

The failure mass is non-increasing in the budget

theorem CatCrypt.NonUniform.whileApprox_apply_none_succ_le (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (n : ℕ) (h : Core.Heap) : (whileApprox guard body (n + 1) h) none ≤ (whileApprox guard body n h) none

Raising the budget by one does not increase the mass at failure.

theorem CatCrypt.NonUniform.whileApprox_apply_none_antitone (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) (n m : ℕ) : n ≤ m → (whileApprox guard body m h) none ≤ (whileApprox guard body n h) none

The mass at failure is non-increasing in the budget.

theorem CatCrypt.NonUniform.antitone_whileApprox_apply_none (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) : Antitone fun (n : ℕ) => (whileApprox guard body n h) none

The mass at failure, as a function of the budget, is antitone.

The value mass is bounded

theorem CatCrypt.NonUniform.whileApprox_apply_le_one (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (n : ℕ) (h : Core.Heap) (p : Unit × Core.Heap) : (whileApprox guard body n h) (some p) ≤ 1

The mass at a single value is at most 1.

theorem CatCrypt.NonUniform.whileApprox_apply_ne_top (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (n : ℕ) (h : Core.Heap) (p : Unit × Core.Heap) : (whileApprox guard body n h) (some p) ≠ ⊤

The mass at a single value is finite.

theorem CatCrypt.NonUniform.tsum_whileApprox_apply_le_one (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (n : ℕ) (h : Core.Heap) : ∑' (p : Unit × Core.Heap), (whileApprox guard body n h) (some p) ≤ 1

The total mass on values is at most 1 at every budget.

The bounds for the supremum over budgets

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

The supremum over budgets of the mass at a value is at most 1.

theorem CatCrypt.NonUniform.tsum_iSup_whileApprox_apply_le_one (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (h : Core.Heap) : ∑' (p : Unit × Core.Heap), ⨆ (n : ℕ), (whileApprox guard body n h) (some p) ≤ 1

The total mass on values of the pointwise supremum over budgets is at most 1, so the supremum is a sub-probability assignment.