pRHL core: a relational wp calculus for ProgramDenotation

ProgramDenotation.rel p q Pre Post is the asymmetric relational lifting: for every pair of postconditions compatible with Post, the wp of p from a Pre-related pair of states is below the wp of q. ProgramDenotation.relE is the symmetric (equality) variant, used for bridging game hops; rel itself is the primitive, used for reductions and up-to-bad inequalities.

Design notes:

• The judgment is defined by its elimination form, so the probability bridges (rel.wp_le, relE.wp_eq) are definitional and every proof rule is a small consequence of the existing unary wp lemma base — no witness couplings, hence no measurability, countability, or a.e.-support side conditions. For discrete subprobabilities this lifting is coextensive with the coupling-based one (Strassen) in the direction proofs consume.
• Heterogeneous state and result types are supported (ProgramDenotation s₁ α vs ProgramDenotation s₂ β): the calculus can relate a concrete game to an abstract schema, or a program to its lens-factored inner core.
• Unsound-rule warning: conjunction of postconditions is NOT admissible. From rel p q Pre Post₁ and rel p q Pre Post₂ one may NOT conclude rel p q Pre (fun x y => Post₁ x y ∧ Post₂ x y). (Standard counterexample: for p = q = a uniform coin, both post x₁ = x₂ and post x₁ ≠ x₂ hold relationally — with different implicit couplings — but their conjunction is empty.) Do not add such a rule.

def GaudisCrypt.ProgramDenotation.rel {s₁ s₂ α β : Type} (p : ProgramDenotation s₁ α) (q : ProgramDenotation s₂ β) (Pre : s₁ → s₂ → Prop) (Post : α × s₁ → β × s₂ → Prop) : Prop

Relational wp judgment (asymmetric form). p.rel q Pre Post holds iff for all post-pairs F ≤ G along Post and all Pre-related starting states, p.wp F ≤ q.wp G.

Equations

• p.rel q Pre Post = ∀ (F : α × s₁ → ENNReal) (G : β × s₂ → ENNReal), (∀ (x : α × s₁) (y : β × s₂), Post x y → F x ≤ G y) → ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → p.wp F σ₁ ≤ q.wp G σ₂

def GaudisCrypt.ProgramDenotation.relE {s₁ s₂ α β : Type} (p : ProgramDenotation s₁ α) (q : ProgramDenotation s₂ β) (Pre : s₁ → s₂ → Prop) (Post : α × s₁ → β × s₂ → Prop) : Prop

Relational wp equivalence: rel in both directions (with flipped relations). The two-sided judgment used for bridging game hops.

Equations

• p.relE q Pre Post = (p.rel q Pre Post ∧ q.rel p (fun (σ₂ : s₂) (σ₁ : s₁) => Pre σ₁ σ₂) fun (y : β × s₂) (x : α × s₁) => Post x y)

Elimination (Pr-bridges)

theorem GaudisCrypt.ProgramDenotation.rel.wp_le {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : p.rel q Pre Post) {F : α × s₁ → ENNReal} {G : β × s₂ → ENNReal} (hFG : ∀ (x : α × s₁) (y : β × s₂), Post x y → F x ≤ G y) {σ₁ : s₁} {σ₂ : s₂} (hpre : Pre σ₁ σ₂) : p.wp F σ₁ ≤ q.wp G σ₂

Elimination form (definitional): a rel judgment yields a wp inequality at any compatible post-pair.

Structural rules

theorem GaudisCrypt.ProgramDenotation.rel.conseq {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre Pre' : s₁ → s₂ → Prop} {Post Post' : α × s₁ → β × s₂ → Prop} (h : p.rel q Pre Post) (hPre : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre' σ₁ σ₂ → Pre σ₁ σ₂) (hPost : ∀ (x : α × s₁) (y : β × s₂), Post x y → Post' x y) : p.rel q Pre' Post'

Consequence: weaken the precondition, strengthen the postcondition.

theorem GaudisCrypt.ProgramDenotation.rel.refl {s α : Type} (p : ProgramDenotation s α) : p.rel p Eq Eq

Reflexivity at the diagonal.

theorem GaudisCrypt.ProgramDenotation.rel.trans {s₁ s₂ s₃ α β γ : Type} {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₁ : p.rel q Pre₁ Post₁) (h₂ : q.rel r Pre₂ Post₂) : p.rel r (fun (σ₁ : s₁) (σ₃ : s₃) => ∃ (σ₂ : s₂), Pre₁ σ₁ σ₂ ∧ Pre₂ σ₂ σ₃) fun (x : α × s₁) (z : γ × s₃) => ∃ (y : β × s₂), Post₁ x y ∧ Post₂ y z

