State-separating handlers: hybrid arguments

Hybrid and linked-game advantage lemmas for QueryImpl.Stateful handlers with explicit initial states.

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

Hybrid lemma for any sequence of stateful handlers and explicit initial states.

theorem QueryImpl.Stateful.advantage_link_left_eq_advantage_shiftLeft {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {ιₘ : Type uₘ} {M : OracleSpec ιₘ} {σP σ₀ σ₁ : Type} (outer : Stateful M E σP) (sP : σP) (inner₀ : Stateful unifSpec M σ₀) (s₀ : σ₀) (inner₁ : Stateful unifSpec M σ₁) (s₁ : σ₁) (A : OracleComp E Bool) : (outer.link inner₀).advantage (sP, s₀) (outer.link inner₁) (sP, s₁) A = inner₀.advantage s₀ inner₁ s₁ (outer.shiftLeft sP A)

Advantage form of the linked-game reduction. The outer handler and its initial state are absorbed into the shifted client.