feat(crypto): realize Pedersen commitments with bounded fair coins

Complexity.lean

@@ -2276,6 +2276,7 @@ public import Complexity.Crypto.Computational.OneWayToPRG
 public import Complexity.Crypto.Computational.OneWayToSignature
 public import Complexity.Crypto.Computational.PRGToOneWay
 public import Complexity.Crypto.Computational.PedersenCommitment
+public import Complexity.Crypto.Computational.PedersenCommitment.ProbComp
 public import Complexity.Crypto.Computational.PedersenCommitment.PublicOperations
 public import Complexity.Crypto.Computational.Prediction
 public import Complexity.Crypto.Computational.Pseudoentropy.Basic
@@ -2814,6 +2815,7 @@ public import Complexity.Languages.Probabilistic.Sum
 public import Complexity.Languages.Probabilistic.Transcript
 public import Complexity.Languages.Probabilistic.Traverse
 public import Complexity.Languages.Probabilistic.UniformNat
+public import Complexity.Languages.Probabilistic.UniformNat.Support
 public import Complexity.Languages.Probabilistic.UntilBad
 public import Complexity.Languages.Probabilistic.Vector
 public import Complexity.Logics.FirstOrder.Basic

Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Computational.PedersenCommitment.PublicOperations
+public import Complexity.Crypto.Computational.DiffieHellman
+import Complexity.Computability.Probabilistic.PPT.Capture
+import Complexity.Foundations.Data.Nat.Bits
+import Complexity.Languages.Probabilistic.UniformNat.Support
+import Complexity.Probability.PMF.Uniform
+
+/-!
+# Fair-coin realization of Pedersen commitments
+
+`PrimeOrderGroupFamily.pedersenCommitProb` samples an exponent using the existing bounded
+`sampleExp` program and evaluates the existing public commitment operations. Its native strict-PPT
+certificate charges the unary accuracy parameter, exactly `pedersenScheme.encodeKey`, and the
+message word. The sampler uses `n + |encNat q|` fair bits for `q = F.order d`, and every opening
+has at most `|encNat q|` bits.
+
+The output law is explicit. Against every randomized Boolean continuation, replacing it by the
+existing ideal `pedersenScheme.commitDist` changes success probability by at most `1 / 2 ^ n`.
+Supported outputs verify for valid messages. This approximates the ideal law; it does not replace
+that law with a claim of exact fair-coin sampling, certify setup generation, or transfer the
+scheme's security games to an executable implementation. The realization and certificate
+packaging here are original.
+
+## Main definitions
+
+* `Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitProb`: bounded fair-coin commitment and opening.
+
+## Main results
+
+* `Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_pedersenCommitProb`: uniform strict PPT from the
+  advertised public key bytes and full input.
+* `Cslib.Crypto.PrimeOrderGroupFamily.eval_pedersenCommitProb`: exact output law.
+* `Cslib.Crypto.PrimeOrderGroupFamily.advantage_bind_pedersenCommitProb_le`: error at most
+  `1 / 2 ^ n` against every randomized Boolean continuation.
+* `Cslib.Crypto.PrimeOrderGroupFamily.pedersenVerify_of_mem_support_pedersenCommitProb`,
+  `Cslib.Crypto.PrimeOrderGroupFamily.length_opening_pedersenCommitProb_le`: support correctness
+  and opening-length bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PrimeOrderGroupFamily
+
+open Probability Turing.MultiTapeTM
+open scoped NNReal
+
+variable (F : PrimeOrderGroupFamily)
+
+/-- Sample a bounded approximately uniform exponent, then evaluate Pedersen's public commitment
+operations on its canonical bit representation. The accuracy parameter controls the sampling
+error; the ideal law remains `pedersenScheme.commitDist`. -/
+noncomputable def pedersenCommitProb (n : ℕ) (key : F.PedersenKey) (message : List Bool) :
+    ProbComp (List Bool × List Bool) := do
+  let r ← F.sampleExp n key.1
+  return F.pedersenPublicOperations.commit key message r.bits
+
+/-- Pedersen commitment sampling is uniformly strict PPT in the unary accuracy parameter, actual
+public key encoding, and message word. -/
+theorem isPPTOn_pedersenCommitProb :
+    IsPPTOn (encPair encUnary (encPair F.pedersenScheme.encodeKey encBits))
+      (encPair encBits encBits)
+      (fun p : ℕ × F.PedersenKey × List Bool => F.pedersenCommitProb p.1 p.2.1 p.2.2) := by
+  let E := encPair encUnary (encPair F.pedersenScheme.encodeKey encBits)
+  have hn := ComputableInPolyTime.fst encUnary (encPair F.pedersenScheme.encodeKey encBits)
+  have hrest := ComputableInPolyTime.snd encUnary (encPair F.pedersenScheme.encodeKey encBits)
+  have hk := (ComputableInPolyTime.fst F.pedersenScheme.encodeKey encBits).comp hrest
+  have hm := (ComputableInPolyTime.snd F.pedersenScheme.encodeKey encBits).comp hrest
+  have hkey : ComputableInPolyTime
+      (fun k : F.PedersenKey => (k.1, F.encode k.1 k.2))
+      F.pedersenScheme.encodeKey (encPair F.encDesc encBits) := .of_eq fun _ => rfl
+  have hd := (hkey.comp hk).fst'
+  have hs := F.isPPTOn_sampleExp hn hd
+  have hinput := ComputableInPolyTime.fst E encNat
+  have hr : ComputableInPolyTime
+      (fun p : (ℕ × F.PedersenKey × List Bool) × ℕ => p.2.bits)
+      (encPair E encNat) encBits :=
+    (ComputableInPolyTime.of_eq fun _ => rfl).comp (ComputableInPolyTime.snd E encNat)
+  have heval := F.pedersenPublicOperations.computableInPolyTime_commit
+    (hk.comp hinput) (hm.comp hinput) hr
+  unfold pedersenCommitProb
+  exact hs.bind_with heval.isPPTOn
+
+/-- The sampled output is the existing Pedersen commitment-and-opening map applied to the
+approximately uniform residue law. -/
+theorem eval_pedersenCommitProb (n : ℕ) (key : F.PedersenKey) (message : List Bool) :
+    ProbComp.eval (F.pedersenCommitProb n key message) =
+      ((ProbComp.eval (F.sampleExp n key.1)).map
+        (Nat.cast : ℕ → ZMod (F.order key.1))).map
+        (fun r =>
+          (F.encode key.1 (F.pedersenCommit key.1 key.2 (ofBits message) r), r.val.bits)) := by
+  simp only [pedersenCommitProb, ProbComp.eval_bind, ProbComp.eval_pure]
+  change (ProbComp.eval (F.sampleExp n key.1)).map
+      (fun r => F.pedersenPublicOperations.commit key message r.bits) = _
+  rw [PMF.map_comp]
+  apply PMF.map_congr_on_support
+  intro r hr
+  have hlt := ProbComp.lt_of_mem_support_sampleModNat (F.prime_order key.1).pos hr
+  have hval : (r : ZMod (F.order key.1)).val = r := ZMod.val_natCast_of_lt hlt
+  simp only [pedersenPublicOperations, encodePedersenCommit_encode, ofBits,
+    Nat.foldr_bit_bits, Function.comp_apply, hval]
+
+/-- Every randomized Boolean continuation changes by at most `1 / 2 ^ n` when the sampled
+commitment is replaced with the existing ideal commitment law. -/
+theorem advantage_bind_pedersenCommitProb_le (n : ℕ) (key : F.PedersenKey)
+    (message : List Bool) (continuation : (List Bool × List Bool) → Game) :
+    Game.advantage ((ProbComp.eval (F.pedersenCommitProb n key message)).bind continuation)
+      ((F.pedersenScheme.commitDist key message).bind continuation) ≤ 1 / 2 ^ n := by
+  rw [F.eval_pedersenCommitProb]
+  simpa only [pedersenScheme, pedersenCommitPairLaw, PMF.bind_map, Function.comp_def] using
+    F.advantage_bind_sampleExp_le n key.1
+      (fun r => continuation
+        (F.encode key.1 (F.pedersenCommit key.1 key.2 (ofBits message) r), r.val.bits))
+
+/-- A sampled commitment and opening verify whenever the message is valid. -/
+theorem pedersenVerify_of_mem_support_pedersenCommitProb (n : ℕ) (key : F.PedersenKey)
+    {message : List Bool} {co : List Bool × List Bool}
+    (hm : F.pedersenScheme.ValidMessage key message)
+    (hco : co ∈ (ProbComp.eval (F.pedersenCommitProb n key message)).support) :
+    F.pedersenScheme.verify key message co.1 co.2 = true := by
+  rw [F.eval_pedersenCommitProb, PMF.support_map] at hco
+  obtain ⟨r, _, rfl⟩ := hco
+  apply F.pedersenScheme.verify_of_mem_support key message _ hm
+  simp only [pedersenScheme, pedersenCommitPairLaw, PMF.support_map]
+  exact ⟨r, by simp, rfl⟩
+
+/-- Every supported opening has at most the bit length of the public group order. -/
+theorem length_opening_pedersenCommitProb_le (n : ℕ) (key : F.PedersenKey)
+    {message : List Bool} {co : List Bool × List Bool}
+    (hco : co ∈ (ProbComp.eval (F.pedersenCommitProb n key message)).support) :
+    co.2.length ≤ (encNat (F.order key.1)).length := by
+  rw [F.eval_pedersenCommitProb, PMF.support_map] at hco
+  obtain ⟨r, _, rfl⟩ := hco
+  simpa only [encNat_apply, ← Nat.size_eq_bits_len] using
+    Nat.size_le_size (ZMod.val_lt r).le
+
+end Cslib.Crypto.PrimeOrderGroupFamily

