State-separating handlers: advantage and evalDist congruences

This file contains the probability-facing lower API for QueryImpl.Stateful. It keeps the proof-theory layer close to the SSP literature while leaving the core handler object as the unbundled QueryImpl.Stateful I E σ.

Bridging to ProbComp

@[reducible]

def QueryImpl.Stateful.runProb {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ α : Type} (h : Stateful unifSpec E σ) (s₀ : σ) (A : OracleComp E α) : ProbComp α

Run a probability-only stateful handler from an explicit initial state.

@[reducible]

def QueryImpl.Stateful.runProb₀ {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ α : Type} [Inhabited σ] (h : Stateful unifSpec E σ) (A : OracleComp E α) : ProbComp α

Run a probability-only stateful handler from the default initial state.

@[simp]

theorem QueryImpl.Stateful.runProb_eq_run {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ α : Type} (h : Stateful unifSpec E σ) (s₀ : σ) (A : OracleComp E α) : h.runProb s₀ A = h.run s₀ A

Advantage and triangle inequality

noncomputable def QueryImpl.Stateful.advantage {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} (h₀ : Stateful unifSpec E σ₀) (s₀ : σ₀) (h₁ : Stateful unifSpec E σ₁) (s₁ : σ₁) (A : OracleComp E Bool) : ℝ

Boolean distinguishing advantage between two probability-only stateful handlers, with explicit initial states.

noncomputable def QueryImpl.Stateful.advantage₀ {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} [Inhabited σ₀] [Inhabited σ₁] (h₀ : Stateful unifSpec E σ₀) (h₁ : Stateful unifSpec E σ₁) (A : OracleComp E Bool) : ℝ

Boolean distinguishing advantage from default initial states.

@[simp]

theorem QueryImpl.Stateful.advantage_self {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ : Type} (h : Stateful unifSpec E σ) (s₀ : σ) (A : OracleComp E Bool) : h.advantage s₀ h s₀ A = 0

theorem QueryImpl.Stateful.advantage_symm {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} (h₀ : Stateful unifSpec E σ₀) (s₀ : σ₀) (h₁ : Stateful unifSpec E σ₁) (s₁ : σ₁) (A : OracleComp E Bool) : h₀.advantage s₀ h₁ s₁ A = h₁.advantage s₁ h₀ s₀ A

theorem QueryImpl.Stateful.advantage_eq_of_evalDist_runProb_eq {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₀' σ₁ : Type} {h₀ : Stateful unifSpec E σ₀} {s₀ : σ₀} {h₀' : Stateful unifSpec E σ₀'} {s₀' : σ₀'} {h₁ : Stateful unifSpec E σ₁} {s₁ : σ₁} {A : OracleComp E Bool} (h_eq : 𝒟[h₀.runProb s₀ A] = 𝒟[h₀'.runProb s₀' A]) : h₀.advantage s₀ h₁ s₁ A = h₀'.advantage s₀' h₁ s₁ A

theorem QueryImpl.Stateful.advantage_eq_of_evalDist_runProb_eq_right {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ σ₁' : Type} {h₀ : Stateful unifSpec E σ₀} {s₀ : σ₀} {h₁ : Stateful unifSpec E σ₁} {s₁ : σ₁} {h₁' : Stateful unifSpec E σ₁'} {s₁' : σ₁'} {A : OracleComp E Bool} (h_eq : 𝒟[h₁.runProb s₁ A] = 𝒟[h₁'.runProb s₁' A]) : h₀.advantage s₀ h₁ s₁ A = h₀.advantage s₀ h₁' s₁' A

theorem QueryImpl.Stateful.advantage_triangle {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ σ₂ : Type} (h₀ : Stateful unifSpec E σ₀) (s₀ : σ₀) (h₁ : Stateful unifSpec E σ₁) (s₁ : σ₁) (h₂ : Stateful unifSpec E σ₂) (s₂ : σ₂) (A : OracleComp E Bool) : h₀.advantage s₀ h₂ s₂ A ≤ h₀.advantage s₀ h₁ s₁ A + h₁.advantage s₁ h₂ s₂ A

evalDist congruence for handlers

theorem QueryImpl.Stateful.simulateQ_evalDist_congr {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {α : Type} {h₁ h₂ : QueryImpl E ProbComp} (hh : ∀ (q : E.Domain), 𝒟[h₁ q] = 𝒟[h₂ q]) (A : OracleComp E α) : 𝒟[simulateQ h₁ A] = 𝒟[simulateQ h₂ A]

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

theorem QueryImpl.Stateful.simulateQ_StateT_evalDist_congr_of_bij {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {α σ₁ σ₂ : Type} (h₁ : QueryImpl E (StateT σ₁ ProbComp)) (h₂ : QueryImpl E (StateT σ₂ ProbComp)) (φ : σ₁ ≃ σ₂) (hh : ∀ (q : E.Domain) (s : σ₁), 𝒟[(h₁ q).run s] = 𝒟[Prod.map id ⇑φ.symm <$> (h₂ q).run (φ s)]) (A : OracleComp E α) (s : σ₁) : 𝒟[(simulateQ h₁ A).run s] = 𝒟[Prod.map id ⇑φ.symm <$> (simulateQ h₂ A).run (φ s)]

Functoriality of runProb

theorem QueryImpl.Stateful.runProb_map {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ α β : Type} (h : Stateful unifSpec E σ) (s₀ : σ) (f : α → β) (A : OracleComp E α) : h.runProb s₀ (f <$> A) = f <$> h.runProb s₀ A