State-Separating Proofs: Hybrid arguments and the linked-game reduction

This file collects two staple SSP results, phrased at the package level:

• Package.advantage_hybrid — the iterated triangle inequality for an n-step hybrid. Given a sequence of games G₀, G₁, ..., Gₙ (with potentially different state types) and a single Boolean adversary A, the distinguishing advantage between G₀ and Gₙ is bounded by the sum of consecutive advantages.

• Package.shiftLeft and Package.run_link_eq_run_shiftLeft — the SSP "reduction" view of run_link: running the linked game (P.link Q) against an adversary A produces the same OracleComp distribution as running the inner game Q against the shifted adversary P.shiftLeft A. The advantage-level corollary Package.advantage_link_left_eq_advantage_shiftLeft says that replacing the inner game in P.link _ only shifts the adversary; the outer reduction package P becomes part of the new adversary, exactly as in SSProve.

These two ingredients together justify the standard SSP game-hopping pattern: produce a chain of intermediate games related by link-ed reductions, then collapse the chain via the hybrid inequality.

Universe layout

Package.shiftLeft and Package.run_link_eq_run_shiftLeft are program-level statements and are kept fully universe-polymorphic in the indices uᵢ, uₘ, uₑ, the import range universe vᵢ, and the export range / state / result universe v (matching Composition.lean). Note that vᵢ does not appear in shiftLeft's own signature: shiftLeft produces an OracleComp M α, which is oblivious to the import spec. vᵢ only enters through the inner package Q : Package I M σ₂ in run_link_eq_run_shiftLeft, whose import range can live in an arbitrary universe independent from v. The hybrid theorem and the advantage-level reduction live in the Type 0 world (forced by ProbComp and Bool); their export indices remain free in uₑ.

Iterated triangle inequality (hybrid argument)

theorem VCVio.SSP.Package.advantage_hybrid {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ : ℕ → Type} (G : (i : ℕ) → Package unifSpec E (σ i)) (A : OracleComp E Bool) (n : ℕ) : (G 0).advantage (G n) A ≤ ∑ i ∈ Finset.range n, (G i).advantage (G (i + 1)) A

Hybrid lemma. For any sequence of games G 0, G 1, ..., G n and any single Boolean adversary A, the distinguishing advantage between the endpoints is bounded by the sum of consecutive advantages.

The state types may differ from step to step: σ : ℕ → Type and G i : Package unifSpec E (σ i). This is just the iterated boolDistAdvantage triangle inequality, packaged for SSP-style game-hopping proofs.

Shifted adversary and the SSP reduction lemma

def VCVio.SSP.Package.shiftLeft {ιₘ : Type uₘ} {ιₑ : Type uₑ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ : Type v} (P : Package M E σ₁) {α : Type v} (A : OracleComp E α) : OracleComp M α

The shifted adversary obtained by absorbing the outer reduction package P into the adversary. Given an outer reduction P : Package M E σ₁ and an external adversary A : OracleComp E α querying the export interface E, this returns an adversary against the intermediate interface M by simulating A through P.impl and projecting away the final outer state.

This is the SSP "reduction-to-the-distinguisher" move: the outer package becomes part of the adversary, so a fresh round of analysis only needs to consider the inner game.

@[simp]

theorem VCVio.SSP.Package.shiftLeft_pure {ιₘ : Type uₘ} {ιₑ : Type uₑ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ : Type v} (P : Package M E σ₁) {α : Type v} (x : α) : P.shiftLeft (pure x) = pure x

theorem VCVio.SSP.Package.run_link_eq_run_shiftLeft {ιₘ : Type uₘ} {ιₑ : Type uₑ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ : Type v} {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {σ₂ α : Type v} (P : Package M E σ₁) (Q : Package I M σ₂) (A : OracleComp E α) : (P.link Q).run A = Q.run (P.shiftLeft A)

SSP reduction (program form). Running the linked game (P.link Q) against adversary A produces the same OracleComp distribution as running the inner game Q against the shifted adversary P.shiftLeft A.

This is the equational form of the "swap the outer reduction into the adversary" step. The advantage-level corollary advantage_link_left_eq_advantage_shiftLeft follows by rewriting both sides under boolDistAdvantage.

Advantage-form reduction

theorem VCVio.SSP.Package.advantage_link_left_eq_advantage_shiftLeft {ιₘ : Type uₘ} {ιₑ : Type uₑ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ_Q₀ σ_Q₁ : Type} (P : Package M E σ₁) (Q₀ : Package unifSpec M σ_Q₀) (Q₁ : Package unifSpec M σ_Q₁) (A : OracleComp E Bool) : (P.link Q₀).advantage (P.link Q₁) A = Q₀.advantage Q₁ (P.shiftLeft A)

SSP reduction (advantage form). With the same outer reduction package P : Package M E σ₁ linked to two candidate inner games Q₀, Q₁ exporting M, the distinguishing advantage between the linked games equals the advantage between the inner games against the shifted adversary P.shiftLeft A. The outer reduction package P is absorbed into the adversary.

Universe-polymorphism sanity checks