Complexity/Languages/Probabilistic/UniformNat/Support.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Languages.Probabilistic.UniformNat
+
+/-!
+# Supported residues of bounded samplers
+
+The positive-modulus support bound for `sampleModNat` lets callers recover a canonical residue
+from a supported sampled natural. It is kept separate from the sampler's definition and exact law.
+
+## Main results
+
+* `Cslib.ProbComp.lt_of_mem_support_sampleModNat`: every sampled residue is below a positive
+  modulus.
+-/
+
+public section
+
+namespace Cslib.ProbComp
+
+open Probability
+
+/-- Every supported residue is strictly below a positive modulus. -/
+theorem lt_of_mem_support_sampleModNat {width modulus value : ℕ} (hmodulus : 0 < modulus)
+    (hvalue : value ∈ (ProbComp.eval (sampleModNat width modulus)).support) :
+    value < modulus := by
+  rw [eval_sampleModNat, PMF.mem_support_map_iff] at hvalue
+  obtain ⟨i, _, rfl⟩ := hvalue
+  exact Nat.mod_lt _ hmodulus
+
+end Cslib.ProbComp

ComplexityTests/Crypto/PedersenSampling.lean

@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Complexity.Crypto.Computational.DiscreteLog.SchnorrGroup
+public import Complexity.Crypto.Computational.PedersenCommitment.ProbComp
+import Complexity.Computability.Probabilistic.PPT.Capture
+import Complexity.Probability.PMF.Uniform
+import Mathlib.Tactic.NormNum.Prime
+
+/-!
+# Pedersen fair-coin sampling clients
+
+The concrete order-11 Schnorr group modulo 23 checks an actual supported commitment, verification,
+opening length and a nonuniform opening probability. A complete public-input client certifies
+sampling followed by verification, with the accuracy parameter and public key charged as input.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.Crypto.PedersenSampling
+
+open Cslib Cslib.Crypto Cslib.Crypto.PrimeOrderGroupFamily Cslib.Probability Turing.MultiTapeTM
+open scoped NNReal
+
+/-- A concrete Schnorr group of order `11` modulo `23`. -/
+def d23 : schnorrGroups.Desc :=
+  ⟨(23, 11, 2), ⟨by norm_num, by norm_num, by norm_num, by norm_num, by norm_num⟩⟩
+
+/-- The public element `h = 8` in the concrete Schnorr group. -/
+def key23 : schnorrGroups.PedersenKey :=
+  ⟨d23, (3 : ZMod (schnorrGroups.order d23)) • schnorrGroups.generator d23⟩
+
+/-- The bounded program can sample opening `5`, yielding commitment `3` to message `4`. -/
+theorem supported_commitment :
+    (Nat.bits 3, Nat.bits 5) ∈
+      (ProbComp.eval (schnorrGroups.pedersenCommitProb 0 key23 (Nat.bits 4))).support := by
+  simp only [pedersenCommitProb, ProbComp.eval_bind, ProbComp.eval_pure,
+    PMF.mem_support_bind_iff, PMF.support_pure, Set.mem_singleton_iff]
+  refine ⟨5, ?_, ?_⟩
+  · rw [sampleExp, ProbComp.eval_sampleModNat, PMF.mem_support_map_iff]
+    refine ⟨⟨5, by decide⟩, PMF.mem_support_uniformOfFintype _, ?_⟩
+    rfl
+  · decide
+
+/-- Supported sampled commitments satisfy the existing verifier. -/
+example : schnorrGroups.pedersenScheme.verify key23 (Nat.bits 4) (Nat.bits 3) (Nat.bits 5) =
+    true := by
+  apply schnorrGroups.pedersenVerify_of_mem_support_pedersenCommitProb 0 key23
+    (co := (Nat.bits 3, Nat.bits 5)) ?_ supported_commitment
+  change ofBits (Nat.bits 4) < 11 ∧ (ofBits (Nat.bits 4)).bits = Nat.bits 4
+  decide
+
+/-- The sampled opening has at most four bits, the encoded length of group order `11`. -/
+example : (Nat.bits 5).length ≤ 4 :=
+  schnorrGroups.length_opening_pedersenCommitProb_le 0 key23 supported_commitment
+
+/-- Four fair bits reduced modulo eleven give opening five probability `1/16`, exhibiting the
+actual bounded sampler rather than asserting exact uniform exponent sampling. -/
+example : (((ProbComp.eval (schnorrGroups.pedersenCommitProb 0 key23 (Nat.bits 4))).map
+    Prod.snd) (Nat.bits 5)).toReal = 1 / 16 := by
+  simp only [pedersenCommitProb, ProbComp.eval_bind, ProbComp.eval_pure, PMF.map_bind,
+    PMF.pure_map, pedersenPublicOperations]
+  change (((ProbComp.eval (schnorrGroups.sampleExp 0 d23)).map Nat.bits) (Nat.bits 5)).toReal = _
+  rw [sampleExp, ProbComp.eval_sampleModNat, PMF.map_comp]
+  change (((PMF.uniformOfFintype (Fin 16)).map (fun i => (i.val % 11).bits))
+    (Nat.bits 5)).toReal = _
+  have hbits (a b : ℕ) : a.bits = b.bits ↔ a = b := encNat.injective.eq_iff
+  simp only [PMF.map_apply, tsum_fintype, PMF.uniformOfFintype_apply, hbits]
+  norm_num [Fin.sum_univ_succ, ENNReal.toReal_mul, ENNReal.toReal_inv]
+
+/-- At accuracy four, even a randomized continuation inspecting both commitment and opening has
+at most `1/16` advantage against the existing ideal law. -/
+example (continuation : (List Bool × List Bool) → Game) :
+    Game.advantage
+      ((ProbComp.eval (schnorrGroups.pedersenCommitProb 4 key23 (Nat.bits 4))).bind continuation)
+      ((schnorrGroups.pedersenScheme.commitDist key23 (Nat.bits 4)).bind continuation) ≤
+        1 / 16 := by
+  have h := schnorrGroups.advantage_bind_pedersenCommitProb_le 4 key23 (Nat.bits 4) continuation
+  norm_num at h ⊢
+  exact h
+
+/-- A complete client samples and verifies, charging the unary accuracy, exact public-key bytes
+and full message word throughout. -/
+example : IsPPTOn
+    (encPair encUnary (encPair schnorrGroups.pedersenScheme.encodeKey encBits)) encBool
+    (fun p : ℕ × schnorrGroups.PedersenKey × List Bool => do
+      let co ← schnorrGroups.pedersenCommitProb p.1 p.2.1 p.2.2
+      return schnorrGroups.pedersenScheme.verify p.2.1 p.2.2 co.1 co.2) := by
+  let E := encPair encUnary (encPair schnorrGroups.pedersenScheme.encodeKey encBits)
+  have hp := ComputableInPolyTime.fst E (encPair encBits encBits)
+  have hco := ComputableInPolyTime.snd E (encPair encBits encBits)
+  have hrest := (ComputableInPolyTime.snd encUnary
+    (encPair schnorrGroups.pedersenScheme.encodeKey encBits)).comp hp
+  have hk := (ComputableInPolyTime.fst schnorrGroups.pedersenScheme.encodeKey encBits).comp hrest
+  have hm := (ComputableInPolyTime.snd schnorrGroups.pedersenScheme.encodeKey encBits).comp hrest
+  have hv := schnorrGroups.pedersenPublicOperations.computableInPolyTime_verify
+    hk hm hco.fst' hco.snd'
+  exact schnorrGroups.isPPTOn_pedersenCommitProb.bind_with hv.isPPTOn
+
+end ComplexityTests.Crypto.PedersenSampling