pRHL, version 2 — the literal explicit-coupling judgment

This module develops the candidate pRHL definition from CLAUDE.md subtask 3 in its most literal form and shows it delivers the same rule set as the existing ProgramDenotation.prhl (PRHL/Prhl.lean).

The difference from ProgramDenotation.prhl

ProgramDenotation.prhl packages the coupling existential inside the ProgramDenotation.Coupling structure, whose marginals are stated in expected-value form (∀ F, μ.expected (F ∘ fst) = c.wp F σ₁) and whose support uses the range form (∀ f vanishing on B, ∫ f dμ = 0).

ProgramDenotation.prhl2 instead spells out the existential directly, exactly as in the subtask-3 text:

prhl2 A c d B := ∀ σ₁ σ₂, A σ₁ σ₂ →
  ∃ μ, map fst μ = c σ₁ ∧ map snd μ = d σ₂ ∧ satisfy μ B

with the marginals as distribution equality (map fst μ = c σ₁, written μ >>= fun x => pure x.1 = c σ₁) and the support as the pointwise SubProbability.satisfies (∀ x, μ {x} ≠ 0 → B x).

What this buys

The two formulations are interderivable, so prhl2 inherits every rule:

• ProgramDenotation.prhl.to_prhl2 (forward) recovers the distribution-equality marginals via Coupling.map_fst/map_snd, and satisfies_of_range turns the range support into the pointwise one.
• ProgramDenotation.prhl2.to_prhl (backward) reads the pointwise satisfies back as the range form because the integral is the sum of its atoms (range_of_satisfies).

Originally the backward direction (and every rule consuming a coupling) carried a [Countable] hypothesis: the atom-sum identity was lintegral_countable'. Since subtask 4 this is gone — the SubProbability discreteness invariant gives the atom-sum (lintegral_eq_tsum_smul), the marginals (discreteMeasure_measure_iUnion), and the sampling swap (lintegral_lintegral_swap_discrete) with no countability of the carriers. So prhl2 and all its rules are now countability-free.

Universes

As in Language/Footprint.lean: states live in Type (max u v) and results in Type v, here for both sides of a judgment, so that a side α × s₁ and the joint (α × s₁) × (β × s₂) share one universe and the marginals are plain >>=. A state in Type 1 with results in Type is covered. The SubProbability helpers are stated in a single universe u; where a sampled value is bound directly into the state (toProgram_bind_apply, swap_sample, rnd) the bind is SubProbability.hbind. The rules that chain a Unit-valued program with the results (prefix_*, cond, the lossless-tail rules) keep the results in Type.

The judgment

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

Literal coupling-based pRHL: the subtask-3 existential, with marginals as distribution equality and support as the pointwise SubProbability.satisfies.

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.SubProbability.expected_map {γ δ : Type u} (μ : SubProbability γ) (g : γ → δ) (F : δ → ENNReal) : (do let x ← μ pure (g x)).expected F = μ.expected fun (x : γ) => F (g x)

Pushforward of expected along a deterministic map: integrating F against map g μ is integrating F ∘ g against μ. The workhorse for manipulating the literal map-marginals.

Discrete disintegration toolkit (for trans)

Over countable carriers (the ⊤ σ-algebra) a SubProbability is determined by its atom weights, and the integral is a countable sum of atoms. These helpers let us build the glued coupling for transitivity as an explicit atomic measure and reason about its marginals by tsum algebra.

theorem GaudisCrypt.SubProbability.expected_eq_tsum {T : Type u} (μ : SubProbability T) (F : T → ENNReal) : μ.expected F = ∑' (t : T), F t * ↑μ {t}

Integral as a sum of atoms. Countability-free (subtask 4): via the discreteness invariant (lintegral_eq_tsum_smul) rather than lintegral_countable'.

