Ergonomic Notation and Convenience Layer for Program Logic

This file provides the lightweight user-facing notation and convenience predicates for game-hopping proofs. It intentionally depends only on the core quantitative definitions, not on the full eRHL theorem development.

The canonical proof mode lives in VCVio/ProgramLogic/Tactics.lean.

Notation (activate with open scoped OracleComp.ProgramLogic)

Prop indicator

• 𝟙⟦P⟧ — inject Prop into ℝ≥0∞ (1 if true, 0 if false)

Unary (Std.Do-inspired)

• wp⟦c⟧ — quantitative WP (partial application, use as wp⟦c⟧ post)
• ⦃P⦄ c ⦃Q⦄ — quantitative Hoare triple (P ≤ wp c Q)

Game-level

• g₁ ≡ₚ g₂ — game equivalence (evalDist g₁ = evalDist g₂)

Relational (EasyCrypt-inspired)

• ⟪c₁ ~ c₂ | R⟫ — pRHL coupling triple
• ⟪c₁ ≈[ε] c₂ | R⟫ — approximate coupling triple
• ⦃f⦄ c₁ ≈ₑ c₂ ⦃g⦄ — eRHL quantitative relational triple

Convenience predicates

• GameEquiv g₁ g₂ — two games have the same output distribution
• AdvBound game ε — advantage of a game is at most ε

Convenience predicates

def OracleComp.ProgramLogic.GameEquiv {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} (g₁ g₂ : OracleComp spec₁ α) : Prop

Two games have the same output distribution.

def OracleComp.ProgramLogic.AdvBound {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] (game : OracleComp spec₁ Bool) (ε : ℝ) : Prop

Advantage of a Boolean game is at most ε (measured as deviation from 1/2).

