Forking Lemma

theorem OracleComp.probFailure_bind_congr {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SelectableType (spec.range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α β γ : Type} [spec.FiniteRange] (oa : OracleComp spec α) {ob : α → OracleComp spec β} {oc : α → OracleComp spec γ} (h : ∀ x ∈ oa.support, [⊥|ob x] = [⊥|oc x]) : [⊥|oa >>= ob] = [⊥|oa >>= oc]

theorem OracleComp.probFailure_bind_congr' {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SelectableType (spec.range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α β γ : Type} [spec.FiniteRange] (oa : OracleComp spec α) {ob : α → OracleComp spec β} {oc : α → OracleComp spec γ} (h : ∀ (x : α), [⊥|ob x] = [⊥|oc x]) : [⊥|oa >>= ob] = [⊥|oa >>= oc]

theorem OracleComp.probFailure_bind_eq_sum_probFailure {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SelectableType (spec.range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α β γ : Type} [spec.FiniteRange] (oa : OracleComp spec α) {ob : α → OracleComp spec β} {σ : Type u_1} {s : Finset σ} {oc : σ → α → OracleComp spec γ} : [⊥|oa >>= ob] = ∑ x ∈ s, [⊥|oa >>= oc x]

structure OracleComp.forkInput {ι : Type} (spec : OracleSpec ι) (α : Type) : Type (u_1 + 1)

• main : OracleComp spec α

  The main program to fork execution of

• queryBound : ι → ℕ

  A bound on the number of queries the adversary makes

• js : List ι

  List of oracles that are queried during computation (used to order seed generation).

def OracleComp.fork' {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SelectableType (spec.range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) : OracleComp spec (α × α)

Version of fork that doesn't choose s ahead of time. Should give better concrete bounds.

Equations

• One or more equations did not get rendered due to their size.

theorem OracleComp.le_probOutput_fork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SelectableType (spec.range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.FiniteRange] (s : Fin (qb i + 1)) : let h := ↑(Fintype.card (spec.range i)); let q := qb i + 1; [=some s|cf <$> main] ^ 2 - [=some s|cf <$> main] / h ≤ [fun (x : α × α) => match x with | (x₁, x₂) => cf x₁ = some s ∧ cf x₂ = some s|main.fork' qb js i cf]

theorem OracleComp.probFailure_fork_le {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SelectableType (spec.range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.FiniteRange] : let acc := 1 - [=none|cf <$> main]; let h := ↑(Fintype.card (spec.range i)); let q := qb i + 1; [⊥|main.fork' qb js i cf] ≤ 1 - acc * (acc / ↑q - h⁻¹)

theorem OracleComp.exists_log_of_mem_support_fork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SelectableType (spec.range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.FiniteRange] (x₁ x₂ : α) (h : (x₁, x₂) ∈ (main.fork' qb js i cf).support) : ∃ (s : Fin (qb i + 1)), cf x₁ = some s ∧ cf x₂ = some s ∧ ∃ (log₁ : spec.QueryLog) (hcf₁ : ↑s < log₁.countQ i) (log₂ : spec.QueryLog) (hcf₁_1 : ↑s < log₂.countQ i), (log₁.getQ i)[s].1 = (log₂.getQ i)[s].1 ∧ (log₁.getQ i)[s].2 ≠ (log₂.getQ i)[s].2 ∧ (x₁, log₁) ∈ (simulateQ loggingOracle main).run.support ∧ (x₂, log₂) ∈ (simulateQ loggingOracle main).run.support