From 89d20c0d69b209881f1f109089bdbceb616ff3ea Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:38:48 -0400 Subject: [PATCH 1/2] 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 From 42c585203d3cd425c3f42c647f496867ae5dd937 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:56:04 -0400 Subject: [PATCH 2/2] feat(crypto): realize Pedersen commitments with bounded fair coins Use the existing sampleExp and public-operation certificates to implement Pedersen commitment and opening as a strict-PPT ProbComp program. Charge unary accuracy, exactly the public-key encoding, and the complete message. Relate its exact output law to the existing ideal commitment distribution with at most 1/2^n error for every randomized Boolean continuation; prove valid-message support correctness and an opening-length bound. A small UniformNat/Support module proves the supported-residue bound without changing the widely imported sampler's interface. Concrete ordinary-module tests cover actual supported outputs, an exact nonuniform opening probability, and sampling followed by public verification. This is original realization/certificate work. Setup generation and security transfers for executable games remain open. Existing security notions and curated-abstract statements/scope are unchanged. Validation on base 89d20c0d69b209881f1f109089bdbceb616ff3ea plus this diff: scripts/check.sh passed all six strict gates on the final topic-module placement. The earlier run was stopped intentionally for that placement change and is incomplete. Changed-file, hygiene and catalogue audits pass; no curated abstract impact (22 entries/35 headlines). Refs #1806; depends on #1801. AI assistance: Codex authored and validated this change. Outside-author-fleet exact-head API/correctness review remains required for the new public approximation claim. --- Complexity.lean | 2 + .../PedersenCommitment/ProbComp.lean | 145 ++++++++++++++++++ .../Probabilistic/UniformNat/Support.lean | 38 +++++ ComplexityTests/Crypto/PedersenSampling.lean | 105 +++++++++++++ 4 files changed, 290 insertions(+) create mode 100644 Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean create mode 100644 Complexity/Languages/Probabilistic/UniformNat/Support.lean create mode 100644 ComplexityTests/Crypto/PedersenSampling.lean diff --git a/Complexity.lean b/Complexity.lean index 5caf1920d..f381e170e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2273,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.ProbComp public import Complexity.Crypto.Computational.PedersenCommitment.PublicOperations public import Complexity.Crypto.Computational.Prediction public import Complexity.Crypto.Computational.Pseudoentropy.Basic @@ -2804,6 +2805,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 diff --git a/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean b/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean new file mode 100644 index 000000000..a5d8b70dc --- /dev/null +++ b/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 diff --git a/Complexity/Languages/Probabilistic/UniformNat/Support.lean b/Complexity/Languages/Probabilistic/UniformNat/Support.lean new file mode 100644 index 000000000..2fe60ee57 --- /dev/null +++ b/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 diff --git a/ComplexityTests/Crypto/PedersenSampling.lean b/ComplexityTests/Crypto/PedersenSampling.lean new file mode 100644 index 000000000..439ab3672 --- /dev/null +++ b/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