Seed-Based Forking Lemma (Bellare-Neven)

The forking lemma is a key tool in provable security. The seeded variant in this file (seededFork) mechanizes the original Bellare-Neven construction (CCS 2006): pre-sample every oracle response into a QuerySeed, run the adversary deterministically against that seed, then re-run it against a seed that has been modified at the chosen fork point.

seededFork returns OracleComp spec (Option (α × α)) with explicit matching on success/failure. The seeded replay uses seededOracle via StateT, and generateSeed produces the initial seed as a ProbComp lifted into spec.

The companion file VCVio/CryptoFoundations/ReplayFork.lean provides the replay variant, which only pre-samples the forked oracle family and answers ambient randomness live; it is the natural choice for reductions like Fiat-Shamir EUF-CMA whose adversaries make both kinds of queries.

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

Bundles the inputs to the forking lemma.

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

def OracleComp.seededFork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] (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)

def OracleComp.seededForkWithSeedValue {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (seed : spec.QuerySeed) (u : spec.Range i) : OracleComp spec (Option (α × α))

The deterministic core of seededFork with the random seed and replacement value already fixed.

Runs main once against seed, checks whether the fork-index selector cf fires, and if so replays main against a modified seed where the (cf x₁)-th answer to oracle i is replaced by u. Returns the pair (x₁, x₂) when both runs agree on the fork index.

The only remaining randomness comes from main's own oracle queries that fall outside the seed (i.e. queries beyond the budget qb).

theorem OracleComp.isPerIndexQueryBound_firstRun_seeded {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) {seed : spec.QuerySeed} (hmain : main.IsPerIndexQueryBound qb) (hseed : ∀ (t : ι), qb t ≤ (seed t).length) : ((simulateQ seededOracle main).run' seed).IsPerIndexQueryBound 0

When the seed has at least qb t pre-generated answers for each oracle t, running main against the seed makes zero live oracle queries (every query is answered from the seed).

theorem OracleComp.isPerIndexQueryBound_replayAfterFork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) {seed : spec.QuerySeed} {u : spec.Range i} (hmain : main.IsPerIndexQueryBound qb) (hseed : ∀ (t : ι), qb t ≤ (seed t).length) (s : Fin (qb i + 1)) : ((simulateQ seededOracle main).run' ((seed.takeAtIndex i ↑s).addValue i u)).IsPerIndexQueryBound (Function.update 0 i (qb i - (↑s + 1)))

After truncating the seed at query index s for oracle i and inserting a fresh answer u, the replayed run can make at most qb i - (s + 1) live queries, all to oracle i. All other oracle families remain fully covered by the seed.

theorem OracleComp.isPerIndexQueryBound_seededForkWithSeedValue {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) {seed : spec.QuerySeed} {u : spec.Range i} (hmain : main.IsPerIndexQueryBound qb) (hseed : ∀ (t : ι), qb t ≤ (seed t).length) : (main.seededForkWithSeedValue qb i cf seed u).IsPerIndexQueryBound (Function.update 0 i (qb i))

seededForkWithSeedValue makes at most qb i live queries, all to oracle i.

The first seeded run is query-free (covered by the seed); the replay after the fork point uses at most the remaining i-budget. The bound holds regardless of which fork index cf returns.

theorem OracleComp.expectedQueryCount_seededForkWithSeedValue_le {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [Finite ι] [spec.Fintype] [spec.Inhabited] (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) (hmain : main.IsPerIndexQueryBound qb) (hjs : SeedListCovers qb js) : (ProgramLogic.wp (generateSeed spec qb js) fun (seed : spec.QuerySeed) => ProgramLogic.wp ($ᵗ spec.Range i) fun (u : spec.Range i) => expectedCost (main.seededForkWithSeedValue qb i cf seed u) CostModel.unit fun (n : ℕ) => ↑n) ≤ ↑(qb i)

The expected unit-cost query count of seededForkWithSeedValue, averaged over the randomly sampled seed and replacement value, is at most qb i.

theorem OracleComp.seededForkExpectedQueryWork_le {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [Finite ι] [spec.Fintype] [spec.Inhabited] (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) (sampleCost : ι → ℕ) (hSample : ∀ (j : ι), (probCompUnitQueryRun ($ᵗ spec.Range j)).QueryCostExactly (sampleCost j)) (hmain : main.IsPerIndexQueryBound qb) (hjs : SeedListCovers qb js) : ((probCompUnitQueryRun (generateSeed spec qb js)).expectedCostNat + (probCompUnitQueryRun ($ᵗ spec.Range i)).expectedCostNat + ProgramLogic.wp (generateSeed spec qb js) fun (seed : spec.QuerySeed) => ProgramLogic.wp ($ᵗ spec.Range i) fun (u : spec.Range i) => expectedCost (main.seededForkWithSeedValue qb i cf seed u) CostModel.unit fun (n : ℕ) => ↑n) ≤ ↑(List.map (fun (j : ι) => qb j * sampleCost j) js).sum + ↑(sampleCost i) + ↑(qb i)

Total expected query work of one fork attempt. The LHS decomposes as three terms:

1. Seed generation: ∑ j in js, qb j * sampleCost j uniform-oracle calls to build the seed.
2. Replacement sample: sampleCost i calls to sample one fresh value at the forked oracle i.
3. Replay queries: at most qb i live queries during the replayed execution.

The RHS is their sum: (∑ j in js, qb j * sampleCost j) + sampleCost i + qb i.

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

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

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

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

theorem OracleComp.le_probOutput_seededFork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] [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 ≤ probEvent (main.seededFork qb js i cf) fun (r : Option (α × α)) => Option.map (cf ∘ Prod.fst) r = some (some s)

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.seededFork_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_seededFork_le {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] [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.seededFork 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_seededFork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] [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⁻¹)) ≤ probEvent (main.seededFork qb js i cf) fun (r : Option (α × α)) => r.isSome = true

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

theorem OracleComp.le_probEvent_isSome_seededFork_sq {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] [spec.Fintype] [spec.Inhabited] [unifSpec.LawfulSubSpec spec] : (∑ s : Fin (qb i + 1), Pr[= some s | cf <$> main]) ^ 2 / ↑(qb i + 1) - (∑ s : Fin (qb i + 1), Pr[= some s | cf <$> main]) / ↑(Fintype.card (spec.Range i)) ≤ probEvent (main.seededFork qb js i cf) fun (r : Option (α × α)) => r.isSome = true

Bellare-Neven seeded forking bound in its canonical acc² / q − acc / h shape, where acc = ∑ₛ Pr[= some s | cf <$> main], q = qb i + 1, and h = |spec.Range i|.

This is the aggregated bound that appears as Lemma 1 of Bellare-Neven (CCS'06): summing the per-index lower bound over all fork points and applying Cauchy-Schwarz reshapes the product form delivered by le_probEvent_isSome_seededFork into the familiar ratio form. Algebraically the two statements are equal (modulo ENNReal.mul_sub under the finiteness of acc); this lemma exposes the ratio form as a public API so that downstream callers can match the textbook presentation directly.