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. 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. Sequencing splits the answers (runWithAnswers_bind), so properties of a program run through a stateful handler follow from properties of single calls (runWithAnswers_run_interpret_invariant). 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 OracleComp.IsQueryBounded.run_interpret_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.

Main definitions

• Cslib.OracleComp.runWithAnswers: run on a list of answers, recording the queries.
• 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, 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.
• Cslib.OracleComp.take_runWithAnswers: a program's first n + 1 queries depend only on its first n answers.
• Cslib.OracleComp.runWithAnswers_run_interpret_invariant: an invariant of a handler's state and the queries asked so far holds after running a program through the handler on fixed answers.

References

• M. Bellare, G. Neven, Multi-Signatures in the Plain Public-Key Model and a General Forking Lemma, Lemma 1.
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Lemma 19.8.

def Cslib.OracleComp.runWithAnswers {Query H α : Type} (default : H) : OracleComp (fun (x : Query) => H) α → List H → α × List Query

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.

@[simp]

theorem Cslib.OracleComp.runWithAnswers_pure {Query H α : Type} (default : H) (a : α) (answers : List H) : runWithAnswers default (pure a) answers = (a, [])

Returning a value asks no query.

@[simp]

theorem Cslib.OracleComp.runWithAnswers_query_bind {Query H α : Type} (default : H) (q : Query) (cont : H → OracleComp (fun (x : Query) => H) α) (answers : List H) : runWithAnswers default (query q >>= cont) answers = ((runWithAnswers default (cont (answers.headD default)) answers.tail).1, q :: (runWithAnswers default (cont (answers.headD default)) answers.tail).2)

A query is answered by the head of the list, and the rest goes to the continuation.

@[simp]

theorem Cslib.OracleComp.runWithAnswers_map_query {Query H α : Type} (default : H) (f : H → α) (q : Query) (answers : List H) : runWithAnswers default (f <$> query q) answers = (f (answers.headD default), [q])

A mapped query is answered by the head of the list.

