feat(crypto): certify public commitment operations

Complexity.lean

@@ -2136,6 +2136,7 @@ public import Complexity.Crypto.Computational.Basic
 public import Complexity.Crypto.Computational.CollisionResistant
 public import Complexity.Crypto.Computational.Commitment
 public import Complexity.Crypto.Computational.Commitment.Basic
+public import Complexity.Crypto.Computational.Commitment.PublicOperations
 public import Complexity.Crypto.Computational.CramerShoup
 public import Complexity.Crypto.Computational.CramerShoup.ProjectiveHash
 public import Complexity.Crypto.Computational.CramerShoup.Reductions
@@ -2272,6 +2273,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.PublicOperations
 public import Complexity.Crypto.Computational.Prediction
 public import Complexity.Crypto.Computational.Pseudoentropy.Basic
 public import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Clipped

Complexity/Crypto/Computational/Commitment/Basic.lean

@@ -15,7 +15,8 @@ public import Complexity.Crypto.Computational.Encryption.Basic
 A `CommitmentScheme` specifies the exact commitment distribution and verification rule under
 public parameters. Its injective public encoding makes every honest operation depend on the
 parameters shown to the adversary. Efficient evaluation and realization of the ideal distributions
-are separate properties.
+are separate properties. `Commitment/PublicOperations` supplies certificates for deterministic
+evaluation on supplied randomness and verification, using exactly this public encoding.
 
 Chosen-message hiding reuses `Encryption.WordAdversary`, with its explicit saved state and uniform
 strict-PPT certificates. Binding asks an adversary for two distinct messages and openings of the

Complexity/Crypto/Computational/Commitment/PublicOperations.lean

@@ -0,0 +1,95 @@
+/-
+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.Commitment.Basic
+
+/-!
+# Efficient public operations for commitment schemes
+
+`CommitmentScheme.PublicOperations` supplies a deterministic commitment-and-opening evaluator
+and polynomial-time certificates for evaluation and verification. Both machines receive the key
+through exactly the public encoding `CommitmentScheme.encodeKey`; supplied randomness and all
+message, commitment and opening words are charged as part of the input.
+
+An ideal `PMF` law for the supplied randomness recovers the scheme's existing commitment law.
+This is separate from an executable sampler: the record does not certify key generation,
+randomness sampling, or a strict-PPT implementation of the commitment distribution. In particular,
+an exact uniform law on a finite group need not have a strict-PPT fair-coin sampler.
+
+This is additional evidence for an existing `CommitmentScheme`, rather than a new security model.
+Its evaluation and verification certificates use the same plain native-machine predicate as
+`BitCommitmentScheme`.
+
+## Main definitions
+
+* `Cslib.Crypto.CommitmentScheme.PublicOperations`: public deterministic operations, their
+  polynomial-time certificates, and their exact relationship to the ideal commitment law.
+
+## Main results
+
+* `Cslib.Crypto.CommitmentScheme.PublicOperations.computableInPolyTime_commit`,
+  `Cslib.Crypto.CommitmentScheme.PublicOperations.computableInPolyTime_verify`: composition with
+  efficiently produced public keys and words.
+-/
+
+public section
+
+namespace Cslib.Crypto.CommitmentScheme
+
+open Turing.MultiTapeTM
+
+/-- Efficient deterministic public operations for `S`, with an ideal supplied-randomness law.
+The input encoding for both certificates is `S.encodeKey`, so the machine receives precisely the
+public key word rather than additional semantic key data. The `randomness` field is an ideal law,
+not an algorithm or an efficiency certificate for sampling. -/
+structure PublicOperations {Key : Type} (S : CommitmentScheme Key) where
+  /-- Compute a commitment and opening from a public key, message and supplied randomness word. -/
+  commit : Key → List Bool → List Bool → List Bool × List Bool
+  /-- Ideal law of the supplied randomness, independent of the message. No sampler is bundled. -/
+  randomness : Key → PMF (List Bool)
+  /-- Evaluation on the ideal randomness law gives exactly the existing commitment distribution. -/
+  map_commit : ∀ k m, (randomness k).map (commit k m) = S.commitDist k m
+  /-- Deterministic evaluation is polynomial-time in the public key, message and randomness word. -/
+  commit_polyTime : ComputableInPolyTime
+    (fun p : Key × List Bool × List Bool => commit p.1 p.2.1 p.2.2)
+    (encPair S.encodeKey (encPair encBits encBits)) (encPair encBits encBits)
+  /-- Verification is polynomial-time in the public key, message, commitment and opening words. -/
+  verify_polyTime : ComputableInPolyTime
+    (fun p : Key × List Bool × List Bool × List Bool => S.verify p.1 p.2.1 p.2.2.1 p.2.2.2)
+    (encPair S.encodeKey (encPair encBits (encPair encBits encBits))) encBool
+
+namespace PublicOperations
+
+variable {Key α : Type} {S : CommitmentScheme Key} {input : α ↪ List Bool}
+
+/-- Compose a public commitment evaluator with efficient producers of its full encoded input. -/
+@[fun_prop]
+theorem computableInPolyTime_commit (ops : S.PublicOperations)
+    {key : α → Key} {message coins : α → List Bool}
+    (hkey : ComputableInPolyTime key input S.encodeKey)
+    (hmessage : ComputableInPolyTime message input encBits)
+    (hcoins : ComputableInPolyTime coins input encBits) :
+    ComputableInPolyTime (fun a => ops.commit (key a) (message a) (coins a))
+      input (encPair encBits encBits) :=
+  ops.commit_polyTime.comp (hkey.prod (hmessage.prod hcoins))
+
+/-- Compose the scheme's verifier with efficient producers of its full encoded input. -/
+theorem computableInPolyTime_verify (ops : S.PublicOperations)
+    {key : α → Key} {message commitment opening : α → List Bool}
+    (hkey : ComputableInPolyTime key input S.encodeKey)
+    (hmessage : ComputableInPolyTime message input encBits)
+    (hcommitment : ComputableInPolyTime commitment input encBits)
+    (hopening : ComputableInPolyTime opening input encBits) :
+    ComputableInPolyTime
+      (fun a => S.verify (key a) (message a) (commitment a) (opening a)) input encBool :=
+  ops.verify_polyTime.comp (hkey.prod (hmessage.prod (hcommitment.prod hopening)))
+
+end PublicOperations
+
+end Cslib.Crypto.CommitmentScheme

Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean

