Forking Lemma

The forking lemma is a key tool in provable security. Given an adversary that succeeds with some probability, the "fork" runs it twice with shared randomness up to a chosen query index, then re-samples one oracle response, bounding the probability that both runs succeed.

API changes from old version

• OracleComp no longer has Alternative, so guard/getM are unavailable. fork now returns OracleComp spec (Option (α × α)) with explicit matching.
• seededOracle uses StateT (not ReaderT), so .run' seed discards the final state.
• Old probability notation [= x | ...] → Pr[= x | ...], [⊥ | ...] → Pr[= none | ...].
• generateSeed returns ProbComp, lifted via liftComp.

structure OracleComp.ForkInput {ι : Type} (spec : OracleSpec ι) (α : Type) : Type u_1

Bundles the inputs to the forking lemma.

• main : OracleComp spec α
• queryBound : ι → ℕ
• js : List ι

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

The forking operation: run main with a random seed, then re-run it with the seed modified at the s-th query to oracle i (where s = cf x₁), checking that both runs agree on cf.

Returns none (failure) when:

• cf x₁ = none (adversary did not choose a fork point)
• the re-sampled oracle response equals the original (no useful fork)
• cf x₂ ≠ cf x₁ (the second run chose a different fork point)

theorem OracleComp.cf_eq_of_mem_support_fork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) (x₁ x₂ : α) (h : some (x₁, x₂) ∈ support (main.fork qb js i cf)) : ∃ (s : Fin (qb i + 1)), cf x₁ = some s ∧ cf x₂ = some s

If fork succeeds (returns some), both runs agree on the fork index.

theorem OracleComp.probEvent_fork_fst_eq_probEvent_pair {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.Fintype] [spec.Inhabited] (s : Fin (qb i + 1)) : Pr[fun (r : Option (α × α)) => Option.map (cf ∘ Prod.fst) r = some (some s) | main.fork qb js i cf] = Pr[fun (r : Option (α × α)) => Option.map (Prod.map cf cf) r = some (some s, some s) | main.fork qb js i cf]

On fork support, first-projection success equals old pair-style success event.

theorem OracleComp.le_probOutput_fork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.Fintype] [spec.Inhabited] [unifSpec.LawfulSubSpec spec] (s : Fin (qb i + 1)) : have h := ↑(Fintype.card (spec.Range i)); Pr[=some s | cf <$> main] ^ 2 - Pr[=some s | cf <$> main] / h ≤ Pr[fun (r : Option (α × α)) => Option.map (cf ∘ Prod.fst) r = some (some s) | main.fork qb js i cf]

Key bound of the forking lemma: the probability that both runs succeed with fork point s is at least Pr[cf(main) = s]² - Pr[cf(main) = s] / |Range i|.

theorem OracleComp.fork_precondition_le_one {ι : Type} {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.Fintype] [spec.Inhabited] : (have acc := ∑ s : Fin (qb i + 1), Pr[=some s | cf <$> main]; have h := ↑(Fintype.card (spec.Range i)); have q := qb i + 1; acc * (acc / ↑q - h⁻¹)) ≤ 1

The standard forking-lemma precondition is itself a valid probability bound.

theorem OracleComp.probOutput_none_fork_le {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.Fintype] [spec.Inhabited] [unifSpec.LawfulSubSpec spec] : have acc := ∑ s : Fin (qb i + 1), Pr[=some s | cf <$> main]; have h := ↑(Fintype.card (spec.Range i)); have q := qb i + 1; Pr[=none | main.fork qb js i cf] ≤ 1 - acc * (acc / ↑q - h⁻¹)

Main forking lemma: the failure probability is bounded by 1 - acc * (acc / q - 1/h).

theorem OracleComp.le_probEvent_isSome_fork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.Fintype] [spec.Inhabited] [unifSpec.LawfulSubSpec spec] : (have acc := ∑ s : Fin (qb i + 1), Pr[=some s | cf <$> main]; have h := ↑(Fintype.card (spec.Range i)); have q := qb i + 1; acc * (acc / ↑q - h⁻¹)) ≤ Pr[fun (r : Option (α × α)) => r.isSome = true | main.fork qb js i cf]

Forking-lemma lower bound, packaged directly as the success-event probability.