Transitivity through a middle program, with composed pre/post relations. No PER or losslessness side conditions: the middle postcondition is interpolated by fun y => ⨆ x, ⨆ (_ : Post₁ x y), F x (possible because posts are ENNReal-valued and need no measurability).

theorem GaudisCrypt.ProgramDenotation.rel.exists_pre {s₁ s₂ α β : Type} {ι : Sort u_1} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre : ι → s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : ∀ (i : ι), p.rel q (Pre i) Post) : p.rel q (fun (σ₁ : s₁) (σ₂ : s₂) => ∃ (i : ι), Pre i σ₁ σ₂) Post

Eliminate an existential in the precondition.

theorem GaudisCrypt.ProgramDenotation.rel.or_pre {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre₁ Pre₂ : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h₁ : p.rel q Pre₁ Post) (h₂ : p.rel q Pre₂ Post) : p.rel q (fun (σ₁ : s₁) (σ₂ : s₂) => Pre₁ σ₁ σ₂ ∨ Pre₂ σ₁ σ₂) Post

Case split on the precondition.

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

Two-sided pure.

theorem GaudisCrypt.ProgramDenotation.rel.bind {s₁ s₂ α₁ α₂ β₁ β₂ : Type} {p₁ : ProgramDenotation s₁ α₁} {p₂ : ProgramDenotation s₂ α₂} {k₁ : α₁ → ProgramDenotation s₁ β₁} {k₂ : α₂ → ProgramDenotation s₂ β₂} {Pre : s₁ → s₂ → Prop} {Mid : α₁ × s₁ → α₂ × s₂ → Prop} {Post : β₁ × s₁ → β₂ × s₂ → Prop} (h_p : p₁.rel p₂ Pre Mid) (h_k : ∀ (x₁ : α₁) (x₂ : α₂), (k₁ x₁).rel (k₂ x₂) (fun (τ₁ : s₁) (τ₂ : s₂) => Mid (x₁, τ₁) (x₂, τ₂)) Post) : (p₁ >>= k₁).rel (p₂ >>= k₂) Pre Post

Sequence rule (the workhorse): relate the prefixes at a middle relation Mid, then the continuations from every Mid-related pair.

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

Prepend a left-only prefix (e.g. a ghost write): if p₀ ~ skip carries Pre to Mid, and k ~ q from Mid, then (p₀; k) ~ q from Pre. Avoids inserting pure () >>= on the right by hand.

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

Prepend a right-only prefix: mirror image of prefix_left.

theorem GaudisCrypt.ProgramDenotation.rel.ite_sync {s₁ s₂ α β : Type} {c₁ c₂ : Prop} [Decidable c₁] [Decidable c₂] {p₁ q₁ : ProgramDenotation s₁ α} {p₂ q₂ : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h_iff : c₁ ↔ c₂) (h_t : c₁ → c₂ → p₁.rel p₂ Pre Post) (h_f : ¬c₁ → ¬c₂ → q₁.rel q₂ Pre Post) : (if c₁ then p₁ else q₁).rel (if c₂ then p₂ else q₂) Pre Post

Synchronized conditional with statically equivalent guards. (For state-dependent guards, the guards become values bound by bind, so they are static by the time this rule applies; for genuinely one-sided conditionals use by_cases at the meta level.)

Assignment rules (ProgramDenotation.set / ProgramDenotation.get)

theorem GaudisCrypt.ProgramDenotation.rel.set_set {s₁ s₂ γ₁ γ₂ : Type} {L₁ : Lens γ₁ s₁} {L₂ : Lens γ₂ s₂} {v₁ : γ₁} {v₂ : γ₂} {Pre : s₁ → s₂ → Prop} {Post : Unit × s₁ → Unit × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post ((), L₁.set v₁ σ₁) ((), L₂.set v₂ σ₂)) : (set L₁ v₁).rel (set L₂ v₂) Pre Post

Two-sided set.

theorem GaudisCrypt.ProgramDenotation.rel.set_left {s₁ s₂ γ β : Type} {L : Lens γ s₁} {v : γ} {x₂ : β} {Pre : s₁ → s₂ → Prop} {Post : Unit × s₁ → β × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post ((), L.set v σ₁) (x₂, σ₂)) : (set L v).rel (pure x₂) Pre Post

Left-only set (against pure on the right): the ghost-write rule.

theorem GaudisCrypt.ProgramDenotation.rel.set_right {s₁ s₂ γ α : Type} {x₁ : α} {L : Lens γ s₂} {v : γ} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → Unit × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post (x₁, σ₁) ((), L.set v σ₂)) : (pure x₁).rel (set L v) Pre Post