theorem OracleComp.ProgramLogic.GameEquiv.rfl {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {g : OracleComp spec₁ α} : GameEquiv g g

theorem OracleComp.ProgramLogic.GameEquiv.symm {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {g₁ g₂ : OracleComp spec₁ α} (h : GameEquiv g₁ g₂) : GameEquiv g₂ g₁

theorem OracleComp.ProgramLogic.GameEquiv.trans {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {g₁ g₂ g₃ : OracleComp spec₁ α} (h₁ : GameEquiv g₁ g₂) (h₂ : GameEquiv g₂ g₃) : GameEquiv g₁ g₃

theorem OracleComp.ProgramLogic.GameEquiv.probOutput_eq {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {g₁ g₂ : OracleComp spec₁ α} (h : GameEquiv g₁ g₂) (x : α) : Pr[= x | g₁] = Pr[= x | g₂]

Prop-to-ℝ≥0∞ indicator

noncomputable def OracleComp.ProgramLogic.propInd (P : Prop) : ENNReal

Indicator embedding: lifts P : Prop into ℝ≥0∞ as 1 (true) or 0 (false). This is the quantitative analogue of Loom's pure proposition assertion, but targets the expectation carrier rather than the current assertion lattice.

@[simp]

theorem OracleComp.ProgramLogic.propInd_true : propInd True = 1

@[simp]

theorem OracleComp.ProgramLogic.propInd_false : propInd False = 0

theorem OracleComp.ProgramLogic.propInd_eq_ite {P : Prop} [Decidable P] : propInd P = if P then 1 else 0

@[simp]

theorem OracleComp.ProgramLogic.propInd_and {P Q : Prop} : propInd (P ∧ Q) = propInd P * propInd Q

theorem OracleComp.ProgramLogic.propInd_mono {P Q : Prop} (h : P → Q) : propInd P ≤ propInd Q

theorem OracleComp.ProgramLogic.propInd_le_one (P : Prop) : propInd P ≤ 1

theorem OracleComp.ProgramLogic.propInd_eq_one_iff {P : Prop} : propInd P = 1 ↔ P

theorem OracleComp.ProgramLogic.propInd_eq_zero_iff {P : Prop} : propInd P = 0 ↔ ¬P

theorem OracleComp.ProgramLogic.propInd_or_le {P Q : Prop} : propInd (P ∨ Q) ≤ propInd P + propInd Q

theorem OracleComp.ProgramLogic.propInd_not {P : Prop} : (propInd ¬P) = 1 - propInd P

Notation

def OracleComp.ProgramLogic.«term𝟙⟦_⟧» : Lean.ParserDescr

Numeric proposition indicator: 𝟙⟦P⟧ = 1 if P holds, 0 otherwise. This is deliberately distinct from Loom's ⌜P⌝, which embeds propositions as top/bottom in the active assertion lattice.

def OracleComp.ProgramLogic.wpBracket : Lean.ParserDescr

Quantitative WP notation. wp⟦c⟧ post directly elaborates to wp c post; wp⟦c⟧ standalone elaborates to the lambda fun post => wp c post for partial application sites (e.g. change wp⟦c⟧ or composition with ≤).

def OracleComp.ProgramLogic.wpBracketApp : Lean.ParserDescr

def OracleComp.ProgramLogic.relWpBracket : Lean.ParserDescr

Raw relational WP notation. rwp⟦c₁ ~ c₂ | post; epost₁, epost₂⟧ elaborates to Std.Do'.rwp. The normal assertion carrier and both exception-post carriers are inferred from post, epost₁, and epost₂, so this notation also works for stateful and exception-aware RelWP instances.

def OracleComp.ProgramLogic.«term_≡ₚ_» : Lean.TrailingParserDescr

Game equivalence: g₁ ≡ₚ g₂ means evalDist g₁ = evalDist g₂. Uses syntax + macro_rules because ≡ conflicts with Mathlib's modular equivalence notation (a ≡ b [MOD n]).

def OracleComp.ProgramLogic.«term⟪_~_|_⟫» : Lean.ParserDescr

pRHL coupling: ⟪c₁ ~ c₂ | R⟫ means RelTriple c₁ c₂ R.

def OracleComp.ProgramLogic.«term⟪_≈[_]_|_⟫» : Lean.ParserDescr

Approximate coupling: ⟪c₁ ≈[ε] c₂ | R⟫ means ApproxRelTriple ε c₁ c₂ R.

def OracleComp.ProgramLogic.«term⦃_⦄_≈ₑ_⦃_⦄» : Lean.ParserDescr

eRHL quantitative relational triple: ⦃f⦄ c₁ ≈ₑ c₂ ⦃g⦄ means the quantitative Std.Do'.RelTriple form.

Bridge lemmas: numeric indicators and existing API

theorem OracleComp.ProgramLogic.probEvent_eq_wp_propInd {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) : probEvent oa p = wp oa fun (x : α) => propInd (p x)

probEvent equals WP of propInd postcondition.

theorem OracleComp.ProgramLogic.Relational.RelPost.indicator_eq_propInd {α β : Type} (R : RelPost α β) (a : α) (b : β) : R.indicator a b = propInd (R a b)

RelPost.indicator is pointwise 𝟙⟦_⟧.

theorem OracleComp.ProgramLogic.triple_propInd_iff_probEvent_eq_one {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) : (Triple (propInd True) oa fun (x : α) => propInd (p x)) ↔ probEvent oa p = 1

Almost-sure correctness: Triple 𝟙⟦True⟧ c (fun x => 𝟙⟦p x⟧) iff Pr[ p | c] = 1.

theorem OracleComp.ProgramLogic.triple_propInd_iff_le_probEvent {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) (r : ENNReal) : (Triple r oa fun (x : α) => propInd (p x)) ↔ r ≤ probEvent oa p

Lower-bound event goals are exactly quantitative triples with indicator postconditions.

Expectation-level bridge lemmas

theorem OracleComp.ProgramLogic.wp_propInd_or_le {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p q : α → Prop) : (wp oa fun (x : α) => propInd (p x ∨ q x)) ≤ (wp oa fun (x : α) => propInd (p x)) + wp oa fun (x : α) => propInd (q x)

WP of a disjunction indicator is bounded by the sum of individual WP indicators.

theorem OracleComp.ProgramLogic.probEvent_mono {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) {p q : α → Prop} (h : ∀ (x : α), p x → q x) : probEvent oa p ≤ probEvent oa q

Monotonicity for event probabilities, exposed through the program-logic namespace.

theorem OracleComp.ProgramLogic.markov_bound {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (f : α → ENNReal) (a : ENNReal) (p : α → Prop) (hf : ∀ (x : α), p x → a ≤ f x) : a * probEvent oa p ≤ wp oa f

Markov inequality: if a ≤ f x whenever p x, then a * Pr[ p | oa] ≤ E[f | oa].

theorem OracleComp.ProgramLogic.triple_propInd_of_support {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) (h : ∀ x ∈ support oa, p x) : Triple 1 oa fun (x : α) => propInd (p x)

Triple with precondition 1 and indicator postcondition when the event is almost sure.

Bridge lemmas: game equivalence and advantage

theorem OracleComp.ProgramLogic.GameEquiv.of_relTriple {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {g₁ g₂ : OracleComp spec₁ α} (h : Relational.RelTriple g₁ g₂ (Relational.EqRel α)) : GameEquiv g₁ g₂

Game equivalence from basic pRHL equality coupling.

theorem OracleComp.ProgramLogic.GameEquiv.map_uniformSample_bij {α : Type} [SampleableType α] {f : α → α} (hf : Function.Bijective f) : GameEquiv (f <$> ($ᵗ α)) ($ᵗ α)

A bijection on a uniform sample is still uniform. This is the key lemma behind OTP-style perfect secrecy proofs.

theorem OracleComp.ProgramLogic.GameEquiv.bind_congr {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α β : Type} {g₁ g₂ : OracleComp spec₁ α} {f₁ f₂ : α → OracleComp spec₁ β} (hg : GameEquiv g₁ g₂) (hf : ∀ (a : α), GameEquiv (f₁ a) (f₂ a)) : GameEquiv (g₁ >>= f₁) (g₂ >>= f₂)

Game equivalence is a congruence for bind.

theorem OracleComp.ProgramLogic.GameEquiv.map_congr {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α β : Type} {g₁ g₂ : OracleComp spec₁ α} (f : α → β) (hg : GameEquiv g₁ g₂) : GameEquiv (f <$> g₁) (f <$> g₂)

Game equivalence is a congruence for map.

theorem OracleComp.ProgramLogic.AdvBound.of_tvDist {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {game₁ game₂ : OracleComp spec₁ Bool} {ε₁ ε₂ : ℝ} (hbound : AdvBound game₁ ε₁) (htv : tvDist game₁ game₂ ≤ ε₂) : AdvBound game₂ (ε₁ + ε₂)

Advantage bound via TV distance.

theorem OracleComp.ProgramLogic.AdvBound.of_gameEquiv {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {g₁ g₂ : OracleComp spec₁ Bool} {ε : ℝ} (heq : GameEquiv g₁ g₂) (hbound : AdvBound g₁ ε) : AdvBound g₂ ε

Transfer advantage bounds across equivalent games.