From c40950166edf99539cdcddde4e1b14069c6f6d5a Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 3 Nov 2026 08:43:19 +0000 Subject: [PATCH] feat(crypto): add computational special HVZK and CloseTo game bridges --- Complexity.lean | 2 + .../Computability/Interactive/Efficient.lean | 13 +- .../Computability/Interactive/Security.lean | 100 +++ .../Crypto/Computational/SchnorrProtocol.lean | 78 +- Complexity/Crypto/Game/CloseTo.lean | 188 +++++ .../SigmaProtocol/Computational.lean | 385 ++++++++++ .../Protocols/SigmaProtocol/Efficient.lean | 11 +- ComplexityTests/ComputationalSpecialHVZK.lean | 722 ++++++++++++++++++ ComplexityTests/EfficientSimulators.lean | 4 +- ComplexityTests/UnboundedSimulators.lean | 26 +- .../interactive-reductions.md | 4 +- .../protocols-and-privacy.md | 9 +- 12 files changed, 1481 insertions(+), 61 deletions(-) create mode 100644 Complexity/Crypto/Game/CloseTo.lean create mode 100644 Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean create mode 100644 ComplexityTests/ComputationalSpecialHVZK.lean diff --git a/Complexity.lean b/Complexity.lean index 84615f7149..89edbbff09 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Computability/Interactive/Efficient.lean b/Complexity/Computability/Interactive/Efficient.lean index facb7fc68f..181f7c7d92 100644 --- a/Complexity/Computability/Interactive/Efficient.lean +++ b/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 diff --git a/Complexity/Computability/Interactive/Security.lean b/Complexity/Computability/Interactive/Security.lean index ad419f73e8..7a7c285033 100644 --- a/Complexity/Computability/Interactive/Security.lean +++ b/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 `ε`. -/ diff --git a/Complexity/Crypto/Computational/SchnorrProtocol.lean b/Complexity/Crypto/Computational/SchnorrProtocol.lean index 69e7cb9d69..b075fe1114 100644 --- a/Complexity/Crypto/Computational/SchnorrProtocol.lean +++ b/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 diff --git a/Complexity/Crypto/Game/CloseTo.lean b/Complexity/Crypto/Game/CloseTo.lean new file mode 100644 index 0000000000..433348926b --- /dev/null +++ b/Complexity/Crypto/Game/CloseTo.lean @@ -0,0 +1,188 @@ +/- +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.Crypto.Game + +/-! +# Bridging Boolean game advantage and all-events statistical closeness + +`Cslib.Interactive.CloseTo` measures total variation distance in `ℝ≥0∞` on an arbitrary discrete +type `α : Type` without `Fintype` or measurability assumptions, while `Cslib.Crypto.Game.advantage` +measures the distinguishing advantage in `ℝ≥0` between two Boolean experiments (`Game = PMF Bool`). + +This module connects the two interfaces in both directions: + +* On `Bool` itself, `CloseTo game1 game2 ε` is equivalent to `(advantage game1 game2 : ℝ≥0∞) ≤ ε` + (`closeTo_iff_coe_advantage_le`, `closeTo_iff_advantage_le`). +* On any `α : Type`, `CloseTo μ ν ε` is equivalent to uniform `ε`-bounded advantage under every + deterministic Boolean predicate `f : α → Bool` (`closeTo_iff_forall_coe_advantage_map_le`, + `closeTo_iff_forall_advantage_map_le`) and under every randomized distinguisher `test : α → Game` + (`closeTo_iff_forall_coe_advantage_bind_le`, `closeTo_iff_forall_advantage_bind_le`). + +Unlike `Complexity.Crypto.Game.Statistical`, which identifies `Game.advantage` with the finite-PMF +metric `nndist`, these bridges require no `Fintype` instance on `α` and apply directly to word +ensembles `PMF (List Bool)` and protocol transcripts. + +## Main results + +* `Cslib.Crypto.Game.closeTo_iff_coe_advantage_le`, `Cslib.Crypto.Game.closeTo_iff_advantage_le`: + statistical closeness of Boolean games is bounded distinguishing advantage. +* `Cslib.Crypto.Game.coe_advantage_map_le_of_closeTo`, + `Cslib.Crypto.Game.advantage_map_le_of_closeTo`, + `Cslib.Crypto.Game.coe_advantage_bind_le_of_closeTo`, + `Cslib.Crypto.Game.advantage_bind_le_of_closeTo`: postprocessing `CloseTo` by a deterministic or + randomized Boolean distinguisher bounds `Game.advantage`. +* `Cslib.Crypto.Game.closeTo_of_coe_advantage_decide_le`, + `Cslib.Crypto.Game.closeTo_of_advantage_decide_le`: indicator-event tests suffice for `CloseTo`. +* `Cslib.Crypto.Game.closeTo_iff_forall_coe_advantage_map_le`, + `Cslib.Crypto.Game.closeTo_iff_forall_advantage_map_le`, + `Cslib.Crypto.Game.closeTo_iff_forall_coe_advantage_bind_le`, + `Cslib.Crypto.Game.closeTo_iff_forall_advantage_bind_le`: variational characterizations of + `CloseTo` via deterministic and randomized Boolean distinguishers. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Game + +open Interactive +open scoped ENNReal NNReal + +private theorem coe_succProbability_ennreal (game : Game) : + (succProbability game : ℝ≥0∞) = game true := + ENNReal.coe_toNNReal (game.apply_ne_top true) + +/-- On Boolean experiments, `ε`-closeness in `ℝ≥0∞` is equivalent to `(advantage : ℝ≥0∞) ≤ ε`. -/ +theorem closeTo_iff_coe_advantage_le {game1 game2 : Game} {ε : ℝ≥0∞} : + CloseTo game1 game2 ε ↔ (advantage game1 game2 : ℝ≥0∞) ≤ ε := by + have hadv : (advantage game1 game2 : ℝ≥0∞) = + max (game1 true - game2 true) (game2 true - game1 true) := by + rw [advantage, NNReal.nndist_eq, ENNReal.coe_max, ENNReal.coe_sub, ENNReal.coe_sub, + coe_succProbability_ennreal, coe_succProbability_ennreal] + constructor + · intro h + rw [hadv] + have h1 : game1 true ≤ game2 true + ε := by + simpa only [PMF.toOuterMeasure_apply_singleton] using h {true} + have h2 : game2 true ≤ game1 true + ε := by + simpa only [PMF.toOuterMeasure_apply_singleton] using h.symm {true} + exact max_le (tsub_le_iff_left.mpr h1) (tsub_le_iff_left.mpr h2) + · intro hadv_le event + rw [hadv, max_le_iff] at hadv_le + have ht1 : game1 true ≤ game2 true + ε := tsub_le_iff_left.mp hadv_le.1 + have ht2 : game2 true ≤ game1 true + ε := tsub_le_iff_left.mp hadv_le.2 + have hsum1 : game1 true + game1 false = 1 := by + simpa only [tsum_bool, add_comm] using game1.tsum_coe + have hsum2 : game2 true + game2 false = 1 := by + simpa only [tsum_bool, add_comm] using game2.tsum_coe + have hf1 : game1 false ≤ game2 false + ε := by + refine WithTop.le_of_add_le_add_left (game2.apply_ne_top true) ?_ + calc + game2 true + game1 false ≤ (game1 true + ε) + game1 false := + add_le_add ht2 le_rfl + _ = (game1 true + game1 false) + ε := by ac_rfl + _ = (game2 true + game2 false) + ε := by rw [hsum1, hsum2] + _ = game2 true + (game2 false + ε) := by ac_rfl + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, tsum_bool, tsum_bool] + by_cases h0 : false ∈ event <;> by_cases h1 : true ∈ event + · simp only [Set.indicator_of_mem h0, Set.indicator_of_mem h1] + rw [add_comm (game1 false), hsum1, add_comm (game2 false), hsum2] + exact le_self_add + · simp only [Set.indicator_of_mem h0, Set.indicator_of_notMem h1, add_zero] + exact hf1 + · simp only [Set.indicator_of_notMem h0, Set.indicator_of_mem h1, zero_add] + exact ht1 + · simp [Set.indicator_of_notMem h0, Set.indicator_of_notMem h1] + +/-- On Boolean experiments, `ε`-closeness for `ε : ℝ≥0` is equivalent to `advantage ≤ ε`. -/ +theorem closeTo_iff_advantage_le {game1 game2 : Game} {ε : ℝ≥0} : + CloseTo game1 game2 ε ↔ advantage game1 game2 ≤ ε := + closeTo_iff_coe_advantage_le.trans ENNReal.coe_le_coe + +/-- Deterministic Boolean postprocessing of `ε`-close distributions has `(advantage : ℝ≥0∞) ≤ ε`. -/ +theorem coe_advantage_map_le_of_closeTo {α : Type} {μ ν : PMF α} {ε : ℝ≥0∞} + (h : CloseTo μ ν ε) (f : α → Bool) : + (advantage (μ.map f) (ν.map f) : ℝ≥0∞) ≤ ε := + closeTo_iff_coe_advantage_le.mp (h.map f) + +/-- Deterministic Boolean postprocessing of `ε`-close distributions has `advantage ≤ ε`. -/ +theorem advantage_map_le_of_closeTo {α : Type} {μ ν : PMF α} {ε : ℝ≥0} + (h : CloseTo μ ν ε) (f : α → Bool) : + advantage (μ.map f) (ν.map f) ≤ ε := + closeTo_iff_advantage_le.mp (h.map f) + +/-- Running any randomized Boolean distinguisher `test : α → Game` on `ε`-close distributions has +`(advantage : ℝ≥0∞) ≤ ε`, without finiteness assumptions on `α`. -/ +theorem coe_advantage_bind_le_of_closeTo {α : Type} {μ ν : PMF α} {ε : ℝ≥0∞} + (h : CloseTo μ ν ε) (test : α → Game) : + (advantage (μ.bind test) (ν.bind test) : ℝ≥0∞) ≤ ε := + closeTo_iff_coe_advantage_le.mp (h.bind_left test) + +/-- Running any randomized Boolean distinguisher `test : α → Game` on `ε`-close distributions has +`advantage ≤ ε`, without finiteness assumptions on `α`. -/ +theorem advantage_bind_le_of_closeTo {α : Type} {μ ν : PMF α} {ε : ℝ≥0} + (h : CloseTo μ ν ε) (test : α → Game) : + advantage (μ.bind test) (ν.bind test) ≤ ε := + closeTo_iff_advantage_le.mp (h.bind_left test) + +open Classical in +/-- A bound in `ℝ≥0∞` on the advantage of every indicator test gives `CloseTo`. -/ +theorem closeTo_of_coe_advantage_decide_le {α : Type} {μ ν : PMF α} {ε : ℝ≥0∞} + (h : ∀ E : Set α, (advantage (μ.map fun a => decide (a ∈ E)) + (ν.map fun a => decide (a ∈ E)) : ℝ≥0∞) ≤ ε) : + CloseTo μ ν ε := fun E => by + 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 hclose := closeTo_iff_coe_advantage_le.mpr (h E) {true} + simpa only [PMF.toOuterMeasure_apply_singleton, hmap] using hclose + +open Classical in +/-- A bound in `ℝ≥0` on the advantage of every indicator test gives `CloseTo`. -/ +theorem closeTo_of_advantage_decide_le {α : Type} {μ ν : PMF α} {ε : ℝ≥0} + (h : ∀ E : Set α, advantage (μ.map fun a => decide (a ∈ E)) + (ν.map fun a => decide (a ∈ E)) ≤ ε) : + CloseTo μ ν ε := + closeTo_of_coe_advantage_decide_le fun E => ENNReal.coe_le_coe.mpr (h E) + +/-- Variational characterization of `CloseTo` in `ℝ≥0∞` via deterministic Boolean tests. -/ +theorem closeTo_iff_forall_coe_advantage_map_le {α : Type} {μ ν : PMF α} {ε : ℝ≥0∞} : + CloseTo μ ν ε ↔ ∀ f : α → Bool, (advantage (μ.map f) (ν.map f) : ℝ≥0∞) ≤ ε := by + classical + exact ⟨coe_advantage_map_le_of_closeTo, fun h => closeTo_of_coe_advantage_decide_le fun E => h _⟩ + +/-- Variational characterization of `CloseTo` for `ε : ℝ≥0` via deterministic Boolean tests. -/ +theorem closeTo_iff_forall_advantage_map_le {α : Type} {μ ν : PMF α} {ε : ℝ≥0} : + CloseTo μ ν ε ↔ ∀ f : α → Bool, advantage (μ.map f) (ν.map f) ≤ ε := by + classical + exact ⟨advantage_map_le_of_closeTo, fun h => closeTo_of_advantage_decide_le fun E => h _⟩ + +/-- Variational characterization of `CloseTo` in `ℝ≥0∞` via randomized Boolean distinguishers. -/ +theorem closeTo_iff_forall_coe_advantage_bind_le {α : Type} {μ ν : PMF α} {ε : ℝ≥0∞} : + CloseTo μ ν ε ↔ ∀ test : α → Game, (advantage (μ.bind test) (ν.bind test) : ℝ≥0∞) ≤ ε := by + rw [closeTo_iff_forall_coe_advantage_map_le] + refine ⟨fun h test => coe_advantage_bind_le_of_closeTo + (closeTo_iff_forall_coe_advantage_map_le.mpr h) test, fun h f => ?_⟩ + rw [← PMF.bind_pure_comp, ← PMF.bind_pure_comp] + exact h _ + +/-- Variational characterization of `CloseTo` for `ε : ℝ≥0` via randomized Boolean +distinguishers. -/ +theorem closeTo_iff_forall_advantage_bind_le {α : Type} {μ ν : PMF α} {ε : ℝ≥0} : + CloseTo μ ν ε ↔ ∀ test : α → Game, advantage (μ.bind test) (ν.bind test) ≤ ε := by + rw [closeTo_iff_forall_advantage_map_le] + refine ⟨fun h test => advantage_bind_le_of_closeTo + (closeTo_iff_forall_advantage_map_le.mpr h) test, fun h f => ?_⟩ + rw [← PMF.bind_pure_comp, ← PMF.bind_pure_comp] + exact h _ + +end Cslib.Crypto.Game diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean new file mode 100644 index 0000000000..d760d797d4 --- /dev/null +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean @@ -0,0 +1,385 @@ +/- +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.Probabilistic.Parameter +public import Complexity.Crypto.Game.CloseTo +public import Complexity.Crypto.Protocols.SigmaProtocol.Efficient + +/-! +# Computational special honest-verifier zero knowledge + +Boneh and Shoup's computational relaxation of special HVZK ([BonehShoup2023], Section 20.4.2, +Attack Game 20.4 and Definition 20.6, p. 840) for an indexed family of Sigma protocols `P i` +equipped with word encodings `enc : SigmaProtocol.Encoding I Y T C Z`, witness encodings +`encW : ∀ i, X i ↪ List Bool`, and a parameter distribution `setup : ℕ → PMF I` ([BonehShoup2023], +Section 2.3.4). + +In Attack Game 20.4, at security parameter `n`, the challenger draws `i ← setup n` and gives +`(n, i)` to `adversary.choose`, which outputs an encoded witness-statement pair `(xw, yw)` together +with a saved state word. When `(xw, yw)` decodes to `(x, y)` in `R i` (uniquely, by injectivity of +`encW i` and `enc.statement i`): + +* **Experiment 0** (`chvzkRealGame`) samples an honest conversation + `(t, c, z) ← (P i).conversation x y`, encodes `(t, c, z)` into words, and passes it with the + saved state to `adversary.guess`. +* **Experiment 1** (`chvzkSimGame`) samples a uniform challenge `c ← PMF.uniformOfFintype (C i)`, + runs the simulator program `sim` on `(i, enc.statement i y, enc.challenge i c)` without using `x` + to obtain `(tw, zw)`, and passes `(tw, enc.challenge i c, zw)` with the saved state to + `adversary.guess`. + +When `(xw, yw)` is not an encoded pair in `R i`, both experiments output `false`, matching the +admissibility convention of `Cslib.Crypto.Encryption.gameOn` so invalid choices contribute zero +advantage without requiring `R i` to be efficiently decidable by the challenger. + +`ComputationalSpecialHVZK P R enc encW setup sim δ` bundles: + +1. Uniform strict PPT admissibility of `sim` on `(i, yw, cw)`. +2. Acceptance on every `(i, y, c)` with probability at least `1 - δ i` (exact Definition 20.6 + acceptance when `δ = 0`; relaxed by `δ` when a strict PPT fair-coin simulator approximates a + non-dyadic distribution). +3. Negligible distinguishing advantage between `chvzkRealGame` and `chvzkSimGame` for every uniform + strict PPT `CHVZKAdversary`. + +Every `EfficientSpecialHVZK` protocol whose realization error `δ` is bounded along `setup` by a +negligible function satisfies `ComputationalSpecialHVZK` — in fact against arbitrary, even +computationally unbounded adversaries at each security parameter +(`SimulatorRealizedBy.advantage_chvzkGame_le`, +`EfficientSpecialHVZK.exists_computationalSpecialHVZK`). As in `EfficientSpecialHVZK`, `δ` is an +explicit parameter of `ComputationalSpecialHVZK` rather than a bundled `Negligible` condition on the +acceptance error alone; exact Definition 20.6 acceptance corresponds to `δ = fun _ => 0` (which +Schnorr's word simulator achieves in `PrimeOrderGroupFamily.computationalSpecialHVZK_schnorr`). + +## Main definitions + +* `Cslib.Crypto.Protocols.SigmaProtocol.CHVZKAdversary`, + `Cslib.Crypto.Protocols.SigmaProtocol.CHVZKAdversary.IsPPT`: two-stage adversaries and uniform + strict PPT admissibility for Attack Game 20.4. +* `Cslib.Crypto.Protocols.SigmaProtocol.encodedConversation`, + `Cslib.Crypto.Protocols.SigmaProtocol.simulatedConversation`: honest and simulated encoded + conversation distributions. +* `Cslib.Crypto.Protocols.SigmaProtocol.chvzkBranch`, + `Cslib.Crypto.Protocols.SigmaProtocol.chvzkGameWith`, + `Cslib.Crypto.Protocols.SigmaProtocol.chvzkRealGame`, + `Cslib.Crypto.Protocols.SigmaProtocol.chvzkSimGame`: Attack Game 20.4 experiments. +* `Cslib.Crypto.Protocols.SigmaProtocol.ComputationalSpecialHVZK`: Definition 20.6 with explicit + simulator and acceptance error `δ`. + +## Main results + +* `Cslib.Crypto.Protocols.SigmaProtocol.chvzkBranch_valid`, + `Cslib.Crypto.Protocols.SigmaProtocol.chvzkBranch_invalid`: reduction of Attack Game 20.4's + validity check on valid and invalid witness-statement pairs. +* `Cslib.Crypto.Protocols.SigmaProtocol.SimulatorRealizedBy.closeTo_conversation`: statistical + closeness of honest and simulated encoded conversations. +* `Cslib.Crypto.Protocols.SigmaProtocol.SimulatorRealizedBy.advantage_chvzkGame_le`: concrete + advantage bound in Attack Game 20.4 against arbitrary adversaries. +* `Cslib.Crypto.Protocols.SigmaProtocol.SimulatorRealizedBy.computationalSpecialHVZK_of_accepts`, + `Cslib.Crypto.Protocols.SigmaProtocol.SimulatorRealizedBy.computationalSpecialHVZK`, + `Cslib.Crypto.Protocols.SigmaProtocol.EfficientSpecialHVZK.exists_computationalSpecialHVZK`: + statistical special HVZK with negligible realization error along `setup` implies computational + special HVZK. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Section 2.3.4 and Section 20.4.2 (Attack Game 20.4 and + Definition 20.6, p. 840). +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.SigmaProtocol + +open Probability Turing.MultiTapeTM Interactive +open scoped ENNReal NNReal + +/-- A two-stage adversary for Attack Game 20.4 ([BonehShoup2023], Section 20.4.2, p. 840) over +index type `I`. Stage 1 (`choose`) receives the security parameter and the sampled index, outputs +an encoded witness-statement pair `(xw, yw)` together with a saved state word; Stage 2 (`guess`) +receives the security parameter, the saved state, and an encoded conversation `(tw, cw, zw)`, and +outputs a distinguishing bit. -/ +structure CHVZKAdversary (I : Type) where + /-- Compute an encoded `(witness, statement)` pair and save state for the guessing phase. -/ + choose : ℕ → I → ProbComp ((List Bool × List Bool) × List Bool) + /-- Distinguish an honest encoded conversation from a simulated one using the saved state. -/ + guess : ℕ → List Bool → List Bool × List Bool × List Bool → ProbComp Bool + +/-- Uniform strict PPT admissibility for both stages of a `CHVZKAdversary`, charging the unary +security parameter, the index encoding `encIdx`, and the full saved state. -/ +structure CHVZKAdversary.IsPPT {I : Type} (encIdx : I ↪ List Bool) + (adversary : CHVZKAdversary I) : Prop where + /-- Choosing the encoded witness-statement pair and saved state is uniform strict PPT. -/ + choose : IsPPTOn (encPair encUnary encIdx) + (encPair (encPair encBits encBits) encBits) + (fun ⟨n, i⟩ => adversary.choose n i) + /-- Guessing from the security parameter, saved state and encoded conversation is uniform strict + PPT. -/ + guess : IsPPTOn + (encPair encUnary (encPair encBits (encPair encBits (encPair encBits encBits)))) + encBool + (fun ⟨n, state, conv⟩ => adversary.guess n state conv) + +variable {I : Type} {X Y T C Z : I → Type} + +/-- Honest conversation of `P i` on `(x, y)`, encoded into bit words via `enc`. -/ +noncomputable def encodedConversation + (P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i)) + [∀ i, Fintype (C i)] [∀ i, Nonempty (C i)] + (enc : Encoding I Y T C Z) (i : I) (x : X i) (y : Y i) : + PMF (List Bool × List Bool × List Bool) := + ((P i).conversation x y).map fun ⟨t, c, z⟩ => + (enc.commitment i t, enc.challenge i c, enc.response i z) + +/-- Simulated encoded conversation on `(i, y)`: sample a uniform challenge `c : C i`, run `sim` on +`(i, enc.statement i y, enc.challenge i c)` to obtain `(tw, zw)`, and return +`(tw, enc.challenge i c, zw)` ([BonehShoup2023], Section 20.4.2, Attack Game 20.4, Experiment 1, +p. 840). -/ +noncomputable def simulatedConversation + [∀ i, Fintype (C i)] [∀ i, Nonempty (C i)] + (enc : Encoding I Y T C Z) + (sim : I × List Bool × List Bool → ProbComp (List Bool × List Bool)) + (i : I) (y : Y i) : PMF (List Bool × List Bool × List Bool) := do + let c ← PMF.uniformOfFintype (C i) + let ⟨tw, zw⟩ ← ProbComp.eval (sim (i, enc.statement i y, enc.challenge i c)) + return (tw, enc.challenge i c, zw) + +open Classical in +/-- Challenger continuation of Attack Game 20.4 after `adversary.choose` outputs `((xw, yw), state)` +at `(n, i)`: if `(xw, yw)` decodes via `encW i` and `enc.statement i` to a valid pair `(x, y)` in +`R i`, sample a conversation with `sampleConv i x y` and run `adversary.guess`; otherwise return +`false`. -/ +noncomputable def chvzkBranch + (R : ∀ i, X i → Y i → Prop) + (enc : Encoding I Y T C Z) (encW : ∀ i, X i ↪ List Bool) + (sampleConv : ∀ i, X i → Y i → PMF (List Bool × List Bool × List Bool)) + (adversary : CHVZKAdversary I) (n : ℕ) (i : I) + (xw yw state : List Bool) : Game := + if h : ∃ p : X i × Y i, encW i p.1 = xw ∧ enc.statement i p.2 = yw ∧ R i p.1 p.2 then + (sampleConv i h.choose.1 h.choose.2).bind fun conv => + ProbComp.eval (adversary.guess n state conv) + else + PMF.pure false + +/-- On an encoded valid pair `(encW i x, enc.statement i y)` with `R i x y`, `chvzkBranch` selects +`(x, y)` uniquely by injectivity of `encW i` and `enc.statement i`. -/ +@[simp] theorem chvzkBranch_valid + {R : ∀ i, X i → Y i → Prop} + {enc : Encoding I Y T C Z} {encW : ∀ i, X i ↪ List Bool} + (sampleConv : ∀ i, X i → Y i → PMF (List Bool × List Bool × List Bool)) + (adversary : CHVZKAdversary I) (n : ℕ) (i : I) + {x : X i} {y : Y i} (hxy : R i x y) (state : List Bool) : + chvzkBranch R enc encW sampleConv adversary n i (encW i x) (enc.statement i y) state = + ((sampleConv i x y).bind fun conv => ProbComp.eval (adversary.guess n state conv)) := by + classical + have hex : ∃ p : X i × Y i, + encW i p.1 = encW i x ∧ enc.statement i p.2 = enc.statement i y ∧ R i p.1 p.2 := + ⟨(x, y), rfl, rfl, hxy⟩ + rw [chvzkBranch, dite_eq_left hex] + have hp : hex.choose = (x, y) := + Prod.ext ((encW i).injective hex.choose_spec.1) + ((enc.statement i).injective hex.choose_spec.2.1) + rw [hp] + +/-- When `(xw, yw)` does not decode to a valid witness-statement pair in `R i`, `chvzkBranch` +outputs `false`. -/ +theorem chvzkBranch_invalid + {R : ∀ i, X i → Y i → Prop} + {enc : Encoding I Y T C Z} {encW : ∀ i, X i ↪ List Bool} + (sampleConv : ∀ i, X i → Y i → PMF (List Bool × List Bool × List Bool)) + (adversary : CHVZKAdversary I) (n : ℕ) (i : I) + {xw yw : List Bool} (state : List Bool) + (hinv : ¬ ∃ p : X i × Y i, encW i p.1 = xw ∧ enc.statement i p.2 = yw ∧ R i p.1 p.2) : + chvzkBranch R enc encW sampleConv adversary n i xw yw state = PMF.pure false := by + classical + rw [chvzkBranch, dite_eq_right hinv] + +/-- Shared Attack Game 20.4 experiment parameterized by the challenger's conversation sampler +`sampleConv`. -/ +noncomputable def chvzkGameWith + (R : ∀ i, X i → Y i → Prop) + (enc : Encoding I Y T C Z) (encW : ∀ i, X i ↪ List Bool) + (setup : ℕ → PMF I) + (sampleConv : ∀ i, X i → Y i → PMF (List Bool × List Bool × List Bool)) + (adversary : CHVZKAdversary I) (n : ℕ) : Game := do + let i ← setup n + let ⟨⟨xw, yw⟩, state⟩ ← ProbComp.eval (adversary.choose n i) + chvzkBranch R enc encW sampleConv adversary n i xw yw state + +/-- Experiment 0 of Attack Game 20.4 ([BonehShoup2023], Section 20.4.2, p. 840): on a valid encoded +witness-statement pair `(x, y)` chosen by `adversary`, give `adversary.guess` an honest encoded +conversation of `P i` on `(x, y)`. -/ +noncomputable def chvzkRealGame + (P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i)) + [∀ i, Fintype (C i)] [∀ i, Nonempty (C i)] + (R : ∀ i, X i → Y i → Prop) + (enc : Encoding I Y T C Z) (encW : ∀ i, X i ↪ List Bool) + (setup : ℕ → PMF I) (adversary : CHVZKAdversary I) (n : ℕ) : Game := + chvzkGameWith R enc encW setup (encodedConversation P enc) adversary n + +/-- Experiment 1 of Attack Game 20.4 ([BonehShoup2023], Section 20.4.2, p. 840): on a valid encoded +witness-statement pair `(x, y)` chosen by `adversary`, give `adversary.guess` a simulated +conversation produced from `y` and a uniform challenge without using `x`. -/ +noncomputable def chvzkSimGame + [∀ i, Fintype (C i)] [∀ i, Nonempty (C i)] + (R : ∀ i, X i → Y i → Prop) + (enc : Encoding I Y T C Z) (encW : ∀ i, X i ↪ List Bool) + (setup : ℕ → PMF I) + (sim : I × List Bool × List Bool → ProbComp (List Bool × List Bool)) + (adversary : CHVZKAdversary I) (n : ℕ) : Game := + chvzkGameWith R enc encW setup (fun i _ y => simulatedConversation enc sim i y) adversary n + +/-- **Computational special honest-verifier zero knowledge** ([BonehShoup2023], Section 20.4.2, +Definition 20.6, p. 840), for a family `P` of Sigma protocols over `setup` with explicit word +simulator `sim` and acceptance error `δ`: `sim` is uniform strict PPT, outputs an encoded accepting +conversation on every `(i, y, c)` with probability at least `1 - δ i` (exact Definition 20.6 +acceptance when `δ = fun _ => 0`), and every uniform strict PPT `CHVZKAdversary` has negligible +distinguishing advantage between `chvzkRealGame` and `chvzkSimGame`. -/ +structure ComputationalSpecialHVZK + (P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i)) + [∀ i, Fintype (C i)] [∀ i, Nonempty (C i)] + (R : ∀ i, X i → Y i → Prop) + (enc : Encoding I Y T C Z) (encW : ∀ i, X i ↪ List Bool) + (setup : ℕ → PMF I) + (sim : I × List Bool × List Bool → ProbComp (List Bool × List Bool)) + (δ : I → ℝ≥0∞) : Prop where + /-- The simulator is uniform strict PPT in the index and the encoded statement and challenge. -/ + ppt : IsPPTOn (encPair enc.index (encPair encBits encBits)) (encPair encBits encBits) sim + /-- On every statement and challenge, `sim` outputs an encoded accepting conversation with + probability at least `1 - δ i`. -/ + accepts : ∀ i (y : Y i) (c : C i), 1 - δ i ≤ + (ProbComp.eval (sim (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} + /-- Honest and simulated conversations are computationally indistinguishable in Attack Game + 20.4. -/ + indistinguishable : + Game.Indistinguishable (chvzkRealGame P R enc encW setup) + (chvzkSimGame R enc encW setup sim) (CHVZKAdversary.IsPPT enc.index) + +/-- Relaxing the acceptance-error bound preserves `ComputationalSpecialHVZK`. -/ +theorem ComputationalSpecialHVZK.mono_error + {P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i)} + [∀ i, Fintype (C i)] [∀ i, Nonempty (C i)] + {R : ∀ i, X i → Y i → Prop} + {enc : Encoding I Y T C Z} {encW : ∀ i, X i ↪ List Bool} + {setup : ℕ → PMF I} + {sim : I × List Bool × List Bool → ProbComp (List Bool × List Bool)} + {δ δ' : I → ℝ≥0∞} + (h : ComputationalSpecialHVZK P R enc encW setup sim δ) (hle : ∀ i, δ i ≤ δ' i) : + ComputationalSpecialHVZK P R enc encW setup sim δ' where + ppt := h.ppt + accepts i y c := (tsub_le_tsub_left (hle i) 1).trans (h.accepts i y c) + indistinguishable := h.indistinguishable + +/-! ### Bridging statistical `EfficientSpecialHVZK` to `ComputationalSpecialHVZK` -/ + +section StatisticalBridge + +variable {P : ∀ i, SigmaProtocol (X i) (Y i) (T i) (C i) (Z i)} + [∀ i, Fintype (C i)] [∀ i, Nonempty (C i)] + {R : ∀ i, X i → Y i → Prop} + {enc : Encoding I Y T C Z} {encW : ∀ i, X i ↪ List Bool} + {setup : ℕ → PMF I} + {simulate : ∀ i, Y i → C i → PMF (T i × Z i)} + {sim : I × List Bool × List Bool → ProbComp (List Bool × List Bool)} + {δ : I → ℝ≥0∞} + +/-- A program realizing a perfect special HVZK simulator up to `δ i` produces simulated encoded +conversations within statistical distance `δ i` of honest encoded conversations, for every valid +witness-statement pair. -/ +theorem SimulatorRealizedBy.closeTo_conversation + (hS : ∀ i, (P i).SpecialHVZK (R i) (simulate i)) + (h : SimulatorRealizedBy enc simulate sim δ) + {i : I} {x : X i} {y : Y i} (hxy : R i x y) : + CloseTo (encodedConversation P enc i x y) (simulatedConversation enc sim i y) (δ i) := by + let post (c : C i) (p : List Bool × List Bool) : List Bool × List Bool × List Bool := + (p.1, enc.challenge i c, p.2) + have henc : encodedConversation P enc i x y = + (PMF.uniformOfFintype (C i)).bind fun c => + ((simulate i y c).map (Prod.map (enc.commitment i) (enc.response i))).map (post c) := by + rw [encodedConversation, (hS i).conversation_eq hxy] + simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.map_bind, PMF.pure_map, + PMF.map_comp] + apply congrArg (PMF.bind _) + funext c + rw [← PMF.bind_pure_comp] + rfl + have hsim : simulatedConversation enc sim i y = + (PMF.uniformOfFintype (C i)).bind fun c => + (ProbComp.eval (sim (i, enc.statement i y, enc.challenge i c))).map (post c) := by + simp only [simulatedConversation, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] + apply congrArg (PMF.bind _) + funext c + rw [← PMF.bind_pure_comp] + rfl + rw [henc, hsim] + exact CloseTo.bind_right (PMF.uniformOfFintype (C i)) fun c _ => (h i y c).map (post c) + +/-- When `δ i ≤ ε` on `(setup n).support`, a program realizing a perfect special HVZK simulator has +Attack Game 20.4 advantage at most `ε` against *every* adversary (including computationally +unbounded adversaries). -/ +theorem SimulatorRealizedBy.advantage_chvzkGame_le + (hS : ∀ i, (P i).SpecialHVZK (R i) (simulate i)) + (h : SimulatorRealizedBy enc simulate sim δ) + {n : ℕ} {ε : ℝ≥0} (hδ : ∀ i ∈ (setup n).support, δ i ≤ ε) + (adversary : CHVZKAdversary I) : + Game.advantage (chvzkRealGame P R enc encW setup adversary n) + (chvzkSimGame R enc encW setup sim adversary n) ≤ ε := by + simp only [chvzkRealGame, chvzkSimGame, chvzkGameWith, PMF.monad_bind_eq_bind] + refine Game.advantage_bind_le_of_support (setup n) _ _ fun i hi => ?_ + refine Game.advantage_bind_le_nnreal (ProbComp.eval (adversary.choose n i)) _ _ + fun ⟨⟨xw, yw⟩, state⟩ => ?_ + classical + by_cases hv : ∃ p : X i × Y i, encW i p.1 = xw ∧ enc.statement i p.2 = yw ∧ R i p.1 p.2 + · obtain ⟨⟨x, y⟩, rfl, rfl, hxy⟩ := hv + simp only [chvzkBranch_valid _ _ _ _ hxy] + exact Game.advantage_bind_le_of_closeTo ((h.closeTo_conversation hS hxy).mono (hδ i hi)) _ + · simp only [chvzkBranch_invalid _ _ _ _ _ hv, Game.advantage_self, zero_le] + +/-- A strict PPT program realizing a perfect special HVZK simulator with negligible statistical +error along `setup` gives `ComputationalSpecialHVZK`, retaining any independently proved acceptance +error `δ'`. -/ +theorem SimulatorRealizedBy.computationalSpecialHVZK_of_accepts + {δ' : I → ℝ≥0∞} + (hS : ∀ i, (P i).SpecialHVZK (R i) (simulate i)) + (hppt : IsPPTOn (encPair enc.index (encPair encBits encBits)) (encPair encBits encBits) sim) + (hreal : SimulatorRealizedBy enc simulate sim δ) + (hacc : ∀ i (y : Y i) (c : C i), 1 - δ' i ≤ + (ProbComp.eval (sim (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}) + (hnegl : ∃ ε : ℕ → ℝ≥0, Negligible ε ∧ ∀ n, ∀ i ∈ (setup n).support, δ i ≤ ε n) : + ComputationalSpecialHVZK P R enc encW setup sim δ' where + ppt := hppt + accepts := hacc + indistinguishable adversary _ := by + obtain ⟨ε, hε, hle⟩ := hnegl + exact negligible_of_le hε fun n => hreal.advantage_chvzkGame_le hS (hle n) adversary + +/-- A strict PPT program realizing a perfect special HVZK simulator with negligible statistical +error along `setup` satisfies `ComputationalSpecialHVZK` with acceptance error `δ`. -/ +theorem SimulatorRealizedBy.computationalSpecialHVZK + (hS : ∀ i, (P i).SpecialHVZK (R i) (simulate i)) + (hppt : IsPPTOn (encPair enc.index (encPair encBits encBits)) (encPair encBits encBits) sim) + (hreal : SimulatorRealizedBy enc simulate sim δ) + (hnegl : ∃ ε : ℕ → ℝ≥0, Negligible ε ∧ ∀ n, ∀ i ∈ (setup n).support, δ i ≤ ε n) : + ComputationalSpecialHVZK P R enc encW setup sim δ := + hreal.computationalSpecialHVZK_of_accepts hS hppt (hreal.one_sub_le_accepts hS) hnegl + +/-- **Efficient statistical special HVZK implies computational special HVZK** whenever the +realization error `δ` is bounded along `setup` by a negligible function. -/ +theorem EfficientSpecialHVZK.exists_computationalSpecialHVZK + (h : EfficientSpecialHVZK P R enc simulate δ) + (encW : ∀ i, X i ↪ List Bool) (setup : ℕ → PMF I) + (hnegl : ∃ ε : ℕ → ℝ≥0, Negligible ε ∧ ∀ n, ∀ i ∈ (setup n).support, δ i ≤ ε n) : + ∃ sim, ComputationalSpecialHVZK P R enc encW setup sim δ := by + obtain ⟨sim, hppt, hreal⟩ := h.realized + exact ⟨sim, hreal.computationalSpecialHVZK h.specialHVZK hppt hnegl⟩ + +end StatisticalBridge + +end Cslib.Crypto.Protocols.SigmaProtocol diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean index 92b2074599..b534ecabec 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean @@ -47,8 +47,15 @@ every theorem about `SpecialSoundness` and `SpecialHVZK` applies to them. The re 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. +Note that `δ` in `EfficientSpecialHVZK` is an unconstrained parameter of the predicate rather than +a bundled `Negligible` condition: at `δ i ≥ 1` (since event probabilities are at most `1`), +`SimulatorRealizedBy` holds trivially for every strict PPT program, reducing `EfficientSpecialHVZK` +to the unbounded `SpecialHVZK` field (`not_efficientSpecialHVZK_sendWitness` in +`ComplexityTests.EfficientSimulators` requires `δ i ≤ 1 / 2`). Computational special HVZK +([BonehShoup2023], Definition 20.6) is defined in +`Complexity.Crypto.Protocols.SigmaProtocol.Computational` +(`SigmaProtocol.ComputationalSpecialHVZK`); when `δ` is bounded along the setup distribution by a +negligible function, `EfficientSpecialHVZK.exists_computationalSpecialHVZK` derives it. ## Main definitions diff --git a/ComplexityTests/ComputationalSpecialHVZK.lean b/ComplexityTests/ComputationalSpecialHVZK.lean new file mode 100644 index 0000000000..ee33a71460 --- /dev/null +++ b/ComplexityTests/ComputationalSpecialHVZK.lean @@ -0,0 +1,722 @@ +/- +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.Crypto.Computational.DiscreteLog.SchnorrGroup +import Complexity.Crypto.Computational.OneWayToPRG +import Complexity.Crypto.Computational.SchnorrProtocol +import Complexity.Crypto.Game.CloseTo +import Complexity.Crypto.Negligible.Basic +import Complexity.Crypto.Protocols.SigmaProtocol.Computational +import Complexity.Probability.PMF.Event +import Complexity.Tactic.PPT +import ComplexityTests.EfficientSimulators +import ComplexityTests.UnboundedSimulators + +/-! +# Computational special HVZK and `Game.advantage`/`CloseTo` bridges + +Checks of `Complexity.Crypto.Game.CloseTo`, `Complexity.Computability.Interactive.Security`'s +`CloseTo` calculus, and `SigmaProtocol.ComputationalSpecialHVZK` ([BonehShoup2023], Section 20.4.2, +Attack Game 20.4 and Definition 20.6, p. 840) on concrete instances and two-sided separations: + +* **Boolean and infinite-type `CloseTo`/`Game` bridges.** Check `Game.closeTo_iff_advantage_le` on + concrete `PMF Bool` laws and `Game.advantage_bind_le_of_closeTo` across `PMF ℕ` without + `Fintype`. +* **Schnorr in `schnorrGroups`.** Instantiate + `PrimeOrderGroupFamily.computationalSpecialHVZK_schnorr` with exact zero acceptance error + (`δ = fun _ => 0`), exercising both `accepts_schnorrSimulateWord` and Attack Game 20.4 + indistinguishability. +* **`SpecialHVZK` does not imply `ComputationalSpecialHVZK` (under discrete log).** The protocol + `sendWitnessFamily F` is perfectly `SpecialHVZK` at every index (`specialHVZK_sendWitness`), yet + under `F.DiscreteLog setup` it fails `ComputationalSpecialHVZK` for *every* simulator `sim` and + *every* acceptance-error parameter `δ` (even `δ = fun _ => ⊤`, without invoking `accepts`), + because Attack Game 20.4's `indistinguishable` obligation alone forces `sim` to invert discrete + logarithms (`not_computationalSpecialHVZK_sendWitness`). +* **`ComputationalSpecialHVZK` does not imply `SpecialHVZK` or `EfficientSpecialHVZK` (from any PRG + or OWF).** For any stretching `PseudorandomGenerator generator length`, the protocol family + `prgWitnessSigma generator length` commits to `generator seed` when the witness bit is `false` and + to a uniform `length n`-bit string when the witness bit is `true`. Its word simulator samples a + uniform `length n`-bit commitment, achieving `ComputationalSpecialHVZK` with exact zero acceptance + error (`computationalSpecialHVZK_prgWitnessSigma`), whereas the `2 ^ n`-element generator image + covers at most half of `{0, 1} ^ (length n)`, ruling out `SpecialHVZK`, `EfficientSpecialHVZK` for + every `δ`, and even unbounded statistical transcript simulation below error `1 / 4` + (`not_specialHVZK_prgWitnessSigma`, `not_efficientSpecialHVZK_prgWitnessSigma`, + `not_statistical_hvzk_prgWitnessSigma`, `exists_computationalSpecialHVZK_and_not_specialHVZK`). +-/ + +namespace ComplexityTests.ComputationalSpecialHVZK + +open Cslib Cslib.Crypto Cslib.Crypto.Protocols Cslib.Crypto.Protocols.SigmaProtocol + Cslib.Interactive Probability Turing.MultiTapeTM + ComplexityTests.UnboundedSimulators.Sigma ComplexityTests.EfficientSimulators +open scoped ENNReal NNReal + +/-! ### `Game.advantage` and `CloseTo` bridges -/ + +/-- A point mass and a fair coin have advantage `1 / 2`, so `CloseTo` holds at `1 / 2` and fails at +`1 / 4`. -/ +example : CloseTo (PMF.pure true) (PMF.uniformOfFintype Bool) ((1 / 2 : ℝ≥0) : ℝ≥0∞) ∧ + ¬ CloseTo (PMF.pure true) (PMF.uniformOfFintype Bool) ((1 / 4 : ℝ≥0) : ℝ≥0∞) := by + have hadv : Game.advantage (PMF.pure true) (PMF.uniformOfFintype Bool) = 1 / 2 := by + apply NNReal.eq + rw [Game.coe_guessingAdvantage] + simp only [Game.succProbability, PMF.pure_apply, ↓reduceIte, ENNReal.toNNReal_one, + NNReal.coe_one] + norm_num + rw [Game.closeTo_iff_advantage_le, Game.closeTo_iff_advantage_le, hadv] + exact ⟨le_rfl, by norm_num⟩ + +/-- `Game.advantage_bind_le_of_closeTo` bounds randomized Boolean distinguishers on `PMF ℕ` without +any `Fintype` assumption. -/ +example (μ ν : PMF ℕ) (h : CloseTo μ ν ((1 / 8 : ℝ≥0) : ℝ≥0∞)) (test : ℕ → Game) : + Game.advantage (μ.bind test) (ν.bind test) ≤ 1 / 8 := + Game.advantage_bind_le_of_closeTo h test + +/-! ### Schnorr in `schnorrGroups` -/ + +/-- Schnorr's Sigma protocol in `schnorrGroups` satisfies `ComputationalSpecialHVZK` with exact zero +acceptance error (`δ = fun _ => 0`) for any group-description setup `setup`. -/ +example (setup : ℕ → PMF schnorrGroups.Desc) : + ComputationalSpecialHVZK schnorrGroups.schnorrFamily + (fun i α u => α • schnorrGroups.generator i.2 = u) + schnorrGroups.schnorrEncoding (fun i => schnorrGroups.encScalar i.2) + (fun n => (setup n).map (n, ·)) schnorrGroups.schnorrSimulateWord (fun _ => 0) := + schnorrGroups.computationalSpecialHVZK_schnorr setup + +/-! ### `SpecialHVZK` does not imply `ComputationalSpecialHVZK` -/ + +section DiscreteLogSeparation + +variable {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} + +/-- Attack Game 20.4 adversary against `sendWitnessFamily F`: sample `s ← F.sampleExp n d`, submit +the valid discrete-logarithm pair `((s mod q).bits, F.encode d (s • g))` while saving +`state = (s mod q).bits`, and check whether the challenger's commitment word equals `state`. -/ +noncomputable def sendWitnessAdversary (F : PrimeOrderGroupFamily) : + CHVZKAdversary (ℕ × F.Desc) where + choose n idx := + let ⟨_, d⟩ := idx + do + let s ← F.sampleExp n d + let xw := (s % F.order d).bits + return ((xw, F.smul (d, s, F.encode d (F.generator d))), xw) + guess _ state conv := + let ⟨tw, _, _⟩ := conv + pure (tw == state) + +theorem isPPT_sendWitnessAdversary (F : PrimeOrderGroupFamily) : + CHVZKAdversary.IsPPT (sendWitnessEncoding F).index (sendWitnessAdversary F) where + choose := by + let encIdx := (sendWitnessEncoding F).index + let encIn := encPair encUnary encIdx + have hn : ComputableInPolyTime (fun p : ℕ × ℕ × F.Desc => p.1) encIn encUnary := by fun_prop + have hp2 : ComputableInPolyTime (fun p : ℕ × ℕ × F.Desc => p.2) encIn encIdx := by fun_prop + have hd : ComputableInPolyTime (fun (⟨_, _, d⟩ : ℕ × ℕ × F.Desc) => d) encIn F.encDesc := + (ComputableInPolyTime.snd encUnary F.encDesc).comp hp2 + change IsPPTOn encIn _ fun ⟨n, _, d⟩ => F.sampleExp n d >>= fun s => + pure (((s % F.order d).bits, + F.smul (d, s, F.encode d (F.generator d))), (s % F.order d).bits) + refine (F.isPPTOn_sampleExp hn hd).bind_with ?_ + let encMid := encPair encIn encNat + have hp1 : ComputableInPolyTime (fun q : (ℕ × ℕ × F.Desc) × ℕ => q.1) encMid encIn := by + fun_prop + have hd' : ComputableInPolyTime (fun (⟨⟨_, _, d⟩, _⟩ : (ℕ × ℕ × F.Desc) × ℕ) => d) + encMid F.encDesc := + hd.comp hp1 + have hs : ComputableInPolyTime (fun q : (ℕ × ℕ × F.Desc) × ℕ => q.2) encMid encNat := by + fun_prop + have hq := F.computableInPolyTime_order.comp hd' + have hmod : ComputableInPolyTime + (fun (⟨⟨_, _, d⟩, s⟩ : (ℕ × ℕ × F.Desc) × ℕ) => s % F.order d) encMid encNat := + ComputableInPolyTime.binary_mod.comp (hs.prod hq) + have hbits : ComputableInPolyTime Nat.bits encNat encBits := + (by fun_prop : ComputableInPolyTime id encNat encNat).of_enc_eq fun _ => rfl + have hxw := hbits.comp hmod + have hg := F.computableInPolyTime_generator.comp hd' + have hyw := F.computableInPolyTime_smul.comp (hd'.prod (hs.prod hg)) + exact ((hxw.prod hyw).prod hxw).isPPTOn + guess := by + let encConv := encPair encBits (encPair encBits encBits) + let encRest := encPair encBits encConv + let encIn := encPair encUnary encRest + have hrest : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool × List Bool × List Bool => p.2) encIn encRest := by + fun_prop + have hst : ComputableInPolyTime + (fun (⟨_, st, _⟩ : ℕ × List Bool × List Bool × List Bool × List Bool) => st) + encIn encBits := + (ComputableInPolyTime.fst encBits encConv).comp hrest + have hconv : ComputableInPolyTime + (fun (⟨_, _, conv⟩ : ℕ × List Bool × List Bool × List Bool × List Bool) => conv) + encIn encConv := + (ComputableInPolyTime.snd encBits encConv).comp hrest + have htw : ComputableInPolyTime + (fun (⟨_, _, tw, _⟩ : ℕ × List Bool × List Bool × List Bool × List Bool) => tw) + encIn encBits := + (ComputableInPolyTime.fst encBits (encPair encBits encBits)).comp hconv + have hbeq : ComputableInPolyTime (fun q : List Bool × List Bool => q.1 == q.2) + (encPair encBits encBits) encBool := by fun_prop + exact (hbeq.comp (htw.prod hst)).isPPTOn + +/-- **Sending the witness is not computationally special HVZK** under the discrete-logarithm +assumption, for *any* simulator `sim` and *any* acceptance-error function `δ` (without using the +`accepts` field): Attack Game 20.4 indistinguishability on `(x, x • g)` forces `sim` to invert +discrete logarithms. -/ +theorem not_computationalSpecialHVZK_sendWitness (hDL : F.DiscreteLog setup) + (sim : (ℕ × F.Desc) × List Bool × List Bool → ProbComp (List Bool × List Bool)) + (δ : ℕ × F.Desc → ℝ≥0∞) : + ¬ ComputationalSpecialHVZK (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) + (fun i => F.encScalar i.2) (fun n => (setup n).map (n, ·)) sim δ := by + intro h + let dlAdv : ℕ → F.Desc × List Bool → ProbComp (List Bool) := fun n input => do + let c ← ProbComp.uniform Bool + Prod.fst <$> sim ((n, input.1), input.2, encBool c) + have hdlAdv : IsPPTOn (encPair encUnary (encPair F.encDesc encBits)) encBits + (fun input => dlAdv input.1 input.2) := by + let encIn := encPair encUnary (encPair F.encDesc encBits) + have hn : ComputableInPolyTime (fun p : ℕ × F.Desc × List Bool => p.1) encIn encUnary := by + fun_prop + have hp2 : ComputableInPolyTime (fun p : ℕ × F.Desc × List Bool => p.2) + encIn (encPair F.encDesc encBits) := by fun_prop + have hd := (ComputableInPolyTime.fst F.encDesc encBits).comp hp2 + have hu := (ComputableInPolyTime.snd F.encDesc encBits).comp hp2 + have hcoin : IsPPTOn encIn encBool (fun _ => ProbComp.uniform Bool) := by ppt + refine hcoin.bind_with ?_ + let encMid := encPair encIn encBool + have hp1 : ComputableInPolyTime (fun q : (ℕ × F.Desc × List Bool) × Bool => q.1) + encMid encIn := by fun_prop + have hc : ComputableInPolyTime (fun q : (ℕ × F.Desc × List Bool) × Bool => encBool q.2) + encMid encBits := by fun_prop + have hprep := ((hn.comp hp1).prod (hd.comp hp1)).prod ((hu.comp hp1).prod hc) + exact (h.ppt.preprocess hprep).map (ComputableInPolyTime.fst encBits encBits) + have hreal (n : ℕ) : + chvzkRealGame (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) + (fun i => F.encScalar i.2) (fun m => (setup m).map (m, ·)) + (sendWitnessAdversary F) n = PMF.pure true := by + have hchoose (d : F.Desc) : (sendWitnessAdversary F).choose n (n, d) = + (F.sampleExp n d >>= fun s => + pure (((s % F.order d).bits, F.smul (d, s, F.encode d (F.generator d))), + (s % F.order d).bits)) := rfl + simp only [chvzkRealGame, chvzkGameWith, PMF.monad_bind_eq_bind, PMF.bind_map, + Function.comp_def, hchoose, ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_bind, + PMF.pure_bind] + have hstep (d : F.Desc) (s : ℕ) : + chvzkBranch (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (encodedConversation (sendWitnessFamily F) (sendWitnessEncoding F)) + (sendWitnessAdversary F) n (n, d) + ((s % F.order d).bits) (F.smul (d, s, F.encode d (F.generator d))) + ((s % F.order d).bits) = PMF.pure true := by + let α : ZMod (F.order d) := (s : ZMod (F.order d)) + have hx : F.encScalar d α = (s % F.order d).bits := by + simp only [PrimeOrderGroupFamily.encScalar, Function.Embedding.coeFn_mk, encNat_apply, α, + ZMod.val_natCast] + have hy : (sendWitnessEncoding F).statement (n, d) (α • F.generator d) = + F.smul (d, s, F.encode d (F.generator d)) := by + simp only [sendWitnessEncoding, PrimeOrderGroupFamily.encodeEmbedding, + Function.Embedding.coeFn_mk, F.smul_encode, α] + rw [← hx, ← hy, chvzkBranch_valid _ _ _ _ (rfl : dlRel F (n, d) α (α • F.generator d))] + simp only [encodedConversation, sendWitnessAdversary, PMF.bind_map, Function.comp_def] + rw [← PMF.bind_const ((sendWitnessFamily F (n, d)).conversation α (α • F.generator d)) + (PMF.pure true)] + refine PMF.bind_congr_on_support _ _ _ fun tcz htcz => ?_ + rcases tcz with ⟨t, c, z⟩ + have ht : t = α := sendWitnessSigma_conversation_fst (dlRel F (n, d)) α _ htcz + subst ht + simp only [sendWitnessEncoding, beq_self_eq_true, ProbComp.eval_pure] + have hbind : (setup n).bind (fun d => (ProbComp.eval (F.sampleExp n d)).bind fun s => + chvzkBranch (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (encodedConversation (sendWitnessFamily F) (sendWitnessEncoding F)) + (sendWitnessAdversary F) n (n, d) + ((s % F.order d).bits) (F.smul (d, s, F.encode d (F.generator d))) + ((s % F.order d).bits)) = PMF.pure true := by + simp_rw [hstep, PMF.bind_const] + exact hbind + have hsim_bound (n : ℕ) : + Game.succProbability + (chvzkSimGame (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (fun m => (setup m).map (m, ·)) sim (sendWitnessAdversary F) n) ≤ + (1 / 2 : ℝ≥0) ^ n + Game.succProbability (F.discreteLogGame setup dlAdv n) := by + let simTest (d : F.Desc) (α : ZMod (F.order d)) : Game := + (simulatedConversation (sendWitnessEncoding F) sim (n, d) (α • F.generator d)).bind + fun conv => + let ⟨tw, _, _⟩ := conv + PMF.pure (tw == F.encScalar d α) + have hsim_eq : + chvzkSimGame (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (fun m => (setup m).map (m, ·)) sim (sendWitnessAdversary F) n = + (setup n).bind fun d => + (((ProbComp.eval (F.sampleExp n d)).map (Nat.cast : ℕ → ZMod (F.order d)))).bind + (simTest d) := by + simp only [chvzkSimGame, chvzkGameWith, sendWitnessAdversary, PMF.monad_bind_eq_bind, + PMF.bind_map, Function.comp_def, ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_bind, + PMF.pure_bind] + congr 1 + funext d + congr 1 + funext s + let α : ZMod (F.order d) := (s : ZMod (F.order d)) + have hx : F.encScalar d α = (s % F.order d).bits := by + simp only [PrimeOrderGroupFamily.encScalar, Function.Embedding.coeFn_mk, encNat_apply, α, + ZMod.val_natCast] + have hy : (sendWitnessEncoding F).statement (n, d) (α • F.generator d) = + F.smul (d, s, F.encode d (F.generator d)) := by + simp only [sendWitnessEncoding, PrimeOrderGroupFamily.encodeEmbedding, + Function.Embedding.coeFn_mk, F.smul_encode, α] + rw [← hx, ← hy, chvzkBranch_valid _ _ _ _ (rfl : dlRel F (n, d) α (α • F.generator d))] + rfl + let unifGame : Game := + (setup n).bind fun d => (PMF.uniformOfFintype (ZMod (F.order d))).bind (simTest d) + have hadv_exp : Game.advantage + ((setup n).bind fun d => + (((ProbComp.eval (F.sampleExp n d)).map (Nat.cast : ℕ → ZMod (F.order d)))).bind + (simTest d)) + unifGame ≤ (1 / 2 : ℝ≥0) ^ n := by + refine Game.advantage_bind_le_nnreal (setup n) _ _ fun d => ?_ + rw [Game.advantage_comm, one_div_pow] + exact Game.advantage_bind_le_of_closeTo (F.closeTo_uniform_sampleExp n d) (simTest d) + have hunif_le : unifGame true ≤ F.discreteLogGame setup dlAdv n true := by + simp only [unifGame, PrimeOrderGroupFamily.discreteLogGame, simTest, simulatedConversation, + dlAdv, sendWitnessEncoding, PrimeOrderGroupFamily.encodeEmbedding, + Function.Embedding.coeFn_mk, ProbComp.eval_bind, ProbComp.eval_uniform, ProbComp.eval_map, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_map, + Function.comp_def, PMF.bind_bind, PMF.pure_bind, PMF.bind_apply] + refine tsum_le_tsum fun d => mul_le_mul_of_nonneg_left (tsum_le_tsum fun α => + mul_le_mul_of_nonneg_left ?_ zero_le) zero_le + refine tsum_le_tsum fun c => mul_le_mul_of_nonneg_left (tsum_le_tsum fun out => + mul_le_mul_of_nonneg_left ?_ zero_le) zero_le + by_cases htw : out.1 = F.encScalar d α + · have hcast : (ofBits (F.encScalar d α) : ZMod (F.order d)) = α := by + change ((ofBits (encNat α.val) : ℕ) : ZMod (F.order d)) = α + rw [encNat_apply, ofBits, Nat.foldr_bit_bits, ZMod.natCast_zmod_val] + simp [htw, hcast] + · simp [htw] + have hunif_succ : Game.succProbability unifGame ≤ + Game.succProbability (F.discreteLogGame setup dlAdv n) := + ENNReal.toNNReal_mono (PMF.apply_ne_top _ _) hunif_le + rw [hsim_eq] + calc + Game.succProbability + ((setup n).bind fun d => + (((ProbComp.eval (F.sampleExp n d)).map (Nat.cast : ℕ → ZMod (F.order d)))).bind + (simTest d)) + ≤ unifGame.succProbability + Game.advantage + ((setup n).bind fun d => + (((ProbComp.eval (F.sampleExp n d)).map (Nat.cast : ℕ → ZMod (F.order d)))).bind + (simTest d)) + unifGame := by + refine tsub_le_iff_left.mp ?_ + rw [Game.advantage, NNReal.nndist_eq] + exact le_max_left _ _ + _ ≤ Game.succProbability (F.discreteLogGame setup dlAdv n) + (1 / 2 : ℝ≥0) ^ n := + add_le_add hunif_succ hadv_exp + _ = (1 / 2 : ℝ≥0) ^ n + Game.succProbability (F.discreteLogGame setup dlAdv n) := + add_comm _ _ + have h1_le (n : ℕ) : (1 : ℝ≥0) ≤ + Game.advantage + (chvzkRealGame (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) + (fun i => F.encScalar i.2) (fun m => (setup m).map (m, ·)) + (sendWitnessAdversary F) n) + (chvzkSimGame (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (fun m => (setup m).map (m, ·)) sim (sendWitnessAdversary F) n) + + ((1 / 2 : ℝ≥0) ^ n + Game.succProbability (F.discreteLogGame setup dlAdv n)) := by + have hreal_succ : + Game.succProbability + (chvzkRealGame (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) + (fun i => F.encScalar i.2) (fun m => (setup m).map (m, ·)) + (sendWitnessAdversary F) n) = 1 := by + simp [hreal n, Game.succProbability] + calc + (1 : ℝ≥0) = Game.succProbability + (chvzkRealGame (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) + (fun i => F.encScalar i.2) (fun m => (setup m).map (m, ·)) + (sendWitnessAdversary F) n) := hreal_succ.symm + _ ≤ Game.succProbability + (chvzkSimGame (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (fun m => (setup m).map (m, ·)) sim (sendWitnessAdversary F) n) + + Game.advantage + (chvzkRealGame (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) + (fun i => F.encScalar i.2) (fun m => (setup m).map (m, ·)) + (sendWitnessAdversary F) n) + (chvzkSimGame (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (fun m => (setup m).map (m, ·)) sim (sendWitnessAdversary F) n) := by + refine tsub_le_iff_left.mp ?_ + rw [Game.advantage, NNReal.nndist_eq] + exact le_max_left _ _ + _ ≤ ((1 / 2 : ℝ≥0) ^ n + Game.succProbability (F.discreteLogGame setup dlAdv n)) + + Game.advantage + (chvzkRealGame (sendWitnessFamily F) (dlRel F) (sendWitnessEncoding F) + (fun i => F.encScalar i.2) (fun m => (setup m).map (m, ·)) + (sendWitnessAdversary F) n) + (chvzkSimGame (dlRel F) (sendWitnessEncoding F) (fun i => F.encScalar i.2) + (fun m => (setup m).map (m, ·)) sim (sendWitnessAdversary F) n) := + add_le_add (hsim_bound n) le_rfl + _ = _ := add_comm _ _ + have hnegl := (h.indistinguishable (sendWitnessAdversary F) + (isPPT_sendWitnessAdversary F)).add + ((negligible_geometric (ratio := 1 / 2) (by norm_num)).add (hDL dlAdv hdlAdv)) + exact not_negligible_const (c := 1) one_ne_zero (negligible_of_le hnegl h1_le) + +end DiscreteLogSeparation + +/-! ### `ComputationalSpecialHVZK` does not imply `SpecialHVZK` or `EfficientSpecialHVZK` -/ + +section PRGSeparation + +/-- Witness-dependent PRG commitment Sigma protocol for the total relation `fun _ _ => True` on +`Bool × Unit`: witness `false` commits to `generator seed` for a uniform `n`-bit seed, witness +`true` commits to a truly uniform `length n`-bit word, and the verifier checks that the commitment +has length `length n`. -/ +noncomputable def prgWitnessSigma (generator : List Bool → List Bool) (length : ℕ → ℕ) (n : ℕ) : + SigmaProtocol Bool Unit (List Bool) Bool Unit where + State := Unit + commit x _ := + if x then + (BitString.uniformList (length n)).map (·, ()) + else + (generatorEnsemble generator n).map (·, ()) + respond _ _ _ _ := () + verify _ t _ _ := decide (t.length = length n) + +/-- Word encodings of `prgWitnessSigma`: unary security parameter, trivial statement/response, and +raw bit-word commitment. -/ +def prgWitnessEncoding : + Encoding ℕ (fun _ => Unit) (fun _ => List Bool) (fun _ => Bool) (fun _ => Unit) where + index := encUnary + statement _ := encUnit + commitment _ := encBits + challenge _ := encBool + response _ := encUnit + +/-- Simulator for `prgWitnessSigma`: ignore the statement and challenge, sample a uniform +`length n`-bit commitment, and return `(t, encUnit ())`. -/ +noncomputable def prgWitnessSim (length : ℕ → ℕ) : + ℕ × List Bool × List Bool → ProbComp (List Bool × List Bool) + | (n, _, _) => do + let t ← BitString.sampleList (length n) + return (t, encUnit ()) + +theorem complete_prgWitnessSigma {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hlen : ∀ word, (generator word).length = length word.length) (n : ℕ) : + (prgWitnessSigma generator length n).Complete (fun _ _ => True) := by + intro x _ _ c tz htz + cases x + · simp only [SigmaProtocol.transcript, prgWitnessSigma, Bool.false_eq_true, ↓reduceIte, + generatorEnsemble, PMF.map_comp, PMF.mem_support_map_iff] at htz + obtain ⟨seed, hseed, rfl⟩ := htz + simp [SigmaProtocol.Accepts, prgWitnessSigma, hlen, + BitString.length_of_mem_support_uniformList hseed] + · simp only [SigmaProtocol.transcript, prgWitnessSigma, ↓reduceIte, PMF.map_comp, + PMF.mem_support_map_iff] at htz + obtain ⟨t, ht, rfl⟩ := htz + simp [SigmaProtocol.Accepts, prgWitnessSigma, BitString.length_of_mem_support_uniformList ht] + +/-- **Every stretching `PseudorandomGenerator` makes `prgWitnessSigma` computationally special +HVZK** with exact zero acceptance error (`δ = fun _ => 0`). -/ +theorem computationalSpecialHVZK_prgWitnessSigma + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hPRG : PseudorandomGenerator generator length) : + ComputationalSpecialHVZK (prgWitnessSigma generator length) (fun _ _ _ => True) + prgWitnessEncoding (fun _ => encBool) PMF.pure (prgWitnessSim length) (fun _ => 0) where + ppt := by + have hlen := hPRG.polyTime_length + let encIn := encPair encUnary (encPair encBits encBits) + have hn : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => length p.1) + encIn encUnary := hlen.comp (by fun_prop) + change IsPPTOn encIn (encPair encBits encBits) fun p => + BitString.sampleList (length p.1) >>= fun t => pure (t, encUnit ()) + have hsample : IsPPTOn encIn encBits (fun p => BitString.sampleList (length p.1)) := by ppt + refine hsample.bind_with ?_ + exact ((ComputableInPolyTime.snd encIn encBits).prod + (ComputableInPolyTime.const (encUnit ()))).isPPTOn + accepts := by + rintro n ⟨⟩ c + dsimp only [prgWitnessEncoding] + have heq : (ProbComp.eval (prgWitnessSim length (n, encUnit (), encBool c))).toOuterMeasure + {w | ∃ t z, w = (encBits t, encUnit z) ∧ + (prgWitnessSigma generator length n).Accepts () t c z} = 1 := by + simp only [prgWitnessSim, ProbComp.eval_bind, BitString.eval_sampleList, ProbComp.eval_pure] + rw [show (fun a : List Bool => PMF.pure (a, encUnit ())) = + PMF.pure ∘ fun a => (a, encUnit ()) from rfl, + PMF.bind_pure_comp, PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply_eq_one_iff] + intro t ht + refine ⟨t, (), rfl, ?_⟩ + simp [SigmaProtocol.Accepts, prgWitnessSigma, BitString.length_of_mem_support_uniformList ht] + simpa only [tsub_zero] using heq.ge + indistinguishable adversary hadv := by + have hlen := hPRG.polyTime_length + let D : Distinguisher := fun n word => do + let choice ← adversary.choose n n + let ⟨⟨xw, yw⟩, state⟩ := choice + if yw == encUnit () then + if xw == encBool false then + let c ← ProbComp.uniform Bool + adversary.guess n state (word, encBool c, encUnit ()) + else if xw == encBool true then + let t ← BitString.sampleList (length n) + let c ← ProbComp.uniform Bool + adversary.guess n state (t, encBool c, encUnit ()) + else + return false + else + return false + have hD : Probability.IsPPT encBool D := by + have hchoose := hadv.choose + have hguess := hadv.guess + let encD := encPair encUnary encBits + have hn : ComputableInPolyTime (fun p : ℕ × List Bool => p.1) encD encUnary := by fun_prop + have hnn : ComputableInPolyTime (fun p : ℕ × List Bool => (p.1, p.1)) + encD (encPair encUnary encUnary) := hn.prod hn + change IsPPTOn encD encBool fun p => + adversary.choose p.1 p.1 >>= fun ⟨⟨xw, yw⟩, state⟩ => + if yw == encUnit () then + if xw == encBool false then + ProbComp.uniform Bool >>= fun c => + adversary.guess p.1 state (p.2, encBool c, encUnit ()) + else if xw == encBool true then + BitString.sampleList (length p.1) >>= fun t => + ProbComp.uniform Bool >>= fun c => + adversary.guess p.1 state (t, encBool c, encUnit ()) + else + pure false + else + pure false + refine (hchoose.preprocess hnn).bind_with ?_ + ppt + have hgame (n : ℕ) : + Game.advantage + (chvzkRealGame (prgWitnessSigma generator length) (fun _ _ _ => True) + prgWitnessEncoding (fun _ => encBool) PMF.pure adversary n) + (chvzkSimGame (fun _ _ _ => True) prgWitnessEncoding (fun _ => encBool) + PMF.pure (prgWitnessSim length) adversary n) = + Game.advantage + (distinguishingGame (generatorEnsemble generator n) (D n)) + (distinguishingGame (BitString.uniformList (length n)) (D n)) := by + have hreal_eq : + chvzkRealGame (prgWitnessSigma generator length) (fun _ _ _ => True) + prgWitnessEncoding (fun _ => encBool) PMF.pure adversary n = + distinguishingGame (generatorEnsemble generator n) (D n) := by + simp only [chvzkRealGame, chvzkGameWith, distinguishingGame, D, PMF.monad_bind_eq_bind, + PMF.pure_bind, ProbComp.eval_bind] + rw [PMF.bind_comm (generatorEnsemble generator n) (ProbComp.eval (adversary.choose n n))] + refine PMF.bind_congr_on_support _ _ _ fun ⟨⟨xw, yw⟩, state⟩ _ => ?_ + by_cases hy : yw = encUnit () + · subst hy + by_cases hxf : xw = encBool false + · subst hxf + simp only [beq_self_eq_true, ↓reduceIte, ProbComp.eval_bind, ProbComp.eval_uniform] + rw [show encBool false = (fun _ : ℕ => encBool) n false from rfl, + show encUnit () = prgWitnessEncoding.statement n () from rfl, + chvzkBranch_valid _ _ _ _ trivial] + simp only [encodedConversation, SigmaProtocol.conversation, prgWitnessSigma, + prgWitnessEncoding, Bool.false_eq_true, ↓reduceIte, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.map_bind, PMF.bind_map, PMF.pure_map, PMF.bind_bind, + PMF.pure_bind, Function.comp_def] + rfl + · by_cases hxt : xw = encBool true + · subst hxt + have htf : (encBool true == encBool false) = false := by decide + simp only [beq_self_eq_true, htf, Bool.false_eq_true, ↓reduceIte, + ProbComp.eval_bind, BitString.eval_sampleList, ProbComp.eval_uniform, + PMF.bind_const] + rw [show encBool true = (fun _ : ℕ => encBool) n true from rfl, + show encUnit () = prgWitnessEncoding.statement n () from rfl, + chvzkBranch_valid _ _ _ _ trivial] + simp only [encodedConversation, SigmaProtocol.conversation, prgWitnessSigma, + prgWitnessEncoding, ↓reduceIte, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + PMF.map_bind, PMF.bind_map, PMF.pure_map, PMF.bind_bind, PMF.pure_bind, + Function.comp_def] + rfl + · have hinv : ¬ ∃ p : Bool × Unit, + encBool p.1 = xw ∧ prgWitnessEncoding.statement n p.2 = encUnit () ∧ True := by + rintro ⟨⟨b, ⟨⟩⟩, hb, -, -⟩ + cases b + · exact hxf hb.symm + · exact hxt hb.symm + have hxf' : (xw == encBool false) = false := beq_false_of_ne hxf + have hxt' : (xw == encBool true) = false := beq_false_of_ne hxt + simp only [beq_self_eq_true, hxf', hxt', Bool.false_eq_true, ↓reduceIte, + ProbComp.eval_pure, PMF.bind_const] + exact chvzkBranch_invalid (R := fun _ _ _ => True) (enc := prgWitnessEncoding) + (encW := fun _ => encBool) _ _ _ _ _ hinv + · have hinv : ¬ ∃ p : Bool × Unit, + encBool p.1 = xw ∧ prgWitnessEncoding.statement n p.2 = yw ∧ True := by + rintro ⟨⟨_, ⟨⟩⟩, -, hy', -⟩ + exact hy hy'.symm + have hy' : (yw == encUnit ()) = false := beq_false_of_ne hy + simp only [hy', Bool.false_eq_true, ↓reduceIte, ProbComp.eval_pure, PMF.bind_const] + exact chvzkBranch_invalid (R := fun _ _ _ => True) (enc := prgWitnessEncoding) + (encW := fun _ => encBool) _ _ _ _ _ hinv + have hsim_eq : + chvzkSimGame (fun _ _ _ => True) prgWitnessEncoding (fun _ => encBool) + PMF.pure (prgWitnessSim length) adversary n = + distinguishingGame (BitString.uniformList (length n)) (D n) := by + simp only [chvzkSimGame, chvzkGameWith, distinguishingGame, D, PMF.monad_bind_eq_bind, + PMF.pure_bind, ProbComp.eval_bind] + rw [PMF.bind_comm (BitString.uniformList (length n)) (ProbComp.eval (adversary.choose n n))] + refine PMF.bind_congr_on_support _ _ _ fun ⟨⟨xw, yw⟩, state⟩ _ => ?_ + by_cases hy : yw = encUnit () + · subst hy + by_cases hxf : xw = encBool false + · subst hxf + simp only [beq_self_eq_true, ↓reduceIte, ProbComp.eval_bind, ProbComp.eval_uniform] + rw [show encBool false = (fun _ : ℕ => encBool) n false from rfl, + show encUnit () = prgWitnessEncoding.statement n () from rfl, + chvzkBranch_valid _ _ _ _ trivial] + simp only [simulatedConversation, prgWitnessSim, prgWitnessEncoding, + ProbComp.eval_bind, BitString.eval_sampleList, ProbComp.eval_pure, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + rw [PMF.bind_comm (PMF.uniformOfFintype Bool) (BitString.uniformList (length n))] + · by_cases hxt : xw = encBool true + · subst hxt + have htf : (encBool true == encBool false) = false := by decide + simp only [beq_self_eq_true, htf, Bool.false_eq_true, ↓reduceIte, + ProbComp.eval_bind, BitString.eval_sampleList, ProbComp.eval_uniform, + PMF.bind_const] + rw [show encBool true = (fun _ : ℕ => encBool) n true from rfl, + show encUnit () = prgWitnessEncoding.statement n () from rfl, + chvzkBranch_valid _ _ _ _ trivial] + simp only [simulatedConversation, prgWitnessSim, prgWitnessEncoding, + ProbComp.eval_bind, BitString.eval_sampleList, ProbComp.eval_pure, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + rw [PMF.bind_comm (PMF.uniformOfFintype Bool) (BitString.uniformList (length n))] + · have hinv : ¬ ∃ p : Bool × Unit, + encBool p.1 = xw ∧ prgWitnessEncoding.statement n p.2 = encUnit () ∧ True := by + rintro ⟨⟨b, ⟨⟩⟩, hb, -, -⟩ + cases b + · exact hxf hb.symm + · exact hxt hb.symm + have hxf' : (xw == encBool false) = false := beq_false_of_ne hxf + have hxt' : (xw == encBool true) = false := beq_false_of_ne hxt + simp only [beq_self_eq_true, hxf', hxt', Bool.false_eq_true, ↓reduceIte, + ProbComp.eval_pure, PMF.bind_const] + exact chvzkBranch_invalid (R := fun _ _ _ => True) (enc := prgWitnessEncoding) + (encW := fun _ => encBool) _ _ _ _ _ hinv + · have hinv : ¬ ∃ p : Bool × Unit, + encBool p.1 = xw ∧ prgWitnessEncoding.statement n p.2 = yw ∧ True := by + rintro ⟨⟨_, ⟨⟩⟩, -, hy', -⟩ + exact hy hy'.symm + have hy' : (yw == encUnit ()) = false := beq_false_of_ne hy + simp only [hy', Bool.false_eq_true, ↓reduceIte, ProbComp.eval_pure, PMF.bind_const] + exact chvzkBranch_invalid (R := fun _ _ _ => True) (enc := prgWitnessEncoding) + (encW := fun _ => encBool) _ _ _ _ _ hinv + rw [hreal_eq, hsim_eq] + exact (hPRG.indistinguishable D hD).congr fun n => (hgame n).symm + +/-- The honest commitment laws for `x = false` and `x = true` in `prgWitnessSigma` have total +variation distance at least `1 / 2` whenever `n < length n`: `generatorEnsemble` puts mass `1` on +the `2 ^ n`-element generator image while `uniformList (length n)` puts mass at most `1 / 2` on +it. -/ +theorem not_statistical_hvzk_prgWitnessSigma + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hstretch : ∀ n, n < length n) (n : ℕ) + (simulate : Unit → Bool → PMF (List Bool × Unit)) + {ε : ℝ≥0∞} (hε : ε < 1 / 4) : + ¬ ∀ x : Bool, + CloseTo ((prgWitnessSigma generator length n).transcript x () false) + (simulate () false) ε := by + classical + intro h + have hclose : CloseTo + ((prgWitnessSigma generator length n).transcript false () false) + ((prgWitnessSigma generator length n).transcript true () false) (ε + ε) := + (h false).trans (h true).symm + let imgFinset : Finset (List Bool) := + (Finset.univ : Finset (Fin n → Bool)).image fun r => generator (List.ofFn r) + let event : Set (List Bool × Unit) := {tz | tz.1 ∈ (imgFinset : Set (List Bool))} + have h1 : ((prgWitnessSigma generator length n).transcript false () false).toOuterMeasure event = + 1 := by + simp only [SigmaProtocol.transcript, prgWitnessSigma, Bool.false_eq_true, ↓reduceIte, + generatorEnsemble, BitString.uniformList, PMF.map_comp] + rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply_eq_one_iff] + intro r _ + exact Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨r, Finset.mem_univ _, rfl⟩) + have h2 : ((prgWitnessSigma generator length n).transcript true () false).toOuterMeasure event ≤ + 1 / 2 := by + simp only [SigmaProtocol.transcript, prgWitnessSigma, ↓reduceIte, PMF.map_comp, + Function.comp_def] + rw [PMF.toOuterMeasure_map_apply] + have hpre : ((fun t : List Bool => (t, ())) ⁻¹' event) = (imgFinset : Set (List Bool)) := by + ext t; rfl + rw [hpre] + have hcard : (imgFinset.card : ℝ≥0∞) ≤ 2 ^ n := by + have hc : imgFinset.card ≤ 2 ^ n := by + simpa [Fintype.card_bool, Fintype.card_fin] using + (Finset.card_image_le (s := (Finset.univ : Finset (Fin n → Bool))) + (f := fun r => generator (List.ofFn r))) + exact_mod_cast hc + have hpow : (2 : ℝ≥0∞) ^ (n + 1) ≤ 2 ^ length n := + pow_le_pow_right₀ (by norm_num) (Nat.succ_le_of_lt (hstretch n)) + have htwo_top : (2 : ℝ≥0∞) ≠ ⊤ := ENNReal.ofNat_ne_top + calc + (BitString.uniformList (length n)).toOuterMeasure imgFinset + ≤ imgFinset.card * (1 / 2 ^ length n) := + BitString.toOuterMeasure_uniformList_finset_le (length n) imgFinset + _ ≤ 2 ^ n * (1 / 2 ^ (n + 1)) := by + gcongr + _ = 1 / 2 := by + rw [pow_succ, one_div, ENNReal.mul_inv (Or.inl (pow_ne_zero n two_ne_zero)) + (Or.inl (ENNReal.pow_ne_top htwo_top)), ← mul_assoc, + ENNReal.mul_inv_cancel (pow_ne_zero n two_ne_zero) + (ENNReal.pow_ne_top htwo_top), one_mul, one_div] + have hineq := hclose event + rw [h1] at hineq + have hlt : (1 / 2 : ℝ≥0∞) + (ε + ε) < 1 := by + have htwo_top : (2 : ℝ≥0∞) ≠ ⊤ := ENNReal.ofNat_ne_top + have hadd : ε + ε < 1 / 4 + 1 / 4 := ENNReal.add_lt_add hε hε + have hquarter : (1 / 4 : ℝ≥0∞) + 1 / 4 = 1 / 2 := by + rw [← two_mul, show (4 : ℝ≥0∞) = 2 * 2 by norm_num, one_div, + ENNReal.mul_inv (Or.inl two_ne_zero) (Or.inl htwo_top), ← mul_assoc, + ENNReal.mul_inv_cancel two_ne_zero htwo_top, one_mul, one_div] + rw [hquarter] at hadd + have hhalf : (1 / 2 : ℝ≥0∞) + 1 / 2 = 1 := by + rw [← two_mul, one_div, ENNReal.mul_inv_cancel two_ne_zero htwo_top] + exact (ENNReal.add_lt_add_left (by norm_num) hadd).trans_eq hhalf + exact (not_le_of_gt (lt_of_le_of_lt (add_le_add h2 le_rfl) hlt)) hineq + +/-- `prgWitnessSigma` fails `SpecialHVZK` at *every* parameter `n` and for *every* unbounded +simulator `simulate`. -/ +theorem not_specialHVZK_prgWitnessSigma + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hstretch : ∀ n, n < length n) (n : ℕ) + (simulate : Unit → Bool → PMF (List Bool × Unit)) : + ¬ (prgWitnessSigma generator length n).SpecialHVZK (fun _ _ => True) simulate := by + intro h + refine not_statistical_hvzk_prgWitnessSigma (generator := generator) hstretch n simulate + (ε := 0) (by norm_num) fun x => ?_ + rw [← h.transcript_eq x () trivial false] + exact CloseTo.refl _ + +/-- `prgWitnessSigma` fails `EfficientSpecialHVZK` for *every* simulator family and *every* +realization error `δ` (including `δ = fun _ => ⊤`). -/ +theorem not_efficientSpecialHVZK_prgWitnessSigma + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hstretch : ∀ n, n < length n) + (simulate : ∀ _ : ℕ, Unit → Bool → PMF (List Bool × Unit)) + (δ : ℕ → ℝ≥0∞) : + ¬ EfficientSpecialHVZK (prgWitnessSigma generator length) (fun _ _ _ => True) + prgWitnessEncoding simulate δ := fun h => + not_specialHVZK_prgWitnessSigma hstretch 0 (simulate 0) (h.specialHVZK 0) + +/-- **Any uniform one-way function yields an explicit complete Sigma protocol family that satisfies +`ComputationalSpecialHVZK` (with exact zero acceptance error) while failing `SpecialHVZK` (and +statistical HVZK with error `< 1 / 4`) at every security parameter.** -/ +theorem exists_computationalSpecialHVZK_and_not_specialHVZK + {f : List Bool → List Bool} (hf : OneWay f) : + ∃ (P : ∀ _ : ℕ, SigmaProtocol Bool Unit (List Bool) Bool Unit) + (sim : ℕ × List Bool × List Bool → ProbComp (List Bool × List Bool)), + (∀ n, (P n).Complete (fun _ _ => True)) ∧ + ComputationalSpecialHVZK P (fun _ _ _ => True) prgWitnessEncoding + (fun _ => encBool) PMF.pure sim (fun _ => 0) ∧ + (∀ n simulate, ¬ (P n).SpecialHVZK (fun _ _ => True) simulate) := by + obtain ⟨generator, hPRG⟩ := hf.exists_pseudorandomGenerator + exact ⟨prgWitnessSigma generator (fun n => n + 1), prgWitnessSim (fun n => n + 1), + complete_prgWitnessSigma hPRG.length_eq, + computationalSpecialHVZK_prgWitnessSigma hPRG, + not_specialHVZK_prgWitnessSigma hPRG.stretch⟩ + +end PRGSeparation + +end ComplexityTests.ComputationalSpecialHVZK diff --git a/ComplexityTests/EfficientSimulators.lean b/ComplexityTests/EfficientSimulators.lean index f01a1e0bfa..e244d00f26 100644 --- a/ComplexityTests/EfficientSimulators.lean +++ b/ComplexityTests/EfficientSimulators.lean @@ -247,10 +247,10 @@ example : Reduction.EfficientHVZK (fun _ => sendWitness fun x w : List Bool => w (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 _ + exact 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)⟩ + exact CloseTo.refl (PMF.pure x)⟩ end SendWitness diff --git a/ComplexityTests/UnboundedSimulators.lean b/ComplexityTests/UnboundedSimulators.lean index 6882c15b79..d178816b88 100644 --- a/ComplexityTests/UnboundedSimulators.lean +++ b/ComplexityTests/UnboundedSimulators.lean @@ -42,28 +42,6 @@ namespace ComplexityTests.UnboundedSimulators open Cslib Cslib.Interactive Spec open scoped ENNReal -/-! ### Statistical closeness -/ - -theorem toOuterMeasure_add_compl {α : Type} (μ : PMF α) (E : Set α) : - μ.toOuterMeasure E + μ.toOuterMeasure Eᶜ = 1 := by - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] - simp only [Set.indicator_self_add_compl_apply] - exact PMF.tsum_coe _ - -/-- Statistical closeness is symmetric. -/ -theorem closeTo_symm {α : Type} {μ ν : PMF α} {ε : ℝ≥0∞} (h : CloseTo μ ν ε) : - CloseTo ν μ ε := fun E => by - have hc := h Eᶜ - have hne : ν.toOuterMeasure Eᶜ ≠ ⊤ := - ne_top_of_le_ne_top ENNReal.one_ne_top (le_add_self.trans_eq (toOuterMeasure_add_compl ν E)) - refine WithTop.le_of_add_le_add_right hne ?_ - calc ν.toOuterMeasure E + ν.toOuterMeasure Eᶜ = 1 := toOuterMeasure_add_compl ν E - _ = μ.toOuterMeasure E + μ.toOuterMeasure Eᶜ := (toOuterMeasure_add_compl μ E).symm - _ ≤ μ.toOuterMeasure E + (ν.toOuterMeasure Eᶜ + ε) := add_le_add le_rfl hc - _ = μ.toOuterMeasure E + ε + ν.toOuterMeasure Eᶜ := by rw [add_comm _ ε, add_assoc] - -theorem closeTo_refl {α : Type} (μ : PMF α) : CloseTo μ μ 0 := fun _ => by rw [add_zero] - /-! ### Interactive HVZK -/ /-- A prover-side program without oracles, as a closed probabilistic program. -/ @@ -130,7 +108,7 @@ theorem closeTo_of_hvzk have h₁ := h x w hw have h₂ := h x w' hw' rw [map_fst_eval_run] at h₁ h₂ - exact CloseTo.trans h₁ (closeTo_symm h₂) + exact CloseTo.trans h₁ h₂.symm /-- **With unique witnesses, every plain reduction is perfectly HVZK**, for the choice simulator; for instance one whose prover sends its witness. -/ @@ -138,7 +116,7 @@ theorem hvzk_of_unique [Nonempty WitIn] (R : Reduction OracleSpec.empty OracleSpec.empty s StmtIn WitIn StmtOut WitOut) {relIn : StmtIn → WitIn → Prop} (huniq : ∀ x w w', relIn x w → relIn x w' → w = w') : R.HVZK relIn (choiceSim R relIn) 0 := - hvzk_choiceSim fun x w w' hw hw' => huniq x w w' hw hw' ▸ closeTo_refl _ + hvzk_choiceSim fun x w w' hw hw' => huniq x w w' hw hw' ▸ CloseTo.refl _ /-! ### Sigma protocols -/ diff --git a/manual/programs-crypto-and-probability/interactive-reductions.md b/manual/programs-crypto-and-probability/interactive-reductions.md index 3f993f08b4..f079df06c2 100644 --- a/manual/programs-crypto-and-probability/interactive-reductions.md +++ b/manual/programs-crypto-and-probability/interactive-reductions.md @@ -21,9 +21,9 @@ | [Verifier.EfficientKnowledgeSound](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Interactive/Efficient.lean#L97) | The same knowledge property at every family index, plus one word function realizing all extractors | One native deterministic polynomial-time function; index, statement, transcript and output witness are encoded inputs | | [Reduction.EfficientHVZK](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Interactive/Efficient.lean#L114) | The same typed simulation at every index, plus one program approximating all encoded simulator laws within `δ` | One uniform strict-PPT program on index and encoded statement | -`CloseTo` is the all-events statistical-distance bound, even for infinite result types. The realization error `δ` permits exact typed laws, such as uniform field challenges, to be approximated by a strict fair-coin machine. [SimulatorRealizedBy.closeTo_run](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Interactive/Efficient.lean#L127) gives total honest-transcript distance `ε(i)+δ(i)` for the native realizing program. The index encoding is supplied explicitly; the interface does not silently fix unary encoding or grant arbitrary advice for free. +`CloseTo` is the all-events statistical-distance bound, even for infinite result types; [Security.lean](../../Complexity/Computability/Interactive/Security.lean#L88-L192) supplies reflexivity (`CloseTo.refl`), monotonicity (`CloseTo.mono`), symmetry (`CloseTo.symm`), deterministic postprocessing (`CloseTo.map`), transitivity (`CloseTo.trans`), and randomized data-processing laws (`CloseTo.bind_left`, `CloseTo.bind_right`, `CloseTo.bind`) without `Fintype` assumptions, and [Game/CloseTo.lean](../../Complexity/Crypto/Game/CloseTo.lean#L63-L186) connects `CloseTo` in both directions to `Game.advantage` via deterministic (`Game.closeTo_iff_forall_advantage_map_le`) and randomized (`Game.closeTo_iff_forall_advantage_bind_le`) Boolean distinguishers (complementing `Complexity/Crypto/Game/Statistical.lean` when the ambient type is infinite, such as `List Bool`). The realization error `δ` permits exact typed laws, such as uniform field challenges, to be approximated by a strict fair-coin machine. [SimulatorRealizedBy.closeTo_run](../../Complexity/Computability/Interactive/Efficient.lean#L134) gives total honest-transcript distance `ε(i)+δ(i)` for the native realizing program. Both `ε` and `δ` in `Verifier.EfficientKnowledgeSound` and `Reduction.EfficientHVZK` are explicit, unconstrained parameters rather than bundled `Negligible` hypotheses (`ε(i) ≥ 1` or `δ(i) ≥ 1` is vacuous because `PMF.toOuterMeasure` never exceeds `1`), so a computational claim must supply an explicit quantitative or `Negligible` bound along its parameter distribution. The index encoding is supplied explicitly; the interface does not silently fix unary encoding or grant arbitrary advice for free. -These efficient properties constrain extractors or simulators. They do not by themselves certify the verifier or honest prover. The raw properties cannot be read as efficient extraction or zero knowledge: `ComplexityTests/InteractiveKnowledgeSound.lean` and `ComplexityTests/UnboundedSimulators.lean` contain examples exposing that distinction. Rewinding extraction, malicious-verifier zero knowledge and computational zero knowledge are separate notions. +These efficient properties constrain extractors or simulators. They do not by themselves certify the verifier or honest prover. The raw properties cannot be read as efficient extraction or zero knowledge: `ComplexityTests/InteractiveKnowledgeSound.lean`, `ComplexityTests/UnboundedSimulators.lean`, and [ComplexityTests/ComputationalSpecialHVZK.lean](../../ComplexityTests/ComputationalSpecialHVZK.lean) contain examples exposing those distinctions. Rewinding extraction, malicious-verifier zero knowledge and computational zero knowledge are separate notions; Sigma-protocol computational special HVZK (`SigmaProtocol.ComputationalSpecialHVZK`) is documented under [Sigma protocols and explicit extraction](protocols-and-privacy.md#sigma-protocols-and-explicit-extraction). ## Composition and model instances diff --git a/manual/programs-crypto-and-probability/protocols-and-privacy.md b/manual/programs-crypto-and-probability/protocols-and-privacy.md index a5a90e3125..9c63188fc4 100644 --- a/manual/programs-crypto-and-probability/protocols-and-privacy.md +++ b/manual/programs-crypto-and-probability/protocols-and-privacy.md @@ -6,7 +6,14 @@ The general [public-coin interactive-reduction model](interactive-reductions.md) [SigmaProtocol](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean#L78) specifies an honest commitment PMF with private state, a deterministic response to a challenge, and Boolean verification. `Complete`, `SpecialSoundness` and `SpecialHVZK` express correctness, extraction from two accepting same-commitment/distinct-challenge transcripts, and exact simulation at each fixed challenge. The extractor may target a different relation, accommodating relaxed lattice witnesses. The generic interface has no native efficiency built in [complexitylib][complexitylib]. -[Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean) adds encodings and machine-backed extraction/simulation predicates. A simulator certificate may compare a strict-PPT realization with the ideal law using an explicit error. These additions do not retroactively make every semantic Sigma instance efficient. Schnorr and Lyubashevsky clients exercise the interfaces; the latter has separate native-extraction modules. +[SigmaProtocol/Efficient.lean](../../Complexity/Crypto/Protocols/SigmaProtocol/Efficient.lean) adds encodings and machine-backed extraction/simulation predicates (`EfficientSpecialSoundness`, `EfficientSpecialHVZK`). A simulator certificate compares a strict-PPT realization with an exact `SpecialHVZK` law using an explicit statistical error `δ : I → ℝ≥0∞`; `δ` is not constrained inside `EfficientSpecialHVZK` (`δ i ≥ 1` makes `SimulatorRealizedBy` vacuous), so security claims must state their concrete or `Negligible` bound on `δ` explicitly. These additions do not retroactively make every semantic Sigma instance efficient. Schnorr and Lyubashevsky clients exercise the interfaces; the latter has separate native-extraction modules. + +When statistical simulation is too strong or callers interact through game indistinguishability, import `Complexity.Crypto.Protocols.SigmaProtocol.Computational` ([SigmaProtocol/Computational.lean](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean)), which formalizes Boneh and Shoup's Attack Game 20.4 and Definition 20.6 ([bs23][bs23], Section 20.4.2, p. 840): + +- **Two-stage distinguishing game ([CHVZKAdversary](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean#L107), [chvzkRealGame](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean#L217), [chvzkSimGame](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean#L228)):** at security parameter `n`, `i ← setup n` is passed to `adversary.choose n i`, which outputs an encoded witness-statement candidate `(xw, yw)` and saved `state` word (`CHVZKAdversary.IsPPT` clocks `choose` on `(1^n, i)` and `guess` on `(1^n, state, conv)`). When `(xw, yw)` decodes via `encW i` and `enc.statement i` to a valid `(x, y)` in `R i`, `chvzkRealGame` runs `adversary.guess` on an honest encoded conversation while `chvzkSimGame` samples `c ← PMF.uniformOfFintype (C i)` and runs the simulator `sim (i, enc.statement i y, enc.challenge i c)` without `x`; invalid choices output `false` in both experiments so `R i` need not be efficiently decidable by the challenger. +- **Predicate and acceptance parameter ([ComputationalSpecialHVZK](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean#L243)):** bundles uniform strict PPT admissibility of `sim`, acceptance probability at least `1 - δ i` on every `(i, y, c)` (`δ = fun _ => 0` gives exact Definition 20.6 acceptance; non-zero `δ` accommodates strict fair-coin approximations of non-dyadic distributions), and `Game.Indistinguishable` against all strict-PPT `CHVZKAdversary` distinguishers. +- **Statistical-to-computational bridge and Schnorr instance:** [SimulatorRealizedBy.advantage_chvzkGame_le](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean#L326) bounds Attack Game 20.4 advantage against *arbitrary* (even unbounded) adversaries via `Game.advantage_bind_le_of_closeTo` ([Game/CloseTo.lean](../../Complexity/Crypto/Game/CloseTo.lean#L130)), yielding [EfficientSpecialHVZK.exists_computationalSpecialHVZK](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean#L375) whenever `δ` is bounded along `setup` by a `Negligible` function and [SimulatorRealizedBy.computationalSpecialHVZK_of_accepts](../../Complexity/Crypto/Protocols/SigmaProtocol/Computational.lean#L347) when exact acceptance holds separately. In [SchnorrProtocol.lean](../../Complexity/Crypto/Computational/SchnorrProtocol.lean#L300), `PrimeOrderGroupFamily.computationalSpecialHVZK_schnorr` establishes `ComputationalSpecialHVZK` with exact zero acceptance error (`δ = fun _ => 0`) for any `setup : ℕ → PMF F.Desc`. +- **Two-sided separations ([ComplexityTests/ComputationalSpecialHVZK.lean](../../ComplexityTests/ComputationalSpecialHVZK.lean)):** `not_computationalSpecialHVZK_sendWitness` proves that the perfectly `SpecialHVZK` protocol `sendWitnessFamily F` fails `ComputationalSpecialHVZK` under `F.DiscreteLog setup` for *every* `sim` and *every* `δ` (without invoking `accepts`), while `computationalSpecialHVZK_prgWitnessSigma` and `exists_computationalSpecialHVZK_and_not_specialHVZK` construct from any stretching `PseudorandomGenerator` (or uniform `OneWay` function) a complete Sigma protocol family satisfying `ComputationalSpecialHVZK` with `δ = fun _ => 0` that fails `SpecialHVZK`, `EfficientSpecialHVZK` for every `δ`, and even unbounded statistical HVZK below error `1 / 4`. Abort is observable in [Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean): accepted transcripts and conversations return `Option`, with `none` representing abort. `NonAbortSpecialHVZK` matches the entire law including abort mass. Nonabort completeness alone does not give a lower bound on success, an expected retry cost, or a strict-PPT rejection-sampling implementation.