State-separating handlers: identical-until-bad

Identical-until-bad wrappers for QueryImpl.Stateful handlers whose state is of the form σ × Bool, with the Boolean component acting as the bad flag.

def QueryImpl.Stateful.PreservesNoBadInvariant {ιₑ : Type} {E : OracleSpec ιₑ} {σ : Type} (h : Stateful unifSpec E (σ × Bool)) (Inv : σ → Prop) : Prop

A stateful handler preserves a state invariant as long as the bad flag has not fired.

theorem QueryImpl.Stateful.advantage_le_expectedQuerySlack_plus_probEvent_bad {ιₑ : Type} {E : OracleSpec ιₑ} {σ : Type} (h₀ h₁ : Stateful unifSpec E (σ × Bool)) (s_init : σ) (chargedQuery : E.Domain → Prop) [DecidablePred chargedQuery] (querySlack : σ → ENNReal) (h_step_tv_charged : ∀ (t : E.Domain), chargedQuery t → ∀ (s : σ), ENNReal.ofReal (tvDist ((h₀ t).run (s, false)) ((h₁ t).run (s, false))) ≤ querySlack s) (h_step_eq_uncharged : ∀ (t : E.Domain), ¬chargedQuery t → ∀ (p : σ × Bool), (h₀ t).run p = (h₁ t).run p) (h_mono₀ : ∀ (t : E.Domain) (p : σ × Bool), p.2 = true → ∀ z ∈ support ((h₀ t).run p), z.2.2 = true) (A : OracleComp E Bool) {queryBudget : ℕ} (h_bound : A.IsQueryBoundP chargedQuery queryBudget) : ENNReal.ofReal (h₀.advantage (s_init, false) h₁ (s_init, false) A) ≤ OracleComp.ProgramLogic.Relational.expectedQuerySlack h₀ chargedQuery querySlack A queryBudget (s_init, false) + probEvent ((simulateQ h₀ A).run (s_init, false)) fun (z : Bool × σ × Bool) => z.2.2 = true

State-dependent ε-perturbed identical-until-bad with output bad flag.

theorem QueryImpl.Stateful.advantage_le_queryBound_mul_slack_plus_probEvent_bad {ιₑ : Type} {E : OracleSpec ιₑ} {σ : Type} (h₀ h₁ : Stateful unifSpec E (σ × Bool)) (s_init : σ) (chargedQuery : E.Domain → Prop) [DecidablePred chargedQuery] (querySlack : ENNReal) (h_step_tv_charged : ∀ (t : E.Domain), chargedQuery t → ∀ (s : σ), ENNReal.ofReal (tvDist ((h₀ t).run (s, false)) ((h₁ t).run (s, false))) ≤ querySlack) (h_step_eq_uncharged : ∀ (t : E.Domain), ¬chargedQuery t → ∀ (p : σ × Bool), (h₀ t).run p = (h₁ t).run p) (h_mono₀ : ∀ (t : E.Domain) (p : σ × Bool), p.2 = true → ∀ z ∈ support ((h₀ t).run p), z.2.2 = true) (A : OracleComp E Bool) {queryBudget : ℕ} (h_bound : A.IsQueryBoundP chargedQuery queryBudget) : ENNReal.ofReal (h₀.advantage (s_init, false) h₁ (s_init, false) A) ≤ ↑queryBudget * querySlack + probEvent ((simulateQ h₀ A).run (s_init, false)) fun (z : Bool × σ × Bool) => z.2.2 = true

Constant-ε identical-until-bad with output bad flag.

Invariant-gated variants

theorem QueryImpl.Stateful.advantage_le_expectedQuerySlack_plus_probEvent_bad_of_inv {ιₑ : Type} {E : OracleSpec ιₑ} {σ : Type} (h₀ h₁ : Stateful unifSpec E (σ × Bool)) (s_init : σ) (Inv : σ → Prop) [DecidablePred Inv] (chargedQuery : E.Domain → Prop) [DecidablePred chargedQuery] (querySlack : σ → ENNReal) (h_step_tv_charged : ∀ (t : E.Domain), chargedQuery t → ∀ (s : σ), Inv s → ENNReal.ofReal (tvDist ((h₀ t).run (s, false)) ((h₁ t).run (s, false))) ≤ querySlack s) (h_step_eq_uncharged : ∀ (t : E.Domain), ¬chargedQuery t → ∀ (p : σ × Bool), (h₀ t).run p = (h₁ t).run p) (h_mono₀ : ∀ (t : E.Domain) (p : σ × Bool), p.2 = true → ∀ z ∈ support ((h₀ t).run p), z.2.2 = true) (A : OracleComp E Bool) {queryBudget : ℕ} (h_bound : A.IsQueryBoundP chargedQuery queryBudget) : ENNReal.ofReal (h₀.advantage (s_init, false) h₁ (s_init, false) A) ≤ OracleComp.ProgramLogic.Relational.expectedQuerySlack h₀ chargedQuery (fun (s : σ) => if Inv s then querySlack s else 1) A queryBudget (s_init, false) + probEvent ((simulateQ h₀ A).run (s_init, false)) fun (z : Bool × σ × Bool) => z.2.2 = true

Invariant-gated state-dependent ε-perturbed identical-until-bad.

The costly-step TV hypothesis is required only for states satisfying Inv. The generated query-slack function charges the intended ε s on invariant states and the conservative fallback cost 1 elsewhere.

theorem QueryImpl.Stateful.advantage_le_expectedQuerySlack_plus_probEvent_bad_of_inv_preserved {ιₑ : Type} {E : OracleSpec ιₑ} {σ : Type} (h₀ h₁ : Stateful unifSpec E (σ × Bool)) (s_init : σ) (Inv : σ → Prop) (h_init_inv : Inv s_init) (h_pres : h₀.PreservesNoBadInvariant Inv) (chargedQuery : E.Domain → Prop) [DecidablePred chargedQuery] (querySlack : σ → ENNReal) (h_step_tv_charged : ∀ (t : E.Domain), chargedQuery t → ∀ (s : σ), Inv s → ENNReal.ofReal (tvDist ((h₀ t).run (s, false)) ((h₁ t).run (s, false))) ≤ querySlack s) (h_step_eq_uncharged : ∀ (t : E.Domain), ¬chargedQuery t → ∀ (p : σ × Bool), (h₀ t).run p = (h₁ t).run p) (h_mono₀ : ∀ (t : E.Domain) (p : σ × Bool), p.2 = true → ∀ z ∈ support ((h₀ t).run p), z.2.2 = true) (A : OracleComp E Bool) {queryBudget : ℕ} (h_bound : A.IsQueryBoundP chargedQuery queryBudget) : ENNReal.ofReal (h₀.advantage (s_init, false) h₁ (s_init, false) A) ≤ OracleComp.ProgramLogic.Relational.expectedQuerySlack h₀ chargedQuery querySlack A queryBudget (s_init, false) + probEvent ((simulateQ h₀ A).run (s_init, false)) fun (z : Bool × σ × Bool) => z.2.2 = true

Invariant-preserving state-dependent ε-perturbed identical-until-bad.

If the real handler preserves Inv from the initial no-bad state, then the fallback branch in the invariant-gated cost is unreachable, so the final expected-cost term uses the tight query-slack function ε.