pRHL sampling rules for arbitrary distributions

The Prob/Coupling.lean notion liftR R d₁ d₂ — a joint sub-distribution with marginals d₁, d₂ whose support lies in R — is already stated for arbitrary SDistr. The rules here consume such a coupling directly, so a pRHL sampling step is available for any pair of distributions, not just uniform ones.

Main results

• rHoare_coupling_step — the general two-sided sampling rule: a coupling of d₁ and d₂ plus the pointwise premise on the continuations gives rHoare Φ (sampleFrom d₁ >>= k₁) (sampleFrom d₂ >>= k₂) Ψ
• rHoare_coupling — bare form, no continuations
• rHoare_bij_step_of_coupling, rHoare_same_step_of_coupling, rHoare_sample_vs_sample_coupling_of_coupling — the uniform rules of Relational/Rules.lean and Relational/Sync.lean re-derived as instances, each with the statement of the existing rule verbatim
• rHoare_sampleFrom_l, rHoare_sampleFrom_r — one-sided rules, requiring the discarded distribution to be total
• eq_of_rHoare_eqPost — a full-equality judgment identifies the output sub-distributions

Pushforward couplings

Prob/Coupling.lean provides liftR_uniform_bij, which couples two uniform distributions along a bijection. Bijectivity is used there only to identify the pushforward of SDistr.uniform α with SDistr.uniform β; the coupling itself exists for an arbitrary function and an arbitrary distribution.

