pRHL with couplings as the primitive judgment (CLAUDE.md subtask 3)

The candidate definition under evaluation:

prhl A c d B  :=  ∀ m₁ m₂, A (m₁, m₂) →
  ∃ μ, map fst μ = c m₁ ∧ map snd μ = d m₂ ∧ satisfy (μ, B)

Here ProgramDenotation.prhl A c d B := ∀ σ₁ σ₂, A σ₁ σ₂ → Nonempty (Coupling …), with ProgramDenotation.Coupling (PRHL/Coupling.lean) playing the role of the existential: its marg₁/marg₂ fields state the marginal conditions in expected-value form (Coupling.map_fst/map_snd below recover the literal map fst μ = c m₁ form), and its supp field is CertiCrypt's range-form of satisfy. SubProbability.satisfies below is the subtask's literal pointwise form ∀ x, μ x ≠ 0 → B x; the two are equivalent for discrete (countable) state — see satisfies_iff_range, whose → direction is exactly where countability is needed.

Evaluation findings (discrete setting)

• The textbook obstacle dissolves. In a general Giry-monad setting the seq rule needs a measurable choice of continuation couplings. With the ⊤ σ-algebra every function is measurable, so Classical.choice composes pointwise and Coupling.comp (below) proves prhl.bind with no side conditions. This is the rule that costs CertiCrypt/SSProve real infrastructure.
• Soundness is one line: prhl.to_relE via relE.of_coupling — every coupling-judgment yields the wp-lifting judgment, so all relE elimination forms (wp_eq, bad_eq, up_to_bad) apply to prhl.
• Open: completeness (discrete Strassen). The converse c.relE d A B → ProgramDenotation.prhl A c d B is true for countable state but amounts to a countable max-flow/min-cut (Hall) argument constructing a witness from the family of wp-inequalities; it is not formalized here. Until it is, prhl is a (possibly strictly) stronger judgment per instance, and the two logics interoperate one-way.
• Open: transitivity. Gluing two couplings along the common middle marginal needs discrete disintegration (division by the middle weights in ENNReal); deferred. The wp-lifting rel.trans needs nothing.
• Open: while. A coupling for a loop needs a fixed point of a coupling transformer; deferred (the wp-lifting rel.while_loop covers loops, and transports to prhl-provable goals via to_relE).

The judgment

def GaudisCrypt.ProgramDenotation.prhl {s₁ s₂ α β : Type} (A : s₁ → s₂ → Prop) (c : ProgramDenotation s₁ α) (d : ProgramDenotation s₂ β) (B : α × s₁ → β × s₂ → Prop) : Prop

Coupling-based pRHL (subtask-3 argument order: predicate, program, program, predicate).

Equations

• GaudisCrypt.ProgramDenotation.prhl A c d B = ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → Nonempty (c.Coupling d σ₁ σ₂ B)

The witness fields recover the literal subtask-3 conditions

theorem GaudisCrypt.SubProbability.ext_of_expected {γ : Type} {μ ν : SubProbability γ} (h : ∀ (f : γ → ENNReal), μ.expected f = ν.expected f) : μ = ν

Subprobabilities with equal expected values are equal.

