feat(Crypto, Interactive): efficient extractors and simulators

Complexity.lean

@@ -1469,6 +1469,7 @@ public import Complexity.Computability.Geometry.Orthogonal.Encoding
 public import Complexity.Computability.Geometry.Orthogonal.Subdivision
 public import Complexity.Computability.Interactive.Basic
 public import Complexity.Computability.Interactive.Bundle
+public import Complexity.Computability.Interactive.Efficient
 public import Complexity.Computability.Interactive.GKR.Layered
 public import Complexity.Computability.Interactive.GKR.Protocol
 public import Complexity.Computability.Interactive.GKR.Summand
@@ -2366,6 +2367,7 @@ public import Complexity.Crypto.Computational.PseudorandomFunction.TruthTable
 public import Complexity.Crypto.Computational.PseudorandomGenerator
 public import Complexity.Crypto.Computational.SIS.Basic
 public import Complexity.Crypto.Computational.SchnorrIdentification
+public import Complexity.Crypto.Computational.SchnorrProtocol
 public import Complexity.Crypto.Computational.Signature
 public import Complexity.Crypto.Computational.Stretch
 public import Complexity.Crypto.Computational.Stretch.Quantitative
@@ -2399,6 +2401,7 @@ public import Complexity.Crypto.Protocols.MPC.SharedMul
 public import Complexity.Crypto.Protocols.SigmaProtocol.Abort
 public import Complexity.Crypto.Protocols.SigmaProtocol.Basic
 public import Complexity.Crypto.Protocols.SigmaProtocol.Composition
+public import Complexity.Crypto.Protocols.SigmaProtocol.Efficient
 public import Complexity.Crypto.Protocols.SigmaProtocol.FiatShamir
 public import Complexity.Crypto.Protocols.SigmaProtocol.Identification
 public import Complexity.Crypto.Protocols.SigmaProtocol.Linear

Complexity/Computability/Interactive/Efficient.lean