@@ -0,0 +1,115 @@
+/-
+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.Commitment.PublicOperations
+public import Complexity.Crypto.Computational.PedersenCommitment
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+
+/-!
+# Public-operation certificates for Pedersen commitments
+
+`PrimeOrderGroupFamily.pedersenPublicOperations` certifies deterministic commitment evaluation
+on supplied randomness and verification using exactly the public key bytes of `pedersenScheme`.
+It reuses `encodePedersenCommit` and its existing polynomial-time certificate. The ideal law
+of the randomness word is the canonical binary encoding of a uniform exponent in `ZMod q`;
+the exact map equation recovers `pedersenCommitPairLaw`.
+
+No executable randomness sampler, setup algorithm, or strict-PPT realization of the ideal
+commitment law is asserted. In particular, the uniform exponent law is still semantic `PMF` data.
+The security games and their existing hiding and binding claims are unchanged.
+
+## Main definitions
+
+* `Cslib.Crypto.PrimeOrderGroupFamily.encodePedersenVerify`: verification on encoded public group
+  elements and message, commitment and opening words.
+* `Cslib.Crypto.PrimeOrderGroupFamily.pedersenPublicOperations`: efficient public deterministic
+  operations with the exact ideal supplied-randomness law.
+
+## Main results
+
+* `Cslib.Crypto.PrimeOrderGroupFamily.encodePedersenVerify_encode`: encoded verification agrees
+  with the existing semantic verifier.
+* `Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodePedersenVerify`: the encoded
+  verifier is polynomial-time.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PrimeOrderGroupFamily
+
+open Probability Turing.MultiTapeTM
+
+variable (F : PrimeOrderGroupFamily)
+
+/-- Pedersen verification from `(description, encoded public element)`, message, commitment and
+opening words. The public element is already encoded; no discrete logarithm or semantic group
+value is supplied to this algorithm. -/
+def encodePedersenVerify
+    (input : (F.Desc × List Bool) × List Bool × List Bool × List Bool) : Bool :=
+  decide (ofBits input.2.1 < F.order input.1.1) &&
+    decide ((ofBits input.2.1).bits = input.2.1) &&
+    decide (F.encodePedersenCommit
+      (input.1.1, input.1.2, ofBits input.2.1, ofBits input.2.2.2) = input.2.2.1)
+
+/-- The encoded verifier computes exactly the verifier used by `pedersenScheme`. -/
+@[simp]
+theorem encodePedersenVerify_encode (d : F.Desc) (h : F.Carrier d) (m c o : List Bool) :
+    F.encodePedersenVerify ((d, F.encode d h), m, c, o) = F.pedersenVerify d h m c o := by
+  simp only [encodePedersenVerify, pedersenVerify, encodePedersenCommit_encode]
+
+/-- Encoded Pedersen verification is polynomial-time in all of its input words. -/
+theorem computableInPolyTime_encodePedersenVerify :
+    ComputableInPolyTime F.encodePedersenVerify
+      (encPair (encPair F.encDesc encBits) (encPair encBits (encPair encBits encBits)))
+      encBool := by
+  have horder := F.computableInPolyTime_order
+  have hcommit := F.computableInPolyTime_encodePedersenCommit
+  unfold encodePedersenVerify
+  fun_prop
+
+/-- Deterministic Pedersen commitment evaluation and verification from `pedersenScheme.encodeKey`,
+with the ideal randomness law given by the canonical bits of a uniform `ZMod q` exponent.
+This does not certify sampling that law or key generation. -/
+noncomputable def pedersenPublicOperations : F.pedersenScheme.PublicOperations where
+  commit k m coins :=
+    (F.encodePedersenCommit (k.1, F.encode k.1 k.2, ofBits m, ofBits coins), coins)
+  randomness k := (PMF.uniformOfFintype (ZMod (F.order k.1))).map (fun r => r.val.bits)
+  map_commit k m := by
+    simp only [PMF.map_comp, pedersenScheme, pedersenCommitPairLaw]
+    congr 1
+    funext r
+    have hr : (ofBits r.val.bits : ZMod (F.order k.1)) = r := by
+      unfold ofBits
+      rw [Nat.foldr_bit_bits, ZMod.natCast_zmod_val]
+    simp only [Function.comp_apply, encodePedersenCommit_encode, hr]
+  commit_polyTime := by
+    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 hpublic := hkey.comp
+      (ComputableInPolyTime.fst F.pedersenScheme.encodeKey (encPair encBits encBits))
+    have hrest := ComputableInPolyTime.snd F.pedersenScheme.encodeKey (encPair encBits encBits)
+    have hm := ComputableInPolyTime.bitsToNat.comp hrest.fst'
+    have hr := ComputableInPolyTime.bitsToNat.comp hrest.snd'
+    exact (F.computableInPolyTime_encodePedersenCommit.comp
+      (hpublic.fst'.prod (hpublic.snd'.prod (hm.prod hr)))).prod hrest.snd'
+  verify_polyTime := by
+    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 hpublic := hkey.comp (ComputableInPolyTime.fst F.pedersenScheme.encodeKey
+      (encPair encBits (encPair encBits encBits)))
+    have hrest := ComputableInPolyTime.snd F.pedersenScheme.encodeKey
+      (encPair encBits (encPair encBits encBits))
+    have hv := F.computableInPolyTime_encodePedersenVerify.comp (hpublic.prod hrest)
+    convert hv using 1
+    funext p
+    exact (F.encodePedersenVerify_encode p.1.1 p.1.2 p.2.1 p.2.2.1 p.2.2.2).symm
+
+end Cslib.Crypto.PrimeOrderGroupFamily

