Losslessness for Stateful Probabilistic Computations

This file defines the isLossless predicate for SPComp computations and proves that basic operations (pure, get, set, sample) are lossless, while fail is not.

A computation is lossless if it has total mass 1 from any initial heap, meaning it never fails (never produces the none outcome in the underlying sub-distribution).

Main definitions

• isLossless - Unconditional losslessness: mass 1 from every heap
• isLosslessIf - Conditional losslessness: mass 1 from heaps satisfying a precondition

Main results

• lossless_pure - pure a is lossless
• lossless_get - get l is lossless
• lossless_set - set l v is lossless
• lossless_sample - sample α is lossless (for finite nonempty types)
• not_lossless_fail - fail is not lossless
• lossless_bind - bind preserves losslessness

References

• EasyCrypt: islossless predicate on distributions
• SSProve (Rocq): lossless reasoning in pHL

Losslessness predicates

def CatCrypt.Unary.isLossless {α : Type u_1} (c : Core.SPComp α) : Prop

A computation is lossless if it has total mass 1 from any initial heap. This means the computation never fails.

Equations

• CatCrypt.Unary.isLossless c = ∀ (h : CatCrypt.Core.Heap), (c h).mass = 1

def CatCrypt.Unary.isLosslessIf {α : Type u_1} (P : UPre) (c : Core.SPComp α) : Prop

Lossless with precondition: only requires mass 1 from heaps satisfying P.

Equations

• CatCrypt.Unary.isLosslessIf P c = ∀ (h : CatCrypt.Core.Heap), P h → (c h).mass = 1

Relationship between isLossless and isLosslessIf

theorem CatCrypt.Unary.isLossless_implies_if {α : Type u_1} (P : UPre) {c : Core.SPComp α} (h : isLossless c) : isLosslessIf P c

Unconditional losslessness implies conditional losslessness for any P.

theorem CatCrypt.Unary.isLosslessIf_truePre {α : Type u_1} {c : Core.SPComp α} : isLosslessIf truePre c ↔ isLossless c

Conditional losslessness with truePre is equivalent to unconditional.

Losslessness of basic operations

theorem CatCrypt.Unary.lossless_pure {α : Type u_1} (a : α) : isLossless (Core.SPComp.pure a)

pure a is lossless: returning a value never fails.

theorem CatCrypt.Unary.lossless_get (l : Core.Location) : isLossless (Core.SPComp.get l)

get l is lossless: reading from a location never fails.

theorem CatCrypt.Unary.lossless_set (l : Core.Location) (v : l.ty) : isLossless (Core.SPComp.set l v)

set l v is lossless: writing to a location never fails.

theorem CatCrypt.Unary.not_lossless_fail {α : Type u_1} : ¬isLossless Core.SPComp.fail

fail is not lossless: it always fails (mass 0).

theorem CatCrypt.Unary.mass_fail_eq_zero {α : Type u_1} (h : Core.Heap) : (Core.SPComp.fail h).mass = 0

The mass of fail is 0, as an explicit lemma for use in proofs.

Helper lemmas for mass reasoning

Losslessness of sample

theorem CatCrypt.Unary.lossless_sample {α : Type u_1} [Fintype α] [Nonempty α] : isLossless (Core.SPComp.sample α)

sample α is lossless: sampling from a finite nonempty type never fails.

Losslessness of bind

theorem CatCrypt.Unary.lossless_bind {α : Type u_1} {β : Type u_2} {c : Core.SPComp α} {f : α → Core.SPComp β} (hc : isLossless c) (hf : ∀ (a : α), isLossless (f a)) : isLossless (c.bind f)

Bind preserves losslessness: if c is lossless and f a is lossless for all a, then c.bind f is lossless.

Proof idea: We need to show (c h).bind (fun (a, h') => f a h') none = 0. Since c is lossless, (c h) none = 0, so the none-to-none path contributes 0. For each (a, h') in the support of c h, f a h' is lossless, so (f a h') none = 0, meaning the some-to-none path also contributes 0.

theorem CatCrypt.Unary.lossless_bind_of_support {α : Type u_1} {β : Type u_2} {c : Core.SPComp α} {f : α → Core.SPComp β} (hc : isLossless c) (hf : ∀ (h : Core.Heap) (a : α) (h' : Core.Heap), (c h) (some (a, h')) ≠ 0 → isLossless (f a)) : isLossless (c.bind f)

Variant of lossless_bind with conditional losslessness for the continuation. The continuation only needs to be lossless for outcomes actually produced by c.

Derived losslessness lemmas

theorem CatCrypt.Unary.lossless_assert_of (P : Prop) [Decidable P] (hp : P) : isLossless (Core.SPComp.assert P)

Assert is lossless when the condition holds.

theorem CatCrypt.Unary.not_lossless_assert_of_not (P : Prop) [Decidable P] (hp : ¬P) : ¬isLossless (Core.SPComp.assert P)

Assert is not lossless when the condition fails.

theorem CatCrypt.Unary.lossless_seq {α : Type u_1} {β : Type u_2} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} (h₁ : isLossless c₁) (h₂ : isLossless c₂) : isLossless (c₁.seq c₂)

Sequential composition preserves losslessness.