diff --git a/Complexity.lean b/Complexity.lean
index 69ba19053..29b77b0a4 100644
--- a/Complexity.lean
+++ b/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
diff --git a/Complexity/Computability/Interactive/Efficient.lean b/Complexity/Computability/Interactive/Efficient.lean
new file mode 100644
index 000000000..facb7fc68
--- /dev/null
+++ b/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
diff --git a/Complexity/Computability/Interactive/Security.lean b/Complexity/Computability/Interactive/Security.lean
index 4a1e2d3ff..ad419f73e 100644
--- a/Complexity/Computability/Interactive/Security.lean
+++ b/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 :=
diff --git a/Complexity/Crypto/Computational/SchnorrIdentification.lean b/Complexity/Crypto/Computational/SchnorrIdentification.lean
index b1c1809d9..1dcfe0214 100644
--- a/Complexity/Crypto/Computational/SchnorrIdentification.lean
+++ b/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)
diff --git a/Complexity/Crypto/Computational/SchnorrProtocol.lean b/Complexity/Crypto/Computational/SchnorrProtocol.lean
new file mode 100644
index 000000000..69e7cb9d6
--- /dev/null
+++ b/Complexity/Crypto/Computational/SchnorrProtocol.lean
@@ -0,0 +1,289 @@
+/-
+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.Crypto.Computational.DiffieHellman
+public import Complexity.Crypto.Computational.SchnorrIdentification
+public import Complexity.Crypto.Protocols.SigmaProtocol.Efficient
+public import Complexity.Crypto.Protocols.SigmaProtocol.Linear
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
+import Complexity.Probability.PMF
+import Complexity.Tactic.PPT
+
+/-!
+# Schnorr's Sigma protocol with an efficient extractor and simulator
+
+Schnorr's Sigma protocol ([BonehShoup2023], Example 19.1) over a `PrimeOrderGroupFamily`, as a
+family indexed by a unary security parameter `n` and a group description `d`, with challenges in
+`ZMod q` for the group order `q`. Group elements are encoded by the family's encoding and scalars
+in binary (`schnorrEncoding`).
+
+* **Efficient special soundness** (`efficientSpecialSoundness_schnorr`, Example 19.2): the
+  extractor `schnorrExtract` computes `(c - c')⁻¹ (z - z')` with `extractNat`, inverting by
+  Fermat's little theorem, in polynomial time.
+* **Efficient special HVZK** (`efficientSpecialHVZK_schnorr`, Example 19.3): Boneh and Shoup's
+  simulator samples a uniform response `z` and outputs `(z • g - c • u, z)`. The strict PPT
+  program `schnorrSimulateWord` samples `z` with `sampleExp`, which is within statistical
+  distance `1 / 2 ^ n` of uniform on `ZMod q`, so it realizes the simulator up to `1 / 2 ^ n`.
+
+The protocol does not depend on the security parameter; only the simulator's sampling error does.
+
+## Main definitions
+
+* `Cslib.Crypto.PrimeOrderGroupFamily.schnorrFamily`: Schnorr's Sigma protocol at each index.
+* `Cslib.Crypto.PrimeOrderGroupFamily.schnorrEncoding`: its word encodings.
+* `Cslib.Crypto.PrimeOrderGroupFamily.schnorrExtract`: the extractor, computed with `extractNat`.
+* `Cslib.Crypto.PrimeOrderGroupFamily.schnorrSimulateWord`: the simulator as a strict PPT program
+  on words.
+
+## Main results
+
+* `Cslib.Crypto.PrimeOrderGroupFamily.efficientSpecialSoundness_schnorr`: efficient special
+  soundness.
+* `Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_schnorrSimulateWord`,
+  `Cslib.Crypto.PrimeOrderGroupFamily.simulatorRealizedBy_schnorrSimulateWord`: the simulator
+  program is strict PPT and realizes Boneh and Shoup's simulator up to `1 / 2 ^ n`.
+* `Cslib.Crypto.PrimeOrderGroupFamily.efficientSpecialHVZK_schnorr`: efficient special HVZK with
+  statistical error `1 / 2 ^ n`.
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Examples 19.1–19.3 and Definitions 19.4–19.5.
+* [C.-P. Schnorr, *Efficient Signature Generation by Smart Cards*][Schnorr1991]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PrimeOrderGroupFamily
+
+open Probability Turing.MultiTapeTM Protocols Protocols.SigmaProtocol Interactive
+open scoped ENNReal NNReal
+
+variable (F : PrimeOrderGroupFamily)
+
+/-- Group elements as words, through the family's injective encoding. -/
+def encodeEmbedding (d : F.Desc) : F.Carrier d ↪ List Bool :=
+  ⟨F.encode d, F.encode_injective d⟩
+
+/-- Scalars modulo the group order as binary numbers, through their least nonnegative
+representatives. -/
+def encScalar (d : F.Desc) : ZMod (F.order d) ↪ List Bool :=
+  ⟨fun a => encNat a.val, encNat.injective.comp (ZMod.val_injective _)⟩
+
+/-- Equality of group elements, decided on their encodings. -/
+instance (d : F.Desc) : DecidableEq (F.Carrier d) := fun a b =>
+  decidable_of_iff (F.encode d a = F.encode d b) (F.encode_injective d).eq_iff
+
+/-- Schnorr's Sigma protocol ([BonehShoup2023], Example 19.1) in the group described by `i.2`,
+with challenges in `ZMod q`. The security parameter `i.1` does not change the protocol. -/
+noncomputable def schnorrFamily (i : ℕ × F.Desc) :
+    SigmaProtocol (ZMod (F.order i.2)) (F.Carrier i.2) (F.Carrier i.2) (ZMod (F.order i.2))
+      (ZMod (F.order i.2)) :=
+  schnorr (Function.Embedding.refl _) (F.generator i.2)
+
+/-- The word encodings of `schnorrFamily`: the unary security parameter with the description,
+group elements by the family's encoding, and challenges and responses in binary. -/
+def schnorrEncoding :
+    Encoding (ℕ × F.Desc) (fun i => F.Carrier i.2) (fun i => F.Carrier i.2)
+      (fun i => ZMod (F.order i.2)) (fun i => ZMod (F.order i.2)) where
+  index := encPair encUnary F.encDesc
+  statement i := F.encodeEmbedding i.2
+  commitment i := F.encodeEmbedding i.2
+  challenge i := F.encScalar i.2
+  response i := F.encScalar i.2
+
+/-- Schnorr's extractor ([BonehShoup2023], Example 19.2), computed with `extractNat`: it is
+`(c - c')⁻¹ (z - z')` whenever `c ≠ c'`. -/
+def schnorrExtract (i : ℕ × F.Desc) (_ _ : F.Carrier i.2) (c z c' z' : ZMod (F.order i.2)) :
+    ZMod (F.order i.2) :=
+  extractNat (F.order i.2) c.val z.val c'.val z'.val
+
+/-- Schnorr's simulator on words ([BonehShoup2023], Example 19.3): on the index `(n, d)`, an
+encoded statement `u` and a binary challenge `c`, sample `s` with `sampleExp n d` and return the
+encodings of `s • g - c • u` and of `s mod q`. -/
+noncomputable def schnorrSimulateWord :
+    (ℕ × F.Desc) × List Bool × List Bool → ProbComp (List Bool × List Bool)
+  | ((n, d), u, c) => do
+    let s ← F.sampleExp n d
+    return (F.add (d, F.smul (d, s, F.encode d (F.generator d)),
+        F.smul (d, F.order d - ofBits c % F.order d, u)),
+      (s % F.order d).bits)
+
+/-! ### Special soundness -/
+
+/-- **Schnorr's protocol has efficient special soundness** ([BonehShoup2023], Example 19.2). -/
+theorem efficientSpecialSoundness_schnorr :
+    EfficientSpecialSoundness F.schnorrFamily (fun i α u => α • F.generator i.2 = u)
+      F.schnorrEncoding (fun i => F.encScalar i.2) F.schnorrExtract where
+  specialSoundness i u t c z c' z' hc hz hz' := by
+    have hcast : ((c.val : ℕ) : ZMod (F.order i.2)) ≠ (c'.val : ℕ) := by
+      simpa only [ZMod.natCast_zmod_val] using hc
+    have h := schnorr_specialSoundness (ι := Function.Embedding.refl _) u t c z c' z' hc hz hz'
+    simp only [linearExtract, Function.Embedding.refl_apply, smul_eq_mul] at h
+    simp only [schnorrExtract, extractNat_cast hcast, ZMod.natCast_zmod_val]
+    exact h
+  polyTime := by
+    let encIn := encPair (encPair encUnary F.encDesc) (encPair encBits (encPair encBits
+      (encPair encBits (encPair encBits (encPair encBits encBits)))))
+    refine ⟨fun p => (extractNat (F.order p.1.2) (ofBits p.2.2.2.1) (ofBits p.2.2.2.2.1)
+      (ofBits p.2.2.2.2.2.1) (ofBits p.2.2.2.2.2.2)).bits, ?_, ?_⟩
+    · have hd : ComputableInPolyTime
+          (fun p : (ℕ × F.Desc) × List Bool × List Bool × List Bool × List Bool × List Bool ×
+            List Bool => p.1.2) encIn F.encDesc := by fun_prop
+      have hword {k : (ℕ × F.Desc) × List Bool × List Bool × List Bool × List Bool × List Bool ×
+          List Bool → List Bool} (hk : ComputableInPolyTime k encIn encBits) :
+          ComputableInPolyTime (fun p => ofBits (k p)) encIn encNat :=
+        .of_tidy (ComputableTidilyInPolyTime.bitsToNat.comp hk.tidy)
+      have hext := computableInPolyTime_extractNat hd
+        (hword (k := fun p => p.2.2.2.1) (by fun_prop))
+        (hword (k := fun p => p.2.2.2.2.1) (by fun_prop))
+        (hword (k := fun p => p.2.2.2.2.2.1) (by fun_prop))
+        (hword (k := fun p => p.2.2.2.2.2.2) (by fun_prop))
+      exact .of_tidy (ComputableTidilyInPolyTime.natBits.comp hext.tidy)
+    · intro i u t c z c' z'
+      simp only [schnorrEncoding, encScalar, encodeEmbedding, Function.Embedding.coeFn_mk,
+        encNat_apply, ofBits, Nat.foldr_bit_bits, schnorrExtract, ZMod.val_natCast, extractNat,
+        Nat.mod_mod]
+
+/-! ### Special HVZK -/
+
+open Classical in
+/-- A bound on the advantage of every event test gives statistical closeness. -/
+private theorem closeTo_of_advantage_le {α : Type} {μ ν : PMF α} {ε : ℝ≥0}
+    (h : ∀ E : Set α, Game.advantage (ν.map fun a => decide (a ∈ E))
+      (μ.map fun a => decide (a ∈ E)) ≤ ε) :
+    CloseTo μ ν ε := by
+  intro E
+  have hmap (p : PMF α) : (p.map fun a => decide (a ∈ E)) true = p.toOuterMeasure E := by
+    rw [← PMF.toOuterMeasure_apply_singleton, PMF.toOuterMeasure_map_apply]
+    congr 1
+    ext a
+    simp
+  have hle : Game.succProbability (μ.map fun a => decide (a ∈ E)) ≤
+      Game.succProbability (ν.map fun a => decide (a ∈ E)) + ε := by
+    refine tsub_le_iff_left.mp (le_trans ?_ (h E))
+    rw [Game.advantage, NNReal.nndist_eq]
+    exact le_max_right _ _
+  have hcoe (p : PMF α) : ((Game.succProbability (p.map fun a => decide (a ∈ E)) : ℝ≥0) :
+      ℝ≥0∞) = p.toOuterMeasure E := by
+    rw [Game.succProbability, ENNReal.coe_toNNReal (PMF.apply_ne_top _ _), hmap]
+  rw [← hcoe μ, ← hcoe ν]
+  exact_mod_cast hle
+
+open Classical in
+/-- An exponent sampled by `sampleExp n d` is within statistical distance `1 / 2 ^ n` of
+uniform on `ZMod q`. -/
+private theorem closeTo_uniform_sampleExp (n : ℕ) (d : F.Desc) :
+    CloseTo (PMF.uniformOfFintype (ZMod (F.order d)))
+      ((ProbComp.eval (F.sampleExp n d)).map (Nat.cast : ℕ → ZMod (F.order d)))
+      (1 / 2 ^ n : ℝ≥0) := by
+  refine closeTo_of_advantage_le fun E => ?_
+  have h := F.advantage_bind_sampleExp_le n d fun a => PMF.pure (decide (a ∈ E))
+  rw [PMF.map_comp, ← PMF.bind_pure_comp, ← PMF.bind_pure_comp]
+  exact h
+
+/-- The law of `schnorrSimulateWord` on an encoded statement and challenge: a sampled exponent,
+read modulo `q`, is the response `z`, and the commitment is `z • g - c • u`. -/
+private theorem eval_schnorrSimulateWord (n : ℕ) (d : F.Desc) (u : F.Carrier d)
+    (c : ZMod (F.order d)) :
+    ProbComp.eval (F.schnorrSimulateWord ((n, d), F.encode d u, encNat c.val)) =
+      ((ProbComp.eval (F.sampleExp n d)).map (Nat.cast : ℕ → ZMod (F.order d))).map
+        fun z => (F.encode d (z • F.generator d - c • u), encNat z.val) := by
+  have hneg : ((F.order d - c.val % F.order d : ℕ) : ZMod (F.order d)) = -c := by
+    rw [Nat.mod_eq_of_lt (ZMod.val_lt c), Nat.cast_sub (ZMod.val_lt c).le, ZMod.natCast_self,
+      ZMod.natCast_zmod_val, zero_sub]
+  rw [schnorrSimulateWord, ProbComp.eval_bind, PMF.map_comp]
+  simp only [ProbComp.eval_pure, encNat_apply, ofBits, Nat.foldr_bit_bits, F.smul_encode,
+    F.add_encode, hneg,
+    neg_smul, ← sub_eq_add_neg]
+  rw [← PMF.bind_pure_comp]
+  congr 1
+  funext a
+  simp only [Function.comp_apply, ZMod.val_natCast]
+
+/-- `schnorrSimulateWord` is uniform strict PPT in the security parameter, the description and the
+encoded statement and challenge. -/
+theorem isPPTOn_schnorrSimulateWord :
+    IsPPTOn (encPair (encPair encUnary F.encDesc) (encPair encBits encBits))
+      (encPair encBits encBits) F.schnorrSimulateWord := by
+  let encIn := encPair (encPair encUnary F.encDesc) (encPair encBits encBits)
+  have hn : ComputableInPolyTime (fun p : (ℕ × F.Desc) × List Bool × List Bool => p.1.1)
+      encIn encUnary := by fun_prop
+  have hd : ComputableInPolyTime (fun p : (ℕ × F.Desc) × List Bool × List Bool => p.1.2)
+      encIn F.encDesc := by fun_prop
+  change IsPPTOn encIn _ fun p => F.sampleExp p.1.1 p.1.2 >>= fun s =>
+    pure (F.add (p.1.2, F.smul (p.1.2, s, F.encode p.1.2 (F.generator p.1.2)),
+        F.smul (p.1.2, F.order p.1.2 - ofBits p.2.2 % F.order p.1.2, p.2.1)),
+      (s % F.order p.1.2).bits)
+  refine (F.isPPTOn_sampleExp hn hd).bind_with ?_
+  let encMid := encPair encIn encNat
+  have hd' : ComputableInPolyTime (fun p : ((ℕ × F.Desc) × List Bool × List Bool) × ℕ =>
+      p.1.1.2) encMid F.encDesc := by fun_prop
+  have hs : ComputableInPolyTime (fun p : ((ℕ × F.Desc) × List Bool × List Bool) × ℕ =>
+      p.2) encMid encNat := by fun_prop
+  have hu : ComputableInPolyTime (fun p : ((ℕ × F.Desc) × List Bool × List Bool) × ℕ =>
+      p.1.2.1) encMid encBits := by fun_prop
+  have hc : ComputableInPolyTime (fun p : ((ℕ × F.Desc) × List Bool × List Bool) × ℕ =>
+      p.1.2.2) encMid encBits := by fun_prop
+  have hq := F.computableInPolyTime_order.comp hd'
+  have hg := F.computableInPolyTime_generator.comp hd'
+  have hsg := F.computableInPolyTime_smul.comp (hd'.prod (hs.prod hg))
+  have hneg : ComputableInPolyTime
+      (fun p : ((ℕ × F.Desc) × List Bool × List Bool) × ℕ =>
+        F.order p.1.1.2 - ofBits p.1.2.2 % F.order p.1.1.2) encMid encNat :=
+    .of_tidy (.binary_sub' hq.tidy (.binary_mod'
+      (ComputableTidilyInPolyTime.bitsToNat.comp hc.tidy) hq.tidy))
+  have hcu := F.computableInPolyTime_smul.comp (hd'.prod (hneg.prod hu))
+  have ht := F.computableInPolyTime_add.comp (hd'.prod (hsg.prod hcu))
+  have hz : ComputableInPolyTime
+      (fun p : ((ℕ × F.Desc) × List Bool × List Bool) × ℕ =>
+        (p.2 % F.order p.1.1.2).bits) encMid encBits :=
+    .of_tidy (ComputableTidilyInPolyTime.natBits.comp (.binary_mod' hs.tidy hq.tidy))
+  exact (ht.prod hz).isPPTOn
+
+/-- `schnorrSimulateWord` realizes Schnorr's perfect simulator `linearSimulate`
+([BonehShoup2023], Example 19.3) up to statistical distance `1 / 2 ^ n` at security parameter
+`n`. -/
+theorem simulatorRealizedBy_schnorrSimulateWord :
+    SimulatorRealizedBy F.schnorrEncoding
+      (fun i => linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod (F.order i.2))
+        (F.Carrier i.2) (F.generator i.2)) id (Function.Embedding.refl _))
+      F.schnorrSimulateWord (fun i => 1 / 2 ^ i.1) := by
+  intro i u c
+  rw [show (F.schnorrEncoding.statement i) u = F.encode i.2 u from rfl,
+    show (F.schnorrEncoding.challenge i) c = encNat c.val from rfl,
+    eval_schnorrSimulateWord]
+  have hsim : (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod (F.order i.2))
+      (F.Carrier i.2) (F.generator i.2)) id (Function.Embedding.refl _) u c).map
+        (Prod.map (F.schnorrEncoding.commitment i) (F.schnorrEncoding.response i)) =
+      (PMF.uniformOfFintype (ZMod (F.order i.2))).map
+        fun z => (F.encode i.2 (z • F.generator i.2 - c • u), encNat z.val) := by
+    rw [linearSimulate, PMF.map_comp]
+    rfl
+  have hδ : (((1 / 2 ^ i.1 : ℝ≥0)) : ℝ≥0∞) = 1 / 2 ^ i.1 := by
+    rw [ENNReal.coe_div (pow_ne_zero _ two_ne_zero), ENNReal.coe_one, ENNReal.coe_pow,
+      ENNReal.coe_ofNat]
+  dsimp only
+  rw [hsim, ← hδ]
+  exact (F.closeTo_uniform_sampleExp i.1 i.2).map _
+
+/-- **Schnorr's protocol has efficient special HVZK** ([BonehShoup2023], Example 19.3), with
+statistical error `1 / 2 ^ n` at security parameter `n`: the perfect simulator `linearSimulate` is
+realized by the strict PPT program `schnorrSimulateWord`. -/
+theorem efficientSpecialHVZK_schnorr :
+    EfficientSpecialHVZK F.schnorrFamily (fun i α u => α • F.generator i.2 = u) F.schnorrEncoding
+      (fun i => linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod (F.order i.2))
+        (F.Carrier i.2) (F.generator i.2)) id (Function.Embedding.refl _))
+      (fun i => 1 / 2 ^ i.1) where
+  specialHVZK _ := schnorr_specialHVZK
+  realized := ⟨_, F.isPPTOn_schnorrSimulateWord, F.simulatorRealizedBy_schnorrSimulateWord⟩
+
+end Cslib.Crypto.PrimeOrderGroupFamily
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
index 03697ab27..e8b48e8d2 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
@@ -27,7 +27,9 @@ functions and distributions, with no efficiency or finiteness assumption; the pr
 exact statements about a single protocol. The same holds for extractors and simulators: Boneh and
 Shoup require them to be efficient algorithms (Definitions 19.4 and 19.5), but `SpecialSoundness`
 and `SpecialHVZK` accept arbitrary functions and distributions, so neither makes an efficiency