Right-only set (against pure on the left).

theorem GaudisCrypt.ProgramDenotation.rel.get_get {s₁ s₂ γ₁ γ₂ : Type} {L₁ : Lens γ₁ s₁} {L₂ : Lens γ₂ s₂} {Pre : s₁ → s₂ → Prop} {Post : γ₁ × s₁ → γ₂ × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post (L₁.get σ₁, σ₁) (L₂.get σ₂, σ₂)) : (get L₁).rel (get L₂) Pre Post

Two-sided get.

theorem GaudisCrypt.ProgramDenotation.rel.get_left {s₁ s₂ γ β : Type} {L : Lens γ s₁} {x₂ : β} {Pre : s₁ → s₂ → Prop} {Post : γ × s₁ → β × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post (L.get σ₁, σ₁) (x₂, σ₂)) : (get L).rel (pure x₂) Pre Post

Left-only get.

theorem GaudisCrypt.ProgramDenotation.rel.get_right {s₁ s₂ γ α : Type} {x₁ : α} {L : Lens γ s₂} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → γ × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post (x₁, σ₁) (L.get σ₂, σ₂)) : (pure x₁).rel (get L) Pre Post

Right-only get.

Sampling rules

theorem GaudisCrypt.ProgramDenotation.rel.uniform_bij {s₁ s₂ α β : Type} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (e : α ≃ β) {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : ∀ (v : α) (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post (v, σ₁) (e v, σ₂)) : uniform.rel uniform Pre Post

Coupled sampling along a bijection (the rnd rule): two uniform samples are related by pairing v with e v.

theorem GaudisCrypt.ProgramDenotation.rel.sample_left {s₁ s₂ α β₁ β₂ : Type} [Fintype α] [Nonempty α] {k : α → ProgramDenotation s₁ β₁} {q : ProgramDenotation s₂ β₂} {Pre : s₁ → s₂ → Prop} {Post : β₁ × s₁ → β₂ × s₂ → Prop} (h : ∀ (v : α), (k v).rel q Pre Post) : (uniform >>= k).rel q Pre Post

Left-only sampling: an average is below any uniform upper bound. No mass side condition.

theorem GaudisCrypt.ProgramDenotation.rel.sample_right {s₁ s₂ α β₁ β₂ : Type} [Fintype α] [Nonempty α] {p : ProgramDenotation s₁ β₁} {k : α → ProgramDenotation s₂ β₂} {Pre : s₁ → s₂ → Prop} {Post : β₁ × s₁ → β₂ × s₂ → Prop} (h : ∀ (v : α), p.rel (k v) Pre Post) : p.rel (uniform >>= k) Pre Post

Right-only sampling (sample introduction): a uniform average of lower bounds is a lower bound. Mass-1 of uniform is what makes this sound.

relE: elimination and mechanical two-sided variants

theorem GaudisCrypt.ProgramDenotation.relE.wp_eq {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : p.relE q Pre Post) {F : α × s₁ → ENNReal} {G : β × s₂ → ENNReal} (hFG : ∀ (x : α × s₁) (y : β × s₂), Post x y → F x = G y) {σ₁ : s₁} {σ₂ : s₂} (hpre : Pre σ₁ σ₂) : p.wp F σ₁ = q.wp G σ₂

Elimination form: a relE judgment yields wp equality at any post-pair that agrees along Post.

theorem GaudisCrypt.ProgramDenotation.relE.refl {s α : Type} (p : ProgramDenotation s α) : p.relE p Eq Eq

Reflexivity.

theorem GaudisCrypt.ProgramDenotation.relE.of_eq {s α : Type} {p q : ProgramDenotation s α} (h : p = q) : p.relE q Eq Eq

ProgramDenotation equality gives the diagonal relE.

theorem GaudisCrypt.ProgramDenotation.relE.symm {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : p.relE q Pre Post) : q.relE p (fun (σ₂ : s₂) (σ₁ : s₁) => Pre σ₁ σ₂) fun (y : β × s₂) (x : α × s₁) => Post x y

Symmetry (with flipped relations).

theorem GaudisCrypt.ProgramDenotation.relE.trans {s₁ s₂ s₃ α β γ : Type} {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₁ : p.relE q Pre₁ Post₁) (h₂ : q.relE r Pre₂ Post₂) : p.relE r (fun (σ₁ : s₁) (σ₃ : s₃) => ∃ (σ₂ : s₂), Pre₁ σ₁ σ₂ ∧ Pre₂ σ₂ σ₃) fun (x : α × s₁) (z : γ × s₃) => ∃ (y : β × s₂), Post₁ x y ∧ Post₂ y z

Transitivity for relE (composed pre/post relations).

theorem GaudisCrypt.ProgramDenotation.relE.exists_pre {s₁ s₂ α β : Type} {ι : Sort u_1} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre : ι → s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : ∀ (i : ι), p.relE q (Pre i) Post) : p.relE q (fun (σ₁ : s₁) (σ₂ : s₂) => ∃ (i : ι), Pre i σ₁ σ₂) Post

