feat(crypto): add computational special HVZK and CloseTo game bridges

Complexity.lean

@@ -2940,6 +2940,7 @@ public import Complexity.Crypto.Computational.ZeroKnowledge.AuxClock
 public import Complexity.Crypto.Computational.ZeroKnowledge.Levin
 public import Complexity.Crypto.Computational.ZeroKnowledge.Soundness
 public import Complexity.Crypto.Game
+public import Complexity.Crypto.Game.CloseTo
 public import Complexity.Crypto.Game.Hybrid
 public import Complexity.Crypto.Game.Statistical
 public import Complexity.Crypto.Game.UntilBad
@@ -2966,6 +2967,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.Computational
 public import Complexity.Crypto.Protocols.SigmaProtocol.Efficient
 public import Complexity.Crypto.Protocols.SigmaProtocol.FiatShamir
 public import Complexity.Crypto.Protocols.SigmaProtocol.Identification

Complexity/Computability/Interactive/Efficient.lean

@@ -36,9 +36,16 @@ on the index, so the algorithms are certified on words, through the encodings co
 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.
+(`SimulatorRealizedBy.closeTo_run`). Note that `ε` and `δ` are explicit, unconstrained parameters
+of these predicates rather than bundled `Negligible` obligations: when `ε i ≥ 1` or `δ i ≥ 1`
+(since event probabilities are at most `1`), `KnowledgeSound` or `SimulatorRealizedBy` holds
+vacuously (`not_efficientKnowledgeSound_dlTrustMe` and `not_efficientHVZK_sendWitnessDL` in
+`ComplexityTests.EfficientSimulators` require `ε i < 1` and `ε i + δ i ≤ 1 / 2`). Computational
+theorems and security claims built on these predicates must therefore pair them with an explicit
+error bound (such as `Negligible`) across the setup distribution. 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
 

Complexity/Computability/Interactive/Security.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Interactive.Basic
+import Complexity.Probability.PMF.Event
 
 /-!
 # Security of interactive reductions
@@ -51,6 +52,14 @@ PPT simulator over an indexed family of reductions.
   `Interactive.RbrFrom`, `Interactive.Verifier.outputOn`, `Interactive.Verifier.RbrSound`.
 * `Interactive.Reduction.HVZK`.
 
