From 0a808b82bcb9ac2a55fd961043b9e30ef366ad1e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 20:09:32 -0400 Subject: [PATCH 1/3] feat(probability): the general forking lemma, also for oracle programs Prove Bellare-Neven's general forking lemma, acc^2/q - acc/|H| <= frk and acc <= q/|H| + sqrt(q frk), for algorithms deterministic in explicit coins and q uniform answers, by the rewinding lemma at each index and Cauchy-Schwarz. For oracle programs with explicit coins, relate uniform answers given as they come to presampled answers through the presampling theorem, and show that both runs of a successful fork ask the same queries up to the named one. Refs #581 (milestone 3a), #640. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 2 + .../Languages/Probabilistic/Forking.lean | 251 +++++++++++++ Complexity/Probability/Forking.lean | 343 ++++++++++++++++++ ComplexityTests.lean | 1 + ComplexityTests/Crypto/Forking.lean | 101 ++++++ ROADMAP.md | 11 +- references.bib | 10 + 7 files changed, 715 insertions(+), 4 deletions(-) create mode 100644 Complexity/Languages/Probabilistic/Forking.lean create mode 100644 Complexity/Probability/Forking.lean create mode 100644 ComplexityTests/Crypto/Forking.lean diff --git a/Complexity.lean b/Complexity.lean index aa5d494bc..7f094c5a0 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1708,6 +1708,7 @@ public import Complexity.Languages.Probabilistic.Basic public import Complexity.Languages.Probabilistic.BitString public import Complexity.Languages.Probabilistic.CenteredBinomial public import Complexity.Languages.Probabilistic.Concentration +public import Complexity.Languages.Probabilistic.Forking public import Complexity.Languages.Probabilistic.Iteration public import Complexity.Languages.Probabilistic.LinearHash public import Complexity.Languages.Probabilistic.Memoize @@ -1849,6 +1850,7 @@ public import Complexity.Probability.Divergence public import Complexity.Probability.Entropy public import Complexity.Probability.EntropyConcentration public import Complexity.Probability.EntropyExtraction +public import Complexity.Probability.Forking public import Complexity.Probability.Guessing public import Complexity.Probability.HashIsolation public import Complexity.Probability.IID diff --git a/Complexity/Languages/Probabilistic/Forking.lean b/Complexity/Languages/Probabilistic/Forking.lean new file mode 100644 index 000000000..95fc56938 --- /dev/null +++ b/Complexity/Languages/Probabilistic/Forking.lean @@ -0,0 +1,251 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Languages.Probabilistic.Oracle.Transcript +public import Complexity.Probability.Forking +import Complexity.Languages.Probabilistic.Presample +import Complexity.Languages.Probabilistic.Repeat +import Complexity.Probability.PMF +import Complexity.Probability.Product + +/-! +# Forking oracle programs + +An oracle program `P s : OracleComp (fun _ : Query => H) (Option ℕ × β)`, with explicit coins +`s`, asks queries whose answers lie in a finite set `H` and finally names one of its queries by +its position, or none. Forking runs it with uniform answers and, if it names the query at +position `j`, runs it again on the same coins with the same answers before `j` and fresh answers +from `j` on. Both runs ask the same first `j + 1` queries (`mem_support_fork`), so the named +query is the same, while its two answers differ. + +`runWithAnswers` runs a program on a list of answers, deterministically, recording its queries. +Answering queries from `q` presampled uniform answers has the law of answering them uniformly as +they come, when the program asks at most `q` queries: this is the presampling theorem +`ProbOracleComp.HasQueryBounds.eval_presample` (`interpret_uniform_eq`). Hence the general forking +lemma (`Probability.Forking.le_add_sqrt_fork`) bounds the acceptance probability of the program +with uniform answers by `q / |H| + √(q · frk)` (`le_add_sqrt_fork`). + +The coins are explicit: the second run replays them. A program with private randomness is put in +this form by drawing its coins in advance. The statements are exact; no efficiency is involved. + +## Main definitions + +* `Cslib.OracleComp.runWithAnswers`: run on a list of answers, recording the queries. +* `Cslib.OracleComp.indexBelow`: the named position, if it is below `q`. +* `Cslib.OracleComp.forkingAlgorithm`: a program on coins and an answer vector, for forking. + +## Main results + +* `Cslib.OracleComp.interpret_uniform_eq`: uniform answers as they come, or presampled. +* `Cslib.OracleComp.le_add_sqrt_fork`: the forking lemma for oracle programs. +* `Cslib.OracleComp.mem_support_fork`: both runs of a successful fork ask the same queries up to + the named one, and answer it differently. +* `Cslib.OracleComp.take_runWithAnswers`: a program's first `n + 1` queries depend only on its + first `n` answers. + +## References + +* [M. Bellare, G. Neven, *Multi-Signatures in the Plain Public-Key Model and a General Forking + Lemma*][BellareNeven2006], Lemma 1. +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Lemma 19.8. +-/ + +@[expose] public section + +namespace Cslib.OracleComp + +open Probability + +variable {Query H α : Type} + +/-- Run a program on a list of answers, in order, answering `default` once the list is exhausted; +return its result and its queries, in order. -/ +def runWithAnswers (default : H) : OracleComp (fun _ : Query => H) α → List H → α × List Query + | .pure a, _ => (a, []) + | .liftBind q cont, answers => + ((runWithAnswers default (cont (answers.headD default)) answers.tail).1, + q :: (runWithAnswers default (cont (answers.headD default)) answers.tail).2) + +/-- A program's first `n + 1` queries depend only on the first `n` answers. -/ +theorem take_runWithAnswers (default : H) (program : OracleComp (fun _ : Query => H) α) : + ∀ {answers answers' : List H} {n : ℕ}, answers.take n = answers'.take n → + (runWithAnswers default program answers).2.take (n + 1) = + (runWithAnswers default program answers').2.take (n + 1) := by + induction program with + | pure a => intros; rfl + | liftBind q cont ih => + intro answers answers' n h + cases n with + | zero => rfl + | succ n => + have hsplit : answers.headD default = answers'.headD default ∧ + answers.tail.take n = answers'.tail.take n := by + cases answers <;> cases answers' <;> simp_all + simp only [runWithAnswers, List.take_succ_cons, hsplit.1, ih _ hsplit.2] + +/-! ### Presampled answers -/ + +/-- Answering the lifted program from a saved list is running it on that list. -/ +private theorem eval_run_withSampleList (default : H) + (program : OracleComp (fun _ : Query => H) α) (answers : List H) : + ProbComp.eval ((fun (result, next, _) => (result, next)) <$> + (interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n)) + (withSampleList default fun v _ s => (pure (v, s) : ProbComp (H × Unit)))) + (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q) + program)).run ((), answers)) = + PMF.pure ((runWithAnswers default program answers).1, ()) := by + induction program generalizing answers with + | pure a => rfl + | liftBind q cont ih => + change _ = PMF.pure ((runWithAnswers default (cont (answers.headD default)) answers.tail).1, ()) + rw [← ih (answers.headD default) answers.tail] + rfl + +/-- Answering lifted queries uniformly as they come is answering them uniformly. -/ +private theorem eval_run_uniform [Fintype H] [Nonempty H] + (program : OracleComp (fun _ : Query => H) α) : + ProbComp.eval ((interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n)) + (fun _ s => do + let value ← ProbComp.uniform H + (pure (value, s) : ProbComp (H × Unit)))) + (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q) + program)).run ()) = + (interpret (fun _ => PMF.uniformOfFintype H) program).map (·, ()) := by + have hstate : (fun (_ : Query) (s : Unit) => do + let value ← ProbComp.uniform H + (pure (value, s) : ProbComp (H × Unit))) = + fun _ s => (fun a => (a, s)) <$> ProbComp.uniform H := by + funext _ s + rw [map_eq_bind_pure_comp] + rfl + have heval : ProbComp.eval (interpret (fun _ => ProbComp.uniform H) program) = + interpret (fun _ => PMF.uniformOfFintype H) program := by + change interpret ProbComp.unifOracle (interpret _ program) = _ + rw [interpret_interpret] + congr 1 + funext q + exact ProbComp.eval_uniform H + rw [interpret_interpret] + simp only [ProbOracleComp.interpret_query] + rw [hstate, run_interpret_stateless, ProbComp.eval_map, heval] + +/-- `q` uniform samples, collected in a list, are the entries of a uniform vector. -/ +private theorem eval_replicate_uniform [Fintype H] [Nonempty H] (q : ℕ) : + ProbComp.eval (replicate q (ProbComp.uniform H)) = + (PMF.uniformOfFintype (Fin q → H)).map List.ofFn := by + induction q with + | zero => + have hconst : (List.ofFn : (Fin 0 → H) → List H) = Function.const _ [] := + funext fun _ => List.ofFn_zero + rw [replicate_zero, ProbComp.eval_pure, hconst, PMF.map_const] + | succ q ih => + rw [replicate_succ, ← Probability.PMF.pi_uniformOfFintype, Probability.PMF.pi_fin_succ, + Probability.PMF.pi_uniformOfFintype] + simp only [ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_uniform, ih, PMF.map_bind, + PMF.map_comp, Function.comp_def, List.ofFn_succ, Fin.cons_zero, Fin.cons_succ] + +/-- The lazy law of uniform answers is the law of `q` presampled uniform answers, for a program +asking at most `q` queries: an instance of the presampling theorem +`ProbOracleComp.HasQueryBounds.eval_presample`. -/ +theorem interpret_uniform_eq [Fintype H] [Nonempty H] (default : H) + (program : OracleComp (fun _ : Query => H) α) {size : Query → ℕ} {q maxSize : ℕ} + (hq : (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q) + program).HasQueryBounds size q maxSize) : + interpret (fun _ => PMF.uniformOfFintype H) program = + (PMF.uniformOfFintype (Fin q → H)).map fun h => + (runWithAnswers default program (List.ofFn h)).1 := by + have hp := hq.eval_presample (ProbComp.uniform H) default + (fun v _ s => (pure (v, s) : ProbComp (H × Unit))) () + rw [eval_run_uniform, ProbComp.eval_bind, eval_replicate_uniform] at hp + simp only [eval_run_withSampleList, PMF.bind_map, Function.comp_def] at hp + have hfst := congrArg (PMF.map Prod.fst) hp + simp only [PMF.map_comp, Function.comp_def] at hfst + rw [show PMF.map (fun x => x) (interpret (fun _ => PMF.uniformOfFintype H) program) = + interpret (fun _ => PMF.uniformOfFintype H) program from PMF.map_id _] at hfst + rw [← hfst, PMF.map_bind] + simp only [PMF.pure_map] + rfl + +/-! ### Forking -/ + +/-- The named position, if it is below `q`. -/ +def indexBelow (q : ℕ) (position : Option ℕ) : Option (Fin q) := + position.bind fun j => if h : j < q then some ⟨j, h⟩ else none + +/-- A program with explicit coins as an algorithm on coins and `q` answers, for the general +forking lemma: the named position below `q`, and the result with the queries. -/ +def forkingAlgorithm {S β : Type} (default : H) (q : ℕ) + (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (s : S) (h : Fin q → H) : + Option (Fin q) × ((Option ℕ × β) × List Query) := + (indexBelow q (runWithAnswers default (program s) (List.ofFn h)).1.1, + runWithAnswers default (program s) (List.ofFn h)) + +variable {S β : Type} [Fintype H] [Nonempty H] [DecidableEq H] + +/-- **The forking lemma for oracle programs** ([BellareNeven2006], Lemma 1): if a program with +explicit coins asks at most `q` queries, and names a position below `q` with probability `acc` +when its queries are answered uniformly as they come, then forking it succeeds with probability +`frk` such that `acc ≤ q / |H| + √(q · frk)`. -/ +theorem le_add_sqrt_fork (first : PMF S) + (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (default : H) + {size : Query → ℕ} {q maxSize : ℕ} + (hq : ∀ s, (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q) + (program s)).HasQueryBounds size q maxSize) : + ((do + let s ← first + let result ← interpret (fun _ => PMF.uniformOfFintype H) (program s) + return (indexBelow q result.1).isSome : PMF Bool) true).toReal ≤ + q / Fintype.card H + √(q * ((Forking.fork first (forkingAlgorithm default q program)).map + Option.isSome true).toReal) := by + have hacc : (do + let s ← first + let result ← interpret (fun _ => PMF.uniformOfFintype H) (program s) + return (indexBelow q result.1).isSome : PMF Bool) = + Forking.accept first (forkingAlgorithm default q program) := by + simp only [Forking.accept, forkingAlgorithm, Probability.PMF.monad_bind_eq_bind, + Probability.PMF.monad_pure_eq_pure] + refine congrArg _ (funext fun s => ?_) + rw [interpret_uniform_eq default (program s) (hq s), PMF.bind_map] + rfl + rw [hacc] + exact Forking.le_add_sqrt_fork first _ + +/-- A successful fork of a program reruns it on the same coins with answers that agree before the +named position `j` and differ at it; both runs name `j` and ask the same first `j + 1` +queries. -/ +theorem mem_support_fork {first : PMF S} + {program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)} {default : H} {q : ℕ} + {j : Fin q} {out out' : (Option ℕ × β) × List Query} + (hfork : some (j, out, out') ∈ + (Forking.fork first (forkingAlgorithm default q program)).support) : + ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧ + out = runWithAnswers default (program s) (List.ofFn h) ∧ + out' = runWithAnswers default (program s) (List.ofFn h') ∧ + out.1.1 = some j.val ∧ out'.1.1 = some j.val ∧ out.2.take (j + 1) = out'.2.take (j + 1) := by + obtain ⟨s, hs, h, h', hagree, hne, hrun, hrun'⟩ := Forking.mem_support_fork hfork + simp only [forkingAlgorithm, Prod.mk.injEq] at hrun hrun' + obtain ⟨hidx, rfl⟩ := hrun + obtain ⟨hidx', rfl⟩ := hrun' + have hpos {r : Option ℕ} (hr : indexBelow q r = some j) : r = some j.val := by + cases r with + | none => simp [indexBelow] at hr + | some r => + simp only [indexBelow, Option.bind_some] at hr + split_ifs at hr with hlt + · simp only [Option.some.injEq, Fin.ext_iff] at hr + rw [hr] + refine ⟨s, hs, h, h', hagree, hne, rfl, rfl, hpos hidx, hpos hidx', + take_runWithAnswers default (program s) ?_⟩ + refine List.ext_getElem (by simp) fun i hi _ => ?_ + simp only [List.length_take, List.length_ofFn] at hi + simp only [List.getElem_take, List.getElem_ofFn] + exact hagree ⟨i, by omega⟩ (Fin.mk_lt_of_lt_val (by omega)) + +end Cslib.OracleComp diff --git a/Complexity/Probability/Forking.lean b/Complexity/Probability/Forking.lean new file mode 100644 index 000000000..f962f08f9 --- /dev/null +++ b/Complexity/Probability/Forking.lean @@ -0,0 +1,343 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Probability.Rewinding +import Complexity.Probability.PMF +import Mathlib.Algebra.Order.Chebyshev + +/-! +# The general forking lemma + +An algorithm `A` gets coins `s`, drawn from a distribution, and `q` answers `h : Fin q → H`, drawn +independently and uniformly from a finite set `H`, and outputs an optional index `j : Fin q` +together with a result. The *forking algorithm* runs `A` once; if it outputs an index `j`, it +runs `A` again on the same coins and the same answers before `j`, with fresh answers from `j` on +(`splice`). It succeeds when the second run outputs the same index `j` and the two answers at `j` +differ, and it returns both results. + +The general forking lemma of Bellare and Neven ([BellareNeven2006], Lemma 1) bounds the success +probability `frk` of forking by the acceptance probability `acc` of one run: +`acc ^ 2 / q - acc / |H| ≤ frk` (`sq_div_sub_le_fork`), and consequently +`acc ≤ q / |H| + √(q · frk)` (`le_add_sqrt_fork`). For each index `j` this is the rewinding lemma +(`Rewinding.sq_sub_le_twice`), with the coins and the answers before `j` as the first stage, the +answer at `j` as the challenge and the answers after `j` as fresh randomness of the second stage; +summing over `j` loses the factor `q` by the Cauchy–Schwarz inequality. Boneh and Shoup prove the +same bound for `r`-impersonation adversaries ([BonehShoup2023], Lemma 19.8). + +The algorithm is deterministic given its coins and answers, which is the form forking needs: the +second run reuses the coins. The statements are exact; no efficiency is involved. + +## Main definitions + +* `Cslib.Probability.Forking.splice`: answers from one vector before an index, another from it on. +* `Cslib.Probability.Forking.accept`: run once and accept when an index is output. +* `Cslib.Probability.Forking.fork`: the forking algorithm. + +## Main results + +* `Cslib.Probability.Forking.sq_div_sub_le_fork`: `acc ^ 2 / q - acc / |H| ≤ frk`. +* `Cslib.Probability.Forking.le_add_sqrt_fork`: `acc ≤ q / |H| + √(q · frk)`. +* `Cslib.Probability.Forking.mem_support_fork`: what a successful fork returns. + +## References + +* [M. Bellare, G. Neven, *Multi-Signatures in the Plain Public-Key Model and a General Forking + Lemma*][BellareNeven2006], Lemma 1. +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Lemma 19.8. +-/ + +@[expose] public section + +namespace Cslib.Probability.Forking + +variable {S H β : Type} {q : ℕ} + +/-- The answers of `h` before the index `j` and those of `h'` from `j` on. -/ +def splice (j : Fin q) (h h' : Fin q → H) : Fin q → H := fun i => if i < j then h i else h' i + +variable [Fintype H] [Nonempty H] + +/-- One run: draw coins and uniform answers, and accept when `A` outputs an index. -/ +noncomputable def accept (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : + PMF Bool := do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + return (A s h).1.isSome + +/-- The forking algorithm ([BellareNeven2006]): run `A` on coins `s` and answers `h`; if it +outputs an index `j`, rerun it on `s` and on `splice j h h'` for fresh answers `h'`, and succeed +with both results when the rerun outputs `j` too and `h j ≠ h' j`. -/ +noncomputable def fork [DecidableEq H] (first : PMF S) + (A : S → (Fin q → H) → Option (Fin q) × β) : PMF (Option (Fin q × β × β)) := do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + let h' ← PMF.uniformOfFintype (Fin q → H) + return match (A s h).1 with + | none => none + | some j => if (A s (splice j h h')).1 = some j ∧ h j ≠ h' j then + some (j, (A s h).2, (A s (splice j h h')).2) else none + +/-! ### Splitting the answers at an index -/ + +/-- Answers from `b` before `j`, the answer `t` at `j`, and answers from `r` after `j`. -/ +private def glue (j : Fin q) (b : Fin q → H) (t : H) (r : Fin q → H) : Fin q → H := + fun i => if i < j then b i else if i = j then t else r i + +/-- Gluing is the first component of an equivalence, whose other components are the unused +parts of `b` and `r`. -/ +private def glueEquiv (j : Fin q) : + (Fin q → H) × H × (Fin q → H) ≃ (Fin q → H) × (Fin q → H) × H where + toFun x := (glue j x.1 x.2.1 x.2.2, fun i => if i < j then x.2.2 i else x.1 i, x.2.2 j) + invFun y := (fun i => if i < j then y.1 i else y.2.1 i, y.1 j, + fun i => if i < j then y.2.1 i else if i = j then y.2.2 else y.1 i) + left_inv x := by + obtain ⟨b, t, r⟩ := x + simp only [glue, lt_self_iff_false, ite_false, ite_true, Prod.mk.injEq] + refine ⟨funext fun i => ?_, trivial, funext fun i => ?_⟩ + · split_ifs <;> rfl + · by_cases h₁ : i < j <;> by_cases h₂ : i = j <;> simp [h₁, h₂] + right_inv y := by + obtain ⟨x, z, u⟩ := y + simp only [lt_self_iff_false, ite_false, ite_true, Prod.mk.injEq] + refine ⟨funext fun i => ?_, funext fun i => ?_, trivial⟩ + · by_cases h₁ : i < j <;> by_cases h₂ : i = j <;> simp [glue, h₁, h₂] + · split_ifs <;> rfl + +/-- Gluing independent uniform parts gives uniform answers. -/ +private theorem bind_glue {γ : Type} (j : Fin q) (k : (Fin q → H) → PMF γ) : + ((PMF.uniformOfFintype (Fin q → H)).bind fun b => (PMF.uniformOfFintype H).bind fun t => + (PMF.uniformOfFintype (Fin q → H)).bind fun r => k (glue j b t r)) = + (PMF.uniformOfFintype (Fin q → H)).bind k := by + have hprod : ((PMF.uniformOfFintype (Fin q → H)).bind fun b => + (PMF.uniformOfFintype H).bind fun t => (PMF.uniformOfFintype (Fin q → H)).bind fun r => + PMF.pure (b, t, r)) = PMF.uniformOfFintype ((Fin q → H) × H × (Fin q → H)) := by + rw [← Probability.PMF.uniformOfFintype_prod, ← Probability.PMF.uniformOfFintype_prod] + simp only [PMF.map, PMF.bind_bind, Function.comp_def, PMF.pure_bind] + have hfst : (PMF.uniformOfFintype ((Fin q → H) × H × (Fin q → H))).map + (fun x => glue j x.1 x.2.1 x.2.2) = PMF.uniformOfFintype (Fin q → H) := by + have := Probability.PMF.uniformOfFintype_prod_map_fst (α := Fin q → H) + (β := (Fin q → H) × H) + rw [← Probability.PMF.uniformOfFintype_map_equiv (glueEquiv j), PMF.map_comp] at this + exact this + calc _ = ((PMF.uniformOfFintype ((Fin q → H) × H × (Fin q → H))).map + (fun x => glue j x.1 x.2.1 x.2.2)).bind k := by + rw [← hprod] + simp only [PMF.bind_map, PMF.bind_bind, PMF.pure_bind, Function.comp_def] + _ = _ := by rw [hfst] + +omit [Fintype H] [Nonempty H] in +private theorem glue_self (j : Fin q) (b : Fin q → H) (t : H) (r : Fin q → H) : + glue j b t r j = t := by + simp [glue] + +omit [Fintype H] [Nonempty H] in +private theorem splice_glue (j : Fin q) (b b' : Fin q → H) (t t' : H) (r r' : Fin q → H) : + splice j (glue j b t r) (glue j b' t' r') = glue j b t' r' := by + funext i + by_cases h₁ : i < j <;> simp [splice, glue, h₁] + +/-! ### One index -/ + +/-- The first stage at an index: coins, and answers to use before the index. -/ +private noncomputable def firstAt (first : PMF S) : PMF (S × (Fin q → H)) := do + let s ← first + let b ← PMF.uniformOfFintype (Fin q → H) + return (s, b) + +/-- Accepting with the index `j` is one run of a rewinding experiment. -/ +private theorem acceptAt_eq_once (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) + (j : Fin q) : + (do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + return decide ((A s h).1 = some j) : PMF Bool) = + Rewinding.once (firstAt first) (fun _ _ => PMF.uniformOfFintype (Fin q → H)) + (fun x t r => decide ((A x.1 (glue j x.2 t r)).1 = some j)) := by + simp only [Rewinding.once, firstAt, Probability.PMF.monad_bind_eq_bind, + Probability.PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + congr 1 + funext s + exact (bind_glue j fun h => PMF.pure (decide ((A s h).1 = some j))).symm + +variable [DecidableEq H] + +/-- Forking with the index `j` is two runs of the rewinding experiment. -/ +private theorem forkAt_eq_twice (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) + (j : Fin q) : + (do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + let h' ← PMF.uniformOfFintype (Fin q → H) + return decide ((A s h).1 = some j ∧ (A s (splice j h h')).1 = some j ∧ h j ≠ h' j) : + PMF Bool) = + Rewinding.twice (firstAt first) (fun _ _ => PMF.uniformOfFintype (Fin q → H)) + (fun x t r => decide ((A x.1 (glue j x.2 t r)).1 = some j)) := by + simp only [Rewinding.twice, firstAt, Probability.PMF.monad_bind_eq_bind, + Probability.PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + congr 1 + funext s + rw [← bind_glue j] + congr 1 + funext b + congr 1 + funext t + conv_lhs => enter [2, r]; rw [← bind_glue j] + simp only [splice_glue, glue_self, PMF.bind_const] + rw [PMF.bind_comm] + congr 1 + funext t' + congr 1 + funext r + congr 1 + funext r' + congr 1 + simp only [Bool.decide_and, ne_eq, decide_not, Bool.and_assoc] + rfl + +/-! ### Summing over the indices -/ + +omit [DecidableEq H] [Fintype H] [Nonempty H] in +/-- An event that names one index is the disjoint union of its events at each index. -/ +private theorem bind_match_apply {X : Type} (μ : PMF X) (index : X → Option (Fin q)) + (event : Fin q → X → Prop) [∀ j x, Decidable (event j x)] : + (μ.bind fun x => PMF.pure (match index x with + | none => false + | some j => decide (event j x))) true = + ∑ j, (μ.bind fun x => PMF.pure (decide (index x = some j ∧ event j x))) true := by + simp only [PMF.bind_apply, PMF.pure_apply] + rw [← Summable.tsum_finsetSum fun _ _ => ENNReal.summable] + refine tsum_congr fun x => ?_ + rw [← Finset.mul_sum] + congr 1 + cases hx : index x with + | none => simp + | some j => + rw [Finset.sum_eq_single j (fun j' _ hj' => by simp [Ne.symm hj']) (by simp)] + simp + +omit [DecidableEq H] in +/-- The acceptance probability, as a real number. -/ +private theorem toReal_accept (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : + (accept first A true).toReal = ∑ j, ((do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + return decide ((A s h).1 = some j) : PMF Bool) true).toReal := by + have h := bind_match_apply ((first.bind fun s => (PMF.uniformOfFintype (Fin q → H)).bind + fun h => PMF.pure (s, h))) (fun x => (A x.1 x.2).1) (fun _ _ => True) + simp only [PMF.bind_bind, PMF.pure_bind, and_true] at h + rw [← ENNReal.toReal_sum fun _ _ => PMF.apply_ne_top _ _] + refine congrArg ENNReal.toReal (Eq.trans ?_ h) + simp only [accept, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure] + refine congrArg (fun p : PMF Bool => p true) + (congrArg _ (funext fun s => congrArg _ (funext fun h => ?_))) + cases (A s h).1 <;> rfl + +/-- The success probability of forking, as a real number. -/ +private theorem toReal_fork (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : + ((fork first A).map Option.isSome true).toReal = ∑ j, ((do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + let h' ← PMF.uniformOfFintype (Fin q → H) + return decide ((A s h).1 = some j ∧ (A s (splice j h h')).1 = some j ∧ h j ≠ h' j) : + PMF Bool) true).toReal := by + have h := bind_match_apply ((first.bind fun s => (PMF.uniformOfFintype (Fin q → H)).bind + fun h => (PMF.uniformOfFintype (Fin q → H)).bind fun h' => PMF.pure (s, h, h'))) + (fun x => (A x.1 x.2.1).1) + (fun j x => (A x.1 (splice j x.2.1 x.2.2)).1 = some j ∧ x.2.1 j ≠ x.2.2 j) + simp only [PMF.bind_bind, PMF.pure_bind] at h + rw [← ENNReal.toReal_sum fun _ _ => PMF.apply_ne_top _ _] + refine congrArg ENNReal.toReal (Eq.trans ?_ h) + simp only [fork, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure, + PMF.map_bind, PMF.pure_map] + refine congrArg (fun p : PMF Bool => p true) (congrArg _ (funext fun s => + congrArg _ (funext fun h => congrArg _ (funext fun h' => ?_)))) + cases (A s h).1 with + | none => rfl + | some j => by_cases hc : (A s (splice j h h')).1 = some j ∧ h j ≠ h' j <;> simp [hc] + +/-! ### The forking lemma -/ + +/-- **The general forking lemma** ([BellareNeven2006], Lemma 1): forking succeeds with +probability at least `acc ^ 2 / q - acc / |H|`, where `acc` is the probability that one run +outputs an index. -/ +theorem sq_div_sub_le_fork (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : + (accept first A true).toReal ^ 2 / q - (accept first A true).toReal / Fintype.card H ≤ + ((fork first A).map Option.isSome true).toReal := by + set N : ℝ := (Fintype.card H : ℝ) + set a : Fin q → ℝ := fun j => ((do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + return decide ((A s h).1 = some j) : PMF Bool) true).toReal + have hj (j : Fin q) : a j ^ 2 - a j / N ≤ ((do + let s ← first + let h ← PMF.uniformOfFintype (Fin q → H) + let h' ← PMF.uniformOfFintype (Fin q → H) + return decide ((A s h).1 = some j ∧ (A s (splice j h h')).1 = some j ∧ h j ≠ h' j) : + PMF Bool) true).toReal := by + simp only [a, acceptAt_eq_once, forkAt_eq_twice] + exact Rewinding.sq_sub_le_twice _ _ _ + rw [toReal_fork, toReal_accept] + have hcs : (∑ j, a j) ^ 2 / q ≤ ∑ j, a j ^ 2 := by + rcases Nat.eq_zero_or_pos q with rfl | hq + · simp + · rw [div_le_iff₀ (by exact_mod_cast hq), mul_comm] + simpa using sq_sum_le_card_mul_sum_sq (s := Finset.univ) (f := a) + calc (∑ j, a j) ^ 2 / q - (∑ j, a j) / N ≤ ∑ j, a j ^ 2 - ∑ j, a j / N := by + rw [Finset.sum_div] + linarith + _ = ∑ j, (a j ^ 2 - a j / N) := by rw [Finset.sum_sub_distrib] + _ ≤ _ := Finset.sum_le_sum fun j _ => hj j + +/-- The forking lemma solved for the acceptance probability: `acc ≤ q / |H| + √(q · frk)`. -/ +theorem le_add_sqrt_fork (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : + (accept first A true).toReal ≤ + q / Fintype.card H + √(q * ((fork first A).map Option.isSome true).toReal) := by + set ε := (accept first A true).toReal with hεdef + set N : ℝ := (Fintype.card H : ℝ) + have hN : 0 < N := Nat.cast_pos.mpr Fintype.card_pos + have hfork := sq_div_sub_le_fork first A + by_cases hε : ε ≤ q / N + · exact hε.trans (le_add_of_nonneg_right (Real.sqrt_nonneg _)) + · have hq : (0 : ℝ) < q := by + rcases Nat.eq_zero_or_pos q with hq0 | hq0 + · subst hq0 + exact absurd (by simp [hεdef, toReal_accept]) hε + · exact_mod_cast hq0 + have hsq : (ε - q / N) ^ 2 ≤ q * ((fork first A).map Option.isSome true).toReal := by + have hmul := mul_le_mul_of_nonneg_left hfork hq.le + refine le_trans ?_ hmul + have hexpand : q * (ε ^ 2 / q - ε / N) = (ε - q / N) ^ 2 + (ε - q / N) * (q / N) := by + field_simp + ring + rw [hexpand] + exact le_add_of_nonneg_right (mul_nonneg (by linarith) (by positivity)) + have := Real.abs_le_sqrt hsq + linarith [le_abs_self (ε - q / N)] + +/-- A successful fork comes from one coin sample and two answer vectors that agree before the +returned index `j` and differ at it, on both of which `A` outputs `j`. -/ +theorem mem_support_fork {first : PMF S} {A : S → (Fin q → H) → Option (Fin q) × β} + {j : Fin q} {out out' : β} (hfork : some (j, out, out') ∈ (fork first A).support) : + ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧ + A s h = (some j, out) ∧ A s h' = (some j, out') := by + simp only [fork, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure, + PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at hfork + obtain ⟨s, hs, h, -, h', -, hres⟩ := hfork + refine ⟨s, hs, h, splice j h h', fun i hi => by simp [splice, hi], ?_⟩ + cases hA : (A s h).1 with + | none => simp [hA] at hres + | some j' => + simp only [hA] at hres + split_ifs at hres with hc + · simp only [Option.some.injEq, Prod.mk.injEq] at hres + obtain ⟨rfl, rfl, rfl⟩ := hres + refine ⟨by simpa [splice] using hc.2, Prod.ext hA rfl, Prod.ext hc.1 rfl⟩ + +end Cslib.Probability.Forking diff --git a/ComplexityTests.lean b/ComplexityTests.lean index c588ffe5d..d31de221c 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -86,6 +86,7 @@ import ComplexityTests.CountingVerifier import ComplexityTests.Crypto.Bootstrapping import ComplexityTests.Crypto.Encryption import ComplexityTests.Crypto.FixedKeySecurity +import ComplexityTests.Crypto.Forking import ComplexityTests.Crypto.GMWPointwise import ComplexityTests.Crypto.GSW import ComplexityTests.Crypto.GSWDecryption diff --git a/ComplexityTests/Crypto/Forking.lean b/ComplexityTests/Crypto/Forking.lean new file mode 100644 index 000000000..a4d611cab --- /dev/null +++ b/ComplexityTests/Crypto/Forking.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Languages.Probabilistic.Forking +import Complexity.Probability.Forking +import Complexity.Probability.PMF + +/-! +# Tests for the forking lemma + +An algorithm that always names its only answer is accepted with probability `1`, so forking it +succeeds with probability at least `1 - 1 / 2`; it succeeds exactly when two independent bits +differ, so the bound is attained. The oracle program that asks one query and names it satisfies +the hypotheses of the oracle forking lemma, which gives a positive forking probability; a +successful fork gives two runs that ask the same query. +-/ + +namespace ComplexityTests.Crypto.Forking + +open Cslib Cslib.Probability + +/-- Always name the only answer. -/ +def always (_ : Unit) (_ : Fin 1 → Bool) : Option (Fin 1) × Unit := (some 0, ()) + +example : (Forking.accept (PMF.pure ()) always true) = 1 := by + simp [Forking.accept, always] + +/-- The general forking lemma for `always`: `1 - 1 / 2 ≤ frk`. -/ +example : (1 : ℝ) / 2 ≤ ((Forking.fork (PMF.pure ()) always).map Option.isSome true).toReal := by + have h := Forking.sq_div_sub_le_fork (PMF.pure ()) always + have hacc : (Forking.accept (PMF.pure ()) always true).toReal = 1 := by + simp [Forking.accept, always] + rw [hacc] at h + simp only [Fintype.card_bool, Nat.cast_ofNat, Nat.cast_one, one_pow, div_one] at h + linarith + +/-! ### Oracle programs -/ + +/-- Ask one query and name it. -/ +def askOnce (_ : Unit) : OracleComp (fun _ : Unit => Bool) (Option ℕ × Bool) := do + let a ← OracleComp.query (spec := fun _ : Unit => Bool) () + return (some 0, a) + +/-- `askOnce` asks one query. -/ +theorem askOnce_queries (s : Unit) : + (OracleComp.interpret (fun q => ProbOracleComp.query (spec := fun _ : Unit => Bool) q) + (askOnce s)).HasQueryBounds (fun _ => 0) 1 0 := by + have h := (ProbOracleComp.HasQueryBounds.query (Response := fun _ : Unit => Bool) () + (fun _ => 0) le_rfl).bind fun a => + ProbOracleComp.HasQueryBounds.pure (Response := fun _ : Unit => Bool) (some 0, a) + (fun _ => 0) 0 + simpa [askOnce] using h + +/-- Forking `askOnce`, which always names its query, succeeds with probability at least +`1 / 4`. -/ +example : (1 : ℝ) / 4 ≤ ((Forking.fork (PMF.pure ()) + (OracleComp.forkingAlgorithm false 1 askOnce)).map Option.isSome true).toReal := by + have h := OracleComp.le_add_sqrt_fork (PMF.pure ()) askOnce false askOnce_queries + have hacc : ((do + let s ← PMF.pure () + let result ← OracleComp.interpret (fun _ => PMF.uniformOfFintype Bool) (askOnce s) + return (OracleComp.indexBelow 1 result.1).isSome : PMF Bool) true).toReal = 1 := by + simp [askOnce, OracleComp.indexBelow] + rw [hacc] at h + simp only [Fintype.card_bool, Nat.cast_ofNat, Nat.cast_one, one_mul] at h + have hsqrt : (1 : ℝ) / 2 ≤ √(((Forking.fork (PMF.pure ()) + (OracleComp.forkingAlgorithm false 1 askOnce)).map Option.isSome true).toReal) := by + linarith + nlinarith [Real.sq_sqrt (ENNReal.toReal_nonneg (a := ((Forking.fork (PMF.pure ()) + (OracleComp.forkingAlgorithm false 1 askOnce)).map Option.isSome true))), Real.sqrt_nonneg + (((Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1 askOnce)).map + Option.isSome true).toReal)] + +/-- Both runs of a successful fork of `askOnce` ask the same query. -/ +example {j : Fin 1} {out out' : (Option ℕ × Bool) × List Unit} + (hfork : some (j, out, out') ∈ + (Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1 askOnce)).support) : + out.2.take (j + 1) = out'.2.take (j + 1) := by + obtain ⟨-, -, -, -, -, -, -, -, -, -, htake⟩ := OracleComp.mem_support_fork hfork + exact htake + +/-! ### Axioms -/ + +/-- +info: 'Cslib.Probability.Forking.sq_div_sub_le_fork' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Forking.sq_div_sub_le_fork + +/-- +info: 'Cslib.OracleComp.le_add_sqrt_fork' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms OracleComp.le_add_sqrt_fork + +end ComplexityTests.Crypto.Forking diff --git a/ROADMAP.md b/ROADMAP.md index 295511540..45b3092c9 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1156,10 +1156,13 @@ Jukna coverage below is an additional target beyond the V1 port: a family of prime-order groups with plain polynomial-time operations, instantiated by [Schnorr groups](Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean), and [Schnorr identification](Complexity/Crypto/Computational/SchnorrIdentification.lean) is secure - against direct attacks by uniform strict PPT impersonators under it. Open: security against - eavesdropping in the strict-PPT model, where simulating transcripts needs approximately uniform - `ZMod q` samples and hence an explicit statistical-distance term, and Fiat–Shamir/Schnorr - signatures in the random-oracle model with the forking bound of Theorem 19.16. + against direct attacks by uniform strict PPT impersonators under it. The general + [forking lemma](Complexity/Probability/Forking.lean) (Bellare–Neven) is proved, also for + [oracle programs](Complexity/Languages/Probabilistic/Forking.lean) with explicit coins and + presampled answers. Open (see #640): Fiat–Shamir/Schnorr signatures in the random-oracle model + with the bound of Theorem 19.16, and security against eavesdropping in the strict-PPT model, + where simulating transcripts needs approximately uniform `ZMod q` samples and hence an explicit + statistical-distance term. The current V1 port excludes the circuitized anti-checker, hardness-magnification argument and MINKT/MINCKT developments. The long-term canon above includes metacomplexity; those results should diff --git a/references.bib b/references.bib index 25cffc233..8d9a6be8c 100644 --- a/references.bib +++ b/references.bib @@ -390,6 +390,16 @@ @inproceedings{BonehHaleviHamburgOstrovsky2008 url = {https://crypto.stanford.edu/~dabo/papers/circular.pdf} } +@inproceedings{BellareNeven2006, + author = {Mihir Bellare and Gregory Neven}, + title = {Multi-Signatures in the Plain Public-Key Model and a General Forking Lemma}, + booktitle = {Proceedings of the 13th ACM Conference on Computer and Communications Security}, + pages = {390--399}, + publisher = {ACM}, + year = {2006}, + doi = {10.1145/1180405.1180453} +} + @misc{BonehShoup2023, author = {Dan Boneh and Victor Shoup}, title = {A Graduate Course in Applied Cryptography}, From 0b27609c1cf34a6aae8c30349e481075d0889f41 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 20:28:27 -0400 Subject: [PATCH 2/3] fix(probability): require forks to name a query that was actually made The oracle forking wrapper now counts a named position only if the program asked a query there (validIndex), measures acceptance with counted uniform answers (countingUniform), and states that both runs of a successful fork asked the named query, the same one. Add simp lemmas for runWithAnswers and a regression test: a program naming a position without querying never forks. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Languages/Probabilistic/Forking.lean | 176 ++++++++++++++---- ComplexityTests/Crypto/Forking.lean | 21 ++- 2 files changed, 154 insertions(+), 43 deletions(-) diff --git a/Complexity/Languages/Probabilistic/Forking.lean b/Complexity/Languages/Probabilistic/Forking.lean index 95fc56938..bab38b63c 100644 --- a/Complexity/Languages/Probabilistic/Forking.lean +++ b/Complexity/Languages/Probabilistic/Forking.lean @@ -19,17 +19,20 @@ import Complexity.Probability.Product An oracle program `P s : OracleComp (fun _ : Query => H) (Option ℕ × β)`, with explicit coins `s`, asks queries whose answers lie in a finite set `H` and finally names one of its queries by -its position, or none. Forking runs it with uniform answers and, if it names the query at -position `j`, runs it again on the same coins with the same answers before `j` and fresh answers -from `j` on. Both runs ask the same first `j + 1` queries (`mem_support_fork`), so the named -query is the same, while its two answers differ. +its position, or none. A name counts only if the program actually asked a query at that position +(`validIndex`). Forking runs the program with uniform answers and, if it validly names position +`j`, runs it again on the same coins with the same answers before `j` and fresh answers from `j` +on; it succeeds when the rerun validly names `j` too and the answers at `j` differ. Both runs then +ask the same first `j + 1` queries, so the named query exists in both and is the same, while its +two answers differ (`mem_support_fork`). `runWithAnswers` runs a program on a list of answers, deterministically, recording its queries. Answering queries from `q` presampled uniform answers has the law of answering them uniformly as they come, when the program asks at most `q` queries: this is the presampling theorem -`ProbOracleComp.HasQueryBounds.eval_presample` (`interpret_uniform_eq`). Hence the general forking -lemma (`Probability.Forking.le_add_sqrt_fork`) bounds the acceptance probability of the program -with uniform answers by `q / |H| + √(q · frk)` (`le_add_sqrt_fork`). +`ProbOracleComp.HasQueryBounds.eval_presample` (`interpret_uniform_eq`, and +`run_interpret_countingUniform_eq` when the queries are also counted). Hence the general forking +lemma (`Probability.Forking.le_add_sqrt_fork`) bounds the probability that the program, with +uniform answers, validly names a query by `q / |H| + √(q · frk)` (`le_add_sqrt_fork`). The coins are explicit: the second run replays them. A program with private randomness is put in this form by drawing its coins in advance. The statements are exact; no efficiency is involved. @@ -37,12 +40,14 @@ this form by drawing its coins in advance. The statements are exact; no efficien ## Main definitions * `Cslib.OracleComp.runWithAnswers`: run on a list of answers, recording the queries. -* `Cslib.OracleComp.indexBelow`: the named position, if it is below `q`. +* `Cslib.OracleComp.validIndex`: the named position, if it is below `q` and was queried. +* `Cslib.OracleComp.countingUniform`: uniform answers as queries come, counting them. * `Cslib.OracleComp.forkingAlgorithm`: a program on coins and an answer vector, for forking. ## Main results -* `Cslib.OracleComp.interpret_uniform_eq`: uniform answers as they come, or presampled. +* `Cslib.OracleComp.interpret_uniform_eq`, `Cslib.OracleComp.run_interpret_countingUniform_eq`: + uniform answers as they come, or presampled. * `Cslib.OracleComp.le_add_sqrt_fork`: the forking lemma for oracle programs. * `Cslib.OracleComp.mem_support_fork`: both runs of a successful fork ask the same queries up to the named one, and answer it differently. @@ -73,6 +78,23 @@ def runWithAnswers (default : H) : OracleComp (fun _ : Query => H) α → List H ((runWithAnswers default (cont (answers.headD default)) answers.tail).1, q :: (runWithAnswers default (cont (answers.headD default)) answers.tail).2) +/-- Returning a value asks no query. -/ +@[simp] theorem runWithAnswers_pure (default : H) (a : α) (answers : List H) : + runWithAnswers default (pure a : OracleComp (fun _ : Query => H) α) answers = (a, []) := rfl + +/-- A query is answered by the head of the list, and the rest goes to the continuation. -/ +@[simp] theorem runWithAnswers_query_bind (default : H) (q : Query) + (cont : H → OracleComp (fun _ : Query => H) α) (answers : List H) : + runWithAnswers default (OracleComp.query (spec := fun _ : Query => H) q >>= cont) answers = + ((runWithAnswers default (cont (answers.headD default)) answers.tail).1, + q :: (runWithAnswers default (cont (answers.headD default)) answers.tail).2) := rfl + +/-- A mapped query is answered by the head of the list. -/ +@[simp] theorem runWithAnswers_map_query (default : H) (f : H → α) (q : Query) + (answers : List H) : + runWithAnswers default (f <$> OracleComp.query (spec := fun _ : Query => H) q) answers = + (f (answers.headD default), [q]) := rfl + /-- A program's first `n + 1` queries depend only on the first `n` answers. -/ theorem take_runWithAnswers (default : H) (program : OracleComp (fun _ : Query => H) α) : ∀ {answers answers' : List H} {n : ℕ}, answers.take n = answers'.take n → @@ -173,25 +195,100 @@ theorem interpret_uniform_eq [Fintype H] [Nonempty H] (default : H) simp only [PMF.pure_map] rfl +/-- Answer queries uniformly as they come, counting them in the state. -/ +noncomputable def countingUniform [Fintype H] [Nonempty H] (_ : Query) : StateT ℕ PMF H := + fun count => (PMF.uniformOfFintype H).map (·, count + 1) + +/-- Answering the lifted program from a saved list, counting the calls, is running it on that +list. -/ +private theorem eval_run_withSampleList_count (default : H) + (program : OracleComp (fun _ : Query => H) α) (count : ℕ) (answers : List H) : + ProbComp.eval ((fun (result, next, _) => (result, next)) <$> + (interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n)) + (withSampleList default fun v _ n => (pure (v, n + 1) : ProbComp (H × ℕ)))) + (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q) + program)).run (count, answers)) = + PMF.pure ((runWithAnswers default program answers).1, + count + (runWithAnswers default program answers).2.length) := by + induction program generalizing count answers with + | pure a => simp only [runWithAnswers, List.length_nil, add_zero]; rfl + | liftBind q cont ih => + change _ = PMF.pure ((runWithAnswers default (cont (answers.headD default)) answers.tail).1, + count + ((runWithAnswers default (cont (answers.headD default)) answers.tail).2.length + 1)) + rw [show count + ((runWithAnswers default (cont (answers.headD default)) answers.tail).2.length + + 1) = (count + 1) + + (runWithAnswers default (cont (answers.headD default)) answers.tail).2.length by omega, + ← ih (answers.headD default) (count + 1) answers.tail] + rfl + +/-- Answering lifted queries uniformly as they come, counting them, is `countingUniform`. -/ +private theorem eval_run_counting [Fintype H] [Nonempty H] + (program : OracleComp (fun _ : Query => H) α) (count : ℕ) : + ProbComp.eval ((interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n)) + (fun _ n => do + let value ← ProbComp.uniform H + (pure (value, n + 1) : ProbComp (H × ℕ)))) + (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q) + program)).run count) = + (interpret countingUniform program).run count := by + rw [ProbOracleComp.eval_run_interpret, interpret_interpret] + congr 1 + congr 1 + funext q n + simp only [ProbOracleComp.interpret_query, ProbComp.eval_bind, ProbComp.eval_uniform, + ProbComp.eval_pure] + rfl + +/-- Counting variant of `interpret_uniform_eq`: answering uniformly as queries come, and counting +them, has the law of running on `q` presampled uniform answers and counting the queries made. -/ +theorem run_interpret_countingUniform_eq [Fintype H] [Nonempty H] (default : H) + (program : OracleComp (fun _ : Query => H) α) {size : Query → ℕ} {q maxSize : ℕ} + (hq : (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q) + program).HasQueryBounds size q maxSize) (count : ℕ) : + (interpret countingUniform program).run count = + (PMF.uniformOfFintype (Fin q → H)).map fun h => + ((runWithAnswers default program (List.ofFn h)).1, + count + (runWithAnswers default program (List.ofFn h)).2.length) := by + have hp := hq.eval_presample (ProbComp.uniform H) default + (fun v _ n => (pure (v, n + 1) : ProbComp (H × ℕ))) count + rw [eval_run_counting, ProbComp.eval_bind, eval_replicate_uniform] at hp + simp only [eval_run_withSampleList_count, PMF.bind_map, Function.comp_def] at hp + rw [← hp] + rfl + /-! ### Forking -/ -/-- The named position, if it is below `q`. -/ -def indexBelow (q : ℕ) (position : Option ℕ) : Option (Fin q) := - position.bind fun j => if h : j < q then some ⟨j, h⟩ else none +/-- The named position, if it is below `q` and names one of the `count` queries made. A program +naming a position it never queried does not count as naming one. -/ +def validIndex (q count : ℕ) (position : Option ℕ) : Option (Fin q) := + position.bind fun j => if h : j < q ∧ j < count then some ⟨j, h.1⟩ else none + +/-- A valid index is a named position below `q` and below the number of queries made. -/ +theorem validIndex_eq_some {q count : ℕ} {position : Option ℕ} {j : Fin q} + (h : validIndex q count position = some j) : position = some j.val ∧ j.val < count := by + cases position with + | none => simp [validIndex] at h + | some p => + simp only [validIndex, Option.bind_some] at h + split_ifs at h with hp + simp only [Option.some.injEq] at h + subst h + exact ⟨rfl, hp.2⟩ /-- A program with explicit coins as an algorithm on coins and `q` answers, for the general -forking lemma: the named position below `q`, and the result with the queries. -/ +forking lemma: the validly named position, and the result with the queries. -/ def forkingAlgorithm {S β : Type} (default : H) (q : ℕ) (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (s : S) (h : Fin q → H) : Option (Fin q) × ((Option ℕ × β) × List Query) := - (indexBelow q (runWithAnswers default (program s) (List.ofFn h)).1.1, + (validIndex q (runWithAnswers default (program s) (List.ofFn h)).2.length + (runWithAnswers default (program s) (List.ofFn h)).1.1, runWithAnswers default (program s) (List.ofFn h)) variable {S β : Type} [Fintype H] [Nonempty H] [DecidableEq H] /-- **The forking lemma for oracle programs** ([BellareNeven2006], Lemma 1): if a program with -explicit coins asks at most `q` queries, and names a position below `q` with probability `acc` -when its queries are answered uniformly as they come, then forking it succeeds with probability +explicit coins asks at most `q` queries, and with probability `acc` names one of the queries it +made when they are answered uniformly as they come, then forking it succeeds with probability `frk` such that `acc ≤ q / |H| + √(q · frk)`. -/ theorem le_add_sqrt_fork (first : PMF S) (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (default : H) @@ -200,26 +297,27 @@ theorem le_add_sqrt_fork (first : PMF S) (program s)).HasQueryBounds size q maxSize) : ((do let s ← first - let result ← interpret (fun _ => PMF.uniformOfFintype H) (program s) - return (indexBelow q result.1).isSome : PMF Bool) true).toReal ≤ + let run ← (interpret countingUniform (program s)).run 0 + return (validIndex q run.2 run.1.1).isSome : PMF Bool) true).toReal ≤ q / Fintype.card H + √(q * ((Forking.fork first (forkingAlgorithm default q program)).map Option.isSome true).toReal) := by have hacc : (do let s ← first - let result ← interpret (fun _ => PMF.uniformOfFintype H) (program s) - return (indexBelow q result.1).isSome : PMF Bool) = + let run ← (interpret countingUniform (program s)).run 0 + return (validIndex q run.2 run.1.1).isSome : PMF Bool) = Forking.accept first (forkingAlgorithm default q program) := by simp only [Forking.accept, forkingAlgorithm, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure] refine congrArg _ (funext fun s => ?_) - rw [interpret_uniform_eq default (program s) (hq s), PMF.bind_map] + rw [run_interpret_countingUniform_eq default (program s) (hq s), PMF.bind_map] + simp only [zero_add] rfl rw [hacc] exact Forking.le_add_sqrt_fork first _ /-- A successful fork of a program reruns it on the same coins with answers that agree before the -named position `j` and differ at it; both runs name `j` and ask the same first `j + 1` -queries. -/ +named position `j` and differ at it. Both runs name `j`, ask the same first `j + 1` queries, and +have actually asked a query at position `j`, the same one. -/ theorem mem_support_fork {first : PMF S} {program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)} {default : H} {q : ℕ} {j : Fin q} {out out' : (Option ℕ × β) × List Query} @@ -228,24 +326,26 @@ theorem mem_support_fork {first : PMF S} ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧ out = runWithAnswers default (program s) (List.ofFn h) ∧ out' = runWithAnswers default (program s) (List.ofFn h') ∧ - out.1.1 = some j.val ∧ out'.1.1 = some j.val ∧ out.2.take (j + 1) = out'.2.take (j + 1) := by + out.1.1 = some j.val ∧ out'.1.1 = some j.val ∧ + out.2.take (j + 1) = out'.2.take (j + 1) ∧ + ∃ query, out.2[j.val]? = some query ∧ out'.2[j.val]? = some query := by obtain ⟨s, hs, h, h', hagree, hne, hrun, hrun'⟩ := Forking.mem_support_fork hfork simp only [forkingAlgorithm, Prod.mk.injEq] at hrun hrun' obtain ⟨hidx, rfl⟩ := hrun obtain ⟨hidx', rfl⟩ := hrun' - have hpos {r : Option ℕ} (hr : indexBelow q r = some j) : r = some j.val := by - cases r with - | none => simp [indexBelow] at hr - | some r => - simp only [indexBelow, Option.bind_some] at hr - split_ifs at hr with hlt - · simp only [Option.some.injEq, Fin.ext_iff] at hr - rw [hr] - refine ⟨s, hs, h, h', hagree, hne, rfl, rfl, hpos hidx, hpos hidx', - take_runWithAnswers default (program s) ?_⟩ - refine List.ext_getElem (by simp) fun i hi _ => ?_ - simp only [List.length_take, List.length_ofFn] at hi - simp only [List.getElem_take, List.getElem_ofFn] - exact hagree ⟨i, by omega⟩ (Fin.mk_lt_of_lt_val (by omega)) + obtain ⟨hpos, hlt⟩ := validIndex_eq_some hidx + obtain ⟨hpos', hlt'⟩ := validIndex_eq_some hidx' + have htake : (runWithAnswers default (program s) (List.ofFn h)).2.take (j + 1) = + (runWithAnswers default (program s) (List.ofFn h')).2.take (j + 1) := by + refine take_runWithAnswers default (program s) ?_ + refine List.ext_getElem (by simp) fun i hi _ => ?_ + simp only [List.length_take, List.length_ofFn] at hi + simp only [List.getElem_take, List.getElem_ofFn] + exact hagree ⟨i, by omega⟩ (Fin.mk_lt_of_lt_val (by omega)) + refine ⟨s, hs, h, h', hagree, hne, rfl, rfl, hpos, hpos', htake, + (runWithAnswers default (program s) (List.ofFn h)).2[j.val], List.getElem?_eq_getElem hlt, ?_⟩ + have hget := congrArg (fun l : List Query => l[j.val]?) htake + simp only [List.getElem?_take, Nat.lt_succ_self, ite_true] at hget + rw [← hget, List.getElem?_eq_getElem hlt] end Cslib.OracleComp diff --git a/ComplexityTests/Crypto/Forking.lean b/ComplexityTests/Crypto/Forking.lean index a4d611cab..5570b3ba6 100644 --- a/ComplexityTests/Crypto/Forking.lean +++ b/ComplexityTests/Crypto/Forking.lean @@ -15,7 +15,8 @@ An algorithm that always names its only answer is accepted with probability `1`, succeeds with probability at least `1 - 1 / 2`; it succeeds exactly when two independent bits differ, so the bound is attained. The oracle program that asks one query and names it satisfies the hypotheses of the oracle forking lemma, which gives a positive forking probability; a -successful fork gives two runs that ask the same query. +successful fork gives two runs that ask the same query. A program that names a position without +asking any query never forks successfully. -/ namespace ComplexityTests.Crypto.Forking @@ -61,9 +62,12 @@ example : (1 : ℝ) / 4 ≤ ((Forking.fork (PMF.pure ()) have h := OracleComp.le_add_sqrt_fork (PMF.pure ()) askOnce false askOnce_queries have hacc : ((do let s ← PMF.pure () - let result ← OracleComp.interpret (fun _ => PMF.uniformOfFintype Bool) (askOnce s) - return (OracleComp.indexBelow 1 result.1).isSome : PMF Bool) true).toReal = 1 := by - simp [askOnce, OracleComp.indexBelow] + let run ← (OracleComp.interpret OracleComp.countingUniform (askOnce s)).run 0 + return (OracleComp.validIndex 1 run.2 run.1.1).isSome : PMF Bool) true).toReal = 1 := by + rw [Probability.PMF.monad_bind_eq_bind, PMF.pure_bind, Probability.PMF.monad_bind_eq_bind, + OracleComp.run_interpret_countingUniform_eq false (askOnce ()) (askOnce_queries ()), + PMF.bind_map] + simp [Function.comp_def, askOnce, OracleComp.validIndex] rw [hacc] at h simp only [Fintype.card_bool, Nat.cast_ofNat, Nat.cast_one, one_mul] at h have hsqrt : (1 : ℝ) / 2 ≤ √(((Forking.fork (PMF.pure ()) @@ -79,9 +83,16 @@ example {j : Fin 1} {out out' : (Option ℕ × Bool) × List Unit} (hfork : some (j, out, out') ∈ (Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1 askOnce)).support) : out.2.take (j + 1) = out'.2.take (j + 1) := by - obtain ⟨-, -, -, -, -, -, -, -, -, -, htake⟩ := OracleComp.mem_support_fork hfork + obtain ⟨-, -, -, -, -, -, -, -, -, -, htake, -⟩ := OracleComp.mem_support_fork hfork exact htake +/-- A program that names position `0` without asking any query does not validly name it, so its +fork never succeeds. -/ +example : (Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1 + (fun _ : Unit => (pure (some 0, ()) : OracleComp (fun _ : Unit => Bool) (Option ℕ × Unit))))).map + Option.isSome true = 0 := by + simp [Forking.fork, OracleComp.forkingAlgorithm, OracleComp.validIndex] + /-! ### Axioms -/ /-- From 2bdbc432435b21549c2e77cf0689db989fe7ac0f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 20:29:29 -0400 Subject: [PATCH 3/3] test(probability): name the degenerate forking program Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ComplexityTests/Crypto/Forking.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/ComplexityTests/Crypto/Forking.lean b/ComplexityTests/Crypto/Forking.lean index 5570b3ba6..218fdc7f4 100644 --- a/ComplexityTests/Crypto/Forking.lean +++ b/ComplexityTests/Crypto/Forking.lean @@ -86,12 +86,15 @@ example {j : Fin 1} {out out' : (Option ℕ × Bool) × List Unit} obtain ⟨-, -, -, -, -, -, -, -, -, -, htake, -⟩ := OracleComp.mem_support_fork hfork exact htake +/-- Name position `0` without asking any query. -/ +def nameWithoutAsking (_ : Unit) : OracleComp (fun _ : Unit => Bool) (Option ℕ × Unit) := + pure (some 0, ()) + /-- A program that names position `0` without asking any query does not validly name it, so its fork never succeeds. -/ example : (Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1 - (fun _ : Unit => (pure (some 0, ()) : OracleComp (fun _ : Unit => Bool) (Option ℕ × Unit))))).map - Option.isSome true = 0 := by - simp [Forking.fork, OracleComp.forkingAlgorithm, OracleComp.validIndex] + nameWithoutAsking)).map Option.isSome true = 0 := by + simp [Forking.fork, OracleComp.forkingAlgorithm, OracleComp.validIndex, nameWithoutAsking] /-! ### Axioms -/