ComplexityTests/Crypto/CommitmentPublicOperations.lean

@@ -0,0 +1,76 @@
+/-
+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
+import Complexity.Crypto.Computational.PedersenCommitment.PublicOperations
+import Mathlib.Tactic.NormNum.Prime
+
+/-!
+# Public-input commitment clients
+
+An ordinary module imports only the exported API. Concrete encoded verification checks use the
+Schnorr group of order `11` modulo `23`; composition clients charge the public key using precisely
+`pedersenScheme.encodeKey`.
+-/
+
+public section
+
+namespace ComplexityTests.Crypto.CommitmentPublicOperations
+
+open Cslib Cslib.Crypto Cslib.Crypto.PrimeOrderGroupFamily Turing.MultiTapeTM
+
+/-- A concrete valid Schnorr group description used by the evaluation checks. -/
+def d23 : schnorrGroups.Desc :=
+  ⟨(23, 11, 2), ⟨by norm_num, by norm_num, by norm_num, by norm_num, by norm_num⟩⟩
+
+/-- Public bytes `h = 8`, message `4` and opening `5` verify commitment `3`. -/
+example : schnorrGroups.encodePedersenVerify
+    ((d23, Nat.bits 8), Nat.bits 4, Nat.bits 3, Nat.bits 5) = true := by decide
+
+/-- A different commitment is rejected with exactly the same public input and opening. -/
+example : schnorrGroups.encodePedersenVerify
+    ((d23, Nat.bits 8), Nat.bits 4, Nat.bits 4, Nat.bits 5) = false := by decide
+
+/-- Noncanonical message words are rejected even if they represent the same exponent. -/
+example : schnorrGroups.encodePedersenVerify
+    ((d23, Nat.bits 8), Nat.bits 4 ++ [false], Nat.bits 3, Nat.bits 5) = false := by decide
+
+/-- The public-operations evaluator computes both commitment and opening for supplied coins. -/
+example : schnorrGroups.pedersenPublicOperations.commit
+    ⟨d23, (3 : ZMod (schnorrGroups.order d23)) • schnorrGroups.generator d23⟩
+    (Nat.bits 4) (Nat.bits 5) =
+      (Nat.bits 3, Nat.bits 5) := by decide
+
+/-- A client can discard the opening after evaluation with fixed supplied randomness, charging
+its arbitrary public key and message as input. -/
+example : ComputableInPolyTime
+    (fun p : schnorrGroups.PedersenKey × List Bool =>
+      (schnorrGroups.pedersenPublicOperations.commit p.1 p.2 (Nat.bits 5)).1)
+    (encPair schnorrGroups.pedersenScheme.encodeKey encBits) encBits := by
+  have hk := ComputableInPolyTime.fst schnorrGroups.pedersenScheme.encodeKey encBits
+  have hm := ComputableInPolyTime.snd schnorrGroups.pedersenScheme.encodeKey encBits
+  exact (schnorrGroups.pedersenPublicOperations.computableInPolyTime_commit
+    hk hm (.const (Nat.bits 5))).fst'
+
+/-- A verifier client recomputes a candidate commitment from supplied coins and verifies the
+result through the general public-operations API, without receiving the semantic key as advice. -/
+example : ComputableInPolyTime
+    (fun p : schnorrGroups.PedersenKey × List Bool × List Bool =>
+      let co := schnorrGroups.pedersenPublicOperations.commit p.1 p.2.1 p.2.2
+      schnorrGroups.pedersenScheme.verify p.1 p.2.1 co.1 co.2)
+    (encPair schnorrGroups.pedersenScheme.encodeKey (encPair encBits encBits)) encBool := by
+  have hk := ComputableInPolyTime.fst schnorrGroups.pedersenScheme.encodeKey
+    (encPair encBits encBits)
+  have hrest := ComputableInPolyTime.snd schnorrGroups.pedersenScheme.encodeKey
+    (encPair encBits encBits)
+  have hco := schnorrGroups.pedersenPublicOperations.computableInPolyTime_commit
+    hk hrest.fst' hrest.snd'
+  exact schnorrGroups.pedersenPublicOperations.computableInPolyTime_verify
+    hk hrest.fst' hco.fst' hco.snd'
+
+end ComplexityTests.Crypto.CommitmentPublicOperations