@@ -0,0 +1,139 @@
+/-
+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
+public import Complexity.Computability.Probabilistic.PPT
+
+/-!
+# Efficient extractors and simulators for interactive reductions
+
+`Interactive.Verifier.KnowledgeSound` and `Interactive.Reduction.HVZK` name their extractor and
+simulator but place no efficiency requirement on them. Without one, knowledge soundness says no
+more than soundness, and HVZK says no more than honest-verifier witness indistinguishability
+(test modules `ComplexityTests.InteractiveKnowledgeSound` and
+`ComplexityTests.UnboundedSimulators`). This module adds the efficient variants.
+
+Efficiency is uniform over a family of reductions indexed by `i : I`, typically a unary security
+parameter together with a system parameter. Statements, witnesses and protocol shapes may depend
+on the index, so the algorithms are certified on words, through the encodings collected in an
+`Interactive.Encoding`.
+
+* `Verifier.EfficientKnowledgeSound V relIn relOut enc encOut encIn E ε`: at every index `E i` is
+  a straight-line extractor with error `ε i`, and one deterministic polynomial-time function of
+  words computes the whole family (`ExtractorRealizedBy`).
+* `Reduction.EfficientHVZK R rel enc Sim ε δ`: at every index `Sim i` is an `ε i`-HVZK simulator,
+  and one uniform strict PPT program realizes the whole family on encoded transcripts up to
+  statistical distance `δ i` (`SimulatorRealizedBy`). A typed simulator may sample from
+  distributions, such as uniform field elements, that a strict PPT machine with fair coins
+  samples only approximately; `δ` accounts for that.
+
+Both variants contain the exact property at every index with the same extractor or simulator, so
+every theorem about `KnowledgeSound` and `HVZK` applies to them; the realizing program of an
+efficient simulator is `ε i + δ i`-close to honest transcripts
+(`SimulatorRealizedBy.closeTo_run`). Extraction here is straight-line, from the transcript, as for
+interactive oracle proofs; rewinding extractors in the sense of Bellare and Goldreich are a
+different notion, as are malicious-verifier zero knowledge and computational zero knowledge.
+
+## Main definitions
+
+* `Interactive.Encoding`: word encodings of an indexed family of reductions.
+* `Interactive.ExtractorRealizedBy`, `Interactive.SimulatorRealizedBy`: a word function or program
+  computes an extractor or simulator family on encodings.
+* `Interactive.Verifier.EfficientKnowledgeSound`: knowledge soundness with a polynomial-time
+  extractor.
+* `Interactive.Reduction.EfficientHVZK`: HVZK with a strict PPT simulator, up to `δ`.
+
+## Main results
+
+* `Interactive.SimulatorRealizedBy.closeTo_run`: the realizing program of an efficient simulator
+  is `ε i + δ i`-close to the honest encoded transcript.
+-/
+
+@[expose] public section
+
+namespace Cslib.Interactive
+
+open scoped ENNReal
+open Spec Probability Turing.MultiTapeTM
+
+/-- Word encodings for a family of reductions indexed by `I`, with rounds `s i` and input
+statements in `Stmt i` at the index `i`. -/
+structure Encoding (I : Type) (s : I → Spec) (Stmt : I → Type) where
+  /-- The index, such as a unary security parameter with a system parameter. -/
+  index : I ↪ List Bool
+  /-- The input statements at each index. -/
+  statement : ∀ i, Stmt i ↪ List Bool
+  /-- The transcripts at each index. -/
+  transcript : ∀ i, Transcript (s i) ↪ List Bool
+
+variable {I : Type} {s : I → Spec} {StmtIn WitIn StmtOut WitOut : I → Type}
+
+/-- The word function `f` computes the extractor family `E` on encodings: from the index, the
+encoded statement, the encoded transcript and the encoded output witness, it returns the encoded
+input witness. -/
+def ExtractorRealizedBy (enc : Encoding I s StmtIn) (encOut : ∀ i, WitOut i ↪ List Bool)
+    (encIn : ∀ i, WitIn i ↪ List Bool) (E : ∀ i, StmtIn i → Transcript (s i) → WitOut i → WitIn i)
+    (f : I × List Bool × List Bool × List Bool → List Bool) : Prop :=
+  ∀ i x τ w, f (i, enc.statement i x, enc.transcript i τ, encOut i w) = encIn i (E i x τ w)
+
+/-- The program `program` realizes the simulator family `Sim` on encodings up to statistical
+distance `δ`: on the index and the encoded statement, its output is within `δ i` of the encoded
+transcript sampled by `Sim i`. -/
+def SimulatorRealizedBy (enc : Encoding I s StmtIn)
+    (Sim : ∀ i, StmtIn i → ProbComp (Transcript (s i)))
+    (program : I × List Bool → ProbComp (List Bool)) (δ : I → ℝ≥0∞) : Prop :=
+  ∀ i x, CloseTo ((ProbComp.eval (Sim i x)).map (enc.transcript i))
+    (ProbComp.eval (program (i, enc.statement i x))) (δ i)
+
+/-- **Efficient straight-line knowledge soundness.** At every index, `E i` is a straight-line
+extractor for `V i` with error `ε i`, in the plain model, and one deterministic polynomial-time
+function of the index and words computes the whole family on encodings. -/
+structure Verifier.EfficientKnowledgeSound
+    (V : ∀ i, Verifier OracleSpec.empty (s i) (StmtIn i) (StmtOut i))
+    (relIn : ∀ i, StmtIn i → WitIn i → Prop) (relOut : ∀ i, StmtOut i → WitOut i → Prop)
+    (enc : Encoding I s StmtIn) (encOut : ∀ i, WitOut i ↪ List Bool)
+    (encIn : ∀ i, WitIn i ↪ List Bool) (E : ∀ i, StmtIn i → Transcript (s i) → WitOut i → WitIn i)
+    (ε : I → ℝ≥0∞) : Prop where
+  /-- `E i` is a straight-line extractor with error `ε i` at every index. -/
+  knowledgeSound : ∀ i, (V i).KnowledgeSound (relIn i) (relOut i) (E i) (ε i)
+  /-- One polynomial-time word function computes the extractor family. -/
+  polyTime : ∃ f, ComputableInPolyTime f
+    (encPair enc.index (encPair encBits (encPair encBits encBits))) encBits ∧
+    ExtractorRealizedBy enc encOut encIn E f
+
+/-- **Efficient honest-verifier zero knowledge**, with simulation error `ε` and realization error
+`δ`. At every index, `Sim i` is an `ε i`-HVZK simulator for `R i`, in the plain model, and one
+uniform strict PPT program of the index and the encoded statement realizes the whole family on
+encoded transcripts up to `δ`. -/
+structure Reduction.EfficientHVZK
+    (R : ∀ i, Reduction OracleSpec.empty OracleSpec.empty (s i) (StmtIn i) (WitIn i) (StmtOut i)
+      (WitOut i))
+    (rel : ∀ i, StmtIn i → WitIn i → Prop) (enc : Encoding I s StmtIn)
+    (Sim : ∀ i, StmtIn i → ProbComp (Transcript (s i))) (ε δ : I → ℝ≥0∞) : Prop where
+  /-- `Sim i` is an `ε i`-HVZK simulator at every index. -/
+  hvzk : ∀ i, (R i).HVZK (rel i) (Sim i) (ε i)
+  /-- One uniform strict PPT program realizes the simulator family up to `δ`. -/
+  realized : ∃ program, IsPPTOn (encPair enc.index encBits) encBits program ∧
+    SimulatorRealizedBy enc Sim program δ
+
+/-- A program realizing an `ε`-HVZK simulator up to `δ` is `ε i + δ i`-close to the honest encoded
+transcript, for every statement and valid witness. -/
+theorem SimulatorRealizedBy.closeTo_run
+    {R : ∀ i, Reduction OracleSpec.empty OracleSpec.empty (s i) (StmtIn i) (WitIn i) (StmtOut i)
+      (WitOut i)}
+    {rel : ∀ i, StmtIn i → WitIn i → Prop} {enc : Encoding I s StmtIn}
+    {Sim : ∀ i, StmtIn i → ProbComp (Transcript (s i))}
+    {program : I × List Bool → ProbComp (List Bool)} {ε δ : I → ℝ≥0∞}
+    (hzk : ∀ i, (R i).HVZK (rel i) (Sim i) (ε i)) (h : SimulatorRealizedBy enc Sim program δ)
+    {i : I} {x : StmtIn i} {w : WitIn i} (hxw : rel i x w) :
+    CloseTo (((World.plain.eval ((R i).run x w)).map Prod.fst).map (enc.transcript i))
+      (ProbComp.eval (program (i, enc.statement i x))) (ε i + δ i) :=
+  ((hzk i x w hxw).map (enc.transcript i)).trans (h i x)
+
+end Cslib.Interactive