theorem GaudisCrypt.ProgramDenotation.Coupling.map_fst {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {σ₁ : s₁} {σ₂ : s₂} {Post : α × s₁ → β × s₂ → Prop} (c : p.Coupling q σ₁ σ₂ Post) : (do let uv ← c.w pure uv.1) = p σ₁

map fst μ = c m₁, literally.

theorem GaudisCrypt.ProgramDenotation.Coupling.map_snd {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {σ₁ : s₁} {σ₂ : s₂} {Post : α × s₁ → β × s₂ → Prop} (c : p.Coupling q σ₁ σ₂ Post) : (do let uv ← c.w pure uv.2) = q σ₂

map snd μ = d m₂, literally.

theorem GaudisCrypt.ProgramDenotation.Coupling.expected_congr {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {σ₁ : s₁} {σ₂ : s₂} {Post : α × s₁ → β × s₂ → Prop} (c : p.Coupling q σ₁ σ₂ Post) {f g : (α × s₁) × β × s₂ → ENNReal} (h : ∀ (uv : (α × s₁) × β × s₂), Post uv.1 uv.2 → f uv = g uv) : c.w.expected f = c.w.expected g

Expected values agree for posts that agree on the support.

The pointwise satisfy and discreteness

Subtask 3 defines satisfy (μ, B) := ∀ x, μ x ≠ 0 → B x. The witness structure uses the range form instead (∀ f vanishing on B, ∫ f dμ = 0), which needs no decidability or countability. The two agree for discrete state — and the proof shows exactly where countability enters: only in the direction pointwise → range (summing the atoms).

def GaudisCrypt.SubProbability.satisfies {γ : Type} (μ : SubProbability γ) (B : γ → Prop) : Prop

The literal subtask-3 satisfy.

Equations

• μ.satisfies B = ∀ (x : γ), ↑μ {x} ≠ 0 → B x

theorem GaudisCrypt.SubProbability.satisfies_of_range {γ : Type} (μ : SubProbability γ) (B : γ → Prop) (h : ∀ (f : γ → ENNReal), (∀ (x : γ), B x → f x = 0) → μ.expected f = 0) : μ.satisfies B

Range form implies pointwise form — no countability needed.

theorem GaudisCrypt.SubProbability.range_of_satisfies {γ : Type} (μ : SubProbability γ) (B : γ → Prop) (h : μ.satisfies B) (f : γ → ENNReal) : (∀ (x : γ), B x → f x = 0) → μ.expected f = 0

Pointwise form implies range form — this is where discreteness is used: the integral is the sum of its atoms. Countability-free (subtask 4): via the discreteness invariant (lintegral_eq_tsum_smul) rather than lintegral_countable'.

theorem GaudisCrypt.SubProbability.satisfies_iff_range {γ : Type} (μ : SubProbability γ) (B : γ → Prop) : μ.satisfies B ↔ ∀ (f : γ → ENNReal), (∀ (x : γ), B x → f x = 0) → μ.expected f = 0

For discrete state the two satisfy formulations coincide.

Soundness with respect to the wp-lifting

theorem GaudisCrypt.ProgramDenotation.prhl.to_relE {s₁ s₂ α β : Type} {A : s₁ → s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {B : α × s₁ → β × s₂ → Prop} (h : prhl A c d B) : c.relE d A B

Every coupling judgment yields the (two-sided) wp-lifting judgment; all relE elimination forms transfer. The converse is discrete Strassen — see the module header.

Structural rules on the coupling judgment

theorem GaudisCrypt.ProgramDenotation.prhl.conseq {s₁ s₂ α β : Type} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {A' : s₁ → s₂ → Prop} {B' : α × s₁ → β × s₂ → Prop} (h : prhl A c d B) (hA : ∀ (σ₁ : s₁) (σ₂ : s₂), A' σ₁ σ₂ → A σ₁ σ₂) (hB : ∀ (u : α × s₁) (v : β × s₂), B u v → B' u v) : prhl A' c d B'

Consequence. The same witness works: the support condition only weakens.

theorem GaudisCrypt.ProgramDenotation.prhl.pure_pure {s₁ s₂ α β : Type} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} {x₁ : α} {x₂ : β} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B (x₁, σ₁) (x₂, σ₂)) : prhl A (pure x₁) (pure x₂) B

Two-sided pure.

noncomputable def GaudisCrypt.ProgramDenotation.prhl.diagCoupling {s γ : Type} (p : ProgramDenotation s γ) (σ : s) : p.Coupling p σ σ fun (u v : γ × s) => u = v

Diagonal coupling: any program relates to itself at equal states.

Equations

• GaudisCrypt.ProgramDenotation.prhl.diagCoupling p σ = { w := do let x ← p σ pure (x, x), marg₁ := ⋯, marg₂ := ⋯, supp := ⋯ }

theorem GaudisCrypt.ProgramDenotation.prhl.refl {s γ : Type} (p : ProgramDenotation s γ) : prhl Eq p p fun (u v : γ × s) => u = v

Reflexivity.

theorem GaudisCrypt.ProgramDenotation.prhl.uniform {s₁ s₂ : Type} {A : s₁ → s₂ → Prop} {α' β' : Type} [Fintype α'] [Nonempty α'] [Fintype β'] [Nonempty β'] (e : α' ≃ β') {B : α' × s₁ → β' × s₂ → Prop} (h : ∀ (t : α') (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B (t, σ₁) (e t, σ₂)) : prhl A ProgramDenotation.uniform ProgramDenotation.uniform B

The rnd rule: uniform samples coupled along a bijection.

theorem GaudisCrypt.ProgramDenotation.prhl.exists_pre {s₁ s₂ α β : Type} {B : α × s₁ → β × s₂ → Prop} {ι : Sort u_1} {A : ι → s₁ → s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} (h : ∀ (i : ι), prhl (A i) c d B) : prhl (fun (σ₁ : s₁) (σ₂ : s₂) => ∃ (i : ι), A i σ₁ σ₂) c d B

Case split / existential / disjunction on the precondition.

theorem GaudisCrypt.ProgramDenotation.prhl.or_pre {s₁ s₂ α β : Type} {B : α × s₁ → β × s₂ → Prop} {A₁ A₂ : s₁ → s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} (h₁ : prhl A₁ c d B) (h₂ : prhl A₂ c d B) : prhl (fun (σ₁ : s₁) (σ₂ : s₂) => A₁ σ₁ σ₂ ∨ A₂ σ₁ σ₂) c d B

The seq rule (the crux of the evaluation)

In a general measure-theoretic setting this rule requires a measurable selection of continuation couplings — the main technical burden of coupling-based pRHL semantics. With the ⊤ σ-algebra, every function is measurable, so a plain Classical.choice per support point suffices and the composite below typechecks with no side conditions.

noncomputable def GaudisCrypt.ProgramDenotation.Coupling.comp {s₁ s₂ α₁ α₂ β₁ β₂ : Type} {p₁ : ProgramDenotation s₁ α₁} {p₂ : ProgramDenotation s₂ α₂} {k₁ : α₁ → ProgramDenotation s₁ β₁} {k₂ : α₂ → ProgramDenotation s₂ β₂} {σ₁ : s₁} {σ₂ : s₂} {M : α₁ × s₁ → α₂ × s₂ → Prop} {B : β₁ × s₁ → β₂ × s₂ → Prop} (μ : p₁.Coupling p₂ σ₁ σ₂ M) (ν : (u : α₁ × s₁) → (v : α₂ × s₂) → M u v → (k₁ u.1).Coupling (k₂ v.1) u.2 v.2 B) : (p₁ >>= k₁).Coupling (p₂ >>= k₂) σ₁ σ₂ B

Composition of couplings through bind: a coupling for the prefixes plus a coupling for the continuations at every support point yields a coupling for the composites.

Equations

• μ.comp ν = { w := do let uv ← μ.w if h : M uv.1 uv.2 then (ν uv.1 uv.2 h).w else ⊥, marg₁ := ⋯, marg₂ := ⋯, supp := ⋯ }

theorem GaudisCrypt.ProgramDenotation.prhl.bind {s₁ s₂ α₁ α₂ β₁ β₂ : Type} {p₁ : ProgramDenotation s₁ α₁} {p₂ : ProgramDenotation s₂ α₂} {k₁ : α₁ → ProgramDenotation s₁ β₁} {k₂ : α₂ → ProgramDenotation s₂ β₂} {A : s₁ → s₂ → Prop} {M : α₁ × s₁ → α₂ × s₂ → Prop} {B : β₁ × s₁ → β₂ × s₂ → Prop} (h₁ : prhl A p₁ p₂ M) (h₂ : ∀ (x₁ : α₁) (x₂ : α₂), prhl (fun (τ₁ : s₁) (τ₂ : s₂) => M (x₁, τ₁) (x₂, τ₂)) (k₁ x₁) (k₂ x₂) B) : prhl A (p₁ >>= k₁) (p₂ >>= k₂) B

The seq rule.

Footprint rules: almost-sure unary facts strengthen the post

noncomputable def GaudisCrypt.ProgramDenotation.Coupling.strengthen_left {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {σ₁ : s₁} {σ₂ : s₂} {Post : α × s₁ → β × s₂ → Prop} {C : α × s₁ → Prop} [DecidablePred C] (c : p.Coupling q σ₁ σ₂ Post) (hC : p.wp (fun (u : α × s₁) => if C u then 0 else 1) σ₁ = 0) : p.Coupling q σ₁ σ₂ fun (u : α × s₁) (v : β × s₂) => Post u v ∧ C u

Strengthen the post with an almost-sure left-side fact (the witness is unchanged; only the support condition is rebalanced). This is how inRange-style footprint facts enter the coupling logic.

Equations

• c.strengthen_left hC = { w := c.w, marg₁ := ⋯, marg₂ := ⋯, supp := ⋯ }

Smoke tests