From 557571160ddd953fca6effa8c71d336be9ea27c0 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:49:44 -0400 Subject: [PATCH 1/7] =?UTF-8?q?doc(bib):=20add=20Ben-Sasson=E2=80=93Chiesa?= =?UTF-8?q?=E2=80=93Spooner=202016=20and=20Canetti=20et=20al.=202019?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- references.bib | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/references.bib b/references.bib index a043d4032a..4bc58c5c61 100644 --- a/references.bib +++ b/references.bib @@ -30,6 +30,18 @@ @article{MorenoRivera2016 note = {Article 1949} } +@inproceedings{BenSassonChiesaSpooner2016, + author = {Eli Ben-Sasson and Alessandro Chiesa and Nicholas Spooner}, + title = {Interactive Oracle Proofs}, + booktitle = {Theory of Cryptography -- TCC 2016-B, Part II}, + series = {Lecture Notes in Computer Science}, + volume = {9986}, + pages = {31--60}, + publisher = {Springer}, + year = {2016}, + doi = {10.1007/978-3-662-53644-5_2} +} + @article{BenSassonWigderson2001, author = {Ben-Sasson, Eli and Wigderson, Avi}, title = {Short Proofs Are Narrow---Resolution Made Simple}, @@ -421,6 +433,18 @@ @misc{BonehShoup2023 url = {https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf} } +@inproceedings{CanettiCHLRRW2019, + author = {Ran Canetti and Yilei Chen and Justin Holmgren and Alex Lombardi and + Guy N. Rothblum and Ron D. Rothblum and Daniel Wichs}, + title = {Fiat--Shamir: From Practice to Theory}, + booktitle = {Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing}, + series = {STOC 2019}, + pages = {1082--1090}, + publisher = {ACM}, + year = {2019}, + doi = {10.1145/3313276.3316380} +} + @inproceedings{CramerDamgardSchoenmakers1994, author = {Ronald Cramer and Ivan Damg{\aa}rd and Berry Schoenmakers}, title = {Proofs of Partial Knowledge and Simplified Design of Witness Hiding Protocols}, From d7d9d2a61294da1f3c78c02a07283ca8a52de4b0 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:49:45 -0400 Subject: [PATCH 2/7] feat(interactive): public-coin interactive reductions and sequential composition Typed public-coin protocols as lists of rounds with oracle interfaces, continuation-tree provers, sampler-and-decision verifiers and worlds; exact completeness, soundness, straight-line knowledge soundness, worst-case round-by-round soundness and HVZK. In the plain model: round-by-round soundness implies soundness, and sequential composition and iteration of completeness, soundness, knowledge soundness and round-by-round soundness. Milestone 1 (part A) of #643. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 4 + .../Computability/Interactive/Basic.lean | 274 ++++++ .../Computability/Interactive/Plain.lean | 224 +++++ .../Computability/Interactive/Security.lean | 168 ++++ .../Computability/Interactive/Sequential.lean | 814 ++++++++++++++++++ ComplexityTests.lean | 1 + ComplexityTests/Interactive.lean | 117 +++ 7 files changed, 1602 insertions(+) create mode 100644 Complexity/Computability/Interactive/Basic.lean create mode 100644 Complexity/Computability/Interactive/Plain.lean create mode 100644 Complexity/Computability/Interactive/Security.lean create mode 100644 Complexity/Computability/Interactive/Sequential.lean create mode 100644 ComplexityTests/Interactive.lean diff --git a/Complexity.lean b/Complexity.lean index e34b9456ee..73e83f43f2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -818,6 +818,10 @@ public import Complexity.Computability.GenericRAM.Simulation.Run public import Complexity.Computability.GenericRAM.Simulation.Turing public import Complexity.Computability.GenericRAM.SparseMemory.Basic public import Complexity.Computability.GenericRAM.SparseMemory.Turing +public import Complexity.Computability.Interactive.Basic +public import Complexity.Computability.Interactive.Plain +public import Complexity.Computability.Interactive.Security +public import Complexity.Computability.Interactive.Sequential public import Complexity.Computability.Kolmogorov.Basic public import Complexity.Computability.Kolmogorov.ChainRule public import Complexity.Computability.Kolmogorov.Depth diff --git a/Complexity/Computability/Interactive/Basic.lean b/Complexity/Computability/Interactive/Basic.lean new file mode 100644 index 0000000000..2d82300a73 --- /dev/null +++ b/Complexity/Computability/Interactive/Basic.lean @@ -0,0 +1,274 @@ +/- +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.Interaction + +/-! +# Public-coin interactive oracle reductions + +An interactive reduction from a relation `R₁` to a relation `R₂` is a public-coin protocol in which +a prover convinces a verifier, who holds a statement of `R₁`, to output a statement of `R₂`, and +whose prover outputs a witness for it [Ben-Sasson, Chiesa and Spooner][BenSassonChiesaSpooner2016]. +Interactive proofs, arguments, interactive oracle proofs and proofs of knowledge are the +reductions to acceptance. + +A protocol is described by its rounds (`Interactive.Spec`, a list of `Interactive.Round`s). In a +prover round the prover sends a message, which the verifier only accesses through the message's +`Interactive.OracleInterface` (reading the whole message is the interface `OracleInterface.full`); +in a verifier round the verifier sends a public random challenge, drawn from a sampler. + +A prover is a strategy tree (`Interactive.ProverStrategy`) in the monad `ProbOracleComp oP`; it may +draw private coins and query its oracles `oP`. A public-coin verifier +(`Interactive.Verifier`) consists of one challenge sampler per verifier round and a decision: a +program that queries its oracles `oV` and the prover's messages, given the statement and the +challenges, and returns the output statement, or `none` to reject. A reduction from a relation +`R₁` to a relation `R₂` (`Interactive.Reduction`) pairs an honest prover with a verifier. + +Runs live in `ProbOracleComp (oP ⊕ₒ oV)`; a `World` implements the joint oracles (the plain +model, a random oracle, an ideal functionality) as one stateful handler, and `World.eval` gives +the output law. + +Shapes depend only on parameters fixed before the interaction (the *index*: field, sizes, +circuit), never on the statement or on earlier messages. Everything indexed by a shape is defined +by structural recursion on its list of rounds, so concatenated protocols compute without casts. + +## Main definitions + +* `Cslib.OracleSpec.sum` (notation `⊕ₒ`, scoped in `Interactive`), `Interactive.emptySpec`. +* `Interactive.OracleInterface`, `Interactive.Round`, `Interactive.Spec`. +* `Interactive.Spec.Transcript`, `Interactive.Spec.PerChallenge`, `Interactive.Spec.MsgQuery`. +* `Interactive.ProverStrategy`, `Interactive.Prover`, `Interactive.Verifier`, + `Interactive.Reduction`. +* `Interactive.runStrategy`, `Interactive.Verifier.execute`, `Interactive.Reduction.run`. +* `Interactive.World`, `Interactive.World.eval`, `Interactive.World.plain`. + +## References + +* [E. Ben-Sasson, A. Chiesa, N. Spooner, *Interactive Oracle Proofs*][BenSassonChiesaSpooner2016] +-/ + +@[expose] public section + +namespace Cslib.Interactive + +open scoped ENNReal + +/-! ### Oracle specifications -/ + +/-- The disjoint union of two oracle interfaces. -/ +abbrev _root_.Cslib.OracleSpec.sum {ι₁ ι₂ : Type} (spec₁ : OracleSpec ι₁) + (spec₂ : OracleSpec ι₂) : OracleSpec (ι₁ ⊕ ι₂) := + Sum.elim spec₁ spec₂ + +@[inherit_doc] scoped infixr:65 " ⊕ₒ " => Cslib.OracleSpec.sum + +/-- The interface without queries, for parties that use no oracle. -/ +abbrev emptySpec : OracleSpec Empty := fun q => q.elim + +/-! ### Messages and rounds -/ + +/-- How the verifier accesses a prover message of type `M`: the queries it may ask and the +responses the message gives. -/ +structure OracleInterface (M : Type) where + /-- The queries the verifier may ask about a message. -/ + Query : Type + /-- The type of the response to each query. -/ + Response : Query → Type + /-- The message's response to each query. -/ + answer : M → (q : Query) → Response q + +/-- Reading the whole message with a single query. -/ +def OracleInterface.full (M : Type) : OracleInterface M where + Query := Unit + Response _ := M + answer m _ := m + +/-- Reading single coordinates of a vector message `ι → A` (as for a codeword or a PCP). -/ +def OracleInterface.coord (ι A : Type) : OracleInterface (ι → A) where + Query := ι + Response _ := A + answer f i := f i + +/-- A round of a public-coin protocol. -/ +inductive Round : Type 1 where + /-- The prover sends a message of type `M`, which the verifier accesses through `I`. -/ + | prover (M : Type) (I : OracleInterface M) + /-- The verifier sends a public random challenge of type `C`. -/ + | verifier (C : Type) + +/-- The type of the message sent in a round. -/ +abbrev Round.Message : Round → Type + | .prover M _ => M + | .verifier C => C + +/-- A protocol specification: its rounds, in order. -/ +abbrev Spec := List Round + +namespace Spec + +/-- A complete transcript: the message of every round. -/ +@[reducible] def Transcript : Spec → Type + | [] => Unit + | r :: s => r.Message × Transcript s + +/-- One value of `F C` for every verifier round with challenges in `C`: the challenges themselves +(`F = id`), their samplers (`F = ProbComp`) or per-round errors (`F = fun _ => ℝ≥0∞`). -/ +@[reducible] def PerChallenge (F : Type → Type) : Spec → Type + | [] => Unit + | .prover _ _ :: s => PerChallenge F s + | .verifier C :: s => F C × PerChallenge F s + +/-- The verifier's challenges in a run. -/ +abbrev Challenges (s : Spec) : Type := PerChallenge id s + +/-- The challenges of a transcript. -/ +def Transcript.challenges : (s : Spec) → Transcript s → Challenges s + | [], _ => () + | .prover _ _ :: s, τ => Transcript.challenges s τ.2 + | .verifier _ :: s, τ => (τ.1, Transcript.challenges s τ.2) + +/-- The queries the verifier may ask about the prover's messages. -/ +@[reducible] def MsgQuery : Spec → Type + | [] => Empty + | .prover _ I :: s => I.Query ⊕ MsgQuery s + | .verifier _ :: s => MsgQuery s + +/-- The response types of the queries about the prover's messages. -/ +@[reducible] def MsgResponse : (s : Spec) → MsgQuery s → Type + | [], q => q.elim + | .prover _ I :: _, .inl q => I.Response q + | .prover _ _ :: s, .inr q => MsgResponse s q + | .verifier _ :: s, q => MsgResponse s q + +/-- The oracle interface of the prover's messages. -/ +abbrev msgSpec (s : Spec) : OracleSpec (MsgQuery s) := MsgResponse s + +/-- The prover's messages in a transcript answer the verifier's queries. -/ +def Transcript.answer : (s : Spec) → Transcript s → (q : MsgQuery s) → MsgResponse s q + | [], _, q => q.elim + | .prover _ I :: _, τ, .inl q => I.answer τ.1 q + | .prover _ _ :: s, τ, .inr q => Transcript.answer s τ.2 q + | .verifier _ :: s, τ, q => Transcript.answer s τ.2 q + +end Spec + +open Spec + +/-! ### Provers and verifiers -/ + +/-- A strategy of a party sending the prover's messages in the rounds `s`, in the monad `m`, ending +with a result of type `α`. In a prover round it computes a message and its continuation; in a +verifier round it awaits the challenge. -/ +@[reducible] def ProverStrategy (m : Type → Type) : Spec → Type → Type + | [], α => α + | .prover M _ :: s, α => m (M × ProverStrategy m s α) + | .verifier C :: s, α => C → m (ProverStrategy m s α) + +/-- A prover from statements `StmtIn` with witnesses `WitIn` to statements `StmtOut` with witnesses +`WitOut`, using the oracles `oP`. -/ +abbrev Prover {ιP : Type} (oP : OracleSpec ιP) (s : Spec) (StmtIn WitIn StmtOut WitOut : Type) := + StmtIn → WitIn → ProbOracleComp oP (ProverStrategy (ProbOracleComp oP) s (StmtOut × WitOut)) + +/-- A public-coin verifier from statements `StmtIn` to statements `StmtOut`, using the oracles +`oV`. Its challenges are drawn from `samplers`. Its decision sees the statement and the challenges, +queries the prover's messages and `oV`, and returns the output statement or rejects (`none`). -/ +structure Verifier {ιV : Type} (oV : OracleSpec ιV) (s : Spec) (StmtIn StmtOut : Type) where + /-- The distribution of each challenge. -/ + samplers : PerChallenge ProbComp s + /-- The decision, with oracle access to the prover's messages. -/ + decide : StmtIn → Challenges s → OracleComp (oV ⊕ₒ msgSpec s) (Option StmtOut) + +/-- An interactive reduction: an honest prover and a public-coin verifier. -/ +structure Reduction {ιP ιV : Type} (oP : OracleSpec ιP) (oV : OracleSpec ιV) (s : Spec) + (StmtIn WitIn StmtOut WitOut : Type) where + /-- The honest prover. -/ + prover : Prover oP s StmtIn WitIn StmtOut WitOut + /-- The verifier. -/ + verifier : Verifier oV s StmtIn StmtOut + +/-! ### Execution -/ + +section Execution + +variable {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} + +/-- Lift a prover computation into the joint oracles. -/ +def liftProver {α : Type} : ProbOracleComp oP α → ProbOracleComp (oP ⊕ₒ oV) α := + OracleComp.interpret (ProbOracleComp.handler + (fun n => OracleComp.query (spec := probOracleSpec (oP ⊕ₒ oV)) (.inl n)) + (fun q => ProbOracleComp.query (spec := oP ⊕ₒ oV) (.inl q))) + +/-- Run a prover strategy against public challenges drawn from `samplers`, returning the transcript +and the strategy's result. -/ +def runStrategy {α : Type} : + (s : Spec) → PerChallenge ProbComp s → ProverStrategy (ProbOracleComp oP) s α → + ProbOracleComp oP (Transcript s × α) + | [], _, a => pure ((), a) + | .prover _ _ :: s, smp, st => do + let (msg, st') ← st + let (τ, a) ← runStrategy s smp st' + return ((msg, τ), a) + | .verifier _ :: s, smp, st => do + let c ← ProbOracleComp.sample smp.1 + let st' ← st c + let (τ, a) ← runStrategy s smp.2 st' + return ((c, τ), a) + +/-- Run the verifier's decision on a transcript, answering its queries about the prover's messages +from the transcript. -/ +def Verifier.output {s : Spec} {StmtIn StmtOut : Type} (V : Verifier oV s StmtIn StmtOut) + (x : StmtIn) (τ : Transcript s) : ProbOracleComp (oP ⊕ₒ oV) (Option StmtOut) := + OracleComp.interpret + (fun q => match q with + | .inl q => ProbOracleComp.query (spec := oP ⊕ₒ oV) (.inr q) + | .inr q => pure (Transcript.answer s τ q)) + (V.decide x (Transcript.challenges s τ)) + +/-- Run the verifier against any (possibly malicious) prover strategy with result type `α`: the +transcript, the verifier's output and the prover's result. -/ +def Verifier.execute {s : Spec} {StmtIn StmtOut α : Type} (V : Verifier oV s StmtIn StmtOut) + (x : StmtIn) (P : ProbOracleComp oP (ProverStrategy (ProbOracleComp oP) s α)) : + ProbOracleComp (oP ⊕ₒ oV) (Transcript s × Option StmtOut × α) := do + let st ← liftProver P + let (τ, a) ← liftProver (runStrategy s V.samplers st) + let out ← V.output (oP := oP) x τ + return (τ, out, a) + +/-- An honest run of a reduction on `x` with witness `w`. -/ +def Reduction.run {s : Spec} {StmtIn WitIn StmtOut WitOut : Type} + (R : Reduction oP oV s StmtIn WitIn StmtOut WitOut) (x : StmtIn) (w : WitIn) : + ProbOracleComp (oP ⊕ₒ oV) (Transcript s × Option StmtOut × (StmtOut × WitOut)) := + R.verifier.execute x (R.prover x w) + +/-- A model of the oracles: one stateful implementation of the prover's and verifier's oracles +(no oracles, a random oracle, an ideal functionality). -/ +structure World {ιP ιV : Type} (oP : OracleSpec ιP) (oV : OracleSpec ιV) where + /-- The private state of the oracles. -/ + State : Type + /-- The initial state. -/ + init : State + /-- The joint implementation. -/ + impl : (q : ιP ⊕ ιV) → StateT State PMF ((oP ⊕ₒ oV) q) + +/-- The output law of a program in a world. -/ +noncomputable def World.eval (W : World oP oV) {α : Type} (program : ProbOracleComp (oP ⊕ₒ oV) α) : + PMF α := + (ProbOracleComp.runWith W.impl program W.init).map Prod.fst + +/-- The plain model: no oracles. -/ +def World.plain : World emptySpec emptySpec where + State := Unit + init := () + impl + | .inl e => e.elim + | .inr e => e.elim + +end Execution + +end Cslib.Interactive diff --git a/Complexity/Computability/Interactive/Plain.lean b/Complexity/Computability/Interactive/Plain.lean new file mode 100644 index 0000000000..8b3bb7d86d --- /dev/null +++ b/Complexity/Computability/Interactive/Plain.lean @@ -0,0 +1,224 @@ +/- +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.Computability.Interactive.Security +import Complexity.Probability.PMF + +/-! +# Interactive reductions in the plain model + +In the plain model neither party has oracles, and a run is an ordinary probabilistic program. +`Interactive.plainLaw` is the law of a prover-side program, and +`Interactive.World.plain_eval_execute` computes the law of a whole execution from the law of the +prover's run. The main result is that round-by-round soundness implies soundness with the sum of +the per-round errors (`Interactive.Verifier.RbrSound.sound`), against arbitrary prover strategies. + +## Main definitions + +* `Interactive.plainLaw`: the law of a program without oracles. + +## Main results + +* `Interactive.World.plain_eval_execute`: the law of an execution in the plain model. +* `Interactive.Verifier.RbrSound.sound`: round-by-round soundness implies soundness. + +## References + +* [R. Canetti, Y. Chen, J. Holmgren, A. Lombardi, G. N. Rothblum, R. D. Rothblum, D. Wichs, + *Fiat–Shamir: from practice to theory*][CanettiCHLRRW2019] +-/ + +@[expose] public section + +namespace Cslib.Interactive + +open scoped ENNReal +open Spec + +/-- The law of a program without external oracles: its private coins are fair. -/ +noncomputable def plainLaw {α : Type} (p : ProbOracleComp emptySpec α) : PMF α := + OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun e => e.elim) p + +/-- The law of a joint program in the plain model. -/ +private noncomputable def runLaw {α : Type} (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) : + PMF α := + OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun q => match q with + | .inl e => e.elim + | .inr e => e.elim) p + +private theorem plain_eval {α : Type} (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) : + World.plain.eval p = runLaw p := by + have h := OracleComp.run_interpret_stateless (m := PMF) (State := Unit) + (ProbOracleComp.handler ProbComp.unifOracle fun q => match q with + | .inl e => e.elim + | .inr e => e.elim) p () + have hh : (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) + World.plain.impl) = + fun q s => (fun a => (a, s)) <$> ProbOracleComp.handler ProbComp.unifOracle + (fun q => match q with + | .inl e => e.elim + | .inr e => e.elim) q := by + funext q s + rcases q with n | e | e + · rfl + · exact e.elim + · exact e.elim + unfold World.eval ProbOracleComp.runWith + erw [hh, h] + exact (PMF.map_comp _ _ _).trans (PMF.map_id _) + +private theorem runLaw_liftProver {α : Type} (p : ProbOracleComp emptySpec α) : + runLaw (liftProver (oV := emptySpec) p) = plainLaw p := by + rw [runLaw, liftProver, OracleComp.interpret_interpret, plainLaw] + congr 1 + funext q + rcases q with n | e + · simp [ProbOracleComp.handler] + · exact e.elim + + +/-- A returned value has a point law. -/ +@[simp] theorem plainLaw_pure {α : Type} (a : α) : + plainLaw (pure a : ProbOracleComp emptySpec α) = PMF.pure a := rfl + +/-- Sequencing is `PMF.bind`. -/ +@[simp] theorem plainLaw_bind {α β : Type} (p : ProbOracleComp emptySpec α) + (f : α → ProbOracleComp emptySpec β) : + plainLaw (p >>= f) = (plainLaw p).bind fun a => plainLaw (f a) := + OracleComp.interpret_bind _ _ _ + +/-- Postprocessing is `PMF.map`. -/ +@[simp] theorem plainLaw_map {α β : Type} (f : α → β) (p : ProbOracleComp emptySpec α) : + plainLaw (f <$> p) = (plainLaw p).map f := + OracleComp.interpret_map _ _ _ + +/-- Embedded sampling has the law of the sampled program. -/ +@[simp] theorem plainLaw_sample {α : Type} (p : ProbComp α) : + plainLaw (ProbOracleComp.sample (spec := emptySpec) p) = ProbComp.eval p := + ProbOracleComp.interpret_sample _ _ _ + +private theorem runLaw_pure {α : Type} (a : α) : + runLaw (pure a : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) = PMF.pure a := rfl + +private theorem runLaw_bind {α β : Type} (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) + (f : α → ProbOracleComp (emptySpec ⊕ₒ emptySpec) β) : + runLaw (p >>= f) = (runLaw p).bind fun a => runLaw (f a) := + OracleComp.interpret_bind _ _ _ + +private theorem runLaw_map {α β : Type} (f : α → β) + (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) : runLaw (f <$> p) = (runLaw p).map f := + OracleComp.interpret_map _ _ _ + +/-- A program whose queries are answered deterministically has a point law. -/ +private theorem interpret_pure_handler {ι : Type} {spec : OracleSpec ι} {α : Type} + (f : (q : ι) → spec q) (p : OracleComp spec α) : + OracleComp.interpret (m := PMF) (fun q => PMF.pure (f q)) p = + PMF.pure (OracleComp.interpret (m := Id) f p) := by + induction p using PFunctor.FreeM.induction with + | pure a => rfl + | lift_bind q cont ih => + rw [show (PFunctor.FreeM.lift q).bind cont = OracleComp.query q >>= cont from rfl, + OracleComp.interpret_bind, OracleComp.interpret_bind, OracleComp.interpret_query, + OracleComp.interpret_query] + simp only [Probability.PMF.monad_bind_eq_bind, PMF.pure_bind] + exact ih (f q) + +private theorem runLaw_output {s : Spec} {StmtIn StmtOut : Type} + (V : Verifier emptySpec s StmtIn StmtOut) + (x : StmtIn) (τ : Transcript s) : + runLaw (V.output (oP := emptySpec) x τ) = PMF.pure (V.outputOn x τ) := by + rw [runLaw, Verifier.output, OracleComp.interpret_interpret, Verifier.outputOn] + rw [← interpret_pure_handler] + congr 1 + funext q + rcases q with e | q + · exact e.elim + · rfl + +private theorem toOuterMeasure_bind_le {α β : Type} (p : PMF α) (f : α → PMF β) (t : Set β) + {K : ℝ≥0∞} (h : ∀ a, (f a).toOuterMeasure t ≤ K) : (p.bind f).toOuterMeasure t ≤ K := by + rw [PMF.toOuterMeasure_bind_apply] + exact Probability.PMF.tsum_mul_le_of_forall_le _ h + +private theorem toOuterMeasure_bind_pure {α β : Type} (p : PMF α) (g : α → β) (t : Set β) : + (p.bind fun a => PMF.pure (g a)).toOuterMeasure t = p.toOuterMeasure (g ⁻¹' t) := by + rw [← PMF.toOuterMeasure_map_apply] + rfl + +/-- **The law of an execution in the plain model**: run the prover's strategy against the +challenge samplers, then apply the verifier's decision to the transcript. -/ +theorem World.plain_eval_execute {s : Spec} {StmtIn StmtOut α : Type} + (V : Verifier emptySpec s StmtIn StmtOut) (x : StmtIn) + (P : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s α)) : + World.plain.eval (V.execute (oP := emptySpec) x P) = + (plainLaw (P >>= runStrategy s V.samplers)).map fun r => (r.1, V.outputOn x r.1, r.2) := by + rw [plain_eval] + simp only [Verifier.execute, runLaw_bind, runLaw_liftProver, runLaw_output, runLaw_pure, + PMF.pure_bind, plainLaw_bind, PMF.map_bind] + rfl + +/-- From a doomed prefix, the rest of a run wins with probability at most the remaining errors. -/ +private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s) + (ε : PerChallenge (fun _ => ℝ≥0∞) s) (S : Prefix s → Prop) (wins : Transcript s → Prop), + RbrFrom s smp ε S wins → ¬ S (Prefix.empty s) → + ∀ {α : Type} (st : ProverStrategy (ProbOracleComp emptySpec) s α), + (plainLaw (runStrategy s smp st)).toOuterMeasure {r | wins r.1} ≤ PerChallenge.sum s ε + | [], _, _, _, wins, h, hS, _, st => by + have hw : ¬ wins () := h hS + simp [runStrategy, hw] + | .prover M I :: s, smp, ε, S, wins, h, hS, _, st => by + simp only [runStrategy, plainLaw_bind] + refine toOuterMeasure_bind_le _ _ _ fun p => ?_ + rcases p with ⟨msg, st'⟩ + simp only [plainLaw_pure] + rw [toOuterMeasure_bind_pure] + exact rbrFrom_le s smp ε (fun p => S (some (msg, p))) (fun τ => wins (msg, τ)) (h.2 msg) + (h.1 hS msg) st' + | .verifier C :: s, smp, ε, S, wins, h, hS, _, st => by + simp only [runStrategy, plainLaw_bind, plainLaw_sample] + rw [PMF.toOuterMeasure_bind_apply] + set A : Set C := {c | S (some (c, Prefix.empty s))} + have hinner : ∀ c, ((plainLaw (st c)).bind fun st' => (plainLaw (runStrategy s smp.2 st')).bind + fun r => plainLaw (pure ((c, r.1), r.2))).toOuterMeasure {r | wins r.1} ≤ + A.indicator 1 c + PerChallenge.sum s ε.2 := by + intro c + by_cases hc : c ∈ A + · refine le_trans ?_ le_self_add + rw [Set.indicator_of_mem hc] + exact Probability.PMF.toOuterMeasure_le_one _ _ + · rw [Set.indicator_of_notMem hc, zero_add] + refine toOuterMeasure_bind_le _ _ _ fun st' => ?_ + simp only [plainLaw_pure] + rw [toOuterMeasure_bind_pure] + exact rbrFrom_le s smp.2 ε.2 (fun p => S (some (c, p))) (fun τ => wins (c, τ)) (h.2 c) hc + st' + calc ∑' c, ProbComp.eval smp.1 c * _ ≤ + ∑' c, ProbComp.eval smp.1 c * (A.indicator 1 c + PerChallenge.sum s ε.2) := + ENNReal.tsum_le_tsum fun c => by gcongr; exact hinner c + _ = (ProbComp.eval smp.1).toOuterMeasure A + PerChallenge.sum s ε.2 := by + simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + PMF.toOuterMeasure_apply] + congr 1 + refine tsum_congr fun c => ?_ + by_cases hc : c ∈ A <;> simp [hc] + _ ≤ ε.1 + PerChallenge.sum s ε.2 := by gcongr; exact h.1 hS + +/-- **Round-by-round soundness implies soundness**, with the sum of the per-round errors. -/ +theorem Verifier.RbrSound.sound {s : Spec} {StmtIn StmtOut : Type} + {V : Verifier emptySpec s StmtIn StmtOut} {langIn : Set StmtIn} + {langOut : Set StmtOut} {ε : PerChallenge (fun _ => ℝ≥0∞) s} + (h : V.RbrSound langIn langOut ε) : + V.Sound (oP := emptySpec) World.plain langIn langOut (PerChallenge.sum s ε) := by + obtain ⟨S, hinit, hround⟩ := h + intro x hx α P + rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply, plainLaw_bind] + exact toOuterMeasure_bind_le _ _ _ fun st => rbrFrom_le s V.samplers ε (S x) _ (hround x) + (hinit x hx) st + +end Cslib.Interactive diff --git a/Complexity/Computability/Interactive/Security.lean b/Complexity/Computability/Interactive/Security.lean new file mode 100644 index 0000000000..cf39a17571 --- /dev/null +++ b/Complexity/Computability/Interactive/Security.lean @@ -0,0 +1,168 @@ +/- +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.Computability.Interactive.Basic + +/-! +# Security of interactive reductions + +Exact security notions for a reduction from a relation `relIn` to a relation `relOut`, in a world +`W` implementing the oracles. All errors are in `ℝ≥0∞`; a perfect notion is error `0`. + +* `Reduction.Complete W R relIn relOut ε`: on every `(x, w)` in `relIn`, the honest run fails with + probability at most `ε`, where success means that the verifier outputs the prover's statement + and the prover's witness is valid for it. +* `Verifier.Sound W V langIn langOut ε`: on every `x ∉ langIn`, every prover strategy makes the + verifier output a statement of `langOut` with probability at most `ε`. +* `Verifier.KnowledgeSound W V relIn relOut E ε`: the straight-line extractor `E` recovers a valid + input witness from the transcript and the prover's output witness, except with probability `ε`. +* `Verifier.RbrSound V langIn langOut ε`: round-by-round soundness in the plain model, with an + error for every challenge round, through a state function on transcript prefixes. +* `Reduction.HVZK W R relIn Sim ε`: the simulator's transcripts are `ε`-close in statistical + distance to honest ones. + +Proof systems, arguments and proofs of knowledge are the reductions to the trivial relation +`Interactive.Accept`, with output language `Set.univ`. Extractors and simulators are named +arguments, so a property cannot hold vacuously through an unconstrained existential. Their +efficiency is a separate layer. + +## Main definitions + +* `Interactive.language`, `Interactive.Accept`, `Interactive.CloseTo`. +* `Interactive.Reduction.Complete`, `Interactive.Verifier.Sound`, + `Interactive.Verifier.KnowledgeSound`. +* `Interactive.Prefix`, `Interactive.RbrFrom`, `Interactive.Verifier.RbrSound`. +* `Interactive.Reduction.HVZK`. + +## References + +* [R. Canetti, Y. Chen, J. Holmgren, A. Lombardi, G. N. Rothblum, R. D. Rothblum, D. Wichs, + *Fiat–Shamir: from practice to theory*][CanettiCHLRRW2019] +-/ + +@[expose] public section + +namespace Cslib.Interactive + +open scoped ENNReal +open Spec + +variable {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : Spec} + {StmtIn WitIn StmtOut WitOut : Type} + +/-- The language of a relation: the statements with a witness. -/ +def language {Stmt Wit : Type} (rel : Stmt → Wit → Prop) : Set Stmt := {x | ∃ w, rel x w} + +/-- The trivial relation that proof systems reduce to: acceptance. -/ +def Accept : Unit → Unit → Prop := fun _ _ => True + +/-- `μ` is within statistical distance `ε` of `ν`: no event is more likely under `μ` than under +`ν` by more than `ε`. Quantifying over all events makes this symmetric, and it is the total +variation distance on any type, finite or not. -/ +def CloseTo {α : Type} (μ ν : PMF α) (ε : ℝ≥0∞) : Prop := + ∀ event : Set α, μ.toOuterMeasure event ≤ ν.toOuterMeasure event + ε + +/-- Statistical closeness is preserved by postprocessing. -/ +theorem CloseTo.map {α β : Type} {μ ν : PMF α} {ε : ℝ≥0∞} (h : CloseTo μ ν ε) (f : α → β) : + CloseTo (μ.map f) (ν.map f) ε := fun event => by + simpa only [PMF.toOuterMeasure_map_apply] using h (f ⁻¹' event) + +/-- Statistical closeness errors add along a chain. -/ +theorem CloseTo.trans {α : Type} {μ ν ρ : PMF α} {ε δ : ℝ≥0∞} (h₁ : CloseTo μ ν ε) + (h₂ : CloseTo ν ρ δ) : CloseTo μ ρ (ε + δ) := fun event => + (h₁ event).trans <| by + rw [add_comm ε δ, ← add_assoc] + exact add_le_add (h₂ event) le_rfl + +/-! ### Completeness, soundness and knowledge soundness -/ + +/-- Completeness with error `ε`. -/ +def Reduction.Complete (W : World oP oV) (R : Reduction oP oV s StmtIn WitIn StmtOut WitOut) + (relIn : StmtIn → WitIn → Prop) (relOut : StmtOut → WitOut → Prop) (ε : ℝ≥0∞) : Prop := + ∀ x w, relIn x w → + (W.eval (R.run x w)).toOuterMeasure + {r | ¬ (r.2.1 = some r.2.2.1 ∧ relOut r.2.2.1 r.2.2.2)} ≤ ε + +/-- Soundness with error `ε`, against every prover strategy. -/ +def Verifier.Sound (W : World oP oV) (V : Verifier oV s StmtIn StmtOut) + (langIn : Set StmtIn) (langOut : Set StmtOut) (ε : ℝ≥0∞) : Prop := + ∀ x ∉ langIn, ∀ (α : Type) (P : ProbOracleComp oP (ProverStrategy (ProbOracleComp oP) s α)), + (W.eval (V.execute x P)).toOuterMeasure {r | ∃ x' ∈ langOut, r.2.1 = some x'} ≤ ε + +/-- Straight-line knowledge soundness with error `ε`: whenever a prover strategy, ending with an +output witness, makes the verifier output a statement for which that witness is valid, the +extractor `E` recovers a valid input witness from the statement, the transcript and the output +witness, except with probability `ε`. -/ +def Verifier.KnowledgeSound (W : World oP oV) (V : Verifier oV s StmtIn StmtOut) + (relIn : StmtIn → WitIn → Prop) (relOut : StmtOut → WitOut → Prop) + (E : StmtIn → Transcript s → WitOut → WitIn) (ε : ℝ≥0∞) : Prop := + ∀ x (P : ProbOracleComp oP (ProverStrategy (ProbOracleComp oP) s WitOut)), + (W.eval (V.execute x P)).toOuterMeasure + {r | (∃ x', r.2.1 = some x' ∧ relOut x' r.2.2) ∧ ¬ relIn x (E x r.1 r.2.2)} ≤ ε + +/-! ### Round-by-round soundness -/ + +/-- The prefixes of transcripts: `none` is the empty prefix of a nonempty protocol, and a protocol +without rounds has only its complete (empty) transcript. -/ +@[reducible] def Prefix : Spec → Type + | [] => Unit + | r :: s => Option (r.Message × Prefix s) + +/-- The empty prefix. -/ +def Prefix.empty : (s : Spec) → Prefix s + | [] => () + | _ :: _ => none + +/-- The total of per-round errors. -/ +def PerChallenge.sum : (s : Spec) → PerChallenge (fun _ => ℝ≥0∞) s → ℝ≥0∞ + | [], _ => 0 + | .prover _ _ :: s, ε => PerChallenge.sum s ε + | .verifier _ :: s, ε => ε.1 + PerChallenge.sum s ε.2 + +/-- The round-by-round condition on the rounds `s`, for the state function `S` on their prefixes +(false on doomed prefixes), per-round errors `ε` and the event `wins` on complete transcripts. A +prover message never leaves a doomed prefix; a challenge leaves one with probability at most its +error; and the verifier's output on a doomed complete transcript never wins. -/ +def RbrFrom : (s : Spec) → PerChallenge ProbComp s → PerChallenge (fun _ => ℝ≥0∞) s → + (Prefix s → Prop) → (Transcript s → Prop) → Prop + | [], _, _, S, wins => ¬ S () → ¬ wins () + | .prover M _ :: s, smp, ε, S, wins => + (¬ S none → ∀ m : M, ¬ S (some (m, Prefix.empty s))) ∧ + ∀ m : M, RbrFrom s smp ε (fun p => S (some (m, p))) (fun τ => wins (m, τ)) + | .verifier C :: s, smp, ε, S, wins => + (¬ S none → + (ProbComp.eval smp.1).toOuterMeasure {c : C | S (some (c, Prefix.empty s))} ≤ ε.1) ∧ + ∀ c : C, RbrFrom s smp.2 ε.2 (fun p => S (some (c, p))) (fun τ => wins (c, τ)) + +/-- The output of a verifier without oracles on a complete transcript. -/ +noncomputable def Verifier.outputOn (V : Verifier emptySpec s StmtIn StmtOut) (x : StmtIn) + (τ : Transcript s) : Option StmtOut := + OracleComp.interpret (m := Id) + (fun q => match q with + | .inl e => e.elim + | .inr q => Transcript.answer s τ q) + (V.decide x (Transcript.challenges s τ)) + +/-- Round-by-round soundness in the plain model with per-round errors `ε`: some state function is +false on the empty prefix of every `x ∉ langIn` and satisfies the round-by-round condition. -/ +def Verifier.RbrSound (V : Verifier emptySpec s StmtIn StmtOut) (langIn : Set StmtIn) + (langOut : Set StmtOut) (ε : PerChallenge (fun _ => ℝ≥0∞) s) : Prop := + ∃ S : StmtIn → Prefix s → Prop, (∀ x ∉ langIn, ¬ S x (Prefix.empty s)) ∧ + ∀ x, RbrFrom s V.samplers ε (S x) fun τ => ∃ x' ∈ langOut, V.outputOn x τ = some x' + +/-! ### Zero knowledge -/ + +/-- Honest-verifier zero knowledge with statistical error `ε` (perfect for `ε = 0`): on every +`(x, w)` in `relIn`, the simulator's transcript law is `ε`-close to the honest one. -/ +def Reduction.HVZK (W : World oP oV) (R : Reduction oP oV s StmtIn WitIn StmtOut WitOut) + (relIn : StmtIn → WitIn → Prop) (Sim : StmtIn → ProbComp (Transcript s)) (ε : ℝ≥0∞) : + Prop := + ∀ x w, relIn x w → CloseTo ((W.eval (R.run x w)).map Prod.fst) (ProbComp.eval (Sim x)) ε + +end Cslib.Interactive diff --git a/Complexity/Computability/Interactive/Sequential.lean b/Complexity/Computability/Interactive/Sequential.lean new file mode 100644 index 0000000000..2fb9002204 --- /dev/null +++ b/Complexity/Computability/Interactive/Sequential.lean @@ -0,0 +1,814 @@ +/- +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.Computability.Interactive.Plain + +/-! +# Sequential composition of interactive reductions + +`Reduction.append` runs a reduction from `rel₁` to `rel₂` and then one from `rel₂` to `rel₃`; its +rounds are the concatenation `s₁ ++ s₂`. Every construction is by structural recursion on `s₁`, +so for a concrete protocol the transcripts, challenges and message queries of the composition +compute to those of the components without casts. + +The composition theorems are stated in the plain model, where every security notion holds from +every state of the (trivial) world; in oracle models one composes interactive protocols first and +compiles them once (Fiat–Shamir, BCS). All errors add up. Straight-line knowledge soundness +composes with the named extractor `Verifier.extractAppend`. Its default intermediate statement is +used only when the first verifier rejects; without one, the composed extractor need not exist +when the intermediate statement type is empty. + +## Main definitions + +* `Interactive.Reduction.append`, `Interactive.Verifier.append`, `Interactive.Reduction.iterate`. +* `Interactive.ProverStrategy.append`, `Interactive.ProverStrategy.split`, + `Interactive.ProverStrategy.bindLeaf`. +* `Interactive.Verifier.extractAppend`. + +## Main results + +* `Interactive.Reduction.Complete.append`, `Interactive.Verifier.Sound.append`, + `Interactive.Verifier.KnowledgeSound.append`, `Interactive.Verifier.RbrSound.append`. +* `Interactive.Reduction.Complete.iterate`, `Interactive.Verifier.RbrSound.iterate`. +* `Interactive.plainLaw_run_append`, `Interactive.plainLaw_run_split`: execution laws of composed + and split strategies. +-/ + +@[expose] public section + +namespace Cslib.Interactive + +open scoped ENNReal +open Spec + +namespace Spec + +variable {F : Type → Type} + +/-- Concatenate transcripts. -/ +def Transcript.append : (s₁ s₂ : Spec) → Transcript s₁ → Transcript s₂ → Transcript (s₁ ++ s₂) + | [], _, _, τ₂ => τ₂ + | _ :: s₁, s₂, τ₁, τ₂ => (τ₁.1, Transcript.append s₁ s₂ τ₁.2 τ₂) + +/-- Split a transcript of a composition. -/ +def Transcript.split : (s₁ s₂ : Spec) → Transcript (s₁ ++ s₂) → Transcript s₁ × Transcript s₂ + | [], _, τ => ((), τ) + | _ :: s₁, s₂, τ => ((τ.1, (Transcript.split s₁ s₂ τ.2).1), (Transcript.split s₁ s₂ τ.2).2) + +/-- Concatenate per-challenge data. -/ +def PerChallenge.append : (s₁ s₂ : Spec) → PerChallenge F s₁ → PerChallenge F s₂ → + PerChallenge F (s₁ ++ s₂) + | [], _, _, b => b + | .prover _ _ :: s₁, s₂, a, b => PerChallenge.append s₁ s₂ a b + | .verifier _ :: s₁, s₂, a, b => (a.1, PerChallenge.append s₁ s₂ a.2 b) + +/-- Split per-challenge data of a composition. -/ +def PerChallenge.split : (s₁ s₂ : Spec) → PerChallenge F (s₁ ++ s₂) → + PerChallenge F s₁ × PerChallenge F s₂ + | [], _, b => ((), b) + | .prover _ _ :: s₁, s₂, a => PerChallenge.split s₁ s₂ a + | .verifier _ :: s₁, s₂, a => + ((a.1, (PerChallenge.split s₁ s₂ a.2).1), (PerChallenge.split s₁ s₂ a.2).2) + +/-- Queries about the messages of `s₁` are queries about those of `s₁ ++ s₂`. -/ +def liftMsgLeft : (s₁ s₂ : Spec) → (q : MsgQuery s₁) → + OracleComp (msgSpec (s₁ ++ s₂)) (MsgResponse s₁ q) + | [], _, q => q.elim + | .prover M I :: s₁, s₂, .inl q => + OracleComp.query (spec := msgSpec (.prover M I :: (s₁ ++ s₂))) (.inl q) + | .prover M I :: s₁, s₂, .inr q => + OracleComp.interpret + (fun q' => OracleComp.query (spec := msgSpec (.prover M I :: (s₁ ++ s₂))) (.inr q')) + (liftMsgLeft s₁ s₂ q) + | .verifier C :: s₁, s₂, q => + OracleComp.interpret + (fun q' => OracleComp.query (spec := msgSpec (.verifier C :: (s₁ ++ s₂))) q') + (liftMsgLeft s₁ s₂ q) + +/-- Queries about the messages of `s₂` are queries about those of `s₁ ++ s₂`. -/ +def liftMsgRight : (s₁ s₂ : Spec) → (q : MsgQuery s₂) → + OracleComp (msgSpec (s₁ ++ s₂)) (MsgResponse s₂ q) + | [], s₂, q => OracleComp.query (spec := msgSpec s₂) q + | .prover M I :: s₁, s₂, q => + OracleComp.interpret + (fun q' => OracleComp.query (spec := msgSpec (.prover M I :: (s₁ ++ s₂))) (.inr q')) + (liftMsgRight s₁ s₂ q) + | .verifier C :: s₁, s₂, q => + OracleComp.interpret + (fun q' => OracleComp.query (spec := msgSpec (.verifier C :: (s₁ ++ s₂))) q') + (liftMsgRight s₁ s₂ q) + +end Spec + +/-- Continue a strategy with another one once it ends. -/ +def ProverStrategy.append {m : Type → Type} [Monad m] {α β : Type} : + (s₁ s₂ : Spec) → ProverStrategy m s₁ α → (α → m (ProverStrategy m s₂ β)) → + m (ProverStrategy m (s₁ ++ s₂) β) + | [], _, a, next => next a + | .prover M _ :: s₁, s₂, st, next => + let st : m (M × ProverStrategy m s₁ α) := st + pure (show m (M × ProverStrategy m (s₁ ++ s₂) β) from do + let (msg, st') ← st + let rest ← ProverStrategy.append s₁ s₂ st' next + return (msg, rest)) + | .verifier C :: s₁, s₂, st, next => + let st : C → m (ProverStrategy m s₁ α) := st + pure (show C → m (ProverStrategy m (s₁ ++ s₂) β) from fun c => do + let st' ← st c + ProverStrategy.append s₁ s₂ st' next) + +variable {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s₁ s₂ : Spec} + {S₁ W₁ S₂ W₂ S₃ W₃ : Type} + +/-- Lift a decision on `s₁` to the composition. -/ +def liftDecisionLeft {α : Type} (s₁ s₂ : Spec) : + OracleComp (oV ⊕ₒ msgSpec s₁) α → OracleComp (oV ⊕ₒ msgSpec (s₁ ++ s₂)) α := + OracleComp.interpret fun q => match q with + | .inl q => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inl q) + | .inr q => OracleComp.interpret + (fun q' => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inr q')) + (liftMsgLeft s₁ s₂ q) + +/-- Lift a decision on `s₂` to the composition. -/ +def liftDecisionRight {α : Type} (s₁ s₂ : Spec) : + OracleComp (oV ⊕ₒ msgSpec s₂) α → OracleComp (oV ⊕ₒ msgSpec (s₁ ++ s₂)) α := + OracleComp.interpret fun q => match q with + | .inl q => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inl q) + | .inr q => OracleComp.interpret + (fun q' => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inr q')) + (liftMsgRight s₁ s₂ q) + +/-- Sequential composition of verifiers: the second decides on the first one's output. -/ +def Verifier.append (V₁ : Verifier oV s₁ S₁ S₂) (V₂ : Verifier oV s₂ S₂ S₃) : + Verifier oV (s₁ ++ s₂) S₁ S₃ where + samplers := PerChallenge.append s₁ s₂ V₁.samplers V₂.samplers + decide x c := do + let cs := PerChallenge.split s₁ s₂ c + match ← liftDecisionLeft s₁ s₂ (V₁.decide x cs.1) with + | none => return none + | some x' => liftDecisionRight s₁ s₂ (V₂.decide x' cs.2) + +/-- Sequential composition of reductions. -/ +def Reduction.append (R₁ : Reduction oP oV s₁ S₁ W₁ S₂ W₂) + (R₂ : Reduction oP oV s₂ S₂ W₂ S₃ W₃) : Reduction oP oV (s₁ ++ s₂) S₁ W₁ S₃ W₃ where + prover x w := do + let st ← R₁.prover x w + ProverStrategy.append s₁ s₂ st fun xw => R₂.prover xw.1 xw.2 + verifier := R₁.verifier.append R₂.verifier + +/-! ### Round-by-round composition (proved) -/ + +section Rbr + +/-- The challenges of a composed transcript split into those of its halves. -/ +private theorem challenges_split : ∀ (s₁ s₂ : Spec) (τ : Transcript (s₁ ++ s₂)), + PerChallenge.split s₁ s₂ (Transcript.challenges (s₁ ++ s₂) τ) = + (Transcript.challenges s₁ (Transcript.split s₁ s₂ τ).1, + Transcript.challenges s₂ (Transcript.split s₁ s₂ τ).2) + | [], _, _ => rfl + | .prover _ _ :: s₁, s₂, τ => challenges_split s₁ s₂ τ.2 + | .verifier _ :: s₁, s₂, τ => by + change ((τ.1, (PerChallenge.split s₁ s₂ (Transcript.challenges (s₁ ++ s₂) τ.2)).1), + (PerChallenge.split s₁ s₂ (Transcript.challenges (s₁ ++ s₂) τ.2)).2) = _ + rw [challenges_split s₁ s₂ τ.2] + rfl + +/-- Lifted message queries of the first half are answered by the first half of the transcript. -/ +private theorem interpret_liftMsgLeft : ∀ (s₁ s₂ : Spec) (τ : Transcript (s₁ ++ s₂)) + (q : MsgQuery s₁), + OracleComp.interpret (m := Id) (Transcript.answer (s₁ ++ s₂) τ) (liftMsgLeft s₁ s₂ q) = + Transcript.answer s₁ (Transcript.split s₁ s₂ τ).1 q + | [], _, _, q => q.elim + | .prover M I :: s₁, s₂, τ, .inl q => rfl + | .prover M I :: s₁, s₂, τ, .inr q => by + rw [liftMsgLeft, OracleComp.interpret_interpret] + exact interpret_liftMsgLeft s₁ s₂ τ.2 q + | .verifier C :: s₁, s₂, τ, q => by + rw [liftMsgLeft, OracleComp.interpret_interpret] + exact interpret_liftMsgLeft s₁ s₂ τ.2 q + +/-- Lifted message queries of the second half are answered by the second half of the transcript. -/ +private theorem interpret_liftMsgRight : ∀ (s₁ s₂ : Spec) (τ : Transcript (s₁ ++ s₂)) + (q : MsgQuery s₂), + OracleComp.interpret (m := Id) (Transcript.answer (s₁ ++ s₂) τ) (liftMsgRight s₁ s₂ q) = + Transcript.answer s₂ (Transcript.split s₁ s₂ τ).2 q + | [], _, _, q => rfl + | .prover M I :: s₁, s₂, τ, q => by + rw [liftMsgRight, OracleComp.interpret_interpret] + exact interpret_liftMsgRight s₁ s₂ τ.2 q + | .verifier C :: s₁, s₂, τ, q => by + rw [liftMsgRight, OracleComp.interpret_interpret] + exact interpret_liftMsgRight s₁ s₂ τ.2 q + + + +/-- The answers to the verifier's queries from a transcript, in the plain model. -/ +private def answerAll (s : Spec) (τ : Transcript s) : + (q : Empty ⊕ MsgQuery s) → (emptySpec ⊕ₒ msgSpec s) q + | .inl e => e.elim + | .inr q => Transcript.answer s τ q + +private theorem outputOn_eq (V : Verifier emptySpec s₁ S₁ S₂) (x : S₁) (τ : Transcript s₁) : + V.outputOn x τ = OracleComp.interpret (m := Id) (answerAll s₁ τ) + (V.decide x (Transcript.challenges s₁ τ)) := by + rw [Verifier.outputOn] + congr 1 + +private theorem interpret_liftDecisionLeft {α : Type} (τ : Transcript (s₁ ++ s₂)) + (p : OracleComp (emptySpec ⊕ₒ msgSpec s₁) α) : + OracleComp.interpret (m := Id) (answerAll (s₁ ++ s₂) τ) (liftDecisionLeft s₁ s₂ p) = + OracleComp.interpret (m := Id) (answerAll s₁ (Transcript.split s₁ s₂ τ).1) p := by + rw [liftDecisionLeft] + refine (OracleComp.interpret_interpret (m := Id) _ _ _).trans ?_ + congr 1 + funext q + rcases q with e | q + · exact e.elim + · refine (OracleComp.interpret_interpret (m := Id) _ _ _).trans ?_ + exact interpret_liftMsgLeft s₁ s₂ τ q + +private theorem interpret_liftDecisionRight {α : Type} (τ : Transcript (s₁ ++ s₂)) + (p : OracleComp (emptySpec ⊕ₒ msgSpec s₂) α) : + OracleComp.interpret (m := Id) (answerAll (s₁ ++ s₂) τ) (liftDecisionRight s₁ s₂ p) = + OracleComp.interpret (m := Id) (answerAll s₂ (Transcript.split s₁ s₂ τ).2) p := by + rw [liftDecisionRight] + refine (OracleComp.interpret_interpret (m := Id) _ _ _).trans ?_ + congr 1 + funext q + rcases q with e | q + · exact e.elim + · refine (OracleComp.interpret_interpret (m := Id) _ _ _).trans ?_ + exact interpret_liftMsgRight s₁ s₂ τ q + +/-- The composed verifier's output is the second verifier's output on the first one's. -/ +theorem outputOn_append (V₁ : Verifier emptySpec s₁ S₁ S₂) (V₂ : Verifier emptySpec s₂ S₂ S₃) + (x : S₁) (τ : Transcript (s₁ ++ s₂)) : + (V₁.append V₂).outputOn x τ = + (V₁.outputOn x (Transcript.split s₁ s₂ τ).1).bind + fun x' => V₂.outputOn x' (Transcript.split s₁ s₂ τ).2 := by + rw [outputOn_eq, outputOn_eq] + simp only [Verifier.append, challenges_split] + refine (OracleComp.interpret_bind (m := Id) _ _ _).trans ?_ + erw [interpret_liftDecisionLeft] + cases h : OracleComp.interpret (m := Id) (answerAll s₁ (Transcript.split s₁ s₂ τ).1) + (V₁.decide x (Transcript.challenges s₁ (Transcript.split s₁ s₂ τ).1)) with + | none => rfl + | some x' => + refine (interpret_liftDecisionRight τ _).trans ?_ + exact (outputOn_eq V₂ x' _).symm + + +/-- The state function of a composition: that of the first half, then, once the first half is +complete, the second half's state function for that first half. -/ +private def compState : + (s₁ s₂ : Spec) → (Prefix s₁ → Prop) → (Transcript s₁ → Prefix s₂ → Prop) → + Prefix (s₁ ++ s₂) → Prop + | [], _, _, next, p => next () p + | _ :: _, _, S, _, none => S none + | _ :: s₁, s₂, S, next, some (m, p) => + compState s₁ s₂ (fun q => S (some (m, q))) (fun τ => next (m, τ)) p + +/-- A doomed start of the first half is a doomed start of the composition. -/ +private theorem not_compState_empty {s₁ s₂ : Spec} {smp : PerChallenge ProbComp s₁} + {ε : PerChallenge (fun _ => ℝ≥0∞) s₁} {S : Prefix s₁ → Prop} {wins : Transcript s₁ → Prop} + {next : Transcript s₁ → Prefix s₂ → Prop} (h : RbrFrom s₁ smp ε S wins) + (hjunc : ∀ τ, ¬ wins τ → ¬ next τ (Prefix.empty s₂)) (hS : ¬ S (Prefix.empty s₁)) : + ¬ compState s₁ s₂ S next (Prefix.empty (s₁ ++ s₂)) := by + cases s₁ with + | nil => exact hjunc () (h hS) + | cons r s₁ => exact hS + +/-- The round-by-round condition holds trivially when nothing is ever alive. -/ +private theorem rbrFrom_false : ∀ (s : Spec) (smp : PerChallenge ProbComp s) + (ε : PerChallenge (fun _ => ℝ≥0∞) s), RbrFrom s smp ε (fun _ => False) (fun _ => False) + | [], _, _ => fun _ h => h + | .prover _ _ :: s, smp, ε => ⟨fun _ _ h => h, fun _ => rbrFrom_false s smp ε⟩ + | .verifier _ :: s, smp, ε => ⟨fun _ => by simp, fun _ => rbrFrom_false s smp.2 ε.2⟩ + +/-- The round-by-round condition is invariant under equivalent state functions and events. -/ +theorem RbrFrom.congr : ∀ {s : Spec} {smp : PerChallenge ProbComp s} + {ε : PerChallenge (fun _ => ℝ≥0∞) s} {S S' : Prefix s → Prop} + {wins wins' : Transcript s → Prop}, + (∀ p, S p ↔ S' p) → (∀ τ, wins τ ↔ wins' τ) → RbrFrom s smp ε S wins → + RbrFrom s smp ε S' wins' + | [], _, _, _, _, _, _, hS, hw, h => fun h' hw' => h (mt (hS ()).1 h') ((hw ()).2 hw') + | .prover _ _ :: s, _, _, _, _, _, _, hS, hw, h => + ⟨fun h0 m h1 => h.1 (mt (hS none).1 h0) m ((hS _).2 h1), + fun m => RbrFrom.congr (fun p => hS _) (fun τ => hw _) (h.2 m)⟩ + | .verifier _ :: s, smp, _, S, S', _, _, hS, hw, h => + ⟨fun h0 => by + have hset : {c | S' (some (c, Prefix.empty s))} = {c | S (some (c, Prefix.empty s))} := + Set.ext fun c => (hS _).symm + rw [hset] + exact h.1 (mt (hS none).1 h0), + fun c => RbrFrom.congr (fun p => hS _) (fun τ => hw _) (h.2 c)⟩ + +/-- **Round-by-round composition, per prefix.** -/ +private theorem rbrFrom_append : ∀ (s₁ s₂ : Spec) (smp₁ : PerChallenge ProbComp s₁) + (smp₂ : PerChallenge ProbComp s₂) (ε₁ : PerChallenge (fun _ => ℝ≥0∞) s₁) + (ε₂ : PerChallenge (fun _ => ℝ≥0∞) s₂) (S : Prefix s₁ → Prop) (wins₁ : Transcript s₁ → Prop) + (next : Transcript s₁ → Prefix s₂ → Prop) (wins₂ : Transcript s₁ → Transcript s₂ → Prop), + RbrFrom s₁ smp₁ ε₁ S wins₁ → (∀ τ, ¬ wins₁ τ → ¬ next τ (Prefix.empty s₂)) → + (∀ τ, RbrFrom s₂ smp₂ ε₂ (next τ) (wins₂ τ)) → + RbrFrom (s₁ ++ s₂) (PerChallenge.append s₁ s₂ smp₁ smp₂) (PerChallenge.append s₁ s₂ ε₁ ε₂) + (compState s₁ s₂ S next) + (fun τ => wins₂ (Transcript.split s₁ s₂ τ).1 (Transcript.split s₁ s₂ τ).2) + | [], _, _, _, _, _, _, _, _, _, _, _, h₂ => h₂ () + | .prover M I :: s₁, s₂, smp₁, smp₂, ε₁, ε₂, S, wins₁, next, wins₂, h₁, hjunc, h₂ => + ⟨fun h0 m => not_compState_empty (h₁.2 m) (fun τ => hjunc (m, τ)) (h₁.1 h0 m), + fun m => rbrFrom_append s₁ s₂ smp₁ smp₂ ε₁ ε₂ _ _ (fun τ => next (m, τ)) + (fun τ => wins₂ (m, τ)) (h₁.2 m) (fun τ => hjunc (m, τ)) (fun τ => h₂ (m, τ))⟩ + | .verifier C :: s₁, s₂, smp₁, smp₂, ε₁, ε₂, S, wins₁, next, wins₂, h₁, hjunc, h₂ => + ⟨fun h0 => by + refine le_trans (MeasureTheory.measure_mono fun c hc => ?_) (h₁.1 h0) + by_contra hS + exact not_compState_empty (h₁.2 c) (fun τ => hjunc (c, τ)) hS hc, + fun c => rbrFrom_append s₁ s₂ smp₁.2 smp₂ ε₁.2 ε₂ _ _ (fun τ => next (c, τ)) + (fun τ => wins₂ (c, τ)) (h₁.2 c) (fun τ => hjunc (c, τ)) (fun τ => h₂ (c, τ))⟩ + + +/-- **Round-by-round soundness composes**, with the concatenated per-round errors. -/ +theorem Verifier.RbrSound.append {V₁ : Verifier emptySpec s₁ S₁ S₂} + {V₂ : Verifier emptySpec s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} + {ε₁ : PerChallenge (fun _ => ℝ≥0∞) s₁} {ε₂ : PerChallenge (fun _ => ℝ≥0∞) s₂} + (h₁ : V₁.RbrSound L₁ L₂ ε₁) (h₂ : V₂.RbrSound L₂ L₃ ε₂) : + (V₁.append V₂).RbrSound L₁ L₃ (PerChallenge.append s₁ s₂ ε₁ ε₂) := by + obtain ⟨T₁, hinit₁, hr₁⟩ := h₁ + obtain ⟨T₂, hinit₂, hr₂⟩ := h₂ + let next : S₁ → Transcript s₁ → Prefix s₂ → Prop := + fun x τ₁ p => ∃ x', V₁.outputOn x τ₁ = some x' ∧ T₂ x' p + have hjunc : ∀ x τ₁, ¬ (∃ x' ∈ L₂, V₁.outputOn x τ₁ = some x') → + ¬ next x τ₁ (Prefix.empty s₂) := by + rintro x τ₁ hw ⟨x', hout, hT⟩ + by_cases hx' : x' ∈ L₂ + · exact hw ⟨x', hx', hout⟩ + · exact hinit₂ x' hx' hT + have hsecond : ∀ x τ₁, RbrFrom s₂ V₂.samplers ε₂ (next x τ₁) + (fun τ₂ => ∃ x'' ∈ L₃, (V₁.outputOn x τ₁).bind (fun x' => V₂.outputOn x' τ₂) = some x'') := by + intro x τ₁ + cases hout : V₁.outputOn x τ₁ with + | none => + refine RbrFrom.congr (fun p => ?_) (fun τ => ?_) (rbrFrom_false s₂ V₂.samplers ε₂) + · simp [next, hout] + · simp + | some x' => + refine RbrFrom.congr (fun p => ?_) (fun τ => ?_) (hr₂ x') + · simp [next, hout] + · simp + refine ⟨fun x => compState s₁ s₂ (T₁ x) (next x), + fun x hx => not_compState_empty (hr₁ x) (hjunc x) (hinit₁ x hx), fun x => ?_⟩ + refine RbrFrom.congr (fun p => Iff.rfl) (fun τ => ?_) + (rbrFrom_append s₁ s₂ V₁.samplers V₂.samplers ε₁ ε₂ (T₁ x) _ (next x) _ (hr₁ x) (hjunc x) + (hsecond x)) + rw [outputOn_append] + +end Rbr + +/-! ### Composition of completeness, soundness and knowledge soundness -/ + +section Plain + +variable {R₁ : Reduction emptySpec emptySpec s₁ S₁ W₁ S₂ W₂} + {R₂ : Reduction emptySpec emptySpec s₂ S₂ W₂ S₃ W₃} + {V₁ : Verifier emptySpec s₁ S₁ S₂} {V₂ : Verifier emptySpec s₂ S₂ S₃} + {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} + {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} {ε₁ ε₂ : ℝ≥0∞} + +/-- The composed straight-line extractor: extract the intermediate witness from the second half of +the transcript, at the statement the first verifier outputs, then the input witness from the first +half. The default intermediate statement `y₀` is used only when the first verifier rejects, when +the composed verifier rejects too. -/ +noncomputable def Verifier.extractAppend (V₁ : Verifier emptySpec s₁ S₁ S₂) + (E₁ : S₁ → Transcript s₁ → W₂ → W₁) (E₂ : S₂ → Transcript s₂ → W₃ → W₂) (y₀ : S₂) : + S₁ → Transcript (s₁ ++ s₂) → W₃ → W₁ := fun x τ w₃ => + E₁ x (Transcript.split s₁ s₂ τ).1 + (E₂ ((V₁.outputOn x (Transcript.split s₁ s₂ τ).1).getD y₀) (Transcript.split s₁ s₂ τ).2 w₃) + +/-- The total error of concatenated per-round errors. -/ +theorem PerChallenge.sum_append (ε₁ : PerChallenge (fun _ => ℝ≥0∞) s₁) + (ε₂ : PerChallenge (fun _ => ℝ≥0∞) s₂) : + PerChallenge.sum (s₁ ++ s₂) (PerChallenge.append s₁ s₂ ε₁ ε₂) = + PerChallenge.sum s₁ ε₁ + PerChallenge.sum s₂ ε₂ := by + induction s₁ with + | nil => simp [PerChallenge.append, PerChallenge.sum] + | cons r s₁ ih => + cases r with + | prover M I => exact ih ε₁ + | verifier C => + change ε₁.1 + PerChallenge.sum (s₁ ++ s₂) (PerChallenge.append s₁ s₂ ε₁.2 ε₂) = _ + rw [ih, PerChallenge.sum, add_assoc] + +end Plain + +/-- Continue a strategy with an effect at its end that sees the transcript. -/ +def ProverStrategy.bindLeaf {m : Type → Type} [Monad m] {α β : Type} : + (s : Spec) → ProverStrategy m s α → (Transcript s → α → m β) → m (ProverStrategy m s β) + | [], a, f => f () a + | .prover M _ :: s, st, f => + let st : m (M × ProverStrategy m s α) := st + pure (show m (M × ProverStrategy m s β) from do + let (msg, st') ← st + let rest ← ProverStrategy.bindLeaf s st' fun τ a => f (msg, τ) a + return (msg, rest)) + | .verifier C :: s, st, f => + let st : C → m (ProverStrategy m s α) := st + pure (show C → m (ProverStrategy m s β) from fun c => do + let st' ← st c + ProverStrategy.bindLeaf s st' fun τ a => f (c, τ) a) + +/-- Running a strategy continued by an effect at its end: the effect sees the transcript. -/ +theorem plainLaw_bindLeaf_run : ∀ (s : Spec) (smp : PerChallenge ProbComp s) {α β : Type} + (st : ProverStrategy (ProbOracleComp emptySpec) s α) + (f : Transcript s → α → ProbOracleComp emptySpec β), + plainLaw (ProverStrategy.bindLeaf s st f >>= runStrategy s smp) = + (plainLaw (runStrategy s smp st)).bind fun r => (plainLaw (f r.1 r.2)).map fun b => (r.1, b) + | [], _, _, _, a, f => by + simp [ProverStrategy.bindLeaf, runStrategy] + | .prover M I :: s, smp, _, _, st, f => by + simp only [ProverStrategy.bindLeaf, runStrategy, plainLaw_bind, plainLaw_pure, PMF.pure_bind, + PMF.bind_bind] + congr 1 + funext a + have ih := plainLaw_bindLeaf_run s smp a.2 (fun τ b => f (a.1, τ) b) + rw [plainLaw_bind] at ih + rw [← PMF.bind_bind, ih, PMF.bind_bind] + congr 1 + funext r + rw [PMF.bind_map] + rfl + | .verifier C :: s, smp, _, _, st, f => by + simp only [ProverStrategy.bindLeaf, runStrategy, plainLaw_bind, plainLaw_pure, plainLaw_sample, + PMF.pure_bind, PMF.bind_bind] + congr 1 + funext c + congr 1 + funext st' + have ih := plainLaw_bindLeaf_run s smp.2 st' (fun τ b => f (c, τ) b) + rw [plainLaw_bind] at ih + rw [← PMF.bind_bind, ih, PMF.bind_bind] + congr 1 + funext r + rw [PMF.bind_map] + rfl + + +/-- Split a strategy for `s₁ ++ s₂` into a strategy for `s₁` ending with one for `s₂`. -/ +def ProverStrategy.split {m : Type → Type} [Monad m] {α : Type} : + (s₁ s₂ : Spec) → ProverStrategy m (s₁ ++ s₂) α → ProverStrategy m s₁ (ProverStrategy m s₂ α) + | [], _, st => st + | .prover M _ :: s₁, s₂, st => + let st : m (M × ProverStrategy m (s₁ ++ s₂) α) := st + show m (M × ProverStrategy m s₁ (ProverStrategy m s₂ α)) from + (fun p => (p.1, ProverStrategy.split s₁ s₂ p.2)) <$> st + | .verifier C :: s₁, s₂, st => + let st : C → m (ProverStrategy m (s₁ ++ s₂) α) := st + show C → m (ProverStrategy m s₁ (ProverStrategy m s₂ α)) from + fun c => ProverStrategy.split s₁ s₂ <$> st c + +/-- Running a composed strategy runs the first part, then the continuation on its result. -/ +theorem plainLaw_run_append : ∀ (s₁ s₂ : Spec) (smp₁ : PerChallenge ProbComp s₁) + (smp₂ : PerChallenge ProbComp s₂) {α β : Type} + (st : ProverStrategy (ProbOracleComp emptySpec) s₁ α) + (next : α → ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s₂ β)), + plainLaw (ProverStrategy.append s₁ s₂ st next >>= + runStrategy (s₁ ++ s₂) (PerChallenge.append s₁ s₂ smp₁ smp₂)) = + (plainLaw (runStrategy s₁ smp₁ st)).bind fun r₁ => + (plainLaw (next r₁.2 >>= runStrategy s₂ smp₂)).map + fun r₂ => (Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2) + | [], s₂, _, smp₂, _, _, a, next => by + simp only [ProverStrategy.append, runStrategy, plainLaw_pure, PMF.pure_bind, + PerChallenge.append, Transcript.append] + exact (PMF.map_id _).symm + | .prover M I :: s₁, s₂, smp₁, smp₂, _, _, st, next => by + simp only [ProverStrategy.append, List.cons_append, runStrategy, plainLaw_bind, plainLaw_pure, + PMF.pure_bind, PMF.bind_bind, PerChallenge.append] + congr 1 + funext a + have ih := plainLaw_run_append s₁ s₂ smp₁ smp₂ a.2 next + rw [plainLaw_bind] at ih + rw [← PMF.bind_bind, ih, PMF.bind_bind] + congr 1 + funext r + rw [PMF.bind_map, plainLaw_bind] + rfl + | .verifier C :: s₁, s₂, smp₁, smp₂, _, _, st, next => by + simp only [ProverStrategy.append, List.cons_append, runStrategy, plainLaw_bind, plainLaw_pure, + plainLaw_sample, PMF.pure_bind, PMF.bind_bind, PerChallenge.append] + congr 1 + funext c + congr 1 + funext st' + have ih := plainLaw_run_append s₁ s₂ smp₁.2 smp₂ st' next + rw [plainLaw_bind] at ih + rw [← PMF.bind_bind, ih, PMF.bind_bind] + congr 1 + funext r + rw [PMF.bind_map, plainLaw_bind] + rfl + +/-- Running any strategy for `s₁ ++ s₂` runs its split: the first part, then the rest. -/ +theorem plainLaw_run_split : ∀ (s₁ s₂ : Spec) (smp₁ : PerChallenge ProbComp s₁) + (smp₂ : PerChallenge ProbComp s₂) {α : Type} + (st : ProverStrategy (ProbOracleComp emptySpec) (s₁ ++ s₂) α), + plainLaw (runStrategy (s₁ ++ s₂) (PerChallenge.append s₁ s₂ smp₁ smp₂) st) = + (plainLaw (runStrategy s₁ smp₁ (ProverStrategy.split s₁ s₂ st))).bind fun r₁ => + (plainLaw (runStrategy s₂ smp₂ r₁.2)).map + fun r₂ => (Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2) + | [], s₂, _, smp₂, _, st => by + simp only [ProverStrategy.split, runStrategy, plainLaw_pure, PMF.pure_bind, PerChallenge.append, + Transcript.append] + exact (PMF.map_id _).symm + | .prover M I :: s₁, s₂, smp₁, smp₂, _, st => by + simp only [ProverStrategy.split, List.cons_append, runStrategy, plainLaw_bind, plainLaw_pure, + plainLaw_map, PMF.pure_bind, PMF.bind_bind, PMF.bind_map, PerChallenge.append, + Function.comp_apply] + congr 1 + funext a + rw [plainLaw_run_split s₁ s₂ smp₁ smp₂ a.2, PMF.bind_bind] + congr 1 + funext r + rw [PMF.bind_map] + rfl + | .verifier C :: s₁, s₂, smp₁, smp₂, _, st => by + simp only [ProverStrategy.split, List.cons_append, runStrategy, plainLaw_bind, plainLaw_pure, + plainLaw_map, plainLaw_sample, PMF.pure_bind, PMF.bind_bind, PMF.bind_map, + PerChallenge.append, Function.comp_apply] + congr 1 + funext c + congr 1 + funext st' + rw [plainLaw_run_split s₁ s₂ smp₁.2 smp₂ st', PMF.bind_bind] + congr 1 + funext r + rw [PMF.bind_map] + rfl + + +/-- Splitting a concatenated transcript recovers its halves. -/ +theorem Spec.Transcript.split_append : ∀ (s₁ s₂ : Spec) (τ₁ : Transcript s₁) + (τ₂ : Transcript s₂), Transcript.split s₁ s₂ (Transcript.append s₁ s₂ τ₁ τ₂) = (τ₁, τ₂) + | [], _, _, _ => rfl + | _ :: s₁, s₂, τ₁, τ₂ => by + simp only [Transcript.split, Transcript.append, Spec.Transcript.split_append s₁ s₂ τ₁.2 τ₂] + +private theorem toOuterMeasure_bind_le_add {α β : Type} (μ : PMF α) (f : α → PMF β) + (t : Set β) (A : Set α) {K : ℝ≥0∞} (h : ∀ a ∉ A, (f a).toOuterMeasure t ≤ K) : + (μ.bind f).toOuterMeasure t ≤ μ.toOuterMeasure A + K := by + simpa only [compl_compl] using + Probability.PMF.toOuterMeasure_bind_failure_le μ f Aᶜ t K fun a _ ha => h a ha + +private theorem toOuterMeasure_bind_le {α β : Type} (p : PMF α) (f : α → PMF β) (t : Set β) + {K : ℝ≥0∞} (h : ∀ a, (f a).toOuterMeasure t ≤ K) : (p.bind f).toOuterMeasure t ≤ K := by + rw [PMF.toOuterMeasure_bind_apply] + exact Probability.PMF.tsum_mul_le_of_forall_le _ h + +section Compose + +/-- The honest run of a composed reduction runs the first reduction, then the second on the +first prover's output. -/ +private theorem plainLaw_run_reductionAppend (R₁ : Reduction emptySpec emptySpec s₁ S₁ W₁ S₂ W₂) + (R₂ : Reduction emptySpec emptySpec s₂ S₂ W₂ S₃ W₃) (x : S₁) (w : W₁) : + plainLaw ((R₁.append R₂).prover x w >>= + runStrategy (s₁ ++ s₂) (R₁.append R₂).verifier.samplers) = + (plainLaw (R₁.prover x w >>= runStrategy s₁ R₁.verifier.samplers)).bind fun r₁ => + (plainLaw (R₂.prover r₁.2.1 r₁.2.2 >>= runStrategy s₂ R₂.verifier.samplers)).map + fun r₂ => (Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2) := by + simp only [Reduction.append, Verifier.append, bind_assoc, plainLaw_bind, PMF.bind_bind] + congr 1 + funext st + rw [← plainLaw_bind, plainLaw_run_append] + simp only [plainLaw_bind] + +/-- **Completeness errors add up under sequential composition.** -/ +theorem Reduction.Complete.append {R₁ : Reduction emptySpec emptySpec s₁ S₁ W₁ S₂ W₂} + {R₂ : Reduction emptySpec emptySpec s₂ S₂ W₂ S₃ W₃} + {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {ε₁ ε₂ : ℝ≥0∞} + (h₁ : R₁.Complete World.plain rel₁ rel₂ ε₁) (h₂ : R₂.Complete World.plain rel₂ rel₃ ε₂) : + (R₁.append R₂).Complete World.plain rel₁ rel₃ (ε₁ + ε₂) := by + intro x w hxw + have hl₁ := h₁ x w hxw + rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hl₁ ⊢ + rw [plainLaw_run_reductionAppend] + refine le_trans (toOuterMeasure_bind_le_add _ _ _ _ fun r₁ hr₁ => ?_) (add_le_add hl₁ le_rfl) + simp only [Set.mem_preimage, Set.mem_ofPred_eq, not_not] at hr₁ + obtain ⟨hout, hrel⟩ := hr₁ + have hl₂ := h₂ r₁.2.1 r₁.2.2 hrel + rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hl₂ + rw [PMF.toOuterMeasure_map_apply] + convert hl₂ using 2 + ext r₂ + simp [Reduction.append, outputOn_append, Spec.Transcript.split_append, hout] + + +/-- A run against a composed verifier is a run of the split strategy against the first, then +of its continuation against the second. -/ +private theorem plainLaw_run_verifierAppend (V₁ : Verifier emptySpec s₁ S₁ S₂) + (V₂ : Verifier emptySpec s₂ S₂ S₃) {α : Type} + (P : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) (s₁ ++ s₂) α)) : + plainLaw (P >>= runStrategy (s₁ ++ s₂) (V₁.append V₂).samplers) = + (plainLaw ((ProverStrategy.split s₁ s₂ ·) <$> P >>= runStrategy s₁ V₁.samplers)).bind + fun r₁ => (plainLaw (runStrategy s₂ V₂.samplers r₁.2)).map + fun r₂ => (Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2) := by + simp only [plainLaw_bind, plainLaw_map, PMF.bind_map, PMF.bind_bind] + congr 1 + funext st + exact plainLaw_run_split s₁ s₂ V₁.samplers V₂.samplers st + +/-- **Soundness errors add up under sequential composition**, through the intermediate +language. -/ +theorem Verifier.Sound.append {V₁ : Verifier emptySpec s₁ S₁ S₂} + {V₂ : Verifier emptySpec s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} + {ε₁ ε₂ : ℝ≥0∞} (h₁ : V₁.Sound (oP := emptySpec) World.plain L₁ L₂ ε₁) + (h₂ : V₂.Sound (oP := emptySpec) World.plain L₂ L₃ ε₂) : + (V₁.append V₂).Sound (oP := emptySpec) World.plain L₁ L₃ (ε₁ + ε₂) := by + intro x hx α P + have hl₁ := h₁ x hx _ ((ProverStrategy.split s₁ s₂ ·) <$> P) + rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hl₁ ⊢ + rw [plainLaw_run_verifierAppend] + refine le_trans (toOuterMeasure_bind_le_add _ _ _ _ fun r₁ hr₁ => ?_) (add_le_add hl₁ le_rfl) + simp only [Set.mem_preimage, Set.mem_ofPred_eq, not_exists, not_and] at hr₁ + rw [PMF.toOuterMeasure_map_apply] + cases hout : V₁.outputOn x r₁.1 with + | none => + have hset : (fun r₂ : Transcript s₂ × α => (Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2)) ⁻¹' + ((fun r : Transcript (s₁ ++ s₂) × α => (r.1, (V₁.append V₂).outputOn x r.1, r.2)) ⁻¹' + {r | ∃ x' ∈ L₃, r.2.1 = some x'}) = ∅ := by + ext r₂ + simp [outputOn_append, Spec.Transcript.split_append, hout] + rw [hset, MeasureTheory.measure_empty] + exact zero_le + | some y => + have hy : y ∉ L₂ := fun hy => hr₁ y hy hout + have hl₂ := h₂ y hy _ (pure r₁.2) + rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hl₂ + simp only [plainLaw_bind, plainLaw_pure, PMF.pure_bind] at hl₂ + convert hl₂ using 2 + ext r₂ + simp [outputOn_append, Spec.Transcript.split_append, hout] + + +/-- **Straight-line extractors compose**, with the sum of the knowledge errors. The first +verifier's knowledge soundness is applied to a prover that simulates the second phase with the +public samplers. -/ +theorem Verifier.KnowledgeSound.append {V₁ : Verifier emptySpec s₁ S₁ S₂} + {V₂ : Verifier emptySpec s₂ S₂ S₃} + {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {ε₁ ε₂ : ℝ≥0∞} + {E₁ : S₁ → Transcript s₁ → W₂ → W₁} {E₂ : S₂ → Transcript s₂ → W₃ → W₂} + (h₁ : V₁.KnowledgeSound (oP := emptySpec) World.plain rel₁ rel₂ E₁ ε₁) + (h₂ : V₂.KnowledgeSound (oP := emptySpec) World.plain rel₂ rel₃ E₂ ε₂) (y₀ : S₂) : + (V₁.append V₂).KnowledgeSound (oP := emptySpec) World.plain rel₁ rel₃ + (V₁.extractAppend E₁ E₂ y₀) (ε₁ + ε₂) := by + intro x P + rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply, plainLaw_run_verifierAppend] + let T₁ : Set (Transcript (s₁ ++ s₂) × W₃) := {r | ∃ y, + V₁.outputOn x (Transcript.split s₁ s₂ r.1).1 = some y ∧ + rel₂ y (E₂ y (Transcript.split s₁ s₂ r.1).2 r.2) ∧ + ¬ rel₁ x (E₁ x (Transcript.split s₁ s₂ r.1).1 (E₂ y (Transcript.split s₁ s₂ r.1).2 r.2))} + let T₂ : Set (Transcript (s₁ ++ s₂) × W₃) := {r | ∃ y, + V₁.outputOn x (Transcript.split s₁ s₂ r.1).1 = some y ∧ + (∃ x'', V₂.outputOn y (Transcript.split s₁ s₂ r.1).2 = some x'' ∧ rel₃ x'' r.2) ∧ + ¬ rel₂ y (E₂ y (Transcript.split s₁ s₂ r.1).2 r.2)} + have hsub : (fun r : Transcript (s₁ ++ s₂) × W₃ => (r.1, (V₁.append V₂).outputOn x r.1, r.2)) ⁻¹' + {r | (∃ x', r.2.1 = some x' ∧ rel₃ x' r.2.2) ∧ + ¬ rel₁ x (V₁.extractAppend E₁ E₂ y₀ x r.1 r.2.2)} ⊆ T₁ ∪ T₂ := by + rintro ⟨τ, w₃⟩ ⟨⟨x'', hout, hrel⟩, hnot⟩ + simp only [outputOn_append] at hout + obtain ⟨y, hy, hy₂⟩ := Option.bind_eq_some_iff.mp hout + by_cases h : rel₂ y (E₂ y (Transcript.split s₁ s₂ τ).2 w₃) + · left + refine ⟨y, hy, h, ?_⟩ + simpa [Verifier.extractAppend, hy] using hnot + · exact Or.inr ⟨y, hy, ⟨x'', hy₂, hrel⟩, h⟩ + refine le_trans (MeasureTheory.measure_mono hsub) + (le_trans (MeasureTheory.measure_union_le _ _) (add_le_add ?_ ?_)) + · let P₁ : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s₁ W₂) := + (ProverStrategy.split s₁ s₂ ·) <$> P >>= fun st₁ => ProverStrategy.bindLeaf s₁ st₁ + fun τ₁ st₂ => (fun r₂ => E₂ ((V₁.outputOn x τ₁).getD y₀) r₂.1 r₂.2) <$> + runStrategy s₂ V₂.samplers st₂ + have hl₁ := h₁ x P₁ + rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hl₁ + have hlaw₁ : plainLaw (P₁ >>= runStrategy s₁ V₁.samplers) = + (plainLaw ((ProverStrategy.split s₁ s₂ ·) <$> P >>= runStrategy s₁ V₁.samplers)).bind + fun r₁ => (plainLaw (runStrategy s₂ V₂.samplers r₁.2)).map + fun r₂ => (r₁.1, E₂ ((V₁.outputOn x r₁.1).getD y₀) r₂.1 r₂.2) := by + simp only [P₁, bind_assoc, plainLaw_bind, PMF.bind_bind] + congr 1 + funext st₁ + rw [← plainLaw_bind, plainLaw_bindLeaf_run] + congr 1 + funext r₁ + rw [plainLaw_map, PMF.map_comp] + rfl + rw [hlaw₁] at hl₁ + refine le_trans (le_of_eq ?_) hl₁ + rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_bind_apply] + refine tsum_congr fun r₁ => ?_ + congr 1 + rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_map_apply] + congr 1 + ext r₂ + cases hout : V₁.outputOn x r₁.1 <;> simp [T₁, Spec.Transcript.split_append, hout] + · refine toOuterMeasure_bind_le _ _ _ fun r₁ => ?_ + rw [PMF.toOuterMeasure_map_apply] + cases hout : V₁.outputOn x r₁.1 with + | none => + have hset : (fun r₂ : Transcript s₂ × W₃ => (Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2)) ⁻¹' + T₂ = ∅ := by + ext r₂ + simp [T₂, Spec.Transcript.split_append, hout] + rw [hset, MeasureTheory.measure_empty] + exact zero_le + | some y => + have hl₂ := h₂ y (pure r₁.2) + rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hl₂ + simp only [plainLaw_bind, plainLaw_pure, PMF.pure_bind] at hl₂ + convert hl₂ using 2 + ext r₂ + simp [T₂, Spec.Transcript.split_append, hout] + +end Compose + +/-! ### Iteration -/ + +/-- `k` repetitions of the rounds `s`. -/ +def iterSpec (s : Spec) : ℕ → Spec + | 0 => [] + | k + 1 => iterSpec s k ++ s + +/-- The reduction without rounds that keeps the statement and the witness. -/ +def Reduction.id {S W : Type} : Reduction oP oV [] S W S W where + prover x w := pure (x, w) + verifier := { samplers := (), decide := fun x _ => pure (some x) } + +/-- Run the reductions `R 0`, …, `R (k - 1)` in sequence. -/ +def Reduction.iterate {s : Spec} {S W : Type} (R : ℕ → Reduction oP oV s S W S W) : + (k : ℕ) → Reduction oP oV (iterSpec s k) S W S W + | 0 => Reduction.id + | k + 1 => (Reduction.iterate R k).append (R k) + +/-- Repeat per-round errors. -/ +def PerChallenge.iterate {s : Spec} (ε : ℕ → PerChallenge (fun _ => ℝ≥0∞) s) : + (k : ℕ) → PerChallenge (fun _ => ℝ≥0∞) (iterSpec s k) + | 0 => () + | k + 1 => PerChallenge.append (iterSpec s k) s (PerChallenge.iterate ε k) (ε k) + +section Plain + +variable {s : Spec} {S W : Type} {R : ℕ → Reduction emptySpec emptySpec s S W S W} + +/-- The reduction without rounds is perfectly complete. -/ +theorem Reduction.id_complete (rel : S → W → Prop) : + (Reduction.id (oP := emptySpec) (oV := emptySpec)).Complete World.plain rel rel 0 := by + intro x w hxw + rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] + simp [Reduction.id, runStrategy, Verifier.outputOn, hxw] + rfl + +/-- The reduction without rounds is round-by-round sound without error. -/ +theorem Reduction.id_rbrSound (L : Set S) : + (Reduction.id (oP := emptySpec) (oV := emptySpec) (W := W)).verifier.RbrSound L L () := by + refine ⟨fun x _ => x ∈ L, fun x hx => hx, fun x hS ⟨x', hx', hout⟩ => hS ?_⟩ + have : x = x' := Option.some.inj hout + exact this ▸ hx' + +/-- **Iterated completeness**: if every step `R i` is complete from `rel i` to `rel (i + 1)` with +error `ε i` for `i < k`, the first `k` steps are complete from `rel 0` to `rel k` with the sum of +the errors. -/ +theorem Reduction.Complete.iterate {rel : ℕ → S → W → Prop} {ε : ℕ → ℝ≥0∞} (k : ℕ) + (h : ∀ i < k, (R i).Complete World.plain (rel i) (rel (i + 1)) (ε i)) : + (Reduction.iterate R k).Complete World.plain (rel 0) (rel k) (∑ i ∈ Finset.range k, ε i) := by + induction k with + | zero => + rw [Finset.sum_range_zero] + exact Reduction.id_complete (rel 0) + | succ k ih => + rw [Finset.sum_range_succ] + exact (ih fun i hi => h i (by omega)).append (h k (by omega)) + +/-- **Iterated round-by-round soundness**, with the per-round errors of the steps in order. -/ +theorem Verifier.RbrSound.iterate {L : ℕ → Set S} {ε : ℕ → PerChallenge (fun _ => ℝ≥0∞) s} + (k : ℕ) (h : ∀ i < k, (R i).verifier.RbrSound (L i) (L (i + 1)) (ε i)) : + (Reduction.iterate R k).verifier.RbrSound (L 0) (L k) (PerChallenge.iterate ε k) := by + induction k with + | zero => exact Reduction.id_rbrSound (L 0) + | succ k ih => exact (ih fun i hi => h i (by omega)).append (h k (by omega)) + +/-- The total error of repeated per-round errors. -/ +theorem PerChallenge.sum_iterate (ε : ℕ → PerChallenge (fun _ => ℝ≥0∞) s) (k : ℕ) : + PerChallenge.sum (iterSpec s k) (PerChallenge.iterate ε k) = + ∑ i ∈ Finset.range k, PerChallenge.sum s (ε i) := by + induction k with + | zero => rfl + | succ k ih => + rw [Finset.sum_range_succ, ← ih] + exact PerChallenge.sum_append _ _ + +end Plain + +end Cslib.Interactive diff --git a/ComplexityTests.lean b/ComplexityTests.lean index fbb107e502..ceb049d0a8 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -211,6 +211,7 @@ import ComplexityTests.Hypercontractivity import ComplexityTests.InductiveCounting import ComplexityTests.IntBinaryDecode import ComplexityTests.IntBinaryDiv +import ComplexityTests.Interactive import ComplexityTests.InteractiveProofs import ComplexityTests.Isolation import ComplexityTests.Iteration diff --git a/ComplexityTests/Interactive.lean b/ComplexityTests/Interactive.lean new file mode 100644 index 0000000000..243c4ea73b --- /dev/null +++ b/ComplexityTests/Interactive.lean @@ -0,0 +1,117 @@ +/- +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.Computability.Interactive.Sequential + +/-! +# Tests for interactive reductions + +A one-challenge reduction `coinStep` on Boolean claims: the verifier sends a fair coin `c` and +outputs the claim `x || c`. It reduces the claim "`x` is `true`" to itself, is perfectly complete, +and is round-by-round sound with error `1 / 2`, since a false claim survives only when `c` is +`true`. Its iterations exercise sequential composition with nonzero errors, so the composition +and iteration theorems are applied to satisfiable hypotheses. +-/ + +namespace ComplexityTests.Interactive + +open Cslib Cslib.Interactive Spec +open scoped ENNReal + +/-- One round: a public fair coin. -/ +abbrev coinSpec : Spec := [.verifier Bool] + +/-- The claim that the Boolean statement is `true`; there is no witness. -/ +def rel : Bool → Unit → Prop := fun x _ => x = true + +/-- The verifier sends a fair coin `c` and both parties continue with the claim `x || c`. -/ +noncomputable def coinStep : Reduction emptySpec emptySpec coinSpec Bool Unit Bool Unit where + prover x _ := pure (show Bool → ProbOracleComp emptySpec (Bool × Unit) from + fun c => pure (x || c, ())) + verifier := + { samplers := (ProbComp.uniform Bool, ()) + decide := fun x c => pure (some (x || c.1)) } + +/-- The coin round is perfectly complete. -/ +theorem coinStep_complete : coinStep.Complete World.plain rel rel 0 := by + rintro x ⟨⟩ (rfl : x = true) + rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] + simp [coinStep, runStrategy, Verifier.outputOn, rel] + rfl + +/-- The coin round is round-by-round sound with error `1 / 2`. -/ +theorem coinStep_rbrSound : + coinStep.verifier.RbrSound (language rel) (language rel) ((1 / 2 : ℝ≥0∞), ()) := by + refine ⟨fun x p => match p with + | none => x = true + | some (c, ()) => (x || c) = true, + fun x hx hS => hx ⟨(), hS⟩, fun x => ⟨fun hx => ?_, fun c hS ⟨x', ⟨⟨⟩, hx'⟩, hout⟩ => ?_⟩⟩ + · have hset : {c : Bool | (x || c) = true} = {true} := by + ext c + cases x <;> cases c <;> simp_all + change (ProbComp.eval (ProbComp.uniform Bool)).toOuterMeasure {c | (x || c) = true} ≤ 1 / 2 + rw [hset, ProbComp.eval_uniform, Probability.PMF.toOuterMeasure_uniformOfFintype] + have hcard : (Finset.univ.filter (· ∈ ({true} : Set Bool))).card = 1 := by decide + rw [hcard, Fintype.card_bool] + simp + · simp only [Verifier.outputOn, coinStep] at hout + exact hS ((Option.some.inj hout).trans hx') + +/-- The coin round is sound with error `1 / 2`, by round-by-round soundness. -/ +theorem coinStep_sound : + coinStep.verifier.Sound (oP := emptySpec) World.plain (language rel) (language rel) + (1 / 2) := by + simpa [PerChallenge.sum] using coinStep_rbrSound.sound + +/-- Two coin rounds in sequence are complete, by composition. -/ +example : (coinStep.append coinStep).Complete World.plain rel rel 0 := by + simpa using coinStep_complete.append coinStep_complete + +/-- Two coin rounds in sequence are sound with error `1`, by composition of round-by-round +soundness; the composed errors are concatenated. -/ +example : + (coinStep.append coinStep).verifier.Sound (oP := emptySpec) World.plain (language rel) + (language rel) (1 / 2 + 1 / 2) := by + have h := (coinStep_rbrSound.append coinStep_rbrSound).sound + simp only [PerChallenge.sum_append, PerChallenge.sum, add_zero] at h + exact h + +/-- Iterated coin rounds are complete, by iterated composition. -/ +example (k : ℕ) : (Reduction.iterate (fun _ => coinStep) k).Complete World.plain rel rel 0 := by + simpa using Reduction.Complete.iterate (rel := fun _ => rel) (ε := fun _ => 0) k + fun _ _ => coinStep_complete + +/-- +info: 'Cslib.Interactive.Reduction.Complete.append' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Interactive.Reduction.Complete.append + +/-- +info: 'Cslib.Interactive.Verifier.Sound.append' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Interactive.Verifier.Sound.append + +/-- +info: 'Cslib.Interactive.Verifier.KnowledgeSound.append' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Interactive.Verifier.KnowledgeSound.append + +/-- +info: 'Cslib.Interactive.Verifier.RbrSound.append' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Interactive.Verifier.RbrSound.append + +/-- +info: 'Cslib.Interactive.Verifier.RbrSound.sound' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Interactive.Verifier.RbrSound.sound + +end ComplexityTests.Interactive From 52fa95d43c173ab59db55345baa2bcaa32a97a61 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:49:45 -0400 Subject: [PATCH 3/7] doc(roadmap): record the interactive-reduction core and its open items Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ROADMAP.md | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 1385d93350..bc3ce1a605 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1215,11 +1215,24 @@ Jukna coverage below is an additional target beyond the V1 port: certificates for the identification simulator and extractor; SIS for a general (prime) modulus; module SIS and module LWE over polynomial rings, and Dilithium-style signatures as theory, not a parameter set or ciphersuite. -* **Zero-knowledge proof systems toward libzk (#643, #640).** A public-coin interactive-reduction - core with sequential composition and round-by-round soundness, and sumcheck as its first client, - are in review (#701, #703). Open, in order: - - oracle statements, so a later phase can query an earlier phase's oracle (ArkLib-style virtual - output oracles), together with knowledge soundness and zero knowledge in oracle worlds; +* **Zero-knowledge proof systems toward libzk (#643, #640).** The + [interactive-reduction core](Complexity/Computability/Interactive/Basic.lean) has typed + public-coin protocols with oracle access to the prover's messages, worlds for the oracle model, + and named extractors and simulators. It defines completeness, soundness, straight-line knowledge + soundness, round-by-round soundness and HVZK; knowledge soundness and HVZK are stated in the + plain model. In the plain model, + [sequential composition](Complexity/Computability/Interactive/Sequential.lean) is proved for + completeness, soundness, knowledge soundness and round-by-round soundness, and so is per-stage + iteration. [Round-by-round soundness implies soundness](Complexity/Computability/Interactive/Plain.lean). + Sumcheck, the first client, is in review (#703). Open, in order: + - the `PublicCoin → IP` bridge, with a uniform word verifier and adversarial decoding; + - parallel and AND/OR composition, and round-by-round knowledge soundness; + - oracle statements. Today a later phase cannot query an earlier phase's oracle message, + because `Verifier.append` routes the second verifier's queries only to its own messages. + Sumcheck followed by an evaluation query on a committed polynomial needs this, and so do FRI + and Ligero. The design item is virtual output oracles, as in ArkLib's + `OracleOutputSimulation`. Knowledge soundness and zero knowledge in oracle worlds go with it: + extractors that see the prover's queries, and simulators that program the world; - efficiency-certified simulators and extractors, and auxiliary-input zero knowledge (#704) on the core; - polynomial commitment and evaluation-query reductions, and the Ligero IOP; @@ -1228,6 +1241,8 @@ Jukna coverage below is an additional target beyond the V1 port: - VOLE as an ideal functionality and VOLE-in-the-head; - the compositional structure of libzk (Shelat's IETF draft) as a composition of these components, stated as theory without concrete ciphersuites. + + The design is on #643, and the TQBF, PCP and GMW bridges are recorded there. * **Classic symmetric constructions (#640, track D).** Proved: PRF-based MACs (#677), keyed collision-resistant hash families and Merkle–Damgård (#678), and universal hashing (#663). Open: Luby–Rackoff (three Feistel rounds over a PRF give a PRP, four give a strong PRP), strongly From f82485948a1e5e747eaaf346471dd55a96dba811 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 23:21:31 -0400 Subject: [PATCH 4/7] refactor(interactive): plain-world knowledge soundness and HVZK; per-stage iteration MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Following the framework comparison on #587 (comment 6379197465, items 2 and 6): Verifier.KnowledgeSound and Reduction.HVZK are stated in the plain model, where the extractor and simulator they name are adequate; the docstrings now say that Verifier.Sound is information-theoretic in every world and that KnowledgeSound is straight-line (IOP-style) extraction, not a rewinding proof of knowledge. Reduction.iterate and its theorems index the stages by s : ℕ → Spec and S W : ℕ → Type, so stage types can change between stages. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Computability/Interactive/Basic.lean | 3 +- .../Computability/Interactive/Security.lean | 49 ++++++++------ .../Computability/Interactive/Sequential.lean | 64 +++++++++++-------- ComplexityTests/Interactive.lean | 4 +- 4 files changed, 71 insertions(+), 49 deletions(-) diff --git a/Complexity/Computability/Interactive/Basic.lean b/Complexity/Computability/Interactive/Basic.lean index 2d82300a73..0c40b43430 100644 --- a/Complexity/Computability/Interactive/Basic.lean +++ b/Complexity/Computability/Interactive/Basic.lean @@ -15,8 +15,7 @@ public import Complexity.Languages.Probabilistic.Oracle.Interaction An interactive reduction from a relation `R₁` to a relation `R₂` is a public-coin protocol in which a prover convinces a verifier, who holds a statement of `R₁`, to output a statement of `R₂`, and whose prover outputs a witness for it [Ben-Sasson, Chiesa and Spooner][BenSassonChiesaSpooner2016]. -Interactive proofs, arguments, interactive oracle proofs and proofs of knowledge are the -reductions to acceptance. +Interactive proofs and interactive oracle proofs are the reductions to acceptance. A protocol is described by its rounds (`Interactive.Spec`, a list of `Interactive.Round`s). In a prover round the prover sends a message, which the verifier only accesses through the message's diff --git a/Complexity/Computability/Interactive/Security.lean b/Complexity/Computability/Interactive/Security.lean index cf39a17571..ec474bfecd 100644 --- a/Complexity/Computability/Interactive/Security.lean +++ b/Complexity/Computability/Interactive/Security.lean @@ -20,15 +20,23 @@ Exact security notions for a reduction from a relation `relIn` to a relation `re and the prover's witness is valid for it. * `Verifier.Sound W V langIn langOut ε`: on every `x ∉ langIn`, every prover strategy makes the verifier output a statement of `langOut` with probability at most `ε`. -* `Verifier.KnowledgeSound W V relIn relOut E ε`: the straight-line extractor `E` recovers a valid - input witness from the transcript and the prover's output witness, except with probability `ε`. +* `Verifier.KnowledgeSound V relIn relOut E ε`: in the plain model, the straight-line extractor + `E` recovers a valid input witness from the transcript and the prover's output witness, except + with probability `ε`. * `Verifier.RbrSound V langIn langOut ε`: round-by-round soundness in the plain model, with an error for every challenge round, through a state function on transcript prefixes. -* `Reduction.HVZK W R relIn Sim ε`: the simulator's transcripts are `ε`-close in statistical - distance to honest ones. - -Proof systems, arguments and proofs of knowledge are the reductions to the trivial relation -`Interactive.Accept`, with output language `Set.univ`. Extractors and simulators are named +* `Reduction.HVZK R relIn Sim ε`: in the plain model, the simulator's transcripts are `ε`-close + in statistical distance to honest ones. + +Interactive proofs and interactive oracle proofs are the reductions to the trivial relation +`Interactive.Accept`, with output language `Set.univ`. `Verifier.Sound` quantifies over all +prover strategies, with no query or time bound, so it is the information-theoretic notion in every +world; arguments and query-bounded soundness in oracle worlds are separate notions. +`Verifier.KnowledgeSound` is straight-line extraction from the transcript, as for interactive +oracle proofs; proofs of knowledge in the sense of Bellare and Goldreich, whose extractors rewind +the prover, are a different notion. Knowledge soundness and zero knowledge are stated in the plain +model: in an oracle world the extractor would need the prover's queries and the simulator the +oracle's view, which these definitions do not provide. Extractors and simulators are named arguments, so a property cannot hold vacuously through an unconstrained existential. Their efficiency is a separate layer. @@ -89,21 +97,22 @@ def Reduction.Complete (W : World oP oV) (R : Reduction oP oV s StmtIn WitIn Stm (W.eval (R.run x w)).toOuterMeasure {r | ¬ (r.2.1 = some r.2.2.1 ∧ relOut r.2.2.1 r.2.2.2)} ≤ ε -/-- Soundness with error `ε`, against every prover strategy. -/ +/-- Soundness with error `ε`, against every prover strategy. Provers are not bounded in time or +in oracle queries, so this is information-theoretic soundness in every world. -/ def Verifier.Sound (W : World oP oV) (V : Verifier oV s StmtIn StmtOut) (langIn : Set StmtIn) (langOut : Set StmtOut) (ε : ℝ≥0∞) : Prop := ∀ x ∉ langIn, ∀ (α : Type) (P : ProbOracleComp oP (ProverStrategy (ProbOracleComp oP) s α)), (W.eval (V.execute x P)).toOuterMeasure {r | ∃ x' ∈ langOut, r.2.1 = some x'} ≤ ε -/-- Straight-line knowledge soundness with error `ε`: whenever a prover strategy, ending with an -output witness, makes the verifier output a statement for which that witness is valid, the -extractor `E` recovers a valid input witness from the statement, the transcript and the output -witness, except with probability `ε`. -/ -def Verifier.KnowledgeSound (W : World oP oV) (V : Verifier oV s StmtIn StmtOut) +/-- Straight-line knowledge soundness with error `ε`, in the plain model: whenever a prover +strategy, ending with an output witness, makes the verifier output a statement for which that +witness is valid, the extractor `E` recovers a valid input witness from the statement, the +transcript and the output witness, except with probability `ε`. -/ +def Verifier.KnowledgeSound (V : Verifier emptySpec s StmtIn StmtOut) (relIn : StmtIn → WitIn → Prop) (relOut : StmtOut → WitOut → Prop) (E : StmtIn → Transcript s → WitOut → WitIn) (ε : ℝ≥0∞) : Prop := - ∀ x (P : ProbOracleComp oP (ProverStrategy (ProbOracleComp oP) s WitOut)), - (W.eval (V.execute x P)).toOuterMeasure + ∀ x (P : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s WitOut)), + (World.plain.eval (V.execute (oP := emptySpec) x P)).toOuterMeasure {r | (∃ x', r.2.1 = some x' ∧ relOut x' r.2.2) ∧ ¬ relIn x (E x r.1 r.2.2)} ≤ ε /-! ### Round-by-round soundness -/ @@ -158,11 +167,13 @@ def Verifier.RbrSound (V : Verifier emptySpec s StmtIn StmtOut) (langIn : Set St /-! ### Zero knowledge -/ -/-- Honest-verifier zero knowledge with statistical error `ε` (perfect for `ε = 0`): on every -`(x, w)` in `relIn`, the simulator's transcript law is `ε`-close to the honest one. -/ -def Reduction.HVZK (W : World oP oV) (R : Reduction oP oV s StmtIn WitIn StmtOut WitOut) +/-- Honest-verifier zero knowledge with statistical error `ε` (perfect for `ε = 0`), in the plain +model: on every `(x, w)` in `relIn`, the simulator's transcript law is `ε`-close to the honest +one. -/ +def Reduction.HVZK (R : Reduction emptySpec emptySpec s StmtIn WitIn StmtOut WitOut) (relIn : StmtIn → WitIn → Prop) (Sim : StmtIn → ProbComp (Transcript s)) (ε : ℝ≥0∞) : Prop := - ∀ x w, relIn x w → CloseTo ((W.eval (R.run x w)).map Prod.fst) (ProbComp.eval (Sim x)) ε + ∀ x w, relIn x w → + CloseTo ((World.plain.eval (R.run x w)).map Prod.fst) (ProbComp.eval (Sim x)) ε end Cslib.Interactive diff --git a/Complexity/Computability/Interactive/Sequential.lean b/Complexity/Computability/Interactive/Sequential.lean index 2fb9002204..26a5a17ead 100644 --- a/Complexity/Computability/Interactive/Sequential.lean +++ b/Complexity/Computability/Interactive/Sequential.lean @@ -660,9 +660,9 @@ theorem Verifier.KnowledgeSound.append {V₁ : Verifier emptySpec s₁ S₁ S₂ {V₂ : Verifier emptySpec s₂ S₂ S₃} {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {ε₁ ε₂ : ℝ≥0∞} {E₁ : S₁ → Transcript s₁ → W₂ → W₁} {E₂ : S₂ → Transcript s₂ → W₃ → W₂} - (h₁ : V₁.KnowledgeSound (oP := emptySpec) World.plain rel₁ rel₂ E₁ ε₁) - (h₂ : V₂.KnowledgeSound (oP := emptySpec) World.plain rel₂ rel₃ E₂ ε₂) (y₀ : S₂) : - (V₁.append V₂).KnowledgeSound (oP := emptySpec) World.plain rel₁ rel₃ + (h₁ : V₁.KnowledgeSound rel₁ rel₂ E₁ ε₁) + (h₂ : V₂.KnowledgeSound rel₂ rel₃ E₂ ε₂) (y₀ : S₂) : + (V₁.append V₂).KnowledgeSound rel₁ rel₃ (V₁.extractAppend E₁ E₂ y₀) (ε₁ + ε₂) := by intro x P rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply, plainLaw_run_verifierAppend] @@ -736,34 +736,36 @@ end Compose /-! ### Iteration -/ -/-- `k` repetitions of the rounds `s`. -/ -def iterSpec (s : Spec) : ℕ → Spec +/-- The rounds of the stages `s 0`, …, `s (k - 1)`, in order. -/ +def iterSpec (s : ℕ → Spec) : ℕ → Spec | 0 => [] - | k + 1 => iterSpec s k ++ s + | k + 1 => iterSpec s k ++ s k /-- The reduction without rounds that keeps the statement and the witness. -/ def Reduction.id {S W : Type} : Reduction oP oV [] S W S W where prover x w := pure (x, w) verifier := { samplers := (), decide := fun x _ => pure (some x) } -/-- Run the reductions `R 0`, …, `R (k - 1)` in sequence. -/ -def Reduction.iterate {s : Spec} {S W : Type} (R : ℕ → Reduction oP oV s S W S W) : - (k : ℕ) → Reduction oP oV (iterSpec s k) S W S W +/-- Run the stages `R 0`, …, `R (k - 1)` in sequence. Stage `i` has its own rounds `s i` and +reduces statements of type `S i` with witnesses `W i` to those of stage `i + 1`. -/ +def Reduction.iterate {s : ℕ → Spec} {S W : ℕ → Type} + (R : (i : ℕ) → Reduction oP oV (s i) (S i) (W i) (S (i + 1)) (W (i + 1))) : + (k : ℕ) → Reduction oP oV (iterSpec s k) (S 0) (W 0) (S k) (W k) | 0 => Reduction.id | k + 1 => (Reduction.iterate R k).append (R k) -/-- Repeat per-round errors. -/ -def PerChallenge.iterate {s : Spec} (ε : ℕ → PerChallenge (fun _ => ℝ≥0∞) s) : +/-- Concatenate per-round errors of the stages. -/ +def PerChallenge.iterate {s : ℕ → Spec} (ε : (i : ℕ) → PerChallenge (fun _ => ℝ≥0∞) (s i)) : (k : ℕ) → PerChallenge (fun _ => ℝ≥0∞) (iterSpec s k) | 0 => () - | k + 1 => PerChallenge.append (iterSpec s k) s (PerChallenge.iterate ε k) (ε k) + | k + 1 => PerChallenge.append (iterSpec s k) (s k) (PerChallenge.iterate ε k) (ε k) -section Plain +section Identity -variable {s : Spec} {S W : Type} {R : ℕ → Reduction emptySpec emptySpec s S W S W} +variable {T U : Type} /-- The reduction without rounds is perfectly complete. -/ -theorem Reduction.id_complete (rel : S → W → Prop) : +theorem Reduction.id_complete (rel : T → U → Prop) : (Reduction.id (oP := emptySpec) (oV := emptySpec)).Complete World.plain rel rel 0 := by intro x w hxw rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] @@ -771,16 +773,23 @@ theorem Reduction.id_complete (rel : S → W → Prop) : rfl /-- The reduction without rounds is round-by-round sound without error. -/ -theorem Reduction.id_rbrSound (L : Set S) : - (Reduction.id (oP := emptySpec) (oV := emptySpec) (W := W)).verifier.RbrSound L L () := by +theorem Reduction.id_rbrSound (L : Set T) : + (Reduction.id (oP := emptySpec) (oV := emptySpec) (W := U)).verifier.RbrSound L L () := by refine ⟨fun x _ => x ∈ L, fun x hx => hx, fun x hS ⟨x', hx', hout⟩ => hS ?_⟩ have : x = x' := Option.some.inj hout exact this ▸ hx' -/-- **Iterated completeness**: if every step `R i` is complete from `rel i` to `rel (i + 1)` with -error `ε i` for `i < k`, the first `k` steps are complete from `rel 0` to `rel k` with the sum of -the errors. -/ -theorem Reduction.Complete.iterate {rel : ℕ → S → W → Prop} {ε : ℕ → ℝ≥0∞} (k : ℕ) +end Identity + +section Plain + +variable {s : ℕ → Spec} {S W : ℕ → Type} + {R : (i : ℕ) → Reduction emptySpec emptySpec (s i) (S i) (W i) (S (i + 1)) (W (i + 1))} + +/-- **Iterated completeness**: if every stage `R i` with `i < k` is complete from `rel i` to +`rel (i + 1)` with error `ε i`, the first `k` stages are complete from `rel 0` to `rel k` with +the sum of the errors. -/ +theorem Reduction.Complete.iterate {rel : (i : ℕ) → S i → W i → Prop} {ε : ℕ → ℝ≥0∞} (k : ℕ) (h : ∀ i < k, (R i).Complete World.plain (rel i) (rel (i + 1)) (ε i)) : (Reduction.iterate R k).Complete World.plain (rel 0) (rel k) (∑ i ∈ Finset.range k, ε i) := by induction k with @@ -791,18 +800,19 @@ theorem Reduction.Complete.iterate {rel : ℕ → S → W → Prop} {ε : ℕ rw [Finset.sum_range_succ] exact (ih fun i hi => h i (by omega)).append (h k (by omega)) -/-- **Iterated round-by-round soundness**, with the per-round errors of the steps in order. -/ -theorem Verifier.RbrSound.iterate {L : ℕ → Set S} {ε : ℕ → PerChallenge (fun _ => ℝ≥0∞) s} - (k : ℕ) (h : ∀ i < k, (R i).verifier.RbrSound (L i) (L (i + 1)) (ε i)) : +/-- **Iterated round-by-round soundness**, with the per-round errors of the stages in order. -/ +theorem Verifier.RbrSound.iterate {L : (i : ℕ) → Set (S i)} + {ε : (i : ℕ) → PerChallenge (fun _ => ℝ≥0∞) (s i)} (k : ℕ) + (h : ∀ i < k, (R i).verifier.RbrSound (L i) (L (i + 1)) (ε i)) : (Reduction.iterate R k).verifier.RbrSound (L 0) (L k) (PerChallenge.iterate ε k) := by induction k with | zero => exact Reduction.id_rbrSound (L 0) | succ k ih => exact (ih fun i hi => h i (by omega)).append (h k (by omega)) -/-- The total error of repeated per-round errors. -/ -theorem PerChallenge.sum_iterate (ε : ℕ → PerChallenge (fun _ => ℝ≥0∞) s) (k : ℕ) : +/-- The total error of the stages' concatenated per-round errors. -/ +theorem PerChallenge.sum_iterate (ε : (i : ℕ) → PerChallenge (fun _ => ℝ≥0∞) (s i)) (k : ℕ) : PerChallenge.sum (iterSpec s k) (PerChallenge.iterate ε k) = - ∑ i ∈ Finset.range k, PerChallenge.sum s (ε i) := by + ∑ i ∈ Finset.range k, PerChallenge.sum (s i) (ε i) := by induction k with | zero => rfl | succ k ih => diff --git a/ComplexityTests/Interactive.lean b/ComplexityTests/Interactive.lean index 243c4ea73b..fb997b0454 100644 --- a/ComplexityTests/Interactive.lean +++ b/ComplexityTests/Interactive.lean @@ -80,7 +80,9 @@ example : exact h /-- Iterated coin rounds are complete, by iterated composition. -/ -example (k : ℕ) : (Reduction.iterate (fun _ => coinStep) k).Complete World.plain rel rel 0 := by +example (k : ℕ) : + (Reduction.iterate (s := fun _ => coinSpec) (S := fun _ => Bool) (W := fun _ => Unit) + (fun _ => coinStep) k).Complete World.plain rel rel 0 := by simpa using Reduction.Complete.iterate (rel := fun _ => rel) (ε := fun _ => 0) k fun _ _ => coinStep_complete From a116754f6d79d15c32ae682e06c30e7988dbc842 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:10:56 -0400 Subject: [PATCH 5/7] style(interactive): replace a non-terminal simp by simp only Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity/Computability/Interactive/Sequential.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Complexity/Computability/Interactive/Sequential.lean b/Complexity/Computability/Interactive/Sequential.lean index 26a5a17ead..4c2aebe3b3 100644 --- a/Complexity/Computability/Interactive/Sequential.lean +++ b/Complexity/Computability/Interactive/Sequential.lean @@ -769,7 +769,10 @@ theorem Reduction.id_complete (rel : T → U → Prop) : (Reduction.id (oP := emptySpec) (oV := emptySpec)).Complete World.plain rel rel 0 := by intro x w hxw rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] - simp [Reduction.id, runStrategy, Verifier.outputOn, hxw] + simp only [Reduction.id, runStrategy, bind_pure_comp, map_pure, plainLaw_pure, + Verifier.outputOn, Sum.elim_inl, OracleComp.interpret_pure, not_and, Set.preimage_ofPred_eq, + PMF.toOuterMeasure_pure_apply, Set.mem_ofPred_eq, hxw, not_true_eq_false, imp_false, + nonpos_iff_eq_zero, ite_eq_right_iff, one_ne_zero, not_not] rfl /-- The reduction without rounds is round-by-round sound without error. -/ From 6474265117f812bf002c0c67cb432687fce10b0a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 02:33:09 -0400 Subject: [PATCH 6/7] refactor(interactive): use the shared sum of oracle interfaces (#732) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove the placeholder Cslib.OracleSpec.sum and Interactive.emptySpec, without aliases, in favour of #732's OracleSpec.sum (⊕ₒ), OracleSpec.empty, OracleComp.sumHandler and OracleComp.liftRight: the verifier's output handler, the plain world's implementation and the composed decision lifts are now sum handlers. No statement changes beyond the renamed empty interface. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Computability/Interactive/Basic.lean | 25 +---- .../Computability/Interactive/Plain.lean | 63 ++++++----- .../Computability/Interactive/Security.lean | 17 ++- .../Computability/Interactive/Sequential.lean | 104 +++++++++--------- ComplexityTests/Interactive.lean | 9 +- 5 files changed, 102 insertions(+), 116 deletions(-) diff --git a/Complexity/Computability/Interactive/Basic.lean b/Complexity/Computability/Interactive/Basic.lean index 0c40b43430..4d810bbf61 100644 --- a/Complexity/Computability/Interactive/Basic.lean +++ b/Complexity/Computability/Interactive/Basic.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Languages.Probabilistic.Oracle.Interaction +public import Complexity.Languages.Probabilistic.Sum /-! # Public-coin interactive oracle reductions @@ -39,7 +40,6 @@ by structural recursion on its list of rounds, so concatenated protocols compute ## Main definitions -* `Cslib.OracleSpec.sum` (notation `⊕ₒ`, scoped in `Interactive`), `Interactive.emptySpec`. * `Interactive.OracleInterface`, `Interactive.Round`, `Interactive.Spec`. * `Interactive.Spec.Transcript`, `Interactive.Spec.PerChallenge`, `Interactive.Spec.MsgQuery`. * `Interactive.ProverStrategy`, `Interactive.Prover`, `Interactive.Verifier`, @@ -58,18 +58,6 @@ namespace Cslib.Interactive open scoped ENNReal -/-! ### Oracle specifications -/ - -/-- The disjoint union of two oracle interfaces. -/ -abbrev _root_.Cslib.OracleSpec.sum {ι₁ ι₂ : Type} (spec₁ : OracleSpec ι₁) - (spec₂ : OracleSpec ι₂) : OracleSpec (ι₁ ⊕ ι₂) := - Sum.elim spec₁ spec₂ - -@[inherit_doc] scoped infixr:65 " ⊕ₒ " => Cslib.OracleSpec.sum - -/-- The interface without queries, for parties that use no oracle. -/ -abbrev emptySpec : OracleSpec Empty := fun q => q.elim - /-! ### Messages and rounds -/ /-- How the verifier accesses a prover message of type `M`: the queries it may ask and the @@ -224,9 +212,8 @@ from the transcript. -/ def Verifier.output {s : Spec} {StmtIn StmtOut : Type} (V : Verifier oV s StmtIn StmtOut) (x : StmtIn) (τ : Transcript s) : ProbOracleComp (oP ⊕ₒ oV) (Option StmtOut) := OracleComp.interpret - (fun q => match q with - | .inl q => ProbOracleComp.query (spec := oP ⊕ₒ oV) (.inr q) - | .inr q => pure (Transcript.answer s τ q)) + (OracleComp.sumHandler (fun q => ProbOracleComp.query (spec := oP ⊕ₒ oV) (.inr q)) + fun q => pure (Transcript.answer s τ q)) (V.decide x (Transcript.challenges s τ)) /-- Run the verifier against any (possibly malicious) prover strategy with result type `α`: the @@ -261,12 +248,10 @@ noncomputable def World.eval (W : World oP oV) {α : Type} (program : ProbOracle (ProbOracleComp.runWith W.impl program W.init).map Prod.fst /-- The plain model: no oracles. -/ -def World.plain : World emptySpec emptySpec where +def World.plain : World OracleSpec.empty OracleSpec.empty where State := Unit init := () - impl - | .inl e => e.elim - | .inr e => e.elim + impl := OracleComp.sumHandler (fun e => e.elim) fun e => e.elim end Execution diff --git a/Complexity/Computability/Interactive/Plain.lean b/Complexity/Computability/Interactive/Plain.lean index 8b3bb7d86d..03de2ed08e 100644 --- a/Complexity/Computability/Interactive/Plain.lean +++ b/Complexity/Computability/Interactive/Plain.lean @@ -42,28 +42,25 @@ open scoped ENNReal open Spec /-- The law of a program without external oracles: its private coins are fair. -/ -noncomputable def plainLaw {α : Type} (p : ProbOracleComp emptySpec α) : PMF α := +noncomputable def plainLaw {α : Type} (p : ProbOracleComp OracleSpec.empty α) : PMF α := OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun e => e.elim) p /-- The law of a joint program in the plain model. -/ -private noncomputable def runLaw {α : Type} (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) : - PMF α := - OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun q => match q with - | .inl e => e.elim - | .inr e => e.elim) p +private noncomputable def runLaw {α : Type} + (p : ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) α) : PMF α := + OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle + (OracleComp.sumHandler (fun e => e.elim) fun e => e.elim)) p -private theorem plain_eval {α : Type} (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) : +private theorem plain_eval {α : Type} + (p : ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) α) : World.plain.eval p = runLaw p := by have h := OracleComp.run_interpret_stateless (m := PMF) (State := Unit) - (ProbOracleComp.handler ProbComp.unifOracle fun q => match q with - | .inl e => e.elim - | .inr e => e.elim) p () + (ProbOracleComp.handler ProbComp.unifOracle + (OracleComp.sumHandler (fun e => e.elim) fun e => e.elim)) p () have hh : (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) World.plain.impl) = fun q s => (fun a => (a, s)) <$> ProbOracleComp.handler ProbComp.unifOracle - (fun q => match q with - | .inl e => e.elim - | .inr e => e.elim) q := by + (OracleComp.sumHandler (fun e => e.elim) fun e => e.elim) q := by funext q s rcases q with n | e | e · rfl @@ -73,8 +70,8 @@ private theorem plain_eval {α : Type} (p : ProbOracleComp (emptySpec ⊕ₒ emp erw [hh, h] exact (PMF.map_comp _ _ _).trans (PMF.map_id _) -private theorem runLaw_liftProver {α : Type} (p : ProbOracleComp emptySpec α) : - runLaw (liftProver (oV := emptySpec) p) = plainLaw p := by +private theorem runLaw_liftProver {α : Type} (p : ProbOracleComp OracleSpec.empty α) : + runLaw (liftProver (oV := OracleSpec.empty) p) = plainLaw p := by rw [runLaw, liftProver, OracleComp.interpret_interpret, plainLaw] congr 1 funext q @@ -85,34 +82,36 @@ private theorem runLaw_liftProver {α : Type} (p : ProbOracleComp emptySpec α) /-- A returned value has a point law. -/ @[simp] theorem plainLaw_pure {α : Type} (a : α) : - plainLaw (pure a : ProbOracleComp emptySpec α) = PMF.pure a := rfl + plainLaw (pure a : ProbOracleComp OracleSpec.empty α) = PMF.pure a := rfl /-- Sequencing is `PMF.bind`. -/ -@[simp] theorem plainLaw_bind {α β : Type} (p : ProbOracleComp emptySpec α) - (f : α → ProbOracleComp emptySpec β) : +@[simp] theorem plainLaw_bind {α β : Type} (p : ProbOracleComp OracleSpec.empty α) + (f : α → ProbOracleComp OracleSpec.empty β) : plainLaw (p >>= f) = (plainLaw p).bind fun a => plainLaw (f a) := OracleComp.interpret_bind _ _ _ /-- Postprocessing is `PMF.map`. -/ -@[simp] theorem plainLaw_map {α β : Type} (f : α → β) (p : ProbOracleComp emptySpec α) : +@[simp] theorem plainLaw_map {α β : Type} (f : α → β) (p : ProbOracleComp OracleSpec.empty α) : plainLaw (f <$> p) = (plainLaw p).map f := OracleComp.interpret_map _ _ _ /-- Embedded sampling has the law of the sampled program. -/ @[simp] theorem plainLaw_sample {α : Type} (p : ProbComp α) : - plainLaw (ProbOracleComp.sample (spec := emptySpec) p) = ProbComp.eval p := + plainLaw (ProbOracleComp.sample (spec := OracleSpec.empty) p) = ProbComp.eval p := ProbOracleComp.interpret_sample _ _ _ private theorem runLaw_pure {α : Type} (a : α) : - runLaw (pure a : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) = PMF.pure a := rfl + runLaw (pure a : ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) α) = PMF.pure a := rfl -private theorem runLaw_bind {α β : Type} (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) - (f : α → ProbOracleComp (emptySpec ⊕ₒ emptySpec) β) : +private theorem runLaw_bind {α β : Type} + (p : ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) α) + (f : α → ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) β) : runLaw (p >>= f) = (runLaw p).bind fun a => runLaw (f a) := OracleComp.interpret_bind _ _ _ private theorem runLaw_map {α β : Type} (f : α → β) - (p : ProbOracleComp (emptySpec ⊕ₒ emptySpec) α) : runLaw (f <$> p) = (runLaw p).map f := + (p : ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) α) : + runLaw (f <$> p) = (runLaw p).map f := OracleComp.interpret_map _ _ _ /-- A program whose queries are answered deterministically has a point law. -/ @@ -130,9 +129,9 @@ private theorem interpret_pure_handler {ι : Type} {spec : OracleSpec ι} {α : exact ih (f q) private theorem runLaw_output {s : Spec} {StmtIn StmtOut : Type} - (V : Verifier emptySpec s StmtIn StmtOut) + (V : Verifier OracleSpec.empty s StmtIn StmtOut) (x : StmtIn) (τ : Transcript s) : - runLaw (V.output (oP := emptySpec) x τ) = PMF.pure (V.outputOn x τ) := by + runLaw (V.output (oP := OracleSpec.empty) x τ) = PMF.pure (V.outputOn x τ) := by rw [runLaw, Verifier.output, OracleComp.interpret_interpret, Verifier.outputOn] rw [← interpret_pure_handler] congr 1 @@ -154,9 +153,9 @@ private theorem toOuterMeasure_bind_pure {α β : Type} (p : PMF α) (g : α → /-- **The law of an execution in the plain model**: run the prover's strategy against the challenge samplers, then apply the verifier's decision to the transcript. -/ theorem World.plain_eval_execute {s : Spec} {StmtIn StmtOut α : Type} - (V : Verifier emptySpec s StmtIn StmtOut) (x : StmtIn) - (P : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s α)) : - World.plain.eval (V.execute (oP := emptySpec) x P) = + (V : Verifier OracleSpec.empty s StmtIn StmtOut) (x : StmtIn) + (P : ProbOracleComp OracleSpec.empty (ProverStrategy (ProbOracleComp OracleSpec.empty) s α)) : + World.plain.eval (V.execute (oP := OracleSpec.empty) x P) = (plainLaw (P >>= runStrategy s V.samplers)).map fun r => (r.1, V.outputOn x r.1, r.2) := by rw [plain_eval] simp only [Verifier.execute, runLaw_bind, runLaw_liftProver, runLaw_output, runLaw_pure, @@ -167,7 +166,7 @@ theorem World.plain_eval_execute {s : Spec} {StmtIn StmtOut α : Type} private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s) (ε : PerChallenge (fun _ => ℝ≥0∞) s) (S : Prefix s → Prop) (wins : Transcript s → Prop), RbrFrom s smp ε S wins → ¬ S (Prefix.empty s) → - ∀ {α : Type} (st : ProverStrategy (ProbOracleComp emptySpec) s α), + ∀ {α : Type} (st : ProverStrategy (ProbOracleComp OracleSpec.empty) s α), (plainLaw (runStrategy s smp st)).toOuterMeasure {r | wins r.1} ≤ PerChallenge.sum s ε | [], _, _, _, wins, h, hS, _, st => by have hw : ¬ wins () := h hS @@ -211,10 +210,10 @@ private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s) /-- **Round-by-round soundness implies soundness**, with the sum of the per-round errors. -/ theorem Verifier.RbrSound.sound {s : Spec} {StmtIn StmtOut : Type} - {V : Verifier emptySpec s StmtIn StmtOut} {langIn : Set StmtIn} + {V : Verifier OracleSpec.empty s StmtIn StmtOut} {langIn : Set StmtIn} {langOut : Set StmtOut} {ε : PerChallenge (fun _ => ℝ≥0∞) s} (h : V.RbrSound langIn langOut ε) : - V.Sound (oP := emptySpec) World.plain langIn langOut (PerChallenge.sum s ε) := by + V.Sound (oP := OracleSpec.empty) World.plain langIn langOut (PerChallenge.sum s ε) := by obtain ⟨S, hinit, hround⟩ := h intro x hx α P rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply, plainLaw_bind] diff --git a/Complexity/Computability/Interactive/Security.lean b/Complexity/Computability/Interactive/Security.lean index ec474bfecd..eb2c4cc141 100644 --- a/Complexity/Computability/Interactive/Security.lean +++ b/Complexity/Computability/Interactive/Security.lean @@ -108,11 +108,12 @@ def Verifier.Sound (W : World oP oV) (V : Verifier oV s StmtIn StmtOut) strategy, ending with an output witness, makes the verifier output a statement for which that witness is valid, the extractor `E` recovers a valid input witness from the statement, the transcript and the output witness, except with probability `ε`. -/ -def Verifier.KnowledgeSound (V : Verifier emptySpec s StmtIn StmtOut) +def Verifier.KnowledgeSound (V : Verifier OracleSpec.empty s StmtIn StmtOut) (relIn : StmtIn → WitIn → Prop) (relOut : StmtOut → WitOut → Prop) (E : StmtIn → Transcript s → WitOut → WitIn) (ε : ℝ≥0∞) : Prop := - ∀ x (P : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s WitOut)), - (World.plain.eval (V.execute (oP := emptySpec) x P)).toOuterMeasure + ∀ x (P : ProbOracleComp OracleSpec.empty + (ProverStrategy (ProbOracleComp OracleSpec.empty) s WitOut)), + (World.plain.eval (V.execute (oP := OracleSpec.empty) x P)).toOuterMeasure {r | (∃ x', r.2.1 = some x' ∧ relOut x' r.2.2) ∧ ¬ relIn x (E x r.1 r.2.2)} ≤ ε /-! ### Round-by-round soundness -/ @@ -150,17 +151,15 @@ def RbrFrom : (s : Spec) → PerChallenge ProbComp s → PerChallenge (fun _ => ∀ c : C, RbrFrom s smp.2 ε.2 (fun p => S (some (c, p))) (fun τ => wins (c, τ)) /-- The output of a verifier without oracles on a complete transcript. -/ -noncomputable def Verifier.outputOn (V : Verifier emptySpec s StmtIn StmtOut) (x : StmtIn) +noncomputable def Verifier.outputOn (V : Verifier OracleSpec.empty s StmtIn StmtOut) (x : StmtIn) (τ : Transcript s) : Option StmtOut := OracleComp.interpret (m := Id) - (fun q => match q with - | .inl e => e.elim - | .inr q => Transcript.answer s τ q) + (OracleComp.sumHandler (fun e => e.elim) (Transcript.answer s τ)) (V.decide x (Transcript.challenges s τ)) /-- Round-by-round soundness in the plain model with per-round errors `ε`: some state function is false on the empty prefix of every `x ∉ langIn` and satisfies the round-by-round condition. -/ -def Verifier.RbrSound (V : Verifier emptySpec s StmtIn StmtOut) (langIn : Set StmtIn) +def Verifier.RbrSound (V : Verifier OracleSpec.empty s StmtIn StmtOut) (langIn : Set StmtIn) (langOut : Set StmtOut) (ε : PerChallenge (fun _ => ℝ≥0∞) s) : Prop := ∃ S : StmtIn → Prefix s → Prop, (∀ x ∉ langIn, ¬ S x (Prefix.empty s)) ∧ ∀ x, RbrFrom s V.samplers ε (S x) fun τ => ∃ x' ∈ langOut, V.outputOn x τ = some x' @@ -170,7 +169,7 @@ def Verifier.RbrSound (V : Verifier emptySpec s StmtIn StmtOut) (langIn : Set St /-- Honest-verifier zero knowledge with statistical error `ε` (perfect for `ε = 0`), in the plain model: on every `(x, w)` in `relIn`, the simulator's transcript law is `ε`-close to the honest one. -/ -def Reduction.HVZK (R : Reduction emptySpec emptySpec s StmtIn WitIn StmtOut WitOut) +def Reduction.HVZK (R : Reduction OracleSpec.empty OracleSpec.empty s StmtIn WitIn StmtOut WitOut) (relIn : StmtIn → WitIn → Prop) (Sim : StmtIn → ProbComp (Transcript s)) (ε : ℝ≥0∞) : Prop := ∀ x w, relIn x w → diff --git a/Complexity/Computability/Interactive/Sequential.lean b/Complexity/Computability/Interactive/Sequential.lean index 4c2aebe3b3..c70fd6f529 100644 --- a/Complexity/Computability/Interactive/Sequential.lean +++ b/Complexity/Computability/Interactive/Sequential.lean @@ -129,20 +129,16 @@ variable {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s₁ s₂ /-- Lift a decision on `s₁` to the composition. -/ def liftDecisionLeft {α : Type} (s₁ s₂ : Spec) : OracleComp (oV ⊕ₒ msgSpec s₁) α → OracleComp (oV ⊕ₒ msgSpec (s₁ ++ s₂)) α := - OracleComp.interpret fun q => match q with - | .inl q => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inl q) - | .inr q => OracleComp.interpret - (fun q' => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inr q')) - (liftMsgLeft s₁ s₂ q) + OracleComp.interpret <| OracleComp.sumHandler + (fun q => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inl q)) + fun q => OracleComp.liftRight (liftMsgLeft s₁ s₂ q) /-- Lift a decision on `s₂` to the composition. -/ def liftDecisionRight {α : Type} (s₁ s₂ : Spec) : OracleComp (oV ⊕ₒ msgSpec s₂) α → OracleComp (oV ⊕ₒ msgSpec (s₁ ++ s₂)) α := - OracleComp.interpret fun q => match q with - | .inl q => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inl q) - | .inr q => OracleComp.interpret - (fun q' => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inr q')) - (liftMsgRight s₁ s₂ q) + OracleComp.interpret <| OracleComp.sumHandler + (fun q => OracleComp.query (spec := oV ⊕ₒ msgSpec (s₁ ++ s₂)) (.inl q)) + fun q => OracleComp.liftRight (liftMsgRight s₁ s₂ q) /-- Sequential composition of verifiers: the second decides on the first one's output. -/ def Verifier.append (V₁ : Verifier oV s₁ S₁ S₂) (V₂ : Verifier oV s₂ S₂ S₃) : @@ -209,19 +205,17 @@ private theorem interpret_liftMsgRight : ∀ (s₁ s₂ : Spec) (τ : Transcript /-- The answers to the verifier's queries from a transcript, in the plain model. -/ -private def answerAll (s : Spec) (τ : Transcript s) : - (q : Empty ⊕ MsgQuery s) → (emptySpec ⊕ₒ msgSpec s) q - | .inl e => e.elim - | .inr q => Transcript.answer s τ q +private abbrev answerAll (s : Spec) (τ : Transcript s) : + (q : Empty ⊕ MsgQuery s) → (OracleSpec.empty ⊕ₒ msgSpec s) q := + OracleComp.sumHandler (m := Id) (fun e : Empty => e.elim) (Transcript.answer s τ) -private theorem outputOn_eq (V : Verifier emptySpec s₁ S₁ S₂) (x : S₁) (τ : Transcript s₁) : +private theorem outputOn_eq (V : Verifier OracleSpec.empty s₁ S₁ S₂) (x : S₁) (τ : Transcript s₁) : V.outputOn x τ = OracleComp.interpret (m := Id) (answerAll s₁ τ) - (V.decide x (Transcript.challenges s₁ τ)) := by - rw [Verifier.outputOn] - congr 1 + (V.decide x (Transcript.challenges s₁ τ)) := + rfl private theorem interpret_liftDecisionLeft {α : Type} (τ : Transcript (s₁ ++ s₂)) - (p : OracleComp (emptySpec ⊕ₒ msgSpec s₁) α) : + (p : OracleComp (OracleSpec.empty ⊕ₒ msgSpec s₁) α) : OracleComp.interpret (m := Id) (answerAll (s₁ ++ s₂) τ) (liftDecisionLeft s₁ s₂ p) = OracleComp.interpret (m := Id) (answerAll s₁ (Transcript.split s₁ s₂ τ).1) p := by rw [liftDecisionLeft] @@ -234,7 +228,7 @@ private theorem interpret_liftDecisionLeft {α : Type} (τ : Transcript (s₁ ++ exact interpret_liftMsgLeft s₁ s₂ τ q private theorem interpret_liftDecisionRight {α : Type} (τ : Transcript (s₁ ++ s₂)) - (p : OracleComp (emptySpec ⊕ₒ msgSpec s₂) α) : + (p : OracleComp (OracleSpec.empty ⊕ₒ msgSpec s₂) α) : OracleComp.interpret (m := Id) (answerAll (s₁ ++ s₂) τ) (liftDecisionRight s₁ s₂ p) = OracleComp.interpret (m := Id) (answerAll s₂ (Transcript.split s₁ s₂ τ).2) p := by rw [liftDecisionRight] @@ -247,7 +241,8 @@ private theorem interpret_liftDecisionRight {α : Type} (τ : Transcript (s₁ + exact interpret_liftMsgRight s₁ s₂ τ q /-- The composed verifier's output is the second verifier's output on the first one's. -/ -theorem outputOn_append (V₁ : Verifier emptySpec s₁ S₁ S₂) (V₂ : Verifier emptySpec s₂ S₂ S₃) +theorem outputOn_append (V₁ : Verifier OracleSpec.empty s₁ S₁ S₂) + (V₂ : Verifier OracleSpec.empty s₂ S₂ S₃) (x : S₁) (τ : Transcript (s₁ ++ s₂)) : (V₁.append V₂).outputOn x τ = (V₁.outputOn x (Transcript.split s₁ s₂ τ).1).bind @@ -334,8 +329,8 @@ private theorem rbrFrom_append : ∀ (s₁ s₂ : Spec) (smp₁ : PerChallenge P /-- **Round-by-round soundness composes**, with the concatenated per-round errors. -/ -theorem Verifier.RbrSound.append {V₁ : Verifier emptySpec s₁ S₁ S₂} - {V₂ : Verifier emptySpec s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} +theorem Verifier.RbrSound.append {V₁ : Verifier OracleSpec.empty s₁ S₁ S₂} + {V₂ : Verifier OracleSpec.empty s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} {ε₁ : PerChallenge (fun _ => ℝ≥0∞) s₁} {ε₂ : PerChallenge (fun _ => ℝ≥0∞) s₂} (h₁ : V₁.RbrSound L₁ L₂ ε₁) (h₂ : V₂.RbrSound L₂ L₃ ε₂) : (V₁.append V₂).RbrSound L₁ L₃ (PerChallenge.append s₁ s₂ ε₁ ε₂) := by @@ -374,9 +369,9 @@ end Rbr section Plain -variable {R₁ : Reduction emptySpec emptySpec s₁ S₁ W₁ S₂ W₂} - {R₂ : Reduction emptySpec emptySpec s₂ S₂ W₂ S₃ W₃} - {V₁ : Verifier emptySpec s₁ S₁ S₂} {V₂ : Verifier emptySpec s₂ S₂ S₃} +variable {R₁ : Reduction OracleSpec.empty OracleSpec.empty s₁ S₁ W₁ S₂ W₂} + {R₂ : Reduction OracleSpec.empty OracleSpec.empty s₂ S₂ W₂ S₃ W₃} + {V₁ : Verifier OracleSpec.empty s₁ S₁ S₂} {V₂ : Verifier OracleSpec.empty s₂ S₂ S₃} {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} {ε₁ ε₂ : ℝ≥0∞} @@ -384,7 +379,7 @@ variable {R₁ : Reduction emptySpec emptySpec s₁ S₁ W₁ S₂ W₂} the transcript, at the statement the first verifier outputs, then the input witness from the first half. The default intermediate statement `y₀` is used only when the first verifier rejects, when the composed verifier rejects too. -/ -noncomputable def Verifier.extractAppend (V₁ : Verifier emptySpec s₁ S₁ S₂) +noncomputable def Verifier.extractAppend (V₁ : Verifier OracleSpec.empty s₁ S₁ S₂) (E₁ : S₁ → Transcript s₁ → W₂ → W₁) (E₂ : S₂ → Transcript s₂ → W₃ → W₂) (y₀ : S₂) : S₁ → Transcript (s₁ ++ s₂) → W₃ → W₁ := fun x τ w₃ => E₁ x (Transcript.split s₁ s₂ τ).1 @@ -424,8 +419,8 @@ def ProverStrategy.bindLeaf {m : Type → Type} [Monad m] {α β : Type} : /-- Running a strategy continued by an effect at its end: the effect sees the transcript. -/ theorem plainLaw_bindLeaf_run : ∀ (s : Spec) (smp : PerChallenge ProbComp s) {α β : Type} - (st : ProverStrategy (ProbOracleComp emptySpec) s α) - (f : Transcript s → α → ProbOracleComp emptySpec β), + (st : ProverStrategy (ProbOracleComp OracleSpec.empty) s α) + (f : Transcript s → α → ProbOracleComp OracleSpec.empty β), plainLaw (ProverStrategy.bindLeaf s st f >>= runStrategy s smp) = (plainLaw (runStrategy s smp st)).bind fun r => (plainLaw (f r.1 r.2)).map fun b => (r.1, b) | [], _, _, _, a, f => by @@ -474,8 +469,9 @@ def ProverStrategy.split {m : Type → Type} [Monad m] {α : Type} : /-- Running a composed strategy runs the first part, then the continuation on its result. -/ theorem plainLaw_run_append : ∀ (s₁ s₂ : Spec) (smp₁ : PerChallenge ProbComp s₁) (smp₂ : PerChallenge ProbComp s₂) {α β : Type} - (st : ProverStrategy (ProbOracleComp emptySpec) s₁ α) - (next : α → ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s₂ β)), + (st : ProverStrategy (ProbOracleComp OracleSpec.empty) s₁ α) + (next : α → ProbOracleComp OracleSpec.empty + (ProverStrategy (ProbOracleComp OracleSpec.empty) s₂ β)), plainLaw (ProverStrategy.append s₁ s₂ st next >>= runStrategy (s₁ ++ s₂) (PerChallenge.append s₁ s₂ smp₁ smp₂)) = (plainLaw (runStrategy s₁ smp₁ st)).bind fun r₁ => @@ -515,7 +511,7 @@ theorem plainLaw_run_append : ∀ (s₁ s₂ : Spec) (smp₁ : PerChallenge Prob /-- Running any strategy for `s₁ ++ s₂` runs its split: the first part, then the rest. -/ theorem plainLaw_run_split : ∀ (s₁ s₂ : Spec) (smp₁ : PerChallenge ProbComp s₁) (smp₂ : PerChallenge ProbComp s₂) {α : Type} - (st : ProverStrategy (ProbOracleComp emptySpec) (s₁ ++ s₂) α), + (st : ProverStrategy (ProbOracleComp OracleSpec.empty) (s₁ ++ s₂) α), plainLaw (runStrategy (s₁ ++ s₂) (PerChallenge.append s₁ s₂ smp₁ smp₂) st) = (plainLaw (runStrategy s₁ smp₁ (ProverStrategy.split s₁ s₂ st))).bind fun r₁ => (plainLaw (runStrategy s₂ smp₂ r₁.2)).map @@ -572,8 +568,9 @@ section Compose /-- The honest run of a composed reduction runs the first reduction, then the second on the first prover's output. -/ -private theorem plainLaw_run_reductionAppend (R₁ : Reduction emptySpec emptySpec s₁ S₁ W₁ S₂ W₂) - (R₂ : Reduction emptySpec emptySpec s₂ S₂ W₂ S₃ W₃) (x : S₁) (w : W₁) : +private theorem plainLaw_run_reductionAppend + (R₁ : Reduction OracleSpec.empty OracleSpec.empty s₁ S₁ W₁ S₂ W₂) + (R₂ : Reduction OracleSpec.empty OracleSpec.empty s₂ S₂ W₂ S₃ W₃) (x : S₁) (w : W₁) : plainLaw ((R₁.append R₂).prover x w >>= runStrategy (s₁ ++ s₂) (R₁.append R₂).verifier.samplers) = (plainLaw (R₁.prover x w >>= runStrategy s₁ R₁.verifier.samplers)).bind fun r₁ => @@ -586,8 +583,8 @@ private theorem plainLaw_run_reductionAppend (R₁ : Reduction emptySpec emptySp simp only [plainLaw_bind] /-- **Completeness errors add up under sequential composition.** -/ -theorem Reduction.Complete.append {R₁ : Reduction emptySpec emptySpec s₁ S₁ W₁ S₂ W₂} - {R₂ : Reduction emptySpec emptySpec s₂ S₂ W₂ S₃ W₃} +theorem Reduction.Complete.append {R₁ : Reduction OracleSpec.empty OracleSpec.empty s₁ S₁ W₁ S₂ W₂} + {R₂ : Reduction OracleSpec.empty OracleSpec.empty s₂ S₂ W₂ S₃ W₃} {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {ε₁ ε₂ : ℝ≥0∞} (h₁ : R₁.Complete World.plain rel₁ rel₂ ε₁) (h₂ : R₂.Complete World.plain rel₂ rel₃ ε₂) : (R₁.append R₂).Complete World.plain rel₁ rel₃ (ε₁ + ε₂) := by @@ -608,9 +605,10 @@ theorem Reduction.Complete.append {R₁ : Reduction emptySpec emptySpec s₁ S /-- A run against a composed verifier is a run of the split strategy against the first, then of its continuation against the second. -/ -private theorem plainLaw_run_verifierAppend (V₁ : Verifier emptySpec s₁ S₁ S₂) - (V₂ : Verifier emptySpec s₂ S₂ S₃) {α : Type} - (P : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) (s₁ ++ s₂) α)) : +private theorem plainLaw_run_verifierAppend (V₁ : Verifier OracleSpec.empty s₁ S₁ S₂) + (V₂ : Verifier OracleSpec.empty s₂ S₂ S₃) {α : Type} + (P : ProbOracleComp OracleSpec.empty + (ProverStrategy (ProbOracleComp OracleSpec.empty) (s₁ ++ s₂) α)) : plainLaw (P >>= runStrategy (s₁ ++ s₂) (V₁.append V₂).samplers) = (plainLaw ((ProverStrategy.split s₁ s₂ ·) <$> P >>= runStrategy s₁ V₁.samplers)).bind fun r₁ => (plainLaw (runStrategy s₂ V₂.samplers r₁.2)).map @@ -622,11 +620,11 @@ private theorem plainLaw_run_verifierAppend (V₁ : Verifier emptySpec s₁ S₁ /-- **Soundness errors add up under sequential composition**, through the intermediate language. -/ -theorem Verifier.Sound.append {V₁ : Verifier emptySpec s₁ S₁ S₂} - {V₂ : Verifier emptySpec s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} - {ε₁ ε₂ : ℝ≥0∞} (h₁ : V₁.Sound (oP := emptySpec) World.plain L₁ L₂ ε₁) - (h₂ : V₂.Sound (oP := emptySpec) World.plain L₂ L₃ ε₂) : - (V₁.append V₂).Sound (oP := emptySpec) World.plain L₁ L₃ (ε₁ + ε₂) := by +theorem Verifier.Sound.append {V₁ : Verifier OracleSpec.empty s₁ S₁ S₂} + {V₂ : Verifier OracleSpec.empty s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} + {ε₁ ε₂ : ℝ≥0∞} (h₁ : V₁.Sound (oP := OracleSpec.empty) World.plain L₁ L₂ ε₁) + (h₂ : V₂.Sound (oP := OracleSpec.empty) World.plain L₂ L₃ ε₂) : + (V₁.append V₂).Sound (oP := OracleSpec.empty) World.plain L₁ L₃ (ε₁ + ε₂) := by intro x hx α P have hl₁ := h₁ x hx _ ((ProverStrategy.split s₁ s₂ ·) <$> P) rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hl₁ ⊢ @@ -656,8 +654,8 @@ theorem Verifier.Sound.append {V₁ : Verifier emptySpec s₁ S₁ S₂} /-- **Straight-line extractors compose**, with the sum of the knowledge errors. The first verifier's knowledge soundness is applied to a prover that simulates the second phase with the public samplers. -/ -theorem Verifier.KnowledgeSound.append {V₁ : Verifier emptySpec s₁ S₁ S₂} - {V₂ : Verifier emptySpec s₂ S₂ S₃} +theorem Verifier.KnowledgeSound.append {V₁ : Verifier OracleSpec.empty s₁ S₁ S₂} + {V₂ : Verifier OracleSpec.empty s₂ S₂ S₃} {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {ε₁ ε₂ : ℝ≥0∞} {E₁ : S₁ → Transcript s₁ → W₂ → W₁} {E₂ : S₂ → Transcript s₂ → W₃ → W₂} (h₁ : V₁.KnowledgeSound rel₁ rel₂ E₁ ε₁) @@ -687,7 +685,8 @@ theorem Verifier.KnowledgeSound.append {V₁ : Verifier emptySpec s₁ S₁ S₂ · exact Or.inr ⟨y, hy, ⟨x'', hy₂, hrel⟩, h⟩ refine le_trans (MeasureTheory.measure_mono hsub) (le_trans (MeasureTheory.measure_union_le _ _) (add_le_add ?_ ?_)) - · let P₁ : ProbOracleComp emptySpec (ProverStrategy (ProbOracleComp emptySpec) s₁ W₂) := + · let P₁ : ProbOracleComp OracleSpec.empty + (ProverStrategy (ProbOracleComp OracleSpec.empty) s₁ W₂) := (ProverStrategy.split s₁ s₂ ·) <$> P >>= fun st₁ => ProverStrategy.bindLeaf s₁ st₁ fun τ₁ st₂ => (fun r₂ => E₂ ((V₁.outputOn x τ₁).getD y₀) r₂.1 r₂.2) <$> runStrategy s₂ V₂.samplers st₂ @@ -766,18 +765,20 @@ variable {T U : Type} /-- The reduction without rounds is perfectly complete. -/ theorem Reduction.id_complete (rel : T → U → Prop) : - (Reduction.id (oP := emptySpec) (oV := emptySpec)).Complete World.plain rel rel 0 := by + (Reduction.id (oP := OracleSpec.empty) (oV := OracleSpec.empty)).Complete World.plain rel rel + 0 := by intro x w hxw rw [Reduction.run, World.plain_eval_execute, PMF.toOuterMeasure_map_apply] simp only [Reduction.id, runStrategy, bind_pure_comp, map_pure, plainLaw_pure, - Verifier.outputOn, Sum.elim_inl, OracleComp.interpret_pure, not_and, Set.preimage_ofPred_eq, + Verifier.outputOn, OracleComp.interpret_pure, not_and, Set.preimage_ofPred_eq, PMF.toOuterMeasure_pure_apply, Set.mem_ofPred_eq, hxw, not_true_eq_false, imp_false, nonpos_iff_eq_zero, ite_eq_right_iff, one_ne_zero, not_not] rfl /-- The reduction without rounds is round-by-round sound without error. -/ theorem Reduction.id_rbrSound (L : Set T) : - (Reduction.id (oP := emptySpec) (oV := emptySpec) (W := U)).verifier.RbrSound L L () := by + (Reduction.id (oP := OracleSpec.empty) (oV := OracleSpec.empty) (W := U)).verifier.RbrSound + L L () := by refine ⟨fun x _ => x ∈ L, fun x hx => hx, fun x hS ⟨x', hx', hout⟩ => hS ?_⟩ have : x = x' := Option.some.inj hout exact this ▸ hx' @@ -787,7 +788,8 @@ end Identity section Plain variable {s : ℕ → Spec} {S W : ℕ → Type} - {R : (i : ℕ) → Reduction emptySpec emptySpec (s i) (S i) (W i) (S (i + 1)) (W (i + 1))} + {R : (i : ℕ) → + Reduction OracleSpec.empty OracleSpec.empty (s i) (S i) (W i) (S (i + 1)) (W (i + 1))} /-- **Iterated completeness**: if every stage `R i` with `i < k` is complete from `rel i` to `rel (i + 1)` with error `ε i`, the first `k` stages are complete from `rel 0` to `rel k` with diff --git a/ComplexityTests/Interactive.lean b/ComplexityTests/Interactive.lean index fb997b0454..58563283c8 100644 --- a/ComplexityTests/Interactive.lean +++ b/ComplexityTests/Interactive.lean @@ -28,8 +28,9 @@ abbrev coinSpec : Spec := [.verifier Bool] def rel : Bool → Unit → Prop := fun x _ => x = true /-- The verifier sends a fair coin `c` and both parties continue with the claim `x || c`. -/ -noncomputable def coinStep : Reduction emptySpec emptySpec coinSpec Bool Unit Bool Unit where - prover x _ := pure (show Bool → ProbOracleComp emptySpec (Bool × Unit) from +noncomputable def coinStep : + Reduction OracleSpec.empty OracleSpec.empty coinSpec Bool Unit Bool Unit where + prover x _ := pure (show Bool → ProbOracleComp OracleSpec.empty (Bool × Unit) from fun c => pure (x || c, ())) verifier := { samplers := (ProbComp.uniform Bool, ()) @@ -62,7 +63,7 @@ theorem coinStep_rbrSound : /-- The coin round is sound with error `1 / 2`, by round-by-round soundness. -/ theorem coinStep_sound : - coinStep.verifier.Sound (oP := emptySpec) World.plain (language rel) (language rel) + coinStep.verifier.Sound (oP := OracleSpec.empty) World.plain (language rel) (language rel) (1 / 2) := by simpa [PerChallenge.sum] using coinStep_rbrSound.sound @@ -73,7 +74,7 @@ example : (coinStep.append coinStep).Complete World.plain rel rel 0 := by /-- Two coin rounds in sequence are sound with error `1`, by composition of round-by-round soundness; the composed errors are concatenated. -/ example : - (coinStep.append coinStep).verifier.Sound (oP := emptySpec) World.plain (language rel) + (coinStep.append coinStep).verifier.Sound (oP := OracleSpec.empty) World.plain (language rel) (language rel) (1 / 2 + 1 / 2) := by have h := (coinStep_rbrSound.append coinStep_rbrSound).sound simp only [PerChallenge.sum_append, PerChallenge.sum, add_zero] at h From 42f14250b859f2fd5117d9b7277cf4321efe114f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 04:40:27 -0400 Subject: [PATCH 7/7] chore(interactive): import the split PMF modules (#693) Plain and Sequential import Probability.PMF.Bind and .Event, and the tests Probability.PMF.Uniform, after the PMF hub split. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity/Computability/Interactive/Plain.lean | 2 ++ Complexity/Computability/Interactive/Sequential.lean | 2 ++ ComplexityTests/Interactive.lean | 1 + 3 files changed, 5 insertions(+) diff --git a/Complexity/Computability/Interactive/Plain.lean b/Complexity/Computability/Interactive/Plain.lean index 03de2ed08e..23a157b846 100644 --- a/Complexity/Computability/Interactive/Plain.lean +++ b/Complexity/Computability/Interactive/Plain.lean @@ -9,6 +9,8 @@ module public import Complexity.Computability.Interactive.Security import Complexity.Probability.PMF +import Complexity.Probability.PMF.Bind +import Complexity.Probability.PMF.Event /-! # Interactive reductions in the plain model diff --git a/Complexity/Computability/Interactive/Sequential.lean b/Complexity/Computability/Interactive/Sequential.lean index c70fd6f529..f7349ebd94 100644 --- a/Complexity/Computability/Interactive/Sequential.lean +++ b/Complexity/Computability/Interactive/Sequential.lean @@ -8,6 +8,8 @@ module -- upstream: candidate public import Complexity.Computability.Interactive.Plain +import Complexity.Probability.PMF.Bind +import Complexity.Probability.PMF.Event /-! # Sequential composition of interactive reductions diff --git a/ComplexityTests/Interactive.lean b/ComplexityTests/Interactive.lean index 58563283c8..c65d5d0c01 100644 --- a/ComplexityTests/Interactive.lean +++ b/ComplexityTests/Interactive.lean @@ -5,6 +5,7 @@ Authors: Samuel Schlesinger -/ import Complexity.Computability.Interactive.Sequential +import Complexity.Probability.PMF.Uniform /-! # Tests for interactive reductions