Complexity/Computability/Interactive/Security.lean

@@ -38,7 +38,9 @@ the prover, are a different notion. Knowledge soundness and zero knowledge are s
 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.
+efficiency is a separate layer: `Verifier.EfficientKnowledgeSound` and `Reduction.EfficientHVZK`
+in `Complexity.Computability.Interactive.Efficient` add a polynomial-time extractor and a strict
+PPT simulator over an indexed family of reductions.
 
 ## Main definitions
 
@@ -108,7 +110,8 @@ def Verifier.Sound (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 `ε`. -/
+transcript and the output witness, except with probability `ε`. The extractor is an arbitrary
+function; `Verifier.EfficientKnowledgeSound` adds the efficiency requirement. -/
 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 :=
@@ -169,7 +172,8 @@ def Verifier.RbrSound (V : Verifier OracleSpec.empty s StmtIn StmtOut) (langIn :
 
 /-- 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. -/
+one. The simulator need not be efficient; `Reduction.EfficientHVZK` adds the efficiency
+requirement. -/
 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 :=

Complexity/Crypto/Computational/SchnorrIdentification.lean

@@ -62,6 +62,9 @@ exactly, which matters for the honest prover and for simulation but not for this
 
 * `Cslib.Crypto.PrimeOrderGroupFamily.succProbability_schnorrDirectGame_le`: `ε ≤ 1 / 2 ^ k + √ε'`
   at each security parameter.
+* `Cslib.Crypto.PrimeOrderGroupFamily.extractNat_cast`,
+  `Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_extractNat`: the extracted witness is
+  `(c - c')⁻¹ (z - z')` modulo `q`, and is computable in polynomial time.
 * `Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_rewind`: the rewinding adversary is uniform strict
   PPT.
 * `Cslib.Crypto.PrimeOrderGroupFamily.negligible_schnorrDirectGame`: Schnorr identification is
@@ -142,8 +145,9 @@ private theorem challenge_ne {q k : ℕ} (hkq : 2 ^ k ≤ q) {c c' : BitString k
     Nat.mod_eq_of_lt ((BitString.lsbValue_lt _).trans_le (by simpa using hkq))] at h
   exact hc (List.ofFn_injective (BitString.lsbValue_injective (by simp) h))
 
-/-- Fermat's little theorem gives the inverse in `extractNat`. -/
-private theorem extractNat_cast {q : ℕ} [Fact q.Prime] {c z c' z' : ℕ}
+/-- Fermat's little theorem gives the inverse in `extractNat`: modulo a prime `q`, it is
+`(c - c')⁻¹ (z - z')` whenever `c` and `c'` are distinct modulo `q`. -/
+theorem extractNat_cast {q : ℕ} [Fact q.Prime] {c z c' z' : ℕ}
     (hc : (c : ZMod q) ≠ c') :
     (extractNat q c z c' z' : ZMod q) = ((c : ZMod q) - c')⁻¹ * ((z : ZMod q) - z') := by
   have hsub (a b : ℕ) : (((a % q + q - b % q) % q : ℕ) : ZMod q) = (a : ZMod q) - b := by
@@ -285,6 +289,16 @@ private theorem computableTidilyInPolyTime_extractNat {α : Type} {input : α 
 
 attribute [local fun_prop] computableTidilyInPolyTime_extractNat
 
+/-- The extracted witness `extractNat` is computable in polynomial time from the group description
+and the four binary numbers. -/
+theorem computableInPolyTime_extractNat {α : Type} {input : α ↪ List Bool}
+    {d : α → F.Desc} {c z c' z' : α → ℕ} (hd : ComputableInPolyTime d input F.encDesc)
+    (hc : ComputableInPolyTime c input encNat) (hz : ComputableInPolyTime z input encNat)
+    (hc' : ComputableInPolyTime c' input encNat) (hz' : ComputableInPolyTime z' input encNat) :
+    ComputableInPolyTime (fun a => extractNat (F.order (d a)) (c a) (z a) (c' a) (z' a))
+      input encNat :=
+  .of_tidy (computableTidilyInPolyTime_extractNat hd.tidy hc.tidy hz.tidy hc'.tidy hz'.tidy)
+
 /-- **The rewinding adversary is uniform strict PPT** when the impersonator is and the challenge
 length is computable in polynomial time. -/
 theorem isPPTOn_rewind {k : ℕ → ℕ} (hk : ComputableInPolyTime k encUnary encUnary)