Forking Lemma

theorem probOutput_prod_mk_seq_map_eq_mul {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (z : α × β) : [=z|(fun (x1 : α) (x2 : β) => (x1, x2)) <$> oa <*> ob] = [=z.1|oa] * [=z.2|ob]

theorem probOutput_prod_mk_seq_map_eq_mul' {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (x : α) (y : β) : [=(x, y)|(fun (x1 : α) (x2 : β) => (x1, x2)) <$> oa <*> ob] = [=x|oa] * [=y|ob]

theorem probOutput_prod_mk_apply_seq_map_eq_mul {ι : Type u} {spec : OracleSpec ι} {α β γ δ : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → γ) (g : β → δ) (z : γ × δ) : [=z|(fun (x1 : α) (x2 : β) => (f x1, g x2)) <$> oa <*> ob] = [=z.1|f <$> oa] * [=z.2|g <$> ob]

theorem probOutput_prod_mk_apply_seq_map_eq_mul' {ι : Type u} {spec : OracleSpec ι} {α β γ δ : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → γ) (g : β → δ) (x : γ) (y : δ) : [=(x, y)|(fun (x1 : α) (x2 : β) => (f x1, g x2)) <$> oa <*> ob] = [=x|f <$> oa] * [=y|g <$> ob]

theorem probOutput_bind_bind_prod_mk_eq_mul {ι : Type u} {spec : OracleSpec ι} {α β γ δ : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → γ) (g : β → δ) (z : γ × δ) : [=z|do let x ← oa let y ← ob pure (f x, g y)] = [=z.1|f <$> oa] * [=z.2|g <$> ob]

@[simp]

theorem probOutput_bind_bind_prod_mk_eq_mul' {ι : Type u} {spec : OracleSpec ι} {α β γ δ : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → γ) (g : β → δ) (x : γ) (y : δ) : [=(x, y)|do let x ← oa let y ← ob pure (f x, g y)] = [=x|f <$> oa] * [=y|g <$> ob]

theorem map_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa₁ oa₂ : OracleComp spec α) (f : α → β) (p : Prop) [Decidable p] : (f <$> if p then oa₁ else oa₂) = if p then f <$> oa₁ else f <$> oa₂

theorem probFailure_bind_eq_sum_probFailure {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} [spec.FiniteRange] (oa : OracleComp spec α) {ob : α → OracleComp spec β} {σ : Type u} {s : Finset σ} {oc : σ → α → OracleComp spec γ} : [⊥|oa >>= ob] = ∑ x ∈ s, [⊥|oa >>= oc x]

theorem probOutput_map_eq_probEvent {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) (y : β) : [=y|f <$> oa] = [fun (x : α) => f x = y|oa]

@[simp]

theorem probOutput_prod_mk_fst_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (y : β) (z : α × β) : [=z|(fun (x : α) => (x, y)) <$> oa] = [=z.1|oa] * [=z.2|pure y]

@[simp]

theorem probOutput_prod_mk_snd_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (ob : OracleComp spec β) (x : α) (z : α × β) : [=z|(fun (x_1 : β) => (x, x_1)) <$> ob] = [=z.1|pure x] * [=z.2|ob]

@[simp]

theorem probOutput_prod_mk_fst_map' {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → γ) (y : β) (z : γ × β) : [=z|(fun (x : α) => (f x, y)) <$> oa] = [=z.1|f <$> oa] * [=z.2|pure y]

@[simp]

theorem probOutput_prod_mk_snd_map' {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} [spec.FiniteRange] (ob : OracleComp spec β) (f : β → γ) (x : α) (z : α × γ) : [=z|(fun (x_1 : β) => (x, f x_1)) <$> ob] = [=z.1|pure x] * [=z.2|f <$> ob]

theorem probOutput_bind_ite_failure_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] [DecidableEq β] (oa : OracleComp spec α) (f : α → β) (p : α → Prop) [DecidablePred p] (y : β) : [=y|do let x ← oa if p x then pure (f x) else failure] = ∑' (x : α), if p x ∧ y = f x then [=x|oa] else 0

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.

@[simp]

theorem OracleComp.support_map_prod_map_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] : (Prod.map cf cf <$> main.fork qb js i cf).support = (fun (s : Option (Fin (qb i + 1))) => (s, s)) '' (cf <$> main).support

@[simp]

theorem OracleComp.finSupport_map_prod_map_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] : (Prod.map cf cf <$> main.fork qb js i cf).finSupport = Finset.image (fun (s : Option (Fin (qb i + 1))) => (s, s)) (cf <$> main).finSupport

theorem OracleComp.apply_eq_apply_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) : cf x₁ = cf x₂

@[simp]

theorem OracleComp.probOutput_none_map_fork_left {ι : 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 : Option (Fin (qb i + 1))) : [=(none, s)|Prod.map cf cf <$> main.fork qb js i cf] = 0

@[simp]

theorem OracleComp.probOutput_none_map_fork_right {ι : 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 : Option (Fin (qb i + 1))) : [=(s, none)|Prod.map cf cf <$> main.fork qb js i cf] = 0

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

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)); [=some s|cf <$> main] ^ 2 - [=some s|cf <$> main] / h ≤ [=(some s, some s)|Prod.map cf cf <$> 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 := ∑ s : Fin (qb i + 1), [=some s|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⁻¹)