feat(Crypto): Commitment Schemes

Cslib.lean

@@ -50,6 +50,9 @@ public import Cslib.Computability.URM.Defs
 public import Cslib.Computability.URM.Execution
 public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
+public import Cslib.Crypto.Protocols.Commitment.Basic
+public import Cslib.Crypto.Protocols.Commitment.Defs
+public import Cslib.Crypto.Protocols.Commitment.Scheme
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
@@ -168,3 +171,4 @@ public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
 public import Cslib.MachineLearning.PACLearning.VersionSpaceLattice
 public import Cslib.Probability.PMF
+public import Cslib.Probability.StatisticalDistance

Cslib/Crypto/Protocols/Commitment/Basic.lean

@@ -0,0 +1,118 @@
+/-
+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 Cslib.Crypto.Protocols.Commitment.Defs
+
+/-!
+# Commitment Schemes
+
+Basic results about information-theoretic commitment schemes.
+
+The main result is the hiding–binding trade-off: a perfectly binding scheme
+places the commitment distributions of distinct messages at the maximum
+statistical distance, so it cannot be statistically hiding for any error below
+one. Hiding and binding can therefore not both hold unconditionally; real
+schemes make at most one side information-theoretic and settle for a
+computational version of the other.
+
+## Main results
+
+- `Scheme.subsingleton_of_statisticallyHiding_of_perfectlyBinding`: a scheme
+  cannot be both statistically hiding with error below one and perfectly
+  binding unless any two messages are equal
+- `Scheme.PerfectlyBinding.statisticalDistance_commitmentDist_eq_one`: perfect
+  binding forces distinct messages' commitment distributions to the maximum
+  statistical distance
+- `Scheme.subsingleton_of_perfectlyHiding_of_perfectlyBinding`: the perfect
+  hiding case, with no finiteness assumption on commitments
+- `Scheme.perfectlyHiding_iff_statisticallyHiding_zero`: perfect hiding is
+  statistical hiding with zero error
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Protocols.Commitment.Scheme
+
+open Cslib.Probability.PMF
+open scoped NNReal
+
+variable {Message Commitment Opening : Type*}
+
+/-- Perfect hiding is exactly statistical hiding with zero error. -/
+theorem perfectlyHiding_iff_statisticallyHiding_zero
+    [Fintype Commitment] (scheme : Scheme Message Commitment Opening) :
+    scheme.PerfectlyHiding ↔ scheme.StatisticallyHiding 0 := by
+  simp [PerfectlyHiding, StatisticallyHiding]
+
+/-- Enlarging the permitted error preserves statistical hiding. -/
+theorem StatisticallyHiding.mono [Fintype Commitment]
+    {scheme : Scheme Message Commitment Opening} {ε δ : ℝ≥0}
+    (h : scheme.StatisticallyHiding ε) (hεδ : ε ≤ δ) :
+    scheme.StatisticallyHiding δ :=
+  fun message₀ message₁ => (h message₀ message₁).mono hεδ
+
+/-- Distinct messages of a perfectly binding scheme have disjoint sets of
+possible commitments. -/
+theorem PerfectlyBinding.disjoint_support_commitmentDist
+    {scheme : Scheme Message Commitment Opening} (hbind : scheme.PerfectlyBinding)
+    {message₀ message₁ : Message} (hne : message₀ ≠ message₁) :
+    Disjoint (scheme.commitmentDist message₀).support
+      (scheme.commitmentDist message₁).support := by
+  rw [Set.disjoint_left]
+  intro commitment h₀ h₁
+  obtain ⟨opening₀, hpair₀⟩ := scheme.mem_support_commitmentDist_iff.mp h₀
+  obtain ⟨opening₁, hpair₁⟩ := scheme.mem_support_commitmentDist_iff.mp h₁
+  exact hne (hbind commitment message₀ opening₀ message₁ opening₁
+    (scheme.accepts_of_mem_support hpair₀) (scheme.accepts_of_mem_support hpair₁))
+
+/-- In a perfectly binding scheme, the commitment distributions of distinct
+messages are at the maximum statistical distance: an unbounded observer can
+read the message off the commitment. -/
+theorem PerfectlyBinding.statisticalDistance_commitmentDist_eq_one
+    [Fintype Commitment] {scheme : Scheme Message Commitment Opening}
+    (hbind : scheme.PerfectlyBinding) {message₀ message₁ : Message}
+    (hne : message₀ ≠ message₁) :
+    statisticalDistance (scheme.commitmentDist message₀)
+      (scheme.commitmentDist message₁) = 1 :=
+  statisticalDistance_eq_one_of_disjoint_support (hbind.disjoint_support_commitmentDist hne)
+
+/-- **The hiding–binding trade-off.** A scheme cannot be both statistically
+hiding with error below one and perfectly binding unless any two messages are
+equal. The error bound is sharp: statistical hiding with error one holds
+vacuously for every scheme. -/
+theorem subsingleton_of_statisticallyHiding_of_perfectlyBinding
+    [Fintype Commitment] (scheme : Scheme Message Commitment Opening) {ε : ℝ≥0}
+    (hε : ε < 1) (hhide : scheme.StatisticallyHiding ε)
+    (hbind : scheme.PerfectlyBinding) : Subsingleton Message := by
+  refine ⟨fun message₀ message₁ => ?_⟩
+  by_contra hne
+  have hone := hbind.statisticalDistance_commitmentDist_eq_one hne
+  have hle : statisticalDistance (scheme.commitmentDist message₀)
+      (scheme.commitmentDist message₁) ≤ (ε : ℝ) := hhide message₀ message₁
+  rw [hone] at hle
+  exact absurd hle (by exact_mod_cast hε.not_ge)
+
+/-- A scheme cannot be both perfectly hiding and perfectly binding unless any
+two messages are equal. Unlike the statistical version, this needs no
+finiteness assumption on the commitment type. -/
+theorem subsingleton_of_perfectlyHiding_of_perfectlyBinding
+    (scheme : Scheme Message Commitment Opening)
+    (hhide : scheme.PerfectlyHiding) (hbind : scheme.PerfectlyBinding) :
+    Subsingleton Message := by
+  refine ⟨fun message₀ message₁ => ?_⟩
+  obtain ⟨commitment, hcommitment⟩ :=
+    (scheme.commitmentDist message₀).support_nonempty
+  obtain ⟨opening₀, hpair₀⟩ :=
+    scheme.mem_support_commitmentDist_iff.mp hcommitment
+  rw [hhide message₀ message₁] at hcommitment
+  obtain ⟨opening₁, hpair₁⟩ :=
+    scheme.mem_support_commitmentDist_iff.mp hcommitment
+  exact hbind commitment message₀ opening₀ message₁ opening₁
+    (scheme.accepts_of_mem_support hpair₀) (scheme.accepts_of_mem_support hpair₁)
+
+end Cslib.Crypto.Protocols.Commitment.Scheme