noncomputable def GaudisCrypt.SubProbability.ofWeights {T : Type u} (w : T → ENNReal) (h : ∑' (t : T), w t ≤ 1) : SubProbability T

An atomic sub-probability built from a summable weight function.

Equations

• GaudisCrypt.SubProbability.ofWeights w h = ⟨MeasureTheory.Measure.sum fun (t : T) => w t • MeasureTheory.Measure.dirac t, ⋯⟩

theorem GaudisCrypt.SubProbability.ofWeights_expected {T : Type u} (w : T → ENNReal) (h : ∑' (t : T), w t ≤ 1) (F : T → ENNReal) : (ofWeights w h).expected F = ∑' (t : T), F t * w t

The integral against an atomic measure is the weighted sum.

theorem GaudisCrypt.SubProbability.marginal_fst_singleton {A B : Type u} (μ : SubProbability (A × B)) (a : A) : ↑(do let w ← μ pure w.1) {a} = ∑' (b : B), ↑μ {(a, b)}

A left-marginal atom is the sum of the joint atoms over the fiber. Countability-free (subtask 4): discreteMeasure_measure_iUnion instead of measure_iUnion.

theorem GaudisCrypt.SubProbability.marginal_snd_singleton {A B : Type u} (μ : SubProbability (A × B)) (b : B) : ↑(do let w ← μ pure w.2) {b} = ∑' (a : A), ↑μ {(a, b)}

A right-marginal atom is the sum of the joint atoms over the fiber. Countability-free (subtask 4): discreteMeasure_measure_iUnion instead of measure_iUnion.

theorem GaudisCrypt.SubProbability.tsum_singleton_le_one {T : Type u} (ν : SubProbability T) : ∑' (t : T), ↑ν {t} ≤ 1

The atom weights of a sub-probability sum to at most one. Countability-free (subtask 4): ∑' t, ν{t} = ν univ directly from the discreteness invariant at univ.

Bind algebra and fixed-point helpers (for while_loop)

theorem GaudisCrypt.SubProbability.toProgram_apply {s α : Type u} (μ : SubProbability α) (σ : s) : μ.toProgramDenotation σ = do let a ← μ pure (a, σ)

A lifted sampling unfolded at a state.

theorem GaudisCrypt.SubProbability.toProgram_bind_apply {s : Type w} {α γ : Type v} (μ : SubProbability α) (K : α → ProgramDenotation s γ) (σ : s) : (μ.toProgramDenotation >>= K) σ = μ.hbind fun (a : α) => K a σ

A lifted sampling threads the state unchanged: (sample; K) σ = μ.hbind K(·,σ) (hbind: the state may live in a different universe from the sampled values).

theorem GaudisCrypt.SubProbability.bind_comm {α β γ : Type u} (μ : SubProbability α) (ν : SubProbability β) (f : α → β → SubProbability γ) : (do let x ← μ let y ← ν f x y) = do let y ← ν let x ← μ f x y

Commutativity of independent sampling (Tonelli): two state-free samplings can be drawn in either order.

theorem GaudisCrypt.SubProbability.swap_sample {s : Type w} {α' β' γ : Type v} (μ : SubProbability α') (ν : SubProbability β') (k : α' → β' → ProgramDenotation s γ) : (do let x ← μ.toProgramDenotation let y ← ν.toProgramDenotation k x y) = do let y ← ν.toProgramDenotation let x ← μ.toProgramDenotation k x y

Swap two independent (state-free) samplings in a program.

theorem GaudisCrypt.SubProbability.bind_fst_left {A B C : Type u} (μ : SubProbability (A × B)) (H : A → SubProbability C) : (do let ab ← μ H ab.1) = (do let ab ← μ pure ab.1) >>= H

A bind whose continuation reads only the first coordinate factors through the first marginal.

theorem GaudisCrypt.SubProbability.bind_snd_left {A B C : Type u} (μ : SubProbability (A × B)) (H : B → SubProbability C) : (do let ab ← μ H ab.2) = (do let ab ← μ pure ab.2) >>= H

A bind whose continuation reads only the second coordinate factors through the second marginal.

theorem GaudisCrypt.SubProbability.bind_congr_support {A C : Type u} (μ : SubProbability A) {F F' : A → SubProbability C} (h : ∀ (a : A), ↑μ {a} ≠ 0 → F a = F' a) : μ >>= F = μ >>= F'

Two binds with continuations agreeing on the support are equal.

theorem GaudisCrypt.SubProbability.expected_lfp_eq_iSup {a : Type u_1} {b : a → Type u} (F : ((x : a) → SubProbability (b x)) →𝒄 (x : a) → SubProbability (b x)) (y : a) (g : b y → ENNReal) : (F.lfp y).expected g = ⨆ (n : ℕ), ((⇑F)^[n] ⊥ y).expected g

The integral against a least fixed point is the supremum of the integrals against the Kleene iterates (monotone convergence).

theorem GaudisCrypt.SubProbability.satisfies_lfp {a : Type u_1} {b : a → Type u} (F : ((x : a) → SubProbability (b x)) →𝒄 (x : a) → SubProbability (b x)) (y : a) (B : b y → Prop) (h : ∀ (n : ℕ), ((⇑F)^[n] ⊥ y).satisfies B) : (F.lfp y).satisfies B

If every Kleene iterate is supported in B, so is the least fixed point.

theorem GaudisCrypt.SubProbability.satisfies_bot {C : Type u} (B : C → Prop) : ⊥.satisfies B

The zero sub-probability is supported anywhere (vacuously).

theorem GaudisCrypt.SubProbability.satisfies_pure {C : Type u} (x : C) (B : C → Prop) (hB : B x) : (pure x).satisfies B

A point mass is supported at its point.

theorem GaudisCrypt.SubProbability.satisfies_bind {A C : Type u} (μ : SubProbability A) {F : A → SubProbability C} {B : C → Prop} (h : ∀ (a : A), ↑μ {a} ≠ 0 → (F a).satisfies B) : (μ >>= F).satisfies B

Support of a bind: if each fibre is supported in B, so is the bind.

theorem GaudisCrypt.SubProbability.satisfies_hbind {A : Type u} {C : Type w} (μ : SubProbability A) {F : A → SubProbability C} {B : C → Prop} (h : ∀ (a : A), ↑μ {a} ≠ 0 → (F a).satisfies B) : (μ.hbind F).satisfies B

satisfies_bind across universes.

theorem GaudisCrypt.expected_while_lfp_iSup {s : Type u} (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) (σ : s) (G : Unit × s → ENNReal) : (while_loop cond body σ).expected G = ⨆ (n : ℕ), ((⇑(while_iteration cond body))^[n] ⊥ () σ).expected G

Monotone convergence for the program while_loop (curried fixed point).

theorem GaudisCrypt.while_iteration_apply {s : Type u} (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) (fp : Unit → ProgramDenotation s Unit) (σ : s) : (while_iteration cond body) fp () σ = do let bσ ← cond σ if bσ.1 = true then do let uσ ← body bσ.2 fp () uσ.2 else pure ((), bσ.2)

Unfold one step of the while_iteration functional at a state.

Bridges to ProgramDenotation.prhl

theorem GaudisCrypt.ProgramDenotation.prhl.to_prhl2 {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {B : α × s₁ → β × s₂ → Prop} (h : prhl A c d B) : prhl2 A c d B

Forward bridge (unconditional): the structure-packaged judgment yields the literal one. Marginals come from Coupling.map_fst/map_snd; the pointwise support comes from the range support via satisfies_of_range.

theorem GaudisCrypt.ProgramDenotation.prhl2.to_prhl {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {B : α × s₁ → β × s₂ → Prop} (h : prhl2 A c d B) : prhl A c d B

Backward bridge (discrete): the literal judgment yields the structure-packaged one. The marginal equalities become the expected-value marginals by integrating both sides; the pointwise support becomes the range support via range_of_satisfies (countability-free since subtask 4, via the discreteness invariant).

theorem GaudisCrypt.ProgramDenotation.prhl2_iff_prhl {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {B : α × s₁ → β × s₂ → Prop} : prhl2 A c d B ↔ prhl A c d B

For discrete (countable) joint type the two formulations coincide.

Soundness with respect to the wp-lifting

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

Every literal coupling judgment yields the two-sided wp-lifting judgment (discrete); all relE elimination forms transfer.

Structural rules

The leaves and the purely structural rules are unconditional; the seq rule inherits the discreteness hypothesis (see the module header).

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

Consequence — same witness, the support and precondition only weaken.

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

Two-sided pure.

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

Reflexivity.

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

The rnd rule: uniform samples coupled along a bijection.

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

Existential in the precondition.

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

Disjunction in the precondition.

theorem GaudisCrypt.ProgramDenotation.prhl2.bind {s₁ s₂ : Type (max u v)} {α₁ α₂ β₁ β₂ : Type v} {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₁ : prhl2 A p₁ p₂ M) (h₂ : ∀ (x₁ : α₁) (x₂ : α₂), prhl2 (fun (τ₁ : s₁) (τ₂ : s₂) => M (x₁, τ₁) (x₂, τ₂)) (k₁ x₁) (k₂ x₂) B) : prhl2 A (p₁ >>= k₁) (p₂ >>= k₂) B

The seq rule (discrete). The composite coupling is built by ProgramDenotation.prhl.bind; the discreteness hypotheses are what let the pointwise-satisfies prefixes and continuations be reassembled.

theorem GaudisCrypt.ProgramDenotation.prhl2.symm {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} (h : prhl2 A c d B) : prhl2 (fun (σ₂ : s₂) (σ₁ : s₁) => A σ₁ σ₂) d c fun (v : β × s₂) (u : α × s₁) => B u v

Symmetry: a coupling is inherently two-sided — swap the joint distribution coordinate-wise. The pointwise satisfies is propagated through the swap map (via the range form), countability-free since subtask 4.

theorem GaudisCrypt.ProgramDenotation.prhl2.get {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {γ₁ γ₂ : Type v} (L₁ : Lens γ₁ s₁) (L₂ : Lens γ₂ s₂) {B : γ₁ × s₁ → γ₂ × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B (L₁.get σ₁, σ₁) (L₂.get σ₂, σ₂)) : prhl2 A (ProgramDenotation.get L₁) (ProgramDenotation.get L₂) B

Read coupling: two gets relate when the read values (and unchanged states) satisfy the post. Unconditional leaf.

theorem GaudisCrypt.ProgramDenotation.prhl2.set {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {γ₁ : Type u_1} {γ₂ : Type u_2} (L₁ : Lens γ₁ s₁) (L₂ : Lens γ₂ s₂) (v₁ : γ₁) (v₂ : γ₂) {B : Unit × s₁ → Unit × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B ((), L₁.set v₁ σ₁) ((), L₂.set v₂ σ₂)) : prhl2 A (ProgramDenotation.set L₁ v₁) (ProgramDenotation.set L₂ v₂) B

Write coupling: two sets relate when the updated states satisfy the post. Unconditional leaf.

theorem GaudisCrypt.ProgramDenotation.prhl2.loop_n {s₁ s₂ : Type (max u v)} {body₁ : ProgramDenotation s₁ Unit} {body₂ : ProgramDenotation s₂ Unit} {Inv : s₁ → s₂ → Prop} (h : prhl2 Inv body₁ body₂ fun (u : Unit × s₁) (v : Unit × s₂) => Inv u.2 v.2) (n : ℕ) : prhl2 Inv (GaudisCrypt.loop_n n body₁) (GaudisCrypt.loop_n n body₂) fun (u : Unit × s₁) (v : Unit × s₂) => Inv u.2 v.2

Bounded-loop congruence: if the bodies preserve the invariant Inv relationally, so do their n-fold iterates. Proved by induction on n using prhl2.bind; covers the loops the crypto clients actually use (oracle_loop_n). The unbounded while fixed point stays open.

theorem GaudisCrypt.ProgramDenotation.prhl2.strengthen_left {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {C : α × s₁ → Prop} [DecidablePred C] (h : prhl2 A c d B) (hC : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → c.wp (fun (u : α × s₁) => if C u then 0 else 1) σ₁ = 0) : prhl2 A c d fun (u : α × s₁) (v : β × s₂) => B u v ∧ C u

Left footprint: strengthen the post with a left-side fact C that holds almost surely for c (i.e. fails with probability 0). This is how inRange-style unary facts enter the coupling logic. Discrete (the support is rebalanced).

theorem GaudisCrypt.ProgramDenotation.prhl2.strengthen_right {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {C : β × s₂ → Prop} [DecidablePred C] (h : prhl2 A c d B) (hC : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → d.wp (fun (v : β × s₂) => if C v then 0 else 1) σ₂ = 0) : prhl2 A c d fun (u : α × s₁) (v : β × s₂) => B u v ∧ C v

Right footprint: the mirror of strengthen_left, obtained by symmetry.

Tier 2: one-sided/frame rules and rnd generalizations

theorem GaudisCrypt.ProgramDenotation.prhl2.prefix_left {s₁ s₂ : Type (max u v)} {β₁ β₂ : Type} {p₀ : ProgramDenotation s₁ Unit} {k : ProgramDenotation s₁ β₁} {q : ProgramDenotation s₂ β₂} {Pre Mid : s₁ → s₂ → Prop} {Post : β₁ × s₁ → β₂ × s₂ → Prop} (h₀ : prhl2 Pre p₀ (pure ()) fun (u : Unit × s₁) (v : Unit × s₂) => Mid u.2 v.2) (h : prhl2 Mid k q Post) : prhl2 Pre (do p₀ k) q Post

Left frame: a left-only prefix p₀ matched against skip on the right (carrying Pre to Mid), then the continuations from Mid, gives (p₀; k) ~ q. Avoids inserting pure () >>= on the right by hand. Derived from bind + the monad law.

theorem GaudisCrypt.ProgramDenotation.prhl2.prefix_right {s₁ s₂ : Type (max u v)} {β₁ β₂ : Type} {p : ProgramDenotation s₁ β₁} {q₀ : ProgramDenotation s₂ Unit} {k : ProgramDenotation s₂ β₂} {Pre Mid : s₁ → s₂ → Prop} {Post : β₁ × s₁ → β₂ × s₂ → Prop} (h₀ : prhl2 Pre (pure ()) q₀ fun (u : Unit × s₁) (v : Unit × s₂) => Mid u.2 v.2) (h : prhl2 Mid p k Post) : prhl2 Pre p (do q₀ k) Post

Right frame: the mirror of prefix_left.

theorem GaudisCrypt.ProgramDenotation.prhl2.set_skip_left {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {γ : Type u_1} (L : Lens γ s₁) (v : γ) {B : Unit × s₁ → Unit × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B ((), L.set v σ₁) ((), σ₂)) : prhl2 A (ProgramDenotation.set L v) (pure ()) B

Left ghost write: a left-only set L v matched against skip. The coupling analogue of EquivModuloLens.set_equiv_pure. Unconditional (both sides are point masses).

theorem GaudisCrypt.ProgramDenotation.prhl2.set_skip_right {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {γ : Type u_1} (L : Lens γ s₂) (v : γ) {B : Unit × s₁ → Unit × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B ((), σ₁) ((), L.set v σ₂)) : prhl2 A (pure ()) (ProgramDenotation.set L v) B

Right ghost write: the mirror of set_skip_left.

theorem GaudisCrypt.ProgramDenotation.prhl2.uniform_id {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {α' : Type v} [Fintype α'] [Nonempty α'] {B : α' × s₁ → α' × s₂ → Prop} (h : ∀ (t : α') (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B (t, σ₁) (t, σ₂)) : prhl2 A ProgramDenotation.uniform ProgramDenotation.uniform B

Synchronized sampling (rnd with the identity coupling): both runs draw the same uniform value. The common special case of uniform.

Tier 3: transitivity by discrete disintegration

theorem GaudisCrypt.ProgramDenotation.prhl2.trans {s₁ s₂ s₃ : Type (max u v)} {α β γ : Type v} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {r : ProgramDenotation s₃ γ} {Pre₁ : s₁ → s₂ → Prop} {Post₁ : α × s₁ → β × s₂ → Prop} {Pre₂ : s₂ → s₃ → Prop} {Post₂ : β × s₂ → γ × s₃ → Prop} (h₁ : prhl2 Pre₁ p q Post₁) (h₂ : prhl2 Pre₂ q r Post₂) : prhl2 (fun (σ₁ : s₁) (σ₃ : s₃) => ∃ (σ₂ : s₂), Pre₁ σ₁ σ₂ ∧ Pre₂ σ₂ σ₃) p r fun (x : α × s₁) (z : γ × s₃) => ∃ (y : β × s₂), Post₁ x y ∧ Post₂ y z

Transitivity: compose a coupling of (p, q) with a coupling of (q, r) into a coupling of (p, r), gluing along the shared middle marginal q σ₂. The glued weight is ν{(x,z)} = ∑ₘ μ₁{(x,m)}·μ₂{(m,z)} / q{m} — the discrete disintegration (independent given the middle), with the middle weights cancelling in each marginal. Countability-free since subtask 4 (the discreteness invariant).

theorem GaudisCrypt.ProgramDenotation.prhl2.while_loop {s₁ s₂ : Type u} {cond₁ : ProgramDenotation s₁ Bool} {body₁ : ProgramDenotation s₁ Unit} {cond₂ : ProgramDenotation s₂ Bool} {body₂ : ProgramDenotation s₂ Unit} {Inv : s₁ → s₂ → Prop} {PostC : Bool → s₁ → s₂ → Prop} (h_cond : prhl2 Inv cond₁ cond₂ fun (u : Bool × s₁) (v : Bool × s₂) => u.1 = v.1 ∧ PostC u.1 u.2 v.2) (h_body : prhl2 (PostC true) body₁ body₂ fun (u : Unit × s₁) (v : Unit × s₂) => Inv u.2 v.2) : prhl2 Inv (GaudisCrypt.while_loop cond₁ body₁) (GaudisCrypt.while_loop cond₂ body₂) fun (u : Unit × s₁) (v : Unit × s₂) => PostC false u.2 v.2

Synchronized while rule (the coupling least fixed point). Under the invariant the guards are coupled to agree (PostC records the invariant refined by the guard value), the bodies preserve the invariant from PostC true, and the loops relate at PostC false. The witness coupling is Φ.lfp, the least fixed point of the coupling transformer that runs the guard coupling and, while it fires, the body coupling.

Core-completion rules (EasyCrypt-style if, case, rnd)

theorem GaudisCrypt.ProgramDenotation.prhl2.cond {s₁ s₂ : Type u} {A : s₁ → s₂ → Prop} {β₁ β₂ : Type} {g₁ : ProgramDenotation s₁ Bool} {g₂ : ProgramDenotation s₂ Bool} {ct₁ ce₁ : ProgramDenotation s₁ β₁} {ct₂ ce₂ : ProgramDenotation s₂ β₂} {Mid : s₁ → s₂ → Prop} {B : β₁ × s₁ → β₂ × s₂ → Prop} (hg : prhl2 A g₁ g₂ fun (u : Bool × s₁) (v : Bool × s₂) => u.1 = v.1 ∧ Mid u.2 v.2) (ht : prhl2 Mid ct₁ ct₂ B) (hf : prhl2 Mid ce₁ ce₂ B) : prhl2 A (do let b ← g₁ if b = true then ct₁ else ce₁) (do let b ← g₂ if b = true then ct₂ else ce₂) B

Synchronized conditional (if): if the guards are coupled to produce equal booleans (carrying Mid), and the branches are related from Mid, then the conditionals are related. (Binds its own s₁ s₂ : Type u: it mentions neither α nor β, so the section's Type (max u v) would leave v free.)

theorem GaudisCrypt.ProgramDenotation.prhl2.case {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} (P : s₁ → s₂ → Prop) {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} (hp : prhl2 (fun (σ₁ : s₁) (σ₂ : s₂) => A σ₁ σ₂ ∧ P σ₁ σ₂) c d B) (hn : prhl2 (fun (σ₁ : s₁) (σ₂ : s₂) => A σ₁ σ₂ ∧ ¬P σ₁ σ₂) c d B) : prhl2 A c d B

Case split on a state predicate P.

theorem GaudisCrypt.ProgramDenotation.prhl2.rnd {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {α' β' : Type v} (μ : SubProbability α') (ν : SubProbability β') (e : α' → β') (he : (do let a ← μ pure (e a)) = ν) {B : α' × s₁ → β' × s₂ → Prop} (h : ∀ (a : α') (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → B (a, σ₁) (e a, σ₂)) : prhl2 A μ.toProgramDenotation ν.toProgramDenotation B

General rnd: couple two samplings μ, ν along a function e that pushes μ to ν (map e μ = ν); the post must hold for every drawn a paired with e a. Subsumes uniform/uniform_id (take μ, ν uniform and e a bijection).

theorem GaudisCrypt.ProgramDenotation.prhl2.kill_left {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {p₀ : ProgramDenotation s₁ Unit} {B : Unit × s₁ → Unit × s₂ → Prop} (hloss : ∀ (σ₁ : s₁), p₀.wp (fun (x : Unit × s₁) => 1) σ₁ = 1) (hsupp : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → (p₀ σ₁).satisfies fun (u : Unit × s₁) => B u ((), σ₂)) : prhl2 A p₀ (pure ()) B

Kill a lossless left-only statement: a lossless p₀ whose output almost-surely satisfies the post (against the unchanged right state) is related to skip. Generalizes set_skip_left from deterministic to any lossless program.

theorem GaudisCrypt.ProgramDenotation.prhl2.swap_left {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {α' β' γ δ : Type v} {μ : SubProbability α'} {ν : SubProbability β'} {k : α' → β' → ProgramDenotation s₁ γ} {d : ProgramDenotation s₂ δ} {B : γ × s₁ → δ × s₂ → Prop} (h : prhl2 A (do let y ← ν.toProgramDenotation let x ← μ.toProgramDenotation k x y) d B) : prhl2 A (do let x ← μ.toProgramDenotation let y ← ν.toProgramDenotation k x y) d B

Swap two independent samplings on the left program.

theorem GaudisCrypt.ProgramDenotation.prhl2.swap_right {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {α' β' γ δ : Type v} {c : ProgramDenotation s₁ γ} {μ : SubProbability α'} {ν : SubProbability β'} {k : α' → β' → ProgramDenotation s₂ δ} {B : γ × s₁ → δ × s₂ → Prop} (h : prhl2 A c (do let y ← ν.toProgramDenotation let x ← μ.toProgramDenotation k x y) B) : prhl2 A c (do let x ← μ.toProgramDenotation let y ← ν.toProgramDenotation k x y) B

Swap two independent samplings on the right program.

One-sided rules (EasyCrypt if⟨i⟩, kill)

theorem GaudisCrypt.ProgramDenotation.prhl2.cond_left {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} (e : s₁ → Bool) {ct₁ ce₁ : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} (ht : prhl2 (fun (σ₁ : s₁) (σ₂ : s₂) => A σ₁ σ₂ ∧ e σ₁ = true) ct₁ d B) (hf : prhl2 (fun (σ₁ : s₁) (σ₂ : s₂) => A σ₁ σ₂ ∧ e σ₁ = false) ce₁ d B) : prhl2 A (fun (σ₁ : s₁) => if e σ₁ = true then ct₁ σ₁ else ce₁ σ₁) d B

One-sided if on the left (if⟨1⟩): a left conditional on a deterministic state guard e, related to an arbitrary right program by relating each branch under the refined precondition.

theorem GaudisCrypt.ProgramDenotation.prhl2.cond_right {s₁ s₂ : Type (max u v)} {α β : Type v} {A : s₁ → s₂ → Prop} {B : α × s₁ → β × s₂ → Prop} (e : s₂ → Bool) {c : ProgramDenotation s₁ α} {dt₂ de₂ : ProgramDenotation s₂ β} (ht : prhl2 (fun (σ₁ : s₁) (σ₂ : s₂) => A σ₁ σ₂ ∧ e σ₂ = true) c dt₂ B) (hf : prhl2 (fun (σ₁ : s₁) (σ₂ : s₂) => A σ₁ σ₂ ∧ e σ₂ = false) c de₂ B) : prhl2 A c (fun (σ₂ : s₂) => if e σ₂ = true then dt₂ σ₂ else de₂ σ₂) B

One-sided if on the right (if⟨2⟩).

theorem GaudisCrypt.ProgramDenotation.prhl2.kill_right {s₁ s₂ : Type (max u v)} {A : s₁ → s₂ → Prop} {q₀ : ProgramDenotation s₂ Unit} {B : Unit × s₁ → Unit × s₂ → Prop} (hloss : ∀ (σ₂ : s₂), q₀.wp (fun (x : Unit × s₂) => 1) σ₂ = 1) (hsupp : ∀ (σ₁ : s₁) (σ₂ : s₂), A σ₁ σ₂ → (q₀ σ₂).satisfies fun (v : Unit × s₂) => B ((), σ₁) v) : prhl2 A (pure ()) q₀ B

Kill a lossless right-only statement (mirror of kill_left).

The adversary / call rule (EasyCrypt call (_ : ={glob A}))

An adversary is a program confined to a state window L (a lens); glob A is exactly this window. Running it from two states that agree on the window returns equal results and states that again agree on the window — ={glob A} ⟹ ={res, glob A}. The coupling is the diagonal one through L: run the inner program once and write its result back into both states.

theorem GaudisCrypt.ProgramDenotation.prhl2.adversary {c s : Type (max u v)} {γ : Type v} (L : Lens c s) (P : ProgramDenotation c γ) : prhl2 (fun (σ₁ σ₂ : s) => L.get σ₁ = L.get σ₂) (L.lift P) (L.lift P) fun (u v : γ × s) => u.1 = v.1 ∧ L.get u.2 = L.get v.2

Adversary call, constructive form: L.lift P (an adversary acting through window L) from L-agreeing states gives equal results and L-agreeing states.

theorem GaudisCrypt.ProgramDenotation.prhl2.adversary_inFootprint {c s : Type (max u v)} {γ : Type v} [Nonempty s] (L : Lens c s) (A : ProgramDenotation s γ) (hA : A.inFootprint L.footprint) : prhl2 (fun (σ₁ σ₂ : s) => L.get σ₁ = L.get σ₂) A A fun (u v : γ × s) => u.1 = v.1 ∧ L.get u.2 = L.get v.2

Adversary call, abstract form: any A confined to the window L (A.inFootprint L.footprint) satisfies the same rule, via the factorization A = L.lift (L.factor A). This is the modular adversary principle.

Smoke tests

Completeness (relE → prhl2)

The converse of prhl2.to_relE — that the wp-lifting judgment yields a coupling — is discrete Strassen (the coupling-lifting theorem), proved in GaudisCrypt/Strassen.lean as PMF.exists_coupling_of_hall.

The wp judgment gives Hall's marginal-domination condition directly: plugging in indicator post-conditions turns rel into it (rel.hall below). Strassen's theorem says this condition is also sufficient for a coupling.

theorem GaudisCrypt.ProgramDenotation.rel.hall {s₁ s₂ : Type (max u v)} {α β : Type v} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : c.rel d Pre Post) {σ₁ : s₁} {σ₂ : s₂} (hpre : Pre σ₁ σ₂) (A : Set (α × s₁)) : ↑(c σ₁) A ≤ ↑(d σ₂) {y : β × s₂ | ∃ x ∈ A, Post x y}

Hall's condition from rel (the necessary half of discrete Strassen): the mass c places on any set A is dominated by the mass d places on the Post-image of A. The converse (Hall ⇒ coupling) is SubProbability.exists_coupling_of_hall.

theorem GaudisCrypt.ProgramDenotation.relE.hall_right {s₁ s₂ : Type (max u v)} {α β : Type v} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : c.relE d Pre Post) {σ₁ : s₁} {σ₂ : s₂} (hpre : Pre σ₁ σ₂) (B : Set (β × s₂)) : ↑(d σ₂) B ≤ ↑(c σ₁) {x : α × s₁ | ∃ y ∈ B, Post x y}

For a two-sided relE, Hall's condition holds in both directions: d's mass on B is dominated by c's mass on the Post-preimage of B.

Scaling a sub-probability (for the mass-normalization reduction)

noncomputable def GaudisCrypt.SubProbability.scale {X : Type u} (c : ENNReal) (ν : SubProbability X) (h : c * ↑ν Set.univ ≤ 1) : SubProbability X

Scale a sub-probability by c (well-defined as a sub-probability when c · (total mass) ≤ 1).

Equations

• GaudisCrypt.SubProbability.scale c ν h = ⟨c • ↑ν, ⋯⟩

@[simp]

theorem GaudisCrypt.SubProbability.scale_expected {X : Type u} (c : ENNReal) (ν : SubProbability X) (h : c * ↑ν Set.univ ≤ 1) (g : X → ENNReal) : (scale c ν h).expected g = c * ν.expected g

theorem GaudisCrypt.SubProbability.scale_satisfies {X : Type u} (c : ENNReal) (ν : SubProbability X) (h : c * ↑ν Set.univ ≤ 1) {B : X → Prop} (hν : ν.satisfies B) : (scale c ν h).satisfies B

theorem GaudisCrypt.SubProbability.exists_coupling_of_hall {X Y : Type u} (p : SubProbability X) (q : SubProbability Y) (R : X → Y → Prop) (hpq : ∀ (A : Set X), ↑p A ≤ ↑q {y : Y | ∃ x ∈ A, R x y}) (hqp : ∀ (B : Set Y), ↑q B ≤ ↑p {x : X | ∃ y ∈ B, R x y}) : ∃ (μ : SubProbability (X × Y)), (do let w ← μ pure w.1) = p ∧ (do let w ← μ pure w.2) = q ∧ μ.satisfies fun (w : X × Y) => R w.1 w.2

Coupling lifting, sub-probability form — derived from discrete Strassen (PMF.exists_coupling_of_hall, GaudisCrypt/Strassen.lean) by mass normalization. Two-sided Hall forces equal total mass; the zero-mass case is the empty coupling, and otherwise we normalize both sides to probability measures, transfer them to PMFs via SubProbability.toPMF, apply Strassen, and scale the resulting coupling back. ProgramDenotation.rel.hall shows the hypotheses are exactly what relE supplies.

Use in coupling-based program logics (the relE ↔ prhl2 correspondence here): Barthe, Espitau, Grégoire, Hsu, Strub, "Probabilistic Couplings for Probabilistic Reasoning", arXiv:1710.09951.

theorem GaudisCrypt.ProgramDenotation.relE.to_prhl2 {s₁ s₂ : Type (max u v)} {α β : Type v} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : c.relE d Pre Post) : prhl2 Pre c d Post

Completeness relE → prhl2: the wp-lifting judgment yields a coupling. Extracts Hall's condition in both directions from relE via rel.hall and feeds it to exists_coupling_of_hall. Together with prhl2.to_relE this shows the two logics coincide.

theorem GaudisCrypt.ProgramDenotation.prhl2_iff_relE {s₁ s₂ : Type (max u v)} {α β : Type v} {c : ProgramDenotation s₁ α} {d : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} : prhl2 Pre c d Post ↔ c.relE d Pre Post

The two relational logics coincide.

Footprint-confined adversary self-coupling

A program confined to a Footprint R self-couples under ={glob} — from states agreeing on the touched content it returns equal results and states again agreeing on the touched content. The EqvGen-closure of a single deterministic Rᶜ-step, glued by coupling transitivity.

theorem GaudisCrypt.adversary_couple_step {s : Type (max u v)} {a : Type v} {R : Footprint s} {p : ProgramDenotation s a} (hp : p.inFootprint R) {f : s → s} (hf : diracKer f ∈ Rᶜ.updates) (σ : s) : ∃ (μ : SubProbability ((a × s) × a × s)), (do let x ← μ pure x.1) = p σ ∧ (do let x ← μ pure x.2) = p (f σ) ∧ μ.satisfies fun (x : (a × s) × a × s) => x.1.1 = x.2.1 ∧ ∃ (g : Function.End s), diracKer g ∈ Rᶜ.updates ∧ g x.1.2 = x.2.2

Adversary rule — single Rᶜ-step (footprint glob). A program confined to R, run from a state σ and its image f σ under one deterministic Rᶜ-update, self-couples: equal results, output states again one Rᶜ-step apart. This is the base case of the ={glob A} adversary rule for glob A = R.touched_getter. The full rule is its EqvGen closure over the Rᶜ-orbit.

theorem GaudisCrypt.prhl2_glob {s : Type (max u v)} {a : Type v} {R : Footprint s} {p : ProgramDenotation s a} (hp : p.inFootprint R) : ProgramDenotation.prhl2 (fun (x y : s) => R.touched_getter.get x = R.touched_getter.get y) p p fun (u v : a × s) => u.1 = v.1 ∧ R.touched_getter.get u.2 = R.touched_getter.get v.2

Adversary rule (full), footprint glob. A program confined to R self-couples under ={glob A} (with glob A = R.touched_getter): from states agreeing on glob A it returns equal results and states that again agree on glob A. The EqvGen-closure of adversary_couple_step — refl/symm/trans on prhl2 (the trans = coupling gluing, ProgramDenotation.prhl2.trans, discrete disintegration).

theorem GaudisCrypt.ProgramDenotation.prhl2_of_lossless_tail_proj_inv {s : Type u} {α : Type} {β : Type u_1} {p q' : ProgramDenotation s α} {c : ProgramDenotation s Unit} (g : s → β) {P : s → s → Prop} (hself : prhl2 P p p fun (u v : α × s) => u.1 = v.1 ∧ g u.2 = g v.2) (hc : ∀ (σ : s), ↑(c σ) Set.univ = 1) (hkeep : ∀ (σ : s), (c σ).satisfies fun (x : Unit × s) => g x.2 = g σ) (heq : (do let a ← p c pure a) = q') : prhl2 P p q' fun (u v : α × s) => u.1 = v.1 ∧ g u.2 = g v.2

Coupling through a lossless, projection-preserving tail, over a base coupling. Given a self-coupling of p under P with equal results and g-equal finals, extending the right leg by a lossless tail c that preserves g on its support couples p against q' = p; c (result kept) with the same pre/post. The equal-initial-states version (prhl2_of_lossless_tail_proj) is the instance at the diagonal coupling.

theorem GaudisCrypt.ProgramDenotation.prhl2_of_lossless_tail_proj {s : Type u} {α : Type} {β : Type u_1} {p q : ProgramDenotation s α} {c : ProgramDenotation s Unit} (g : s → β) (hc : ∀ (σ : s), ↑(c σ) Set.univ = 1) (hkeep : ∀ (σ : s), (c σ).satisfies fun (x : Unit × s) => g x.2 = g σ) (heq : (do let a ← p c pure a) = q) : prhl2 (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u.1 = v.1 ∧ g u.2 = g v.2

Coupling through a lossless, projection-preserving tail (equal initial states): the diagonal instance of prhl2_of_lossless_tail_proj_inv. Converts distribution-level transfer equations (Lib/RO/TransferConvert.lean) into prhl2.

theorem GaudisCrypt.ProgramDenotation.prhl2_of_lossless_tail {s : Type u} {α : Type} {p q : ProgramDenotation s α} {c : ProgramDenotation s Unit} (hc : ∀ (σ : s), ↑(c σ) Set.univ = 1) (heq : (do let a ← p c pure a) = q) : prhl2 (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u.1 = v.1

Coupling through a lossless tail. If q equals p followed by a lossless state-only post-processor c (which keeps p's result), then p and q couple from equal initial states with equal results: route the diagonal coupling of p through c on the right leg. The projection-free instance of prhl2_of_lossless_tail_proj.