Documentation

CatCryptCore.NonUniform.WhileApprox

Bounded approximants of an unbounded loop #

whileApprox guard body n runs body at most n times, continuing while guard holds of the current heap, and fails when the budget is exhausted. It is the finite unrolling whose limit denotes while guard do body: the mass whileApprox guard body n assigns to a heap is the probability of reaching that heap and leaving the loop within n iterations.

Failure at zero is what makes the sequence increasing in n: a run that has not yet left the loop contributes no mass, so extending the budget can only add mass at a value, never move it.

The loop itself is the limit of this sequence, which is developed separately; this file fixes the approximants and their defining equations.

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

The n-step approximant of while guard do body: run body while guard holds, for at most n iterations, and fail if the budget runs out.

Equations
Instances For
    source
    @[simp]
    theorem CatCrypt.NonUniform.whileApprox_zero (guard : Core.Heap → Bool) (body : Core.SPComp Unit) :
    whileApprox guard body 0 = Core.SPComp.fail
    source
    theorem CatCrypt.NonUniform.whileApprox_succ (guard : Core.Heap → Bool) (body : Core.SPComp Unit) (n : ℕ) (h : Core.Heap) :
    whileApprox guard body (n + 1) h = if guard h = true then body.bind (fun (x : Unit) => whileApprox guard body n) h else Core.SPComp.pure () h
    source
    theorem CatCrypt.NonUniform.whileApprox_succ_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.bind (fun (x : Unit) => whileApprox guard body n) h
    source
    theorem CatCrypt.NonUniform.whileApprox_succ_of_not_guard {guard : Core.Heap → Bool} {body : Core.SPComp Unit} {h : Core.Heap} (hg : guard h = false) (n : ℕ) :
    whileApprox guard body (n + 1) h = Core.SPComp.pure () h