State-separating handlers: distributional equivalence

QueryImpl.Stateful.DistEquiv h₀ s₀ h₁ s₁ says that two stateful handlers, started from explicit initial states, produce the same output distribution against every client computation.

def QueryImpl.Stateful.DistEquiv {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} [I.Fintype] [I.Inhabited] {σ₀ σ₁ : Type} (h₀ : Stateful I E σ₀) (s₀ : σ₀) (h₁ : Stateful I E σ₁) (s₁ : σ₁) : Prop

Perfect distributional equivalence of two stateful handlers from explicit initial states.

def QueryImpl.Stateful.«term(_,_)≡ᵈ(_,_)» : Lean.ParserDescr

Perfect distributional equivalence of two stateful handlers from explicit initial states.

def QueryImpl.Stateful.DistEquiv₀ {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} [I.Fintype] [I.Inhabited] {σ₀ σ₁ : Type} [Inhabited σ₀] [Inhabited σ₁] (h₀ : Stateful I E σ₀) (h₁ : Stateful I E σ₁) : Prop

Perfect distributional equivalence from default initial states.

def QueryImpl.Stateful.«term_≡ᵈ₀_» : Lean.TrailingParserDescr

Perfect distributional equivalence from default initial states.

Relation laws

theorem QueryImpl.Stateful.DistEquiv.refl {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ : Type} [I.Fintype] [I.Inhabited] (h : Stateful I E σ) (s : σ) : h.DistEquiv s h s

theorem QueryImpl.Stateful.DistEquiv.symm {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} [I.Fintype] [I.Inhabited] {h₀ : Stateful I E σ₀} {s₀ : σ₀} {h₁ : Stateful I E σ₁} {s₁ : σ₁} (h : h₀.DistEquiv s₀ h₁ s₁) : h₁.DistEquiv s₁ h₀ s₀

theorem QueryImpl.Stateful.DistEquiv.trans {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ σ₂ : Type} [I.Fintype] [I.Inhabited] {h₀ : Stateful I E σ₀} {s₀ : σ₀} {h₁ : Stateful I E σ₁} {s₁ : σ₁} {h₂ : Stateful I E σ₂} {s₂ : σ₂} (h₀₁ : h₀.DistEquiv s₀ h₁ s₁) (h₁₂ : h₁.DistEquiv s₁ h₂ s₂) : h₀.DistEquiv s₀ h₂ s₂

Constructors

theorem QueryImpl.Stateful.DistEquiv.of_run_evalDist {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} [I.Fintype] [I.Inhabited] {h₀ : Stateful I E σ₀} {s₀ : σ₀} {h₁ : Stateful I E σ₁} {s₁ : σ₁} (h : ∀ {α : Type} (A : OracleComp E α), 𝒟[h₀.run s₀ A] = 𝒟[h₁.run s₁ A]) : h₀.DistEquiv s₀ h₁ s₁

theorem QueryImpl.Stateful.DistEquiv.run_evalDist_eq {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} [I.Fintype] [I.Inhabited] {h₀ : Stateful I E σ₀} {s₀ : σ₀} {h₁ : Stateful I E σ₁} {s₁ : σ₁} (h : h₀.DistEquiv s₀ h₁ s₁) {α : Type} (A : OracleComp E α) : 𝒟[h₀.run s₀ A] = 𝒟[h₁.run s₁ A]

theorem QueryImpl.Stateful.DistEquiv.run₀_evalDist_eq {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} [I.Fintype] [I.Inhabited] {h₀ : Stateful I E σ₀} {h₁ : Stateful I E σ₁} [Inhabited σ₀] [Inhabited σ₁] (h : h₀.DistEquiv₀ h₁) {α : Type} (A : OracleComp E α) : 𝒟[h₀.run₀ A] = 𝒟[h₁.run₀ A]

theorem QueryImpl.Stateful.DistEquiv.runProb_evalDist_eq {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} {h₀ : Stateful unifSpec E σ₀} {s₀ : σ₀} {h₁ : Stateful unifSpec E σ₁} {s₁ : σ₁} (h : h₀.DistEquiv s₀ h₁ s₁) {α : Type} (A : OracleComp E α) : 𝒟[h₀.runProb s₀ A] = 𝒟[h₁.runProb s₁ A]