+## Main results
+
+* `Interactive.CloseTo.refl`, `Interactive.CloseTo.mono`, `Interactive.CloseTo.symm`,
+  `Interactive.CloseTo.map`, `Interactive.CloseTo.trans`: equivalence-like and postprocessing laws
+  for all-events statistical distance.
+* `Interactive.CloseTo.bind_left`, `Interactive.CloseTo.bind_right`, `Interactive.CloseTo.bind`:
+  data processing across randomized continuations without finiteness assumptions.
+
 ## References
 
 * [R. Canetti, Y. Chen, J. Holmgren, A. Lombardi, G. N. Rothblum, R. D. Rothblum, D. Wichs,
@@ -79,6 +88,31 @@ variation distance on any type, finite or not. -/
 def CloseTo {α : Type} (μ ν : PMF α) (ε : ℝ≥0∞) : Prop :=
   ∀ event : Set α, μ.toOuterMeasure event ≤ ν.toOuterMeasure event + ε
 
+/-- Every distribution is `0`-close to itself. -/
+@[simp] theorem CloseTo.refl {α : Type} (μ : PMF α) : CloseTo μ μ 0 :=
+  fun _ => by rw [add_zero]
+
+/-- Enlarging the error bound preserves statistical closeness. -/
+theorem CloseTo.mono {α : Type} {μ ν : PMF α} {ε δ : ℝ≥0∞} (h : CloseTo μ ν ε)
+    (hle : ε ≤ δ) : CloseTo μ ν δ :=
+  fun event => (h event).trans (add_le_add le_rfl hle)
+
+/-- Statistical closeness is symmetric, on any type. -/
+theorem CloseTo.symm {α : Type} {μ ν : PMF α} {ε : ℝ≥0∞} (h : CloseTo μ ν ε) :
+    CloseTo ν μ ε := fun event => by
+  have hc := h eventᶜ
+  refine WithTop.le_of_add_le_add_right
+    (Cslib.Probability.PMF.toOuterMeasure_ne_top ν eventᶜ) ?_
+  calc
+    ν.toOuterMeasure event + ν.toOuterMeasure eventᶜ = 1 :=
+      Cslib.Probability.PMF.toOuterMeasure_add_compl_ennreal ν event
+    _ = μ.toOuterMeasure event + μ.toOuterMeasure eventᶜ :=
+      (Cslib.Probability.PMF.toOuterMeasure_add_compl_ennreal μ event).symm
+    _ ≤ μ.toOuterMeasure event + (ν.toOuterMeasure eventᶜ + ε) :=
+      add_le_add le_rfl hc
+    _ = μ.toOuterMeasure event + ε + ν.toOuterMeasure eventᶜ := by
+      rw [add_comm _ ε, add_assoc]
+
 /-- Statistical closeness is preserved by postprocessing. -/
 theorem CloseTo.map {α β : Type} {μ ν : PMF α} {ε : ℝ≥0∞} (h : CloseTo μ ν ε) (f : α → β) :
     CloseTo (μ.map f) (ν.map f) ε := fun event => by
@@ -91,6 +125,72 @@ theorem CloseTo.trans {α : Type} {μ ν ρ : PMF α} {ε δ : ℝ≥0∞} (h₁
     rw [add_comm ε δ, ← add_assoc]
     exact add_le_add (h₂ event) le_rfl
 
+/-- Data processing in the first stage: replacing `μ` by an `ε`-close `ν` before a common
+randomized continuation `f` preserves `ε`-closeness, without finiteness assumptions. -/
+theorem CloseTo.bind_left {α β : Type} {μ ν : PMF α} {ε : ℝ≥0∞} (h : CloseTo μ ν ε)
+    (f : α → PMF β) : CloseTo (μ.bind f) (ν.bind f) ε := fun event => by
+  classical
+  let S : Set α := {a | ν a ≤ μ a}
+  let d : α → ℝ≥0∞ := S.indicator fun a => μ a - ν a
+  have hpt (a : α) : S.indicator ν a + d a = S.indicator μ a := by
+    by_cases ha : a ∈ S
+    · simp only [d, Set.indicator_of_mem ha]
+      exact add_tsub_cancel_of_le ha
+    · simp only [d, Set.indicator_of_notMem ha, add_zero]
+  have hd_sum : ∑' a, d a ≤ ε := by
+    refine (ENNReal.add_le_add_iff_left
+      (Cslib.Probability.PMF.toOuterMeasure_ne_top ν S)).mp ?_
+    rw [PMF.toOuterMeasure_apply, ← tsum_add]
+    simp_rw [hpt]
+    simpa only [PMF.toOuterMeasure_apply] using h S
+  rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_bind_apply]
+  calc
+    ∑' a, μ a * (f a).toOuterMeasure event
+      ≤ ∑' a, (ν a * (f a).toOuterMeasure event + d a) := by
+        refine tsum_le_tsum fun a => ?_
+        by_cases ha : a ∈ S
+        · simp only [d, Set.indicator_of_mem ha]
+          calc
+            μ a * (f a).toOuterMeasure event
+              = (ν a + (μ a - ν a)) * (f a).toOuterMeasure event := by
+                rw [add_tsub_cancel_of_le ha]
+            _ = ν a * (f a).toOuterMeasure event +
+                  (μ a - ν a) * (f a).toOuterMeasure event := add_mul _ _ _
+            _ ≤ ν a * (f a).toOuterMeasure event + (μ a - ν a) := by
+                refine add_le_add le_rfl ?_
+                exact (mul_le_mul_of_nonneg_left
+                  (Cslib.Probability.PMF.toOuterMeasure_le_one (f a) event) zero_le).trans
+                  (mul_one _).le
+        · have hle : μ a ≤ ν a := le_of_not_ge ha
+          simp only [d, Set.indicator_of_notMem ha, add_zero]
+          exact mul_le_mul_of_nonneg_right hle zero_le
+    _ = ∑' a, ν a * (f a).toOuterMeasure event + ∑' a, d a := tsum_add
+    _ ≤ ∑' a, ν a * (f a).toOuterMeasure event + ε := add_le_add le_rfl hd_sum
+
+/-- Pointwise statistical closeness of continuations on `μ.support` is preserved across
+`PMF.bind`. -/
+theorem CloseTo.bind_right {α β : Type} (μ : PMF α) {f g : α → PMF β} {ε : ℝ≥0∞}
+    (h : ∀ a ∈ μ.support, CloseTo (f a) (g a) ε) :
+    CloseTo (μ.bind f) (μ.bind g) ε := fun event => by
+  rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_bind_apply]
+  calc
+    ∑' a, μ a * (f a).toOuterMeasure event
+      ≤ ∑' a, μ a * ((g a).toOuterMeasure event + ε) := by
+        refine tsum_le_tsum fun a => ?_
+        by_cases ha : a ∈ μ.support
+        · exact mul_le_mul_of_nonneg_left (h a ha event) zero_le
+        · have hz : μ a = 0 := (PMF.apply_eq_zero_iff μ a).mpr ha
+          simp [hz]
+    _ = ∑' a, μ a * (g a).toOuterMeasure event + ε := by
+        simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, μ.tsum_coe, one_mul]
+
+/-- Combining `CloseTo.bind_left` and `CloseTo.bind_right` adds the first-stage and continuation
+errors. -/
+theorem CloseTo.bind {α β : Type} {μ ν : PMF α} {f g : α → PMF β} {ε δ : ℝ≥0∞}
+    (h₁ : CloseTo μ ν ε) (h₂ : ∀ a ∈ ν.support, CloseTo (f a) (g a) δ) :
+    CloseTo (μ.bind f) (ν.bind g) (ε + δ) :=
+  (h₁.bind_left f).trans (CloseTo.bind_right ν h₂)
+
 /-! ### Completeness, soundness and knowledge soundness -/
 
 /-- Completeness with error `ε`. -/

