From 89d20c0d69b209881f1f109089bdbceb616ff3ea Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:38:48 -0400 Subject: [PATCH] feat(crypto): certify public commitment operations Record deterministic commitment and verifier efficiency under the exact public parameter encoding of an existing CommitmentScheme. Instantiate the bundle for Pedersen using its encoded evaluator and the ideal law of canonical uniform exponent bits; add ordinary-module composition and concrete accepted/rejected verification clients. The ideal PMF law does not certify executable sampling or key generation. Existing security games/statements and curated abstract scope are unchanged. This is original API packaging and an efficiency proof. Validation on base 7e32b15027471135130bc65c6746f2d42c72c963 plus this diff: scripts/check.sh passed all six strict gates. Changed-file, hygiene and catalogue audits passed. No curated abstract impact (22 entries/35 headlines). Refs #1720. AI assistance: Codex authored and validated this change. Independent exact-revision API/correctness review remains required. --- Complexity.lean | 2 + .../Computational/Commitment/Basic.lean | 3 +- .../Commitment/PublicOperations.lean | 95 +++++++++++++++ .../PedersenCommitment/PublicOperations.lean | 115 ++++++++++++++++++ .../Crypto/CommitmentPublicOperations.lean | 76 ++++++++++++ 5 files changed, 290 insertions(+), 1 deletion(-) create mode 100644 Complexity/Crypto/Computational/Commitment/PublicOperations.lean create mode 100644 Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean create mode 100644 ComplexityTests/Crypto/CommitmentPublicOperations.lean diff --git a/Complexity.lean b/Complexity.lean index d8bc086f0..5caf1920d 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Crypto/Computational/Commitment/Basic.lean b/Complexity/Crypto/Computational/Commitment/Basic.lean index 7cb2f76ae..e7abb15ec 100644 --- a/Complexity/Crypto/Computational/Commitment/Basic.lean +++ b/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 diff --git a/Complexity/Crypto/Computational/Commitment/PublicOperations.lean b/Complexity/Crypto/Computational/Commitment/PublicOperations.lean new file mode 100644 index 000000000..82322e34e --- /dev/null +++ b/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 diff --git a/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean b/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean new file mode 100644 index 000000000..a52a22729 --- /dev/null +++ b/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 diff --git a/ComplexityTests/Crypto/CommitmentPublicOperations.lean b/ComplexityTests/Crypto/CommitmentPublicOperations.lean new file mode 100644 index 000000000..1dfe4c93e --- /dev/null +++ b/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