theorem Cslib.OracleComp.take_runWithAnswers {Query H α : Type} (default : H) (program : OracleComp (fun (x : Query) => H) α) {answers answers' : List H} {n : ℕ} : List.take n answers = List.take n answers' → List.take (n + 1) (runWithAnswers default program answers).2 = List.take (n + 1) (runWithAnswers default program answers').2

A program's first n + 1 queries depend only on the first n answers.

theorem Cslib.OracleComp.runWithAnswers_bind {Query H α β : Type} (default : H) (program : OracleComp (fun (x : Query) => H) α) (next : α → OracleComp (fun (x : Query) => H) β) (answers : List H) : runWithAnswers default (program >>= next) answers = ((runWithAnswers default (next (runWithAnswers default program answers).1) (List.drop (runWithAnswers default program answers).2.length answers)).1, (runWithAnswers default program answers).2 ++ (runWithAnswers default (next (runWithAnswers default program answers).1) (List.drop (runWithAnswers default program answers).2.length answers)).2)

Running a sequenced program on a list of answers runs the first part on the list and the second part on the answers the first part left unused.

theorem Cslib.OracleComp.IsQueryBounded.length_runWithAnswers_le {Query H α : Type} (default : H) {program : OracleComp (fun (x : Query) => H) α} {n : ℕ} (h : program.IsQueryBounded n) (answers : List H) : (runWithAnswers default program answers).2.length ≤ n

A program making at most n calls asks at most n queries on every list of answers.

theorem Cslib.OracleComp.runWithAnswers_run_interpret_invariant {Query H ι σ β : Type} {spec : ι → Type} (default : H) (handler : (q : ι) → StateT σ (OracleComp fun (x : Query) => H) (spec q)) (answers : List H) (invariant : σ → List Query → Prop) (step : ∀ (q : ι) (s : σ) (queries : List Query), invariant s queries → invariant (runWithAnswers default ((handler q).run s) (List.drop queries.length answers)).1.2 (queries ++ (runWithAnswers default ((handler q).run s) (List.drop queries.length answers)).2)) (program : OracleComp spec β) (s : σ) (queries : List Query) (hs : invariant s queries) : invariant (runWithAnswers default ((interpret handler program).run s) (List.drop queries.length answers)).1.2 (queries ++ (runWithAnswers default ((interpret handler program).run s) (List.drop queries.length answers)).2)

An invariant of a handler's run on a list of answers. A program runs through a stateful handler whose calls are oracle programs, and the resulting program runs on a list of answers. A property of the handler's state and of the queries asked so far that every handler call preserves, when run on the answers not yet used, holds at the end.

Presampled answers

theorem Cslib.OracleComp.interpret_uniform_eq {Query H α : Type} [Fintype H] [Nonempty H] (default : H) (program : OracleComp (fun (x : Query) => H) α) {q : ℕ} (hq : program.IsQueryBounded q) : interpret (fun (x : Query) => Probability.PMF.uniformOfFintype H) program = PMF.map (fun (h : Fin q → H) => (runWithAnswers default program (List.ofFn h)).1) (Probability.PMF.uniformOfFintype (Fin q → H))

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.IsQueryBounded.eval_presample.

noncomputable def Cslib.OracleComp.countingUniform {Query H : Type} [Fintype H] [Nonempty H] : Query → StateT ℕ PMF H

Answer queries uniformly as they come, counting them in the state.

theorem Cslib.OracleComp.run_interpret_countingUniform_eq {Query H α : Type} [Fintype H] [Nonempty H] (default : H) (program : OracleComp (fun (x : Query) => H) α) {q : ℕ} (hq : program.IsQueryBounded q) (count : ℕ) : (interpret countingUniform program).run count = PMF.map (fun (h : Fin q → H) => ((runWithAnswers default program (List.ofFn h)).1, count + (runWithAnswers default program (List.ofFn h)).2.length)) (Probability.PMF.uniformOfFintype (Fin q → H))

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.

Forking

def Cslib.OracleComp.validIndex (q count : ℕ) (position : Option ℕ) : Option (Fin q)

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.

theorem Cslib.OracleComp.validIndex_eq_some {q count : ℕ} {position : Option ℕ} {j : Fin q} (h : validIndex q count position = some j) : position = some ↑j ∧ ↑j < count

A valid index is a named position below q and below the number of queries made.

def Cslib.OracleComp.forkingAlgorithm {Query H S β : Type} (default : H) (q : ℕ) (program : S → OracleComp (fun (x : Query) => H) (Option ℕ × β)) (s : S) (h : Fin q → H) : Option (Fin q) × (Option ℕ × β) × List Query

A program with explicit coins as an algorithm on coins and q answers, for the general forking lemma: the validly named position, and the result with the queries.

theorem Cslib.OracleComp.le_add_sqrt_fork {Query H S β : Type} [Fintype H] [Nonempty H] [DecidableEq H] (first : PMF S) (program : S → OracleComp (fun (x : Query) => H) (Option ℕ × β)) (default : H) {q : ℕ} (hq : ∀ (s : S), (program s).IsQueryBounded q) : ((do let s ← first let run ← (interpret countingUniform (program s)).run 0 pure (validIndex q run.2 run.1.1).isSome) true).toReal ≤ ↑q / ↑(Fintype.card H) + √(↑q * ((PMF.map Option.isSome (Probability.Forking.fork first (forkingAlgorithm default q program))) true).toReal)

The forking lemma for oracle programs ([BN06], Lemma 1): if a program with 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 Cslib.OracleComp.mem_support_fork {Query H S β : Type} [Fintype H] [Nonempty H] [DecidableEq H] {first : PMF S} {program : S → OracleComp (fun (x : Query) => H) (Option ℕ × β)} {default : H} {q : ℕ} {j : Fin q} {out out' : (Option ℕ × β) × List Query} (hfork : some (j, out, out') ∈ (Probability.Forking.fork first (forkingAlgorithm default q program)).support) : ∃ s ∈ first.support, ∃ (h : Fin q → 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 ∧ out'.1.1 = some ↑j ∧ List.take (↑j + 1) out.2 = List.take (↑j + 1) out'.2 ∧ ∃ (query : Query), out.2[↑j]? = some query ∧ out'.2[↑j]? = some query

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, ask the same first j + 1 queries, and have actually asked a query at position j, the same one.