fix(crypto): require faithful public commitment parameters

Complexity/Crypto/Computational/Commitment.lean

@@ -1244,6 +1244,10 @@ theorem OneWay.exists_bitCommitmentScheme {f : List Bool → List Bool} (hf : On
 /-- A commitment scheme `(C, V)` with public parameters ([BonehShoup2023], Section 8.12, p. 344,
 and Definition 8.8):
 * `encodeKey k`: the encoded public parameter string presented to the adversary for key `k`.
+  This encoding is injective: equal public strings determine the same key and hence the same
+  valid messages, commitment distributions, and verification results.
+  Injectivity is an information-theoretic condition; decoding and evaluating honest operations
+  from this string need separate efficiency certificates.
 * `ValidMessage k m`: predicate characterizing valid message words `m` in the message space for key
   `k`.
 * `commitDist k msg`: the distribution of `(c, o)` (encoded commitment string `c` and encoded
@@ -1264,8 +1268,8 @@ Chosen-message hiding reuses `Encryption.WordAdversary` (`Encryption.AdversaryOf
 `Complexity/Crypto/Computational/Encryption/Basic.lean`), matching Boneh–Shoup's semantic-security
 formulation of commitment hiding. -/
 structure CommitmentScheme (Key : Type) where
-  /-- Encoded public parameter presented to the adversary for key `k`. -/
-  encodeKey : Key → List Bool
+  /-- Faithful encoding of the entire public parameter presented to the adversary. -/
+  encodeKey : Key ↪ List Bool
   /-- Predicate characterizing valid message words in the message space for key `k`. -/
   ValidMessage : Key → List Bool → Prop
   /-- Distribution of `(c, o)` (encoded commitment string and encoded opening string) for message

Complexity/Crypto/Computational/PedersenCommitment.lean

@@ -321,7 +321,12 @@ noncomputable def pedersenKeyDist (setup : ℕ → PMF F.Desc) (n : ℕ) : PMF F
 ([BonehShoup2023], Section 8.12, Definition 8.8, p. 344, and Section 10.6.1, p. 414;
 [Pedersen1991], Section 3). -/
 noncomputable def pedersenScheme : CommitmentScheme F.PedersenKey where
-  encodeKey k := encPair F.encDesc encBits (k.1, F.encode k.1 k.2)
+  encodeKey := ⟨fun k => encPair F.encDesc encBits (k.1, F.encode k.1 k.2), by
+    rintro ⟨d, h⟩ ⟨d', h'⟩ heq
+    obtain ⟨hd, hh⟩ := Prod.ext_iff.mp ((encPair F.encDesc encBits).injective heq)
+    cases hd
+    cases F.encode_injective d hh
+    rfl⟩
   ValidMessage k := F.ValidPedersenMessage k.1
   commitDist k msg := F.pedersenCommitPairLaw k.1 k.2 (ofBits msg)
   verify k := F.pedersenVerify k.1 k.2

ComplexityTests/Crypto/CommitmentPublicSetup.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Crypto.Computational.Commitment
+import Complexity.Crypto.Negligible.Basic
+
+/-!
+# Public setup for commitment schemes
+
+Regressions for the concealed setup bit reported in issue #1716. The public encoding must
+determine every honest operation. Exposing the setup bit in the XOR construction lets a
+chosen-message adversary recover the challenge bit exactly.
+-/
+
+namespace ComplexityTests.Crypto.CommitmentPublicSetup
+
+open Cslib Cslib.Probability Cslib.Crypto
+
+/-- Two distinct Boolean setup keys cannot both be advertised by the empty string. -/
+example (S : CommitmentScheme Bool) : ¬ (∀ k, S.encodeKey k = []) := by
+  intro h
+  have hkey : false = true := S.encodeKey.injective ((h false).trans (h true).symm)
+  cases hkey
+
+/-- Equal exposed public parameters determine all three honest operations. -/
+example {Key : Type} (S : CommitmentScheme Key) {k₁ k₂ : Key}
+    (h : S.encodeKey k₁ = S.encodeKey k₂) :
+    S.ValidMessage k₁ = S.ValidMessage k₂ ∧
+      S.commitDist k₁ = S.commitDist k₂ ∧ S.verify k₁ = S.verify k₂ := by
+  cases S.encodeKey.injective h
+  exact ⟨rfl, rfl, rfl⟩
+
+/-- The XOR verifier from the reported example, with an empty opening. -/
+def xorVerify (k : Bool) (m c o : List Bool) : Bool :=
+  decide (m.length = 1 ∧ o = [] ∧ c = [m.headD false ^^ k])
+
+/-- Erasing the setup bit prevents the XOR verifier from factoring through the public string. -/
+example : ¬ ∃ V : List Bool → List Bool → List Bool → List Bool → Bool,
+    ∀ k m c o, xorVerify k m c o = V [] m c o := by
+  rintro ⟨V, h⟩
+  have hfalse := h false [false] [false] []
+  have htrue := h true [false] [false] []
+  have hbad : true = false := hfalse.trans htrue.symm
+  cases hbad
+
+/-- The XOR construction with its setup bit actually public. -/
+noncomputable def xorScheme : CommitmentScheme Bool where
+  encodeKey := ⟨fun k => [k], by intro a b h; simpa using h⟩
+  ValidMessage _ m := m.length = 1
+  commitDist k m := PMF.pure ([m.headD false ^^ k], [])
+  verify := xorVerify
+  validMessage_of_verify _ _ _ _ h := (of_decide_eq_true h).1
+  verify_of_mem_support _ _ co hm hco := by
+    rw [PMF.support_pure, Set.mem_singleton_iff] at hco
+    subst co
+    simp [xorVerify, hm]
+
+theorem xorScheme_encodeKey (k : Bool) : xorScheme.encodeKey k = [k] := rfl
+
+/-- Retain the public bit, then XOR it with the commitment to recover the chosen message. -/
+def xorAdversary : Encryption.WordAdversary where
+  choose _ pk := pure (([false], [true]), pk)
+  guess _ pk c := pure (c.headD false ^^ pk.headD false)
+
+/-- Recovery is exact at each setup key, so it does not depend on the setup distribution. -/
+theorem xor_hidingForKey (k bit : Bool) (n : ℕ) :
+    xorScheme.hidingForKey k xorAdversary bit n = PMF.pure bit := by
+  simp only [CommitmentScheme.hidingForKey, xorScheme_encodeKey, xorAdversary]
+  cases k <;> cases bit <;> simp [xorScheme]
+
+/-- Public setup rules out statistical hiding for the XOR construction under every setup law. -/
+example (keyDist : ℕ → PMF Bool) : ¬ xorScheme.StatisticalHiding keyDist := by
+  intro h
+  have hgame (bit : Bool) (n : ℕ) :
+      xorScheme.hidingGame keyDist xorAdversary bit n = PMF.pure bit := by
+    simp [CommitmentScheme.hidingGame, xor_hidingForKey]
+  exact not_negligible_const (c := 1) one_ne_zero (by
+    simpa [hgame, Game.advantage, Game.succProbability] using h xorAdversary trivial)
+
+end ComplexityTests.Crypto.CommitmentPublicSetup

ComplexityTests/Crypto/PedersenCommitment.lean

@@ -117,7 +117,7 @@ example (setup : ℕ → PMF schnorrGroups.Desc) (hDL : schnorrGroups.DiscreteLo
 /-- Regression witness (`openScheme`): a scheme with empty commitment string and opening equal to
 the message is perfectly hiding, and is rejected by `CommitmentScheme.Binding`. -/
 noncomputable def openScheme : CommitmentScheme Unit where
-  encodeKey _ := []
+  encodeKey := ⟨fun _ => [], fun _ _ _ => Subsingleton.elim _ _⟩
   ValidMessage _ _ := True
   commitDist _ m := PMF.pure ([], m)
   verify _ m c o := decide (c = [] ∧ o = m)
@@ -150,7 +150,7 @@ example : ¬ openScheme.Binding (fun _ => PMF.pure ()) := by
 commitment string equals the message word satisfies `StatisticalHiding` because `hidingForKey`
 commits to `m_bit` only when both challenge words satisfy `ValidMessage`. -/
 noncomputable def singletonScheme : CommitmentScheme Unit where
-  encodeKey _ := []
+  encodeKey := ⟨fun _ => [], fun _ _ _ => Subsingleton.elim _ _⟩
   ValidMessage _ m := m = []
   commitDist _ m := PMF.pure (m, [])
   verify _ m c _ := decide (m = [] ∧ c = [])