Eliminate an existential in the precondition.

theorem GaudisCrypt.ProgramDenotation.relE.or_pre {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre₁ Pre₂ : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h₁ : p.relE q Pre₁ Post) (h₂ : p.relE q Pre₂ Post) : p.relE q (fun (σ₁ : s₁) (σ₂ : s₂) => Pre₁ σ₁ σ₂ ∨ Pre₂ σ₁ σ₂) Post

Case split on the precondition, for relE.

theorem GaudisCrypt.ProgramDenotation.relE.conseq {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre Pre' : s₁ → s₂ → Prop} {Post Post' : α × s₁ → β × s₂ → Prop} (h : p.relE q Pre Post) (hPre : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre' σ₁ σ₂ → Pre σ₁ σ₂) (hPost : ∀ (x : α × s₁) (y : β × s₂), Post x y → Post' x y) : p.relE q Pre' Post'

Consequence for relE.

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

Two-sided pure for relE.

theorem GaudisCrypt.ProgramDenotation.relE.bind {s₁ s₂ α₁ α₂ β₁ β₂ : Type} {p₁ : ProgramDenotation s₁ α₁} {p₂ : ProgramDenotation s₂ α₂} {k₁ : α₁ → ProgramDenotation s₁ β₁} {k₂ : α₂ → ProgramDenotation s₂ β₂} {Pre : s₁ → s₂ → Prop} {Mid : α₁ × s₁ → α₂ × s₂ → Prop} {Post : β₁ × s₁ → β₂ × s₂ → Prop} (h_p : p₁.relE p₂ Pre Mid) (h_k : ∀ (x₁ : α₁) (x₂ : α₂), (k₁ x₁).relE (k₂ x₂) (fun (τ₁ : s₁) (τ₂ : s₂) => Mid (x₁, τ₁) (x₂, τ₂)) Post) : (p₁ >>= k₁).relE (p₂ >>= k₂) Pre Post

Sequence rule for relE.

theorem GaudisCrypt.ProgramDenotation.relE.set_set {s₁ s₂ γ₁ γ₂ : Type} {L₁ : Lens γ₁ s₁} {L₂ : Lens γ₂ s₂} {v₁ : γ₁} {v₂ : γ₂} {Pre : s₁ → s₂ → Prop} {Post : Unit × s₁ → Unit × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post ((), L₁.set v₁ σ₁) ((), L₂.set v₂ σ₂)) : (set L₁ v₁).relE (set L₂ v₂) Pre Post

Two-sided set for relE.

theorem GaudisCrypt.ProgramDenotation.relE.get_get {s₁ s₂ γ₁ γ₂ : Type} {L₁ : Lens γ₁ s₁} {L₂ : Lens γ₂ s₂} {Pre : s₁ → s₂ → Prop} {Post : γ₁ × s₁ → γ₂ × s₂ → Prop} (h : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post (L₁.get σ₁, σ₁) (L₂.get σ₂, σ₂)) : (get L₁).relE (get L₂) Pre Post

Two-sided get for relE.

theorem GaudisCrypt.ProgramDenotation.relE.uniform_bij {s₁ s₂ α β : Type} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (e : α ≃ β) {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : ∀ (v : α) (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → Post (v, σ₁) (e v, σ₂)) : uniform.relE uniform Pre Post

Coupled sampling along a bijection, for relE.

theorem GaudisCrypt.ProgramDenotation.relE.ite_sync {s₁ s₂ α β : Type} {c₁ c₂ : Prop} [Decidable c₁] [Decidable c₂] {p₁ q₁ : ProgramDenotation s₁ α} {p₂ q₂ : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h_iff : c₁ ↔ c₂) (h_t : c₁ → c₂ → p₁.relE p₂ Pre Post) (h_f : ¬c₁ → ¬c₂ → q₁.relE q₂ Pre Post) : (if c₁ then p₁ else q₁).relE (if c₂ then p₂ else q₂) Pre Post

Synchronized conditional for relE.