Cslib/Crypto/Protocols/Commitment/Defs.lean

@@ -0,0 +1,77 @@
+/-
+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 Cslib.Crypto.Protocols.Commitment.Scheme
+public import Cslib.Probability.StatisticalDistance
+
+/-!
+# Commitment Schemes: Information-Theoretic Security
+
+Hiding and binding for commitment schemes, in their information-theoretic forms
+([BonehShoup2023], Section 8.12). Perfect hiding: every message yields the same
+commitment distribution. Statistical hiding: any two commitment distributions
+are within statistical distance `ε`. Perfect binding: no commitment can be
+opened to two different messages, even by an unbounded committer.
+
+Each definition is about a single, fixed scheme; statistical hiding carries an
+explicit error bound, and the perfect notions have no error at all. The
+asymptotic notions in the book — negligible statistical distance for families
+of distributions ([BonehShoup2023], Definition 3.6), or security against
+efficient adversaries (Section 8.12) — can be layered on top of these later.
+
+## Main definitions
+
+- `Scheme.PerfectlyHiding`: the commitment distributions are equal for every
+  pair of messages
+- `Scheme.StatisticallyHiding`: the commitment distributions are statistically
+  close with error `ε`
+- `Scheme.PerfectlyBinding`: no commitment has accepted openings to two
+  different messages
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Protocols.Commitment.Scheme
+
+open Cslib.Probability.PMF
+open scoped NNReal
+
+variable {Message Commitment Opening : Type*}
+
+/-- A scheme is perfectly hiding when every message yields the same commitment
+distribution, so a commitment reveals nothing about the message as long as its
+opening is withheld ([BonehShoup2023], Section 8.12). -/
+def PerfectlyHiding (scheme : Scheme Message Commitment Opening) : Prop :=
+  ∀ message₀ message₁ : Message,
+    scheme.commitmentDist message₀ = scheme.commitmentDist message₁
+
+/-- A scheme is statistically hiding with error `ε` when the commitment
+distributions of any two messages are within statistical distance `ε`
+([BonehShoup2023], Definition 3.5 and Section 8.12). -/
+def StatisticallyHiding [Fintype Commitment]
+    (scheme : Scheme Message Commitment Opening) (ε : ℝ≥0) : Prop :=
+  ∀ message₀ message₁ : Message,
+    StatisticallyClose (scheme.commitmentDist message₀)
+      (scheme.commitmentDist message₁) ε
+
+/-- A scheme is perfectly binding when a commitment can be opened to at most
+one message: any two accepted openings of the same commitment agree on the
+message ([BonehShoup2023], Section 8.12). Different openings of the same
+message are still allowed. -/
+def PerfectlyBinding (scheme : Scheme Message Commitment Opening) : Prop :=
+  ∀ commitment message₀ opening₀ message₁ opening₁,
+    scheme.Accepts message₀ commitment opening₀ →
+      scheme.Accepts message₁ commitment opening₁ →
+        message₀ = message₁
+
+end Cslib.Crypto.Protocols.Commitment.Scheme

