Event Probability for Unary Computations

This file defines the probability of events for single computations, bridging pHL judgments to actual probability bounds.

Main definitions

• prEvent d E - Probability that event E holds under sub-distribution d
• prEventComp c h₀ E - Probability that event E holds for computation c starting from heap h₀

Main results

• prEvent_le_mass - Event probability is at most the total mass
• prEvent_complement - Complementary event probabilities sum to 1 (when mass = 1)
• prEvent_union_le - Union bound: Pr[E₁ ∨ E₂] ≤ Pr[E₁] + Pr[E₂]
• prEvent_mono - Monotonicity of event probability
• prEvent_of_pHoare - If all outcomes satisfy E, then Pr[E] = mass
• prEvent_zero_of_pHoare_neg - If no outcome satisfies E, then Pr[E] = 0

References

• EasyCrypt pHL (unary probabilistic Hoare logic)
• CatCrypt.Unary.Judgment (pHL judgment definition)

noncomputable def CatCrypt.Unary.prEvent {α : Type u_1} (d : Prob.SDistr (α × Core.Heap)) (E : α → Core.Heap → Prop) : ENNReal

Probability of an event E under a sub-distribution over (value, heap) pairs. This sums the probability of all outcomes satisfying the predicate.

Equations

• CatCrypt.Unary.prEvent d E = ∑' (p : α × CatCrypt.Core.Heap), if E p.1 p.2 then d (some p) else 0

noncomputable def CatCrypt.Unary.prEventComp {α : Type u_1} (c : Core.SPComp α) (h₀ : Core.Heap) (E : α → Core.Heap → Prop) : ENNReal

Probability of an event for a computation from a given initial heap

Equations

• CatCrypt.Unary.prEventComp c h₀ E = CatCrypt.Unary.prEvent (c h₀) E

theorem CatCrypt.Unary.prEvent_le_mass {α : Type u_1} (d : Prob.SDistr (α × Core.Heap)) (E : α → Core.Heap → Prop) : prEvent d E ≤ d.mass

Event probability is at most the total mass. This holds because prEvent sums over a subset of outcomes (those satisfying E), while mass sums over all outcomes.

theorem CatCrypt.Unary.prEvent_complement {α : Type u_1} (d : Prob.SDistr (α × Core.Heap)) (E : α → Core.Heap → Prop) (hmass : d.mass = 1) : (prEvent d E + prEvent d fun (a : α) (h : Core.Heap) => ¬E a h) = 1

Complementary events: if mass = 1, Pr[E] + Pr[not E] = 1. Every outcome satisfies exactly one of E or not E, so their probabilities partition the total mass.

theorem CatCrypt.Unary.prEvent_union_le {α : Type u_1} (d : Prob.SDistr (α × Core.Heap)) (E₁ E₂ : α → Core.Heap → Prop) : (prEvent d fun (a : α) (h : Core.Heap) => E₁ a h ∨ E₂ a h) ≤ prEvent d E₁ + prEvent d E₂

Union bound: Pr[E₁ ∨ E₂] ≤ Pr[E₁] + Pr[E₂]. Standard inclusion-exclusion upper bound.

theorem CatCrypt.Unary.prEvent_mono {α : Type u_1} (d : Prob.SDistr (α × Core.Heap)) (E₁ E₂ : α → Core.Heap → Prop) (h : ∀ (a : α) (h : Core.Heap), E₁ a h → E₂ a h) : prEvent d E₁ ≤ prEvent d E₂

Monotonicity: if E₁ → E₂, then Pr[E₁] ≤ Pr[E₂]

theorem CatCrypt.Unary.prEvent_true {α : Type u_1} (d : Prob.SDistr (α × Core.Heap)) : (prEvent d fun (x : α) (x_1 : Core.Heap) => True) = d.mass

True event has probability equal to mass. Since every outcome satisfies True, the sum is over all outcomes.

theorem CatCrypt.Unary.prEvent_false {α : Type u_1} (d : Prob.SDistr (α × Core.Heap)) : (prEvent d fun (x : α) (x_1 : Core.Heap) => False) = 0

False event has probability 0

theorem CatCrypt.Unary.prEvent_of_pHoare {α : Type u_1} {P : UPre} {c : Core.SPComp α} {E : α → Core.Heap → Prop} (hph : ∀ (h₀ : Core.Heap), P h₀ → ∀ (a : α) (h' : Core.Heap), (c h₀) (some (a, h')) ≠ 0 → E a h') (h₀ : Core.Heap) (hP : P h₀) : prEvent (c h₀) E = (c h₀).mass

If pHoare says all outcomes satisfy E (and computation is lossless), Pr[E] = mass. When every nonzero-probability outcome satisfies E, the filtered sum equals the unfiltered sum.

theorem CatCrypt.Unary.prEvent_zero_of_pHoare_neg {α : Type u_1} {P : UPre} {c : Core.SPComp α} {E : α → Core.Heap → Prop} (hph : ∀ (h₀ : Core.Heap), P h₀ → ∀ (a : α) (h' : Core.Heap), (c h₀) (some (a, h')) ≠ 0 → ¬E a h') (h₀ : Core.Heap) (hP : P h₀) : prEvent (c h₀) E = 0

If pHoare says no outcomes satisfy E, Pr[E] = 0. Every term in the sum is 0: either E doesn't hold (if-branch gives 0) or the probability is 0 (by the pHoare hypothesis).