General Hybrid Argument Theory

This file provides reusable infrastructure for hybrid argument proofs, following the approach in "Mechanizing Nested Hybrid Arguments in Nominal-CatCrypt" (Larsen & Schurmann, CSF 2025).

Main Results

• advantage_hybrid_dep - Dependent hybrid inequality: when step advantages differ, Adv(G 0, G n) ≤ Σᵢ Adv(G i, G (i+1))
• advantage_hybrid_uniform - Uniform hybrid bound: Adv(G 0, G n) ≤ n * ε when each step is bounded by ε
• advantage_hybrid_eq - Hybrid equality (strengthening of the paper's main theorem): When all adjacent games are perfectly indistinguishable, Advantage (G 0) (G n) = 0

Overview

The standard game-hopping proof technique transitions through a sequence of hybrid games G₀, G₁, ..., Gₙ. The triangle inequality gives:

Adv(G₀, Gₙ) ≤ Σᵢ Adv(Gᵢ, Gᵢ₊₁)

The CSF 2025 paper strengthens this to an equality when all step advantages are equal, using the law of total probability and CONST/RAND packages. At the distribution level (without stateful packages), the key insight is simpler: the triangle inequality already provides the bound, and the equality case follows from zero-advantage of perfectly indistinguishable games.

References

• [Larsen & Schurmann, Mechanizing Nested Hybrid Arguments, CSF 2025]
• CatCrypt/Lean: CatCrypt/Tactics/Triangle.lean (basic triangle chains)
• CatCrypt/Lean: CatCrypt/Examples/SymmRatchet.lean (concrete hybrid argument)

Telescoping Sum Helpers

noncomputable def CatCrypt.Crypto.HybridArgument.telescope_sum (f : ℕ → ENNReal) (n : ℕ) : ENNReal

Telescoping sum: the sum of consecutive differences. This is the fundamental decomposition used in hybrid arguments.

Equations

• CatCrypt.Crypto.HybridArgument.telescope_sum f n = ∑ i ∈ Finset.range n, max (f i - f (i + 1)) (f (i + 1) - f i)

Core Hybrid Argument Theorems

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_dep {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (n : ℕ) : AdvantageA (G 0) (G n) A ≤ ∑ i ∈ Finset.range n, AdvantageA (G i) (G (i + 1)) A

Dependent hybrid inequality (general form).

For a sequence of games G : Fin (n+1) → SPComp α and an adversary A, the advantage between the first and last game is bounded by the sum of per-step advantages.

This generalizes advantageA_triangle_n from SymmRatchet.lean to a reusable theorem. Unlike AdvantageA_triangle_chain (which uses List), this uses ℕ-indexed games for easier composition with Finset.sum.

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_dep_bool (G : ℕ → Core.SPComp Bool) (n : ℕ) : Advantage (G 0) (G n) ≤ ∑ i ∈ Finset.range n, Advantage (G i) (G (i + 1))

Dependent hybrid inequality for Advantage (Bool games, no adversary).

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_uniform {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (n : ℕ) (ε : ENNReal) (hstep : ∀ i < n, AdvantageA (G i) (G (i + 1)) A ≤ ε) : AdvantageA (G 0) (G n) A ≤ ↑n * ε

Uniform hybrid bound: when each step is bounded by the same ε, the total advantage is at most n * ε.

This is the typical use case: all hybrid steps have the same security level (e.g., each step reduces to one CPA query).

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_zero {α : Type} (G : ℕ → Core.SPComp α) (n : ℕ) (hperf : ∀ i < n, Relational.rHoare Relational.eqPre (G i) (G (i + 1)) Relational.eqPost) (A : α → Core.SPComp Bool) : AdvantageA (G 0) (G n) A = 0

Hybrid equality: when all adjacent games are perfectly indistinguishable (via rHoare eqPre/eqPost), the advantage is 0.

This captures the "equality" case from the CSF 2025 paper: when transitions are information-theoretically perfect, the total advantage vanishes.

Boundary Composition Helpers

These helpers allow composing hybrid arguments with boundary conditions:
when the first hybrid game equals the "real" game and the last equals the "ideal" game. 

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_bound {α : Type} (real ideal : Core.SPComp α) (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (n : ℕ) (ε : ENNReal) (hleft : real = G 0) (hright : ideal = G n) (hstep : ∀ i < n, AdvantageA (G i) (G (i + 1)) A ≤ ε) : AdvantageA real ideal A ≤ ↑n * ε

Hybrid argument with boundary conditions: if real = G 0 and ideal = G n, then Adv(real, ideal) ≤ n * ε.

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_dep_bound {α : Type} (real ideal : Core.SPComp α) (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (n : ℕ) (ε : ℕ → ENNReal) (hleft : real = G 0) (hright : ideal = G n) (hstep : ∀ i < n, AdvantageA (G i) (G (i + 1)) A ≤ ε i) : AdvantageA real ideal A ≤ ∑ i ∈ Finset.range n, ε i

Hybrid argument with dependent bounds and boundary conditions: the general form with different per-step bounds.

Factorization + Hybrid Composition

A common pattern: factor out a common post-processing step, apply the hybrid
argument to the core computation, then compose. 

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_factored {α β : Type} (G_base : ℕ → Core.SPComp α) (f : α → Core.SPComp β) (A : β → Core.SPComp Bool) (n : ℕ) (ε : ENNReal) (hstep : ∀ i < n, (AdvantageA (G_base i) (G_base (i + 1)) fun (x : α) => (f x).bind A) ≤ ε) : AdvantageA ((G_base 0).bind f) ((G_base n).bind f) A ≤ ↑n * ε

Factored hybrid bound: when real and ideal games factor through a common post-processing f, apply the hybrid argument to the base games.

Nested Hybrid Arguments

For multi-dimensional hybrid arguments (e.g., multi-instance + multi-query),
the inner and outer hybrid bounds compose multiplicatively. 

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_nested {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (m q : ℕ) (ε : ENNReal) (hstep : ∀ i < m, AdvantageA (G i) (G (i + 1)) A ≤ ↑q * ε) : AdvantageA (G 0) (G m) A ≤ ↑m * (↑q * ε)

Nested hybrid bound: composing two levels of hybrid arguments.

If the outer hybrid has m steps each bounded by ε_outer, and ε_outer is itself bounded by an inner hybrid with q steps each ≤ ε, then the total bound is m * q * ε.

Equality Forms

The standard hybrid argument gives `≤`. When all step advantages are
*equal* (not just bounded), and the per-step advantage comes from an
equality (like `dHybrid_step_eq`), we can derive tighter statements.

The key insight: if `Adv(G i, G(i+1)) = ε` for all `i < n`, then
`Adv(G 0, G n) ≤ n * ε`. The converse (achieving equality) requires
monotonicity of `Pr[A ∘ G i = true]` in `i`, which ensures the
telescoping sum has consistent signs.

We provide the "≤" version with step equalities, which is the most
practically useful form. 

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_uniform_eq {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (n : ℕ) (ε : ENNReal) (hstep : ∀ i < n, AdvantageA (G i) (G (i + 1)) A = ε) : AdvantageA (G 0) (G n) A ≤ ↑n * ε

Uniform hybrid bound from equalities: when each step advantage equals ε, the total advantage is at most n * ε.

This is the distributional analogue of the CSF 2025 paper's Theorem 4. The bound is tight when the telescoping sum has consistent signs.

theorem CatCrypt.Crypto.HybridArgument.advantage_hybrid_nested_eq {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (m q : ℕ) (ε : ENNReal) (hstep : ∀ i < m, AdvantageA (G i) (G (i + 1)) A ≤ ↑q * ε) : AdvantageA (G 0) (G m) A ≤ ↑m * ↑q * ε

Nested hybrid bound from equalities: composing two levels of hybrid arguments where both inner and outer step advantages are exact equalities.