-claim.
+claim. The efficient variants, `EfficientSpecialSoundness` and `EfficientSpecialHVZK` in
+`Complexity.Crypto.Protocols.SigmaProtocol.Efficient`, add a polynomial-time extractor and a strict
+PPT simulator over an indexed family of protocols.
 
 Each property carries its algorithm explicitly. `SpecialSoundness R extract` says that the
 deterministic `extract` computes a witness from any two accepting conversations that share a
@@ -114,7 +116,7 @@ statement from two accepting conversations with a common commitment and distinct
 The extracted witness has a type `W` and a relation `R` of its own. Usually these are the
 prover's witness type and relation; lattice-based protocols extract a witness of a relaxed
 relation instead. The book requires an efficient deterministic extractor; `extract` here is an
-arbitrary function. -/
+arbitrary function, and `EfficientSpecialSoundness` adds the efficiency requirement. -/
 def SpecialSoundness {W : Type*} (R : W → Y → Prop) (extract : Y → T → C → Z → C → Z → W) :
     Prop :=
   ∀ y t c z c' z', c ≠ c' → P.Accepts y t c z → P.Accepts y t c' z' →
@@ -123,7 +125,8 @@ def SpecialSoundness {W : Type*} (R : W → Y → Prop) (extract : Y → T → C
 /-- Special honest-verifier zero knowledge ([BonehShoup2023], Definition 19.5) with the explicit
 simulator `simulate`. The simulator gets a statement and a challenge and returns a commitment
 and a response. The book requires an efficient probabilistic simulator; `simulate` here is an
-arbitrary distribution-valued function. -/
+arbitrary distribution-valued function, and `EfficientSpecialHVZK` adds the efficiency
+requirement. -/
 structure SpecialHVZK (R : X → Y → Prop) (simulate : Y → C → PMF (T × Z)) : Prop where
   /-- Simulated conversations are accepting, for every statement and challenge. -/
   accepts : ∀ y c, ∀ tz ∈ (simulate y c).support, P.Accepts y tz.1 c tz.2
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean
new file mode 100644
index 000000000..92b207459
--- /dev/null
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean
@@ -0,0 +1,170 @@
+/-
+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.Crypto.Protocols.SigmaProtocol.Basic
+public import Complexity.Computability.Interactive.Security
+public import Complexity.Computability.Probabilistic.PPT
+
+/-!
+# Efficient special soundness and special HVZK
+
+`SigmaProtocol.SpecialSoundness` and `SigmaProtocol.SpecialHVZK` name their extractor and
+simulator but accept arbitrary functions and distributions. Boneh and Shoup require an efficient
+deterministic extractor (Definition 19.4) and an efficient probabilistic simulator
+(Definition 19.5). Without that requirement the notions say little: a Sigma protocol has some
+extractor exactly when two accepting conversations with a common commitment and distinct
+challenges certify that the statement has a witness, and for a relation in which every statement
+has exactly one witness, even the protocol that reveals its witness is special HVZK (test module
+`ComplexityTests.UnboundedSimulators`). This module adds the efficient variants; the test module
+`ComplexityTests.EfficientSimulators` shows that, under the discrete-logarithm assumption, they
+rule out both examples.
+
+Efficiency is uniform over a family `P i` of Sigma protocols indexed by `i : I`, typically a
+unary security parameter together with a system parameter such as a group description
+([BonehShoup2023], Definition 2.9). The types of statements, commitments, challenges and responses
+may depend on the index, so the algorithms are certified on words, through the encodings
+collected in a `SigmaProtocol.Encoding`.
+
+* `EfficientSpecialSoundness P R enc encW extract`: at every index `extract i` is a witness
+  extractor, and one deterministic polynomial-time function of words computes the whole family
+  (`ExtractorRealizedBy`).
+* `EfficientSpecialHVZK P R enc simulate δ`: at every index `simulate i` is a perfect simulator,
+  and one uniform strict PPT program realizes the whole family on words up to statistical
+  distance `δ i` (`SimulatorRealizedBy`). The error is needed because a strict PPT machine has a
+  fixed clock and only fair coins, so it cannot sample `ZMod q` exactly when `q` is not a power
+  of two; with `ProbComp.sampleModNat` the error is exponentially small. Boneh and Shoup's
+  efficient algorithms (Definition 2.8) may instead exceed their time bound with negligible
+  probability, which permits exact rejection sampling.
+
+Both variants contain the exact property at every index with the same extractor or simulator, so
+every theorem about `SpecialSoundness` and `SpecialHVZK` applies to them. The realizing program of
+an efficient simulator is `δ i`-close to honest transcripts
+(`SimulatorRealizedBy.closeTo_transcript`) and outputs an accepting conversation except with
+probability `δ i` (`SimulatorRealizedBy.one_sub_le_accepts`), which relaxes Definition 19.5 (i).
+Computational special HVZK ([BonehShoup2023], Definition 20.6) is a further relaxation that is not
+defined here.
+
+## Main definitions
+
+* `SigmaProtocol.Encoding`: word encodings of an indexed family of Sigma protocols.
+* `SigmaProtocol.ExtractorRealizedBy`, `SigmaProtocol.SimulatorRealizedBy`: a word function or
+  program computes an extractor or simulator family on encodings.
+* `SigmaProtocol.EfficientSpecialSoundness`: special soundness with a polynomial-time extractor.
+* `SigmaProtocol.EfficientSpecialHVZK`: special HVZK with a strict PPT simulator, up to `δ`.
+
+## Main results
+
+* `SigmaProtocol.SimulatorRealizedBy.closeTo_transcript`: the realizing program is `δ i`-close to
+  the honest prover's commitment and response at every challenge.
+* `SigmaProtocol.SimulatorRealizedBy.one_sub_le_accepts`: the realizing program outputs an
+  accepting conversation with probability at least `1 - δ i`.
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Definitions 2.8, 2.9, 19.4, 19.5 and 20.6.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Protocols.SigmaProtocol
+
+open Probability Turing.MultiTapeTM Interactive
+open scoped ENNReal
+
+/-- Word encodings for a family of Sigma protocols indexed by `I`, with statements in `Y i`,
+commitments in `T i`, challenges in `C i` and responses in `Z i` at the index `i`. -/
+structure Encoding (I : Type) (Y T C Z : I → Type) where
+  /-- The index, such as a unary security parameter with a system parameter. -/
+  index : I ↪ List Bool
+  /-- The statements at each index. -/
+  statement : ∀ i, Y i ↪ List Bool
+  /-- The commitments at each index. -/
+  commitment : ∀ i, T i ↪ List Bool
+  /-- The challenges at each index. -/
+  challenge : ∀ i, C i ↪ List Bool
+  /-- The responses at each index. -/
+  response : ∀ i, Z i ↪ List Bool
+
+variable {I : Type} {X Y T C Z W : I → Type}
+
+/-- The word function `f` computes the extractor family `extract` on encodings: from the index,
+the encoded statement and the encoded conversations `(t, c, z)` and `(t, c', z')`, it returns the
+encoded witness. -/
+def ExtractorRealizedBy (enc : Encoding I Y T C Z) (encW : ∀ i, W i ↪ List Bool)
+    (extract : ∀ i, Y i → T i → C i → Z i → C i → Z i → W i)
+    (f : I × List Bool × List Bool × List Bool × List Bool × List Bool × List Bool → List Bool) :
+    Prop :=
+  ∀ i y t c z c' z', f (i, enc.statement i y, enc.commitment i t, enc.challenge i c,
+    enc.response i z, enc.challenge i c', enc.response i z') = encW i (extract i y t c z c' z')
+
+/-- The program `program` realizes the simulator family `simulate` on encodings up to statistical
+distance `δ`: on the index, the encoded statement and the encoded challenge, its output is within
+`δ i` of the encoded commitment and response sampled by `simulate i`. -/
+def SimulatorRealizedBy (enc : Encoding I Y T C Z) (simulate : ∀ i, Y i → C i → PMF (T i × Z i))
+    (program : I × List Bool × List Bool → ProbComp (List Bool × List Bool)) (δ : I → ℝ≥0∞) :
+    Prop :=
+  ∀ i y c, CloseTo ((simulate i y c).map (Prod.map (enc.commitment i) (enc.response i)))
+    (ProbComp.eval (program (i, enc.statement i y, enc.challenge i c))) (δ i)
+
+/-- **Efficient special soundness** ([BonehShoup2023], Definition 19.4). At every index,
+`extract i` is a witness extractor for `P i`, and one deterministic polynomial-time function of the
+index and words computes the whole family on encodings. As in `SpecialSoundness`, the extracted
+witness has a type `W i` and a relation `R i` of its own. -/
+structure EfficientSpecialSoundness (P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i))
+    (R : ∀ i, W i → Y i → Prop) (enc : Encoding I Y T C Z) (encW : ∀ i, W i ↪ List Bool)
+    (extract : ∀ i, Y i → T i → C i → Z i → C i → Z i → W i) : Prop where
+  /-- `extract i` is a witness extractor at every index. -/
+  specialSoundness : ∀ i, (P i).SpecialSoundness (R i) (extract i)
+  /-- One polynomial-time word function computes the extractor family. -/
+  polyTime : ∃ f, ComputableInPolyTime f (encPair enc.index (encPair encBits (encPair encBits
+    (encPair encBits (encPair encBits (encPair encBits encBits)))))) encBits ∧
+    ExtractorRealizedBy enc encW extract f
+
+/-- **Efficient special HVZK** ([BonehShoup2023], Definition 19.5), up to a statistical error
+`δ`. At every index, `simulate i` is a perfect special HVZK simulator for `P i`, and one uniform
+strict PPT program of the index and words realizes the whole family up to `δ`, for every
+statement and challenge. -/
+structure EfficientSpecialHVZK (P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i))
+    (R : ∀ i, X i → Y i → Prop) (enc : Encoding I Y T C Z)
+    (simulate : ∀ i, Y i → C i → PMF (T i × Z i)) (δ : I → ℝ≥0∞) : Prop where
+  /-- `simulate i` is a perfect special HVZK simulator at every index. -/
+  specialHVZK : ∀ i, (P i).SpecialHVZK (R i) (simulate i)
+  /-- One uniform strict PPT program realizes the simulator family up to `δ`. -/
+  realized : ∃ program, IsPPTOn (encPair enc.index (encPair encBits encBits))
+    (encPair encBits encBits) program ∧ SimulatorRealizedBy enc simulate program δ
+
+variable {P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i)} {R : ∀ i, X i → Y i → Prop}
+  {enc : Encoding I Y T C Z} {simulate : ∀ i, Y i → C i → PMF (T i × Z i)}
+  {program : I × List Bool × List Bool → ProbComp (List Bool × List Bool)} {δ : I → ℝ≥0∞}
+
+/-- A program realizing a perfect simulator is `δ i`-close to the honest prover's encoded
+commitment and response, for every witness-statement pair and every challenge. -/
+theorem SimulatorRealizedBy.closeTo_transcript (hS : ∀ i, (P i).SpecialHVZK (R i) (simulate i))
+    (h : SimulatorRealizedBy enc simulate program δ) {i : I} {x : X i} {y : Y i} (hxy : R i x y)
+    (c : C i) :
+    CloseTo (((P i).transcript x y c).map (Prod.map (enc.commitment i) (enc.response i)))
+      (ProbComp.eval (program (i, enc.statement i y, enc.challenge i c))) (δ i) := by
+  rw [← (hS i).transcript_eq x y hxy c]
+  exact h i y c
+
+/-- A program realizing a perfect simulator outputs an encoded accepting conversation with
+probability at least `1 - δ i`, for every statement and challenge (a relaxation of
+[BonehShoup2023], Definition 19.5 (i)). -/
+theorem SimulatorRealizedBy.one_sub_le_accepts (hS : ∀ i, (P i).SpecialHVZK (R i) (simulate i))
+    (h : SimulatorRealizedBy enc simulate program δ) (i : I) (y : Y i) (c : C i) :
+    1 - δ i ≤ (ProbComp.eval (program (i, enc.statement i y, enc.challenge i c))).toOuterMeasure
+      {w | ∃ t z, w = (enc.commitment i t, enc.response i z) ∧ (P i).Accepts y t c z} := by
+  have hone : ((simulate i y c).map (Prod.map (enc.commitment i) (enc.response i))).toOuterMeasure
+      {w | ∃ t z, w = (enc.commitment i t, enc.response i z) ∧ (P i).Accepts y t c z} = 1 := by
+    rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply_eq_one_iff]
+    exact fun tz htz => ⟨tz.1, tz.2, rfl, (hS i).accepts y c tz htz⟩
+  exact tsub_le_iff_right.mpr (hone ▸ h i y c _)
+
+end Cslib.Crypto.Protocols.SigmaProtocol
diff --git a/ComplexityTests/EfficientSimulators.lean b/ComplexityTests/EfficientSimulators.lean
new file mode 100644
index 000000000..f01a1e0bf
--- /dev/null
+++ b/ComplexityTests/EfficientSimulators.lean
@@ -0,0 +1,369 @@
+/-
+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.Efficient
+import Complexity.Computability.Interactive.Plain
+import Complexity.Crypto.Computational.SchnorrProtocol
+import Complexity.Crypto.Computational.DiscreteLog.SchnorrGroup
+import Complexity.Crypto.Negligible.Basic
+import Complexity.Probability.PMF.Bind
+import ComplexityTests.InteractiveKnowledgeSound
+import ComplexityTests.UnboundedSimulators
+
+/-!
+# Efficient extractors and simulators
+
+Checks of `SigmaProtocol.EfficientSpecialSoundness`, `SigmaProtocol.EfficientSpecialHVZK`,
+`Interactive.Verifier.EfficientKnowledgeSound` and `Interactive.Reduction.EfficientHVZK` on both
+sides.
+
+* **Schnorr** satisfies both. The extractor computes `(c - c')⁻¹ (z - z')` with `extractNat`
+  (evaluated here on concrete numbers), and the strict PPT simulator outputs an accepting
+  conversation with probability at least `1 - 1 / 2 ^ n`, here in Schnorr groups.
+* **The efficient notions are strictly stronger, under the discrete-logarithm assumption.** For
+  discrete logarithms with witnesses in `ZMod q`, every statement has exactly one witness, so the
+  unbounded notions hold for protocols that reveal or ignore the witness
+  (`ComplexityTests/UnboundedSimulators.lean`): `sendWitnessSigma` is special HVZK and
+  `trustMeSigma` is special sound (`specialHVZK_sendWitness`, `exists_specialSoundness_trustMe`).
+  An efficient simulator for the first, or an efficient extractor for the second, would be a
+  strict PPT algorithm computing discrete logarithms. So under `PrimeOrderGroupFamily.DiscreteLog`
+  neither is efficient, for any simulator error at most `1/2`
+  (`not_efficientSpecialHVZK_sendWitness`, `not_efficientSpecialSoundness_trustMe`).
+* **Interactive reductions.** Sending the witness is efficiently knowledge sound, and efficiently
+  HVZK when the witness is the statement. For discrete logarithms, the verifier that accepts
+  without interaction is knowledge sound and sending the witness is HVZK, both with unbounded
+  algorithms (`exists_knowledgeSound_dlTrustMe`, `hvzk_sendWitnessDL`); under the
+  discrete-logarithm assumption neither is efficient (`not_efficientKnowledgeSound_dlTrustMe`
+  for any error below `1`, `not_efficientHVZK_sendWitnessDL` for `ε + δ ≤ 1/2`).
+-/
+
+namespace ComplexityTests.EfficientSimulators
+
+open Cslib Cslib.Crypto Cslib.Crypto.Protocols Cslib.Crypto.Protocols.SigmaProtocol
+  Cslib.Interactive Probability Turing.MultiTapeTM ComplexityTests.UnboundedSimulators.Sigma
+  Interactive.Spec
+open scoped ENNReal NNReal
+
+/-! ### Schnorr -/
+
+/-- `extractNat` inverts by Fermat's little theorem: modulo `7`, `(3 - 1)⁻¹ (5 - 2) = 4 · 3 = 5`. -/
+example : PrimeOrderGroupFamily.extractNat 7 3 5 1 2 = 5 := by decide
+
+/-- The strict PPT Schnorr simulator for Schnorr groups outputs an accepting conversation with
+probability at least `1 - 1 / 2 ^ n`, for every statement and challenge. -/
+example (n : ℕ) (d : schnorrGroups.Desc) (u : schnorrGroups.Carrier d)
+    (c : ZMod (schnorrGroups.order d)) :
+    1 - 1 / 2 ^ n ≤ (ProbComp.eval (schnorrGroups.schnorrSimulateWord
+      ((n, d), schnorrGroups.encode d u, encNat c.val))).toOuterMeasure
+      {w | ∃ t z, w = (schnorrGroups.encode d t, encNat (ZMod.val z)) ∧
+        (schnorrGroups.schnorrFamily (n, d)).Accepts u t c z} :=
+  schnorrGroups.simulatorRealizedBy_schnorrSimulateWord.one_sub_le_accepts
+    schnorrGroups.efficientSpecialHVZK_schnorr.specialHVZK (n, d) u c
+
+/-! ### Discrete logarithms -/
+
+variable {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc}
+
+/-- The discrete-logarithm relation in the group of the description `i.2`, with witnesses in
+`ZMod q`: every statement has exactly one witness. -/
+abbrev dlRel (F : PrimeOrderGroupFamily) (i : ℕ × F.Desc) (α : ZMod (F.order i.2))
+    (u : F.Carrier i.2) : Prop :=
+  α • F.generator i.2 = u
+
+theorem dlRel_total (i : ℕ × F.Desc) (u : F.Carrier i.2) : ∃ α, dlRel F i α u :=
+  F.smul_generator_surjective i.2 u
+
+theorem dlRel_unique (i : ℕ × F.Desc) {α α' : ZMod (F.order i.2)} {u : F.Carrier i.2}
+    (h : dlRel F i α u) (h' : dlRel F i α' u) : α = α' :=
+  F.smul_generator_injective i.2 (h.trans h'.symm)
+
+/-- Under the discrete-logarithm assumption, no uniform strict PPT adversary finds the discrete
+logarithm with probability at least `1/2` on every instance. -/
+theorem not_half_le_discreteLog (hDL : F.DiscreteLog setup)
+    {adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool)}
+    (hA : IsPPTOn (encPair encUnary (encPair F.encDesc encBits)) encBits
+      fun input => adversary input.1 input.2)
+    (h : ∀ n d (α : ZMod (F.order d)), 1 / 2 ≤
+      (ProbComp.eval (adversary n (d, F.encode d (α • F.generator d)))).toOuterMeasure
+        {w | (ofBits w : ZMod (F.order d)) = α}) : False := by
+  have hgame (n : ℕ) : (1 / 2 : ℝ≥0∞) ≤ F.discreteLogGame setup adversary n true := by
+    simp only [PrimeOrderGroupFamily.discreteLogGame, PMF.monad_bind_eq_bind,
+      PMF.monad_pure_eq_pure]
+    refine PMF.le_bind_apply_on_support _ fun d _ => PMF.le_bind_apply_on_support _ fun α _ => ?_
+    rw [show ∀ (p : PMF (List Bool)) (f : List Bool → Bool),
+        p.bind (fun guess => PMF.pure (f guess)) = p.map f from fun p f => PMF.bind_pure_comp f p,
+      ← PMF.toOuterMeasure_apply_singleton, PMF.toOuterMeasure_map_apply]
+    refine le_trans (h n d α) (le_of_eq (congrArg _ ?_))
+    ext w
+    simp
+  refine not_negligible_const (c := 1 / 2) (by norm_num) (negligible_of_le (hDL _ hA) fun n => ?_)
+  rw [Game.succProbability, ← ENNReal.coe_le_coe, ENNReal.coe_toNNReal (PMF.apply_ne_top _ _)]
+  simpa using hgame n
+
+/-! ### Sending the witness is special HVZK, but not efficiently -/
+
+/-- The protocol that sends the witness, for discrete logarithms. -/
+noncomputable abbrev sendWitnessFamily (F : PrimeOrderGroupFamily) (i : ℕ × F.Desc) :=
+  sendWitnessSigma (dlRel F i)
+
+/-- Its word encodings: scalars in binary, group elements by the family's encoding and challenges
+as single bits. -/
+def sendWitnessEncoding (F : PrimeOrderGroupFamily) :
+    Encoding (ℕ × F.Desc) (fun i => F.Carrier i.2) (fun i => ZMod (F.order i.2)) (fun _ => Bool)
+      (fun i => ZMod (F.order i.2)) where
+  index := encPair encUnary F.encDesc
+  statement i := F.encodeEmbedding i.2
+  commitment i := F.encScalar i.2
+  challenge _ := encBool
+  response i := F.encScalar i.2
+
+/-- Sending the witness is special HVZK at every index, with an unbounded simulator. -/
+theorem specialHVZK_sendWitness (i : ℕ × F.Desc) :
+    (sendWitnessFamily F i).SpecialHVZK (dlRel F i)
+      (choiceSimulate (sendWitnessFamily F i) (dlRel F i)) :=
+  sendWitnessSigma_specialHVZK _ (dlRel_total i) fun _ _ _ h h' => dlRel_unique i h h'
+
+/-- **Sending the witness is not efficiently special HVZK** under the discrete-logarithm
+assumption, with any simulator and any error at most `1/2`: the simulator's commitment is the
+discrete logarithm of its statement. -/
+theorem not_efficientSpecialHVZK_sendWitness (hDL : F.DiscreteLog setup)
+    (simulate : ∀ i : ℕ × F.Desc, F.Carrier i.2 → Bool → PMF (ZMod (F.order i.2) ×
+      ZMod (F.order i.2)))
+    {δ : ℕ × F.Desc → ℝ≥0∞} (hδ : ∀ i, δ i ≤ 1 / 2) :
+    ¬ EfficientSpecialHVZK (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) simulate δ := by
+  intro h
+  obtain ⟨program, hppt, hreal⟩ := h.realized
+  refine not_half_le_discreteLog hDL
+    (adversary := fun n input => Prod.fst <$> program ((n, input.1), input.2, encBool true))
+    ((hppt.preprocess (prepare := fun input : ℕ × F.Desc × List Bool =>
+      ((input.1, input.2.1), input.2.2, encBool true)) (by fun_prop)).map
+        (ComputableInPolyTime.fst _ _)) fun n d α => ?_
+  have hacc := hreal.one_sub_le_accepts h.specialHVZK (n, d) (α • F.generator d) true
+  calc (1 / 2 : ℝ≥0∞) = 1 - 1 / 2 := by rw [one_div, ENNReal.one_sub_inv_two]
+    _ ≤ 1 - δ (n, d) := tsub_le_tsub_left (hδ _) 1
+    _ ≤ _ := hacc
+    _ ≤ _ := by
+      rw [ProbComp.eval_map, PMF.toOuterMeasure_map_apply]
+      refine MeasureTheory.measure_mono ?_
+      rintro _ ⟨t, z, rfl, ht⟩
+      have hα : t = α := dlRel_unique (n, d) (of_decide_eq_true ht) rfl
+      change ((ofBits (encNat t.val) : ℕ) : ZMod (F.order d)) = α
+      rw [encNat_apply, ofBits, Nat.foldr_bit_bits, ZMod.natCast_zmod_val, hα]
+
+/-! ### Accepting everything is special sound, but not efficiently -/
+
+/-- The protocol whose verifier accepts every conversation, for discrete logarithms. -/
+noncomputable abbrev trustMeFamily (F : PrimeOrderGroupFamily) (i : ℕ × F.Desc) :=
+  trustMeSigma (ZMod (F.order i.2)) (F.Carrier i.2)
+
+/-- Its word encodings: trivial commitments and responses, and challenges as single bits. -/
+def trustMeEncoding (F : PrimeOrderGroupFamily) :
+    Encoding (ℕ × F.Desc) (fun i => F.Carrier i.2) (fun _ => Unit) (fun _ => Bool)
+      (fun _ => Unit) where
+  index := encPair encUnary F.encDesc
+  statement i := F.encodeEmbedding i.2
+  commitment _ := encUnit
+  challenge _ := encBool
+  response _ := encUnit
+
+/-- Accepting everything is special sound at every index, with an unbounded extractor. -/
+theorem exists_specialSoundness_trustMe (i : ℕ × F.Desc) :
+    ∃ extract, (trustMeFamily F i).SpecialSoundness (dlRel F i) extract :=
+  (exists_specialSoundness_iff _ _).2 fun u _ _ _ _ _ _ _ _ => dlRel_total i u
+
+/-- **Accepting everything is not efficiently special sound** under the discrete-logarithm
+assumption, with any extractor: from two trivial conversations it would compute discrete
+logarithms. -/
+theorem not_efficientSpecialSoundness_trustMe (hDL : F.DiscreteLog setup)
+    (extract : ∀ i : ℕ × F.Desc, F.Carrier i.2 → Unit → Bool → Unit → Bool → Unit →
+      ZMod (F.order i.2)) :
+    ¬ EfficientSpecialSoundness (trustMeFamily F) (dlRel F) (trustMeEncoding F)
+      (fun i => F.encScalar i.2) extract := by
+  intro h
+  obtain ⟨f, hf, hreal⟩ := h.polyTime
+  let prepare : ℕ × F.Desc × List Bool →
+      (ℕ × F.Desc) × List Bool × List Bool × List Bool × List Bool × List Bool × List Bool :=
+    fun input => ((input.1, input.2.1), input.2.2, encUnit (), encBool true, encUnit (),
+      encBool false, encUnit ())
+  refine not_half_le_discreteLog hDL (adversary := fun n input => pure (f (prepare (n, input))))
+    (hf.comp (show ComputableInPolyTime prepare _ _ by fun_prop)).isPPTOn fun n d α => ?_
+  have hword := hreal (n, d) (α • F.generator d) () true () false ()
+  have hα : extract (n, d) (α • F.generator d) () true () false () = α :=
+    dlRel_unique (n, d) (h.specialSoundness (n, d) _ () true () false () (by decide) rfl rfl) rfl
+  have hmem : f (prepare (n, d, F.encode d (α • F.generator d))) ∈
+      {w : List Bool | (ofBits w : ZMod (F.order d)) = α} := by
+    change ((ofBits (f (prepare (n, d, F.encode d (α • F.generator d)))) : ℕ) :
+      ZMod (F.order d)) = α
+    rw [show f (prepare (n, d, F.encode d (α • F.generator d))) =
+      F.encScalar d (extract (n, d) (α • F.generator d) () true () false ()) from hword, hα]
+    change ((ofBits (encNat α.val) : ℕ) : ZMod (F.order d)) = α
+    rw [encNat_apply, ofBits, Nat.foldr_bit_bits, ZMod.natCast_zmod_val]
+  rw [ProbComp.eval_pure, PMF.toOuterMeasure_pure_apply]
+  simp [hmem]
+
+/-! ### Interactive reductions: sending the witness -/
+
+/-- Transcripts of one message, encoded by the message. -/
+def messageEncoding {W : Type} (enc : W ↪ List Bool) :
+    Transcript (InteractiveKnowledgeSound.witnessSpec W) ↪ List Bool :=
+  ⟨fun τ => enc τ.1, fun _ _ h => Prod.ext (enc.injective h) rfl⟩
+
+section SendWitness
+
+open ComplexityTests.InteractiveKnowledgeSound
+
+/-- The honest transcript of sending the witness is the witness. -/
+theorem sendWitness_transcript {X W : Type} (rel : X → W → Prop) [∀ x w, Decidable (rel x w)]
+    (x : X) (w : W) :
+    (World.plain.eval ((sendWitness rel).run x w)).map Prod.fst = PMF.pure (w, ()) := by
+  rw [Reduction.run, World.plain_eval_execute, PMF.map_comp]
+  simp only [sendWitness, runStrategy, plainLaw_bind, plainLaw_pure, PMF.pure_bind, PMF.pure_map]
+  rfl
+
+variable (rel : List Bool → List Bool → Prop) [∀ x w, Decidable (rel x w)]
+
+/-- The word encodings of sending a word witness for a word statement, over a unary security
+parameter that the protocol ignores. -/
+def wordEncoding :
+    Interactive.Encoding ℕ (fun _ => witnessSpec (List Bool)) (fun _ => List Bool) where
+  index := encUnary
+  statement _ := encBits
+  transcript _ := messageEncoding encBits
+
+/-- **Sending the witness is efficiently knowledge sound** with error `0`: the extractor reads
+the witness off the transcript. -/
+example : Verifier.EfficientKnowledgeSound (fun _ => (sendWitness rel).verifier) (fun _ => rel)
+    (fun _ => Accept) (wordEncoding) (fun _ => encUnit) (fun _ => encBits) (fun _ _ τ _ => τ.1)
+    (fun _ => 0) where
+  knowledgeSound _ := sendWitness_knowledgeSound rel
+  polyTime := ⟨fun p => p.2.2.1, by fun_prop, fun _ _ _ _ => by rfl⟩
+
+/-- **Sending the witness is efficiently perfectly HVZK when the witness is the statement**: the
+simulator echoes the statement. -/
+example : Reduction.EfficientHVZK (fun _ => sendWitness fun x w : List Bool => w = x)
+    (fun _ x w => w = x) wordEncoding (fun _ x => pure (x, ())) (fun _ => 0) (fun _ => 0) where
+  hvzk _ x w hxw := by
+    rw [sendWitness_transcript, hxw, ProbComp.eval_pure]
+    exact ComplexityTests.UnboundedSimulators.closeTo_refl _
+  realized := ⟨fun p => pure p.2, (ComputableInPolyTime.snd _ _).isPPTOn, fun _ x => by
+    rw [ProbComp.eval_pure, ProbComp.eval_pure, PMF.pure_map]
+    exact ComplexityTests.UnboundedSimulators.closeTo_refl (PMF.pure x)⟩
+
+end SendWitness
+
+/-! ### Interactive reductions for discrete logarithms -/
+
+section DiscreteLog
+
+open ComplexityTests.InteractiveKnowledgeSound
+
+/-- The discrete-logarithm relation with the statement first, as interactive reductions take
+it. -/
+abbrev dlStmtRel (F : PrimeOrderGroupFamily) (i : ℕ × F.Desc) (u : F.Carrier i.2)
+    (α : ZMod (F.order i.2)) : Prop :=
+  dlRel F i α u
+
+/-- The verifier for discrete logarithms that accepts without interaction. -/
+def dlTrustMe (F : PrimeOrderGroupFamily) (i : ℕ × F.Desc) :
+    Verifier OracleSpec.empty [] (F.Carrier i.2) Unit where
+  samplers := ()
+  decide _ _ := pure (some ())
+
+/-- Its word encodings: statements by the family's encoding, and the empty transcript. -/
+def dlTrustMeEncoding (F : PrimeOrderGroupFamily) :
+    Interactive.Encoding (ℕ × F.Desc) (fun _ => []) (fun i => F.Carrier i.2) where
+  index := encPair encUnary F.encDesc
+  statement i := F.encodeEmbedding i.2
+  transcript _ := encUnit
+
+/-- Accepting without interaction is knowledge sound with error `0` at every index, with an
+unbounded extractor: every statement has a witness. -/
+theorem exists_knowledgeSound_dlTrustMe (i : ℕ × F.Desc) :
+    ∃ E, (dlTrustMe F i).KnowledgeSound (dlStmtRel F i) Accept E 0 :=
+  ⟨fun u _ _ => (dlRel_total i u).choose, knowledgeSound_of_sound _
+    (fun u _ _ _ => (dlRel_total i u).choose_spec) fun u hu => absurd (dlRel_total i u) hu⟩
+
+/-- **Accepting without interaction is not efficiently knowledge sound** under the
+discrete-logarithm assumption, with any extractor and any error below `1`: the extractor would
+compute discrete logarithms from the statement alone. -/
+theorem not_efficientKnowledgeSound_dlTrustMe (hDL : F.DiscreteLog setup)
+    (E : ∀ i : ℕ × F.Desc, F.Carrier i.2 → Transcript [] → Unit → ZMod (F.order i.2))
+    {ε : ℕ × F.Desc → ℝ≥0∞} (hε : ∀ i, ε i < 1) :
+    ¬ Verifier.EfficientKnowledgeSound (dlTrustMe F) (dlStmtRel F) (fun _ => Accept)
+      (dlTrustMeEncoding F) (fun _ => encUnit) (fun i => F.encScalar i.2) E ε := by
+  intro h
+  obtain ⟨f, hf, hreal⟩ := h.polyTime
+  have hE (i : ℕ × F.Desc) (u : F.Carrier i.2) : dlStmtRel F i u (E i u () ()) := by
+    by_contra hnot
+    have hk := h.knowledgeSound i u (pure ())
+    rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply] at hk
+    simp only [runStrategy, plainLaw_bind, plainLaw_pure, PMF.pure_bind] at hk
+    rw [PMF.toOuterMeasure_pure_apply, ite_eq_left (show _ from ⟨⟨(), rfl, trivial⟩, hnot⟩)] at hk
+    exact absurd hk (not_le.mpr (hε i))
+  let prepare : ℕ × F.Desc × List Bool → (ℕ × F.Desc) × List Bool × List Bool × List Bool :=
+    fun input => ((input.1, input.2.1), input.2.2, encUnit (), encUnit ())
+  refine not_half_le_discreteLog hDL (adversary := fun n input => pure (f (prepare (n, input))))
+    (hf.comp (show ComputableInPolyTime prepare _ _ by fun_prop)).isPPTOn fun n d α => ?_
+  have hα : E (n, d) (α • F.generator d) () () = α :=
+    dlRel_unique (n, d) (hE (n, d) _) rfl
+  have hmem : f (prepare (n, d, F.encode d (α • F.generator d))) ∈
+      {w : List Bool | (ofBits w : ZMod (F.order d)) = α} := by
+    change ((ofBits (f (prepare (n, d, F.encode d (α • F.generator d)))) : ℕ) :
+      ZMod (F.order d)) = α
+    rw [show f (prepare (n, d, F.encode d (α • F.generator d))) =
+      F.encScalar d (E (n, d) (α • F.generator d) () ()) from hreal (n, d) _ () (), hα]
+    change ((ofBits (encNat α.val) : ℕ) : ZMod (F.order d)) = α
+    rw [encNat_apply, ofBits, Nat.foldr_bit_bits, ZMod.natCast_zmod_val]
+  rw [ProbComp.eval_pure, PMF.toOuterMeasure_pure_apply]
+  simp [hmem]
+
+/-- Sending the witness, for discrete logarithms. -/
+noncomputable abbrev sendWitnessDL (F : PrimeOrderGroupFamily) (i : ℕ × F.Desc) :=
+  sendWitness (dlStmtRel F i)
+
+/-- Its word encodings: statements by the family's encoding, and the transcript by its scalar in
+binary. -/
+def sendWitnessDLEncoding (F : PrimeOrderGroupFamily) :
+    Interactive.Encoding (ℕ × F.Desc) (fun i => witnessSpec (ZMod (F.order i.2)))
+      (fun i => F.Carrier i.2) where
+  index := encPair encUnary F.encDesc
+  statement i := F.encodeEmbedding i.2
+  transcript i := messageEncoding (F.encScalar i.2)
+
+/-- Sending the witness is perfectly HVZK at every index, with an unbounded simulator: every
+statement has exactly one witness. -/
+theorem hvzk_sendWitnessDL (i : ℕ × F.Desc) :
+    (sendWitnessDL F i).HVZK (dlStmtRel F i)
+      (ComplexityTests.UnboundedSimulators.choiceSim (sendWitnessDL F i) (dlStmtRel F i)) 0 :=
+  ComplexityTests.UnboundedSimulators.hvzk_of_unique _ fun _ _ _ h h' => dlRel_unique i h h'
+
+/-- **Sending the witness is not efficiently HVZK** under the discrete-logarithm assumption, with
+any simulator and errors with `ε + δ ≤ 1/2`: the realizing program outputs the discrete
+logarithm. -/
+theorem not_efficientHVZK_sendWitnessDL (hDL : F.DiscreteLog setup)
+    (Sim : ∀ i : ℕ × F.Desc, F.Carrier i.2 → ProbComp (Transcript (witnessSpec
+      (ZMod (F.order i.2)))))
+    {ε δ : ℕ × F.Desc → ℝ≥0∞} (hεδ : ∀ i, ε i + δ i ≤ 1 / 2) :
+    ¬ Reduction.EfficientHVZK (sendWitnessDL F) (dlStmtRel F) (sendWitnessDLEncoding F) Sim ε
+      δ := by
+  intro h
+  obtain ⟨program, hppt, hreal⟩ := h.realized
+  refine not_half_le_discreteLog hDL
+    (adversary := fun n input => program ((n, input.1), input.2))
+    (hppt.preprocess (prepare := fun input : ℕ × F.Desc × List Bool =>
+      ((input.1, input.2.1), input.2.2)) (by fun_prop)) fun n d α => ?_
+  have hclose := hreal.closeTo_run h.hvzk (i := (n, d)) (x := α • F.generator d) (w := α) rfl
+    {w | (ofBits w : ZMod (F.order d)) = α}
+  rw [sendWitness_transcript, PMF.pure_map, PMF.toOuterMeasure_pure_apply, ite_eq_left (by
+    change ((ofBits (encNat α.val) : ℕ) : ZMod (F.order d)) = α
+    rw [encNat_apply, ofBits, Nat.foldr_bit_bits, ZMod.natCast_zmod_val])] at hclose
+  calc (1 / 2 : ℝ≥0∞) = 1 - 1 / 2 := by rw [one_div, ENNReal.one_sub_inv_two]
+    _ ≤ 1 - (ε (n, d) + δ (n, d)) := tsub_le_tsub_left (hεδ _) 1
+    _ ≤ _ := tsub_le_iff_right.mpr hclose
+
+end DiscreteLog
+
+end ComplexityTests.EfficientSimulators