State-Separating Proofs: Advantage and evalDist congruences

This file bridges the SSP Package layer to VCVio's probability machinery.

• Package.runProb reads off the ProbComp produced by running a probability-only package (imports = unifSpec) against an adversary.
• Package.advantage measures the Boolean distinguishing advantage between two packages G₀ G₁ : Package unifSpec E σ against an external adversary A : OracleComp E Bool. It is built directly out of ProbComp.boolDistAdvantage from VCVio.CryptoFoundations.SecExp, and inherits its triangle inequality.
• Package.simulateQ_evalDist_congr is the SSP-flavoured "rewrite the handler up to evalDist" rule: two query implementations that agree pointwise under evalDist yield the same simulation distribution, even when the underlying ProbComps are not propositionally equal.

The program-level reduction lemmas (simulateQ_link_run, run_link, run_link_ofStateless) live in VCVio.SSP.Composition, since they do not involve ProbComp and are stated for the fully universe-polymorphic Package.

Universe layout

Everything in this file is fixed at Type 0: ProbComp : Type → Type and the adversary returns a Bool : Type, so the export indices, ranges, and state are all Type. Only the import range universe and import index universe could a priori be larger, but runProb ties the import to unifSpec : OracleSpec ℕ whose own indices and ranges are in Type.

Bridging to ProbComp

@[reducible]

def VCVio.SSP.Package.runProb {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ α : Type} (P : Package unifSpec E σ) (A : OracleComp E α) : ProbComp α

Run a probability-only package (imports = unifSpec) against an adversary. The result is a ProbComp, ready to be measured with Pr[= true | _] and boolDistAdvantage.

@[simp]

theorem VCVio.SSP.Package.runProb_eq_run {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ α : Type} (P : Package unifSpec E σ) (A : OracleComp E α) : P.runProb A = P.run A

runProb unfolds to run definitionally; exposed as a simp lemma so that SSP-facing lemmas phrased in terms of runProb rewrite cleanly against run-phrased ones in VCVio.SSP.Composition.

Advantage and triangle inequality

noncomputable def VCVio.SSP.Package.advantage {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} (G₀ : Package unifSpec E σ₀) (G₁ : Package unifSpec E σ₁) (A : OracleComp E Bool) : ℝ

The Boolean distinguishing advantage between two probability-only packages, against a single Boolean-valued adversary. The internal state types σ₀, σ₁ of the two games are independent: from the adversary's point of view only the export interface and the resulting output distribution matter.

This quantity is always nonnegative and symmetric in its first two arguments (see advantage_symm), so it should be read as an unsigned gap rather than a signed quantity.

@[simp]

theorem VCVio.SSP.Package.advantage_self {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ : Type} (G : Package unifSpec E σ) (A : OracleComp E Bool) : G.advantage G A = 0

theorem VCVio.SSP.Package.advantage_symm {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} (G₀ : Package unifSpec E σ₀) (G₁ : Package unifSpec E σ₁) (A : OracleComp E Bool) : G₀.advantage G₁ A = G₁.advantage G₀ A

theorem VCVio.SSP.Package.advantage_eq_of_evalDist_runProb_eq {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₀' σ₁ : Type} {G₀ : Package unifSpec E σ₀} {G₀' : Package unifSpec E σ₀'} {G₁ : Package unifSpec E σ₁} {A : OracleComp E Bool} (h : evalDist (G₀.runProb A) = evalDist (G₀'.runProb A)) : G₀.advantage G₁ A = G₀'.advantage G₁ A

If two packages run an adversary to the same ProbComp Bool up to evalDist, their distinguishing advantages against any third package coincide. This is the basic "replace by equivalent game" rule that underlies SSP game-hopping at the advantage level: only the output distributions matter, not the syntactic form of the resulting OracleComp.

theorem VCVio.SSP.Package.advantage_eq_of_evalDist_runProb_eq_right {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ σ₁' : Type} {G₀ : Package unifSpec E σ₀} {G₁ : Package unifSpec E σ₁} {G₁' : Package unifSpec E σ₁'} {A : OracleComp E Bool} (h : evalDist (G₁.runProb A) = evalDist (G₁'.runProb A)) : G₀.advantage G₁ A = G₀.advantage G₁' A

theorem VCVio.SSP.Package.advantage_triangle {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ σ₂ : Type} (G₀ : Package unifSpec E σ₀) (G₁ : Package unifSpec E σ₁) (G₂ : Package unifSpec E σ₂) (A : OracleComp E Bool) : G₀.advantage G₂ A ≤ G₀.advantage G₁ A + G₁.advantage G₂ A

evalDist congruence for handlers

theorem VCVio.SSP.Package.simulateQ_evalDist_congr {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {α : Type} {h₁ h₂ : QueryImpl E ProbComp} (hh : ∀ (q : E.Domain), evalDist (h₁ q) = evalDist (h₂ q)) (A : OracleComp E α) : evalDist (simulateQ h₁ A) = evalDist (simulateQ h₂ A)

Two ProbComp-valued query implementations that agree on every input under evalDist yield identical evaluations of any simulateQ. This is the SSP-flavoured "rewrite the handler up to evalDist" rule used to discharge program equivalences whose underlying computations are not propositionally equal but agree distributionally.

theorem VCVio.SSP.Package.simulateQ_StateT_evalDist_congr {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ α : Type} {h₁ h₂ : QueryImpl E (StateT σ ProbComp)} (hh : ∀ (q : E.Domain) (s : σ), evalDist ((h₁ q).run s) = evalDist ((h₂ q).run s)) (A : OracleComp E α) (s : σ) : evalDist ((simulateQ h₁ A).run s) = evalDist ((simulateQ h₂ A).run s)

Stateful generalization of simulateQ_evalDist_congr: two StateT σ ProbComp-valued query implementations that agree on every (input, state) pair under evalDist yield identical evaluations of (simulateQ _ A).run s for every starting state s.

This is the lemma to use when both sides of a game equivalence are stateful packages with the same internal state type and only their per-query handlers differ up to distribution (e.g., a dhTripleReal-vs-dhTripleRand swap propagated through a stateless reduction).