Unary rules for sampling from an arbitrary distribution

Event and success probabilities of a program that starts with sampleFrom d average the continuation's probabilities against the weights d (some a).

Main results

• sampleFrom_bind_apply_some — the pointwise mass of sampleFrom d >>= k
• prEvent_pure_indicator — event probability of a point mass
• prEvent_sampleFrom_bind — Pr[E] = ∑' a, d a * Pr[E after k a]
• prTrue_bind_sampleFrom — the same for the prTrue of a Boolean game
• prTrue_bind_sample_of_sampleFrom — Crypto.prTrue_bind_sample re-derived as the uniform instance, with the statement of the existing lemma verbatim
• mass_bind_sampleFrom — mass averages the same way

Pointwise mass

theorem CatCrypt.NonUniform.sampleFrom_bind_apply_some {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (k : α → Core.SPComp β) (h₀ : Core.Heap) (p : β × Core.Heap) : ((sampleFrom d).bind k h₀) (some p) = ∑' (a : α), d (some a) * (k a h₀) (some p)

The probability that sampleFrom d >>= k produces the outcome p is the d-average of the continuation's probabilities of producing p.

theorem CatCrypt.NonUniform.sampleFrom_bind_apply_none {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (k : α → Core.SPComp β) (h₀ : Core.Heap) : ((sampleFrom d).bind k h₀) none = d none + ∑' (a : α), d (some a) * (k a h₀) none

The failure probability of sampleFrom d >>= k is the failure probability of d plus the d-average of the continuations' failure probabilities.

Event probability

theorem CatCrypt.NonUniform.prEvent_pure_indicator {α : Type u_1} (a : α) (h₀ : Core.Heap) (E : α → Core.Heap → Prop) : Unary.prEvent (Prob.SDistr.pure (a, h₀)) E = if E a h₀ then 1 else 0

Event probability of a point mass is the indicator of the event. Generalizes Unary.prEvent_pure, whose event depends on the heap only.

theorem CatCrypt.NonUniform.prEvent_pure_comp {α : Type u_1} (a : α) (h₀ : Core.Heap) (E : α → Core.Heap → Prop) : Unary.prEvent (Core.SPComp.pure a h₀) E = if E a h₀ then 1 else 0

prEvent_pure_indicator in the SPComp form used by the averaging rule.

theorem CatCrypt.NonUniform.prEvent_sampleFrom_bind {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (k : α → Core.SPComp β) (h₀ : Core.Heap) (E : β → Core.Heap → Prop) : Unary.prEvent ((sampleFrom d).bind k h₀) E = ∑' (a : α), d (some a) * Unary.prEvent (k a h₀) E

Average-over-the-distribution characterisation of the event probability of a program that starts with a general sample.

theorem CatCrypt.NonUniform.prEvent_sampleFrom {α : Type u_1} (d : Prob.SDistr α) (h₀ : Core.Heap) (E : α → Core.Heap → Prop) : Unary.prEvent (sampleFrom d h₀) E = ∑' (a : α), if E a h₀ then d (some a) else 0

Event probability of a bare general sample: the heap is unchanged, so the event is decided by the sampled value alone.

Success probability of a Boolean game

theorem CatCrypt.NonUniform.prTrue_bind_sampleFrom {α : Type u_1} (d : Prob.SDistr α) (k : α → Core.SPComp Bool) (h₀ : Core.Heap) : Crypto.prTrue ((sampleFrom d).bind k) h₀ = ∑' (a : α), d (some a) * Crypto.prTrue (k a) h₀

Average-over-the-distribution characterisation of the success probability of a Boolean game that starts with a general sample.

theorem CatCrypt.NonUniform.prTrue_sampleFrom (d : Prob.SDistr Bool) (h₀ : Core.Heap) : Crypto.prTrue (sampleFrom d) h₀ = d (some true)

Success probability of a bare general Boolean sample.

Mass

theorem CatCrypt.NonUniform.mass_bind_sampleFrom {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (k : α → Core.SPComp β) (h₀ : Core.Heap) (hk : ∀ (a : α), (k a h₀).mass = 1) : ((sampleFrom d).bind k h₀).mass = d.mass

If every continuation is lossless, the mass of sampleFrom d >>= k is the mass of d.

The uniform instance

theorem CatCrypt.NonUniform.prTrue_bind_sample_of_sampleFrom {α : Type u_3} [Fintype α] [Nonempty α] (F : α → Core.SPComp Bool) (h₀ : Core.Heap) : Crypto.prTrue ((Core.SPComp.sample α).bind F) h₀ = ∑ x : α, (↑(Fintype.card α))⁻¹ * Crypto.prTrue (F x) h₀

Crypto.prTrue_bind_sample derived from prTrue_bind_sampleFrom.