Complexity/Crypto/Computational/SchnorrProtocol.lean

@@ -9,11 +9,12 @@ module
 
 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.Computational
 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.Crypto.Negligible.Basic
 import Complexity.Probability.PMF
 import Complexity.Tactic.PPT
 
@@ -32,6 +33,11 @@ in binary (`schnorrEncoding`).
   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`.
+* **Computational special HVZK** (`computationalSpecialHVZK_schnorr`, Definition 20.6): because
+  every output of `schnorrSimulateWord` satisfies `z • g = (z • g - c • u) + c • u` exactly
+  (`accepts_schnorrSimulateWord`, acceptance error `0`), and `1 / 2 ^ n` is negligible along any
+  group-description setup `(setup n).map (n, ·)`, `schnorrSimulateWord` satisfies Definition 20.6
+  with zero acceptance error.
 
 The protocol does not depend on the security parameter; only the simulator's sampling error does.
 
@@ -52,11 +58,14 @@ The protocol does not depend on the security parameter; only the simulator's sam
   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`.
+* `Cslib.Crypto.PrimeOrderGroupFamily.accepts_schnorrSimulateWord`,
+  `Cslib.Crypto.PrimeOrderGroupFamily.computationalSpecialHVZK_schnorr`: exact acceptance (`δ = 0`)
+  and computational special HVZK (Definition 20.6).
 
 ## 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.
+  Version 0.6][BonehShoup2023], Examples 19.1–19.3, Definitions 19.4–19.5, and Definition 20.6.
 * [C.-P. Schnorr, *Efficient Signature Generation by Smart Cards*][Schnorr1991]
 -/
 
@@ -155,37 +164,15 @@ theorem efficientSpecialSoundness_schnorr :
 
 /-! ### 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) :
+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 => ?_
+  refine Game.closeTo_of_advantage_decide_le fun E => ?_
+  rw [Game.advantage_comm]
   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
@@ -286,4 +273,41 @@ theorem efficientSpecialHVZK_schnorr :
   specialHVZK _ := schnorr_specialHVZK
   realized := ⟨_, F.isPPTOn_schnorrSimulateWord, F.simulatorRealizedBy_schnorrSimulateWord⟩
 
+/-- Every output of `schnorrSimulateWord` on an encoded statement and challenge is an encoded
+accepting conversation (acceptance error `0`): for every sampled `z`, `(z • g - c • u) + c • u =
+z • g`. -/
+theorem accepts_schnorrSimulateWord (i : ℕ × F.Desc) (u : F.Carrier i.2)
+    (c : ZMod (F.order i.2)) :
+    1 ≤ (ProbComp.eval (F.schnorrSimulateWord
+      (i, F.schnorrEncoding.statement i u, F.schnorrEncoding.challenge i c))).toOuterMeasure
+      {w | ∃ t z, w = (F.schnorrEncoding.commitment i t, F.schnorrEncoding.response i z) ∧
+        (F.schnorrFamily i).Accepts u t c z} := by
+  have heq : (ProbComp.eval (F.schnorrSimulateWord
+      (i, F.schnorrEncoding.statement i u, F.schnorrEncoding.challenge i c))).toOuterMeasure
+      {w | ∃ t z, w = (F.schnorrEncoding.commitment i t, F.schnorrEncoding.response i z) ∧
+        (F.schnorrFamily i).Accepts u t c z} = 1 := by
+    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, PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply_eq_one_iff]
+    intro z _
+    refine ⟨z • F.generator i.2 - c • u, z, rfl, ?_⟩
+    simp only [schnorrFamily, schnorr_accepts_iff, Function.Embedding.refl_apply, sub_add_cancel]
+  exact heq.ge
+
+/-- **Schnorr's protocol has computational special HVZK** ([BonehShoup2023], Definition 20.6) with
+zero acceptance error (`δ = fun _ => 0`) over any group-description setup `setup : ℕ → PMF F.Desc`
+paired with the security parameter. -/
+theorem computationalSpecialHVZK_schnorr (setup : ℕ → PMF F.Desc) :
+    ComputationalSpecialHVZK F.schnorrFamily (fun i α u => α • F.generator i.2 = u)
+      F.schnorrEncoding (fun i => F.encScalar i.2) (fun n => (setup n).map (n, ·))
+      F.schnorrSimulateWord (fun _ => 0) := by
+  refine F.simulatorRealizedBy_schnorrSimulateWord.computationalSpecialHVZK_of_accepts
+    (fun _ => schnorr_specialHVZK) F.isPPTOn_schnorrSimulateWord
+    (fun i u c => by simpa only [tsub_zero] using F.accepts_schnorrSimulateWord i u c)
+    ⟨fun n => (1 / 2 : ℝ≥0) ^ n, negligible_geometric (by norm_num), fun n i hi => ?_⟩
+  obtain ⟨d, -, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hi
+  dsimp only
+  rw [one_div_pow, ENNReal.coe_div (pow_ne_zero _ two_ne_zero), ENNReal.coe_one, ENNReal.coe_pow,
+    ENNReal.coe_ofNat]
+
 end Cslib.Crypto.PrimeOrderGroupFamily