theorem QueryImpl.Stateful.DistEquiv.runProb₀_evalDist_eq {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} {h₀ : Stateful unifSpec E σ₀} {h₁ : Stateful unifSpec E σ₁} [Inhabited σ₀] [Inhabited σ₁] (h : h₀.DistEquiv₀ h₁) {α : Type} (A : OracleComp E α) : 𝒟[h₀.runProb₀ A] = 𝒟[h₁.runProb₀ A]

theorem QueryImpl.Stateful.DistEquiv.of_run_eq {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} [I.Fintype] [I.Inhabited] {h₀ : Stateful I E σ₀} {s₀ : σ₀} {h₁ : Stateful I E σ₁} {s₁ : σ₁} (h : ∀ {α : Type} (A : OracleComp E α), h₀.run s₀ A = h₁.run s₁ A) : h₀.DistEquiv s₀ h₁ s₁

theorem QueryImpl.Stateful.DistEquiv.of_step {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ : Type} [I.Fintype] [I.Inhabited] {h₀ h₁ : Stateful I E σ} (h_impl : ∀ (q : E.Domain) (s : σ), 𝒟[(h₀ q).run s] = 𝒟[(h₁ q).run s]) (s₀ : σ) : h₀.DistEquiv s₀ h₁ s₀

theorem QueryImpl.Stateful.DistEquiv.of_step_bij {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} (h₀ : Stateful unifSpec E σ₀) (h₁ : Stateful unifSpec E σ₁) (φ : σ₀ ≃ σ₁) (h_impl : ∀ (q : E.Domain) (s : σ₀), 𝒟[(h₀ q).run s] = 𝒟[Prod.map id ⇑φ.symm <$> (h₁ q).run (φ s)]) (s₀ : σ₀) : h₀.DistEquiv s₀ h₁ (φ s₀)

Bridge to advantage

theorem QueryImpl.Stateful.DistEquiv.advantage_left {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ σ₀ σ₁ : Type} {h₀ : Stateful unifSpec E σ₀} {s₀ : σ₀} {h₀' : Stateful unifSpec E σ} {s₀' : σ} (h : h₀.DistEquiv s₀ h₀' 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.DistEquiv.advantage_right {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ σ₀ σ₁ : Type} (h₀ : Stateful unifSpec E σ₀) (s₀ : σ₀) {h₁ : Stateful unifSpec E σ₁} {s₁ : σ₁} {h₁' : Stateful unifSpec E σ} {s₁' : σ} (h : h₁.DistEquiv s₁ h₁' s₁') (A : OracleComp E Bool) : h₀.advantage s₀ h₁ s₁ A = h₀.advantage s₀ h₁' s₁' A

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

Compositional congruences

theorem QueryImpl.Stateful.DistEquiv.link_inner_congr {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₀ σ₁ : Type} {ιₘ : Type uₘ} {M : OracleSpec ιₘ} {σ_P : Type} (outer : Stateful M E σ_P) (sP : σ_P) {inner₀ : Stateful unifSpec M σ₀} {s₀ : σ₀} {inner₁ : Stateful unifSpec M σ₁} {s₁ : σ₁} (h : inner₀.DistEquiv s₀ inner₁ s₁) : (outer.link inner₀).DistEquiv (sP, s₀) (outer.link inner₁) (sP, s₁)

theorem QueryImpl.Stateful.DistEquiv.parSum_congr {ιᵢ₁ ιᵢ₂ : Type uₘ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} [I₁.Fintype] [I₁.Inhabited] [I₂.Fintype] [I₂.Inhabited] {ιₑ₁ ιₑ₂ : Type uₑ} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} {σ₁ σ₂ : Type} {h₁ h₁' : Stateful I₁ E₁ σ₁} {s₁ : σ₁} {h₂ h₂' : Stateful I₂ E₂ σ₂} {s₂ : σ₂} (hh₁ : ∀ (q : E₁.Domain) (s : σ₁), 𝒟[(h₁ q).run s] = 𝒟[(h₁' q).run s]) (hh₂ : ∀ (q : E₂.Domain) (s : σ₂), 𝒟[(h₂ q).run s] = 𝒟[(h₂' q).run s]) : (h₁.parSum h₂).DistEquiv (s₁, s₂) (h₁'.parSum h₂') (s₁, s₂)

parSum congruence on both sides from per-factor handler equivalences with explicit initial states.