noncomputable def CatCrypt.NonUniform.Coupling.graph {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (f : α → β) : Prob.Coupling d (d.bind fun (a : α) => Prob.SDistr.pure (f a))

Graph coupling: an arbitrary function f couples d with its pushforward along f, the joint distribution being supported on the graph of f.

Equations

• CatCrypt.NonUniform.Coupling.graph d f = { joint := d.bind fun (a : α) => CatCrypt.Prob.SDistr.pure (a, f a), left_marginal := ⋯, right_marginal := ⋯ }

theorem CatCrypt.NonUniform.liftR_graph {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (f : α → β) : d ⟨fun (a : α) (b : β) => f a = b⟩# d.bind fun (a : α) => Prob.SDistr.pure (f a)

The graph coupling lifts the graph relation of f.

theorem CatCrypt.NonUniform.liftR_pushforward {α : Type u_1} {β : Type u_2} {d : Prob.SDistr α} {e : Prob.SDistr β} {f : α → β} (h : (d.bind fun (a : α) => Prob.SDistr.pure (f a)) = e) : d ⟨fun (a : α) (b : β) => f a = b⟩# e

If the pushforward of d along f is e, then f's graph relation lifts to d and e.

theorem CatCrypt.NonUniform.liftR_uniform_bij_of_pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (f : α ≃ β) : Prob.SDistr.uniform α ⟨fun (a : α) (b : β) => f a = b⟩# Prob.SDistr.uniform β

Prob.liftR_uniform_bij derived from liftR_pushforward: a bijection's only role is to make the pushforward of uniform uniform again.

The general two-sided rule

theorem CatCrypt.NonUniform.rHoare_coupling_step {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {Φ : Relational.RPre} {Ψ : Relational.RPost γ δ} {R : α → β → Prop} {d₁ : Prob.SDistr α} {d₂ : Prob.SDistr β} (hd : d₁ ⟨R⟩# d₂) {k₁ : α → Core.SPComp γ} {k₂ : β → Core.SPComp δ} (hk : ∀ (a : α) (b : β), R a b → Relational.rHoare Φ (k₁ a) (k₂ b) Ψ) : Relational.rHoare Φ ((sampleFrom d₁).bind k₁) ((sampleFrom d₂).bind k₂) Ψ

Sampling rule for two arbitrary distributions related by a coupling.

Given a coupling of d₁ and d₂ supported in R, and continuations that are related whenever their arguments are R-related, the two sampling programs are related. Specialising d₁ = d₂ = SDistr.uniform and R to the graph of a bijection recovers rHoare_bij_step; see rHoare_bij_step_of_coupling.

theorem CatCrypt.NonUniform.rHoare_coupling {α : Type u_1} {β : Type u_2} {Φ : Relational.RPre} {R : α → β → Prop} {d₁ : Prob.SDistr α} {d₂ : Prob.SDistr β} (hd : d₁ ⟨R⟩# d₂) : Relational.rHoare Φ (sampleFrom d₁) (sampleFrom d₂) fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ R a b

Bare form of rHoare_coupling_step: the coupling relation appears in the postcondition alongside the preserved precondition.

theorem CatCrypt.NonUniform.rHoare_sampleFrom_same {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {Φ : Relational.RPre} {Ψ : Relational.RPost γ δ} (d : Prob.SDistr α) {k₁ : α → Core.SPComp γ} {k₂ : α → Core.SPComp δ} (hk : ∀ (a : α), Relational.rHoare Φ (k₁ a) (k₂ a) Ψ) : Relational.rHoare Φ ((sampleFrom d).bind k₁) ((sampleFrom d).bind k₂) Ψ

Same distribution on both sides, diagonal coupling.

The uniform rules as instances

Each rule below restates a uniform rule already in the library and proves it from rHoare_coupling_step. The example after each one equates the two constants, so the kernel checks that the restatement is the same proposition.

theorem CatCrypt.NonUniform.rHoare_bij_step_of_coupling {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} {Φ : Relational.RPre} {Ψ : Relational.RPost γ δ} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (f : α ≃ β) {k₁ : α → Core.SPComp γ} {k₂ : β → Core.SPComp δ} (h : ∀ (a : α), Relational.rHoare Φ (k₁ a) (k₂ (f a)) Ψ) : Relational.rHoare Φ ((Core.SPComp.sample α).bind k₁) ((Core.SPComp.sample β).bind k₂) Ψ

Relational.rHoare_bij_step derived from rHoare_coupling_step. SPComp.sample α is sampleFrom (SDistr.uniform α) by definition, and liftR_uniform_bij supplies the coupling.

theorem CatCrypt.NonUniform.rHoare_same_step_of_coupling {α : Type u_5} {γ : Type u_6} {δ : Type u_7} {Φ : Relational.RPre} {Ψ : Relational.RPost γ δ} [Fintype α] [Nonempty α] {k₁ : α → Core.SPComp γ} {k₂ : α → Core.SPComp δ} (h : ∀ (a : α), Relational.rHoare Φ (k₁ a) (k₂ a) Ψ) : Relational.rHoare Φ ((Core.SPComp.sample α).bind k₁) ((Core.SPComp.sample α).bind k₂) Ψ

Relational.rHoare_same_step derived from rHoare_coupling_step.

theorem CatCrypt.NonUniform.r_sample_vs_sample_coupling_of_coupling {Φ : Relational.RPre} (α : Type u_5) (β : Type u_6) [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (R : α → β → Prop) (hCoupling : Prob.SDistr.uniform α ⟨R⟩# Prob.SDistr.uniform β) : Relational.rHoare Φ (Core.SPComp.sample α) (Core.SPComp.sample β) fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ R a b

Relational.r_sample_vs_sample_coupling derived from rHoare_coupling. That rule takes a coupling of two uniform distributions; here the uniformity is only used to name the programs.

One-sided rules

A one-sided rule averages the other side over the sampled distribution, so the sampled distribution must be total: if SDistr.mass d < 1 the left program has strictly smaller mass than the right and no coupling exists.

theorem CatCrypt.NonUniform.rHoare_sampleFrom_l {σ : Type u_5} {τ : Type u_6} {ρ : Type u_7} {Φ : Relational.RPre} {Ψ : Relational.RPost τ ρ} {d : Prob.SDistr σ} (hd : d.mass = 1) {c₂ : Core.SPComp ρ} {f : σ → Core.SPComp τ} (h : ∀ (a : σ), Relational.rHoare Φ (f a) c₂ Ψ) : Relational.rHoare Φ ((sampleFrom d).bind f) c₂ Ψ

One-sided sample on the left, for a total distribution.

theorem CatCrypt.NonUniform.rHoare_sampleFrom_r {σ : Type u_5} {τ : Type u_6} {ρ : Type u_7} {Φ : Relational.RPre} {Ψ : Relational.RPost ρ τ} {d : Prob.SDistr σ} (hd : d.mass = 1) {c₁ : Core.SPComp ρ} {f : σ → Core.SPComp τ} (h : ∀ (a : σ), Relational.rHoare Φ c₁ (f a) Ψ) : Relational.rHoare Φ c₁ ((sampleFrom d).bind f) Ψ

One-sided sample on the right, for a total distribution.

From a full-equality judgment to distribution equality

theorem CatCrypt.NonUniform.eq_of_rHoare_eqPost {α : Type u_1} {c₁ c₂ : Core.SPComp α} (h : Relational.rHoare Relational.eqPre c₁ c₂ Relational.eqPost) (h₀ : Core.Heap) : c₁ h₀ = c₂ h₀

A judgment with eqPre/eqPost says the two programs have the same output sub-distribution from every heap: an equality coupling forces all mass onto the diagonal, and the two marginals then agree.