Cslib/Crypto/Protocols/Commitment/Scheme.lean

@@ -0,0 +1,101 @@
+/-
+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 Cslib.Init
+public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+
+/-!
+# Commitment Schemes: Syntax and Correctness
+
+The syntax of a commitment scheme ([BonehShoup2023], Section 8.12): committing
+to a message samples a commitment-opening pair `(c, o)`, verification of a
+claimed opening is deterministic, and honestly generated pairs always verify.
+
+The algorithms are plain functions, with no efficiency or finiteness
+assumptions. Security notions live in separate definitions, so the same syntax
+can carry perfect, statistical, or computational security.
+
+## Main definitions
+
+- `Scheme`: commitment syntax with perfect correctness
+- `Scheme.commitmentDist`: the public commitment distribution for a message
+- `Scheme.mem_support_commitmentDist_iff`: a commitment is possible exactly
+  when it has a possible opening
+- `Scheme.Accepts`: the verifier's acceptance relation
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Protocols.Commitment
+
+/-- A noninteractive, unkeyed commitment scheme over message, commitment, and
+opening types ([BonehShoup2023], Section 8.12).
+
+Committing is randomized and produces the commitment and opening together,
+since the two may be correlated. Correctness requires that every
+commitment-opening pair the honest committer can output is accepted by the
+verifier; for a `PMF`, this says honest openings verify with probability
+one. -/
+structure Scheme (Message Commitment Opening : Type*) where
+  /-- Randomized commitment and opening generation. -/
+  commit (message : Message) : PMF (Commitment × Opening)
+  /-- Deterministic verification of a claimed opening. -/
+  verify (message : Message) (commitment : Commitment) (opening : Opening) : Bool
+  /-- Every honestly generated commitment-opening pair verifies. -/
+  correct : ∀ message commitment opening,
+    (commitment, opening) ∈ (commit message).support →
+      verify message commitment opening = true
+
+namespace Scheme
+
+variable {Message Commitment Opening : Type*}
+
+/-- The public commitment distribution obtained by forgetting the opening. -/
+noncomputable def commitmentDist (scheme : Scheme Message Commitment Opening)
+    (message : Message) : PMF Commitment :=
+  (scheme.commit message).map Prod.fst
+
+/-- A commitment lies in the public distribution's support exactly when some
+opening makes the corresponding pair an honest possible output. -/
+theorem mem_support_commitmentDist_iff
+    (scheme : Scheme Message Commitment Opening) {message : Message}
+    {commitment : Commitment} :
+    commitment ∈ (scheme.commitmentDist message).support ↔
+      ∃ opening, (commitment, opening) ∈ (scheme.commit message).support := by
+  simp [commitmentDist]
+
+/-- The proposition that an opening is accepted for a commitment and message. -/
+def Accepts (scheme : Scheme Message Commitment Opening) (message : Message)
+    (commitment : Commitment) (opening : Opening) : Prop :=
+  scheme.verify message commitment opening = true
+
+/-- Every pair in the support of honest commitment is accepted. -/
+theorem accepts_of_mem_support (scheme : Scheme Message Commitment Opening)
+    {message : Message} {commitment : Commitment} {opening : Opening}
+    (h : (commitment, opening) ∈ (scheme.commit message).support) :
+    scheme.Accepts message commitment opening :=
+  scheme.correct message commitment opening h
+
+/-- Build a commitment scheme from deterministic commitment generation. -/
+noncomputable def ofPure (commit : Message → Commitment × Opening)
+    (verify : Message → Commitment → Opening → Bool)
+    (correct : ∀ message, verify message (commit message).1 (commit message).2 = true) :
+    Scheme Message Commitment Opening where
+  commit message := PMF.pure (commit message)
+  verify := verify
+  correct message commitment opening h := by
+    grind [PMF.mem_support_pure_iff]
+
+end Scheme
+
+end Cslib.Crypto.Protocols.Commitment