From a83b7195a4f7b47e585400037e1521034171b588 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Wed, 25 Feb 2026 20:29:54 -0800
Subject: [PATCH 1/2] refactor: rename parameters

---
 VerifiedCommitments/ElgamalCommitments.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index 24fb2d8..4807bb3 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -50,7 +50,7 @@ end DDH
 
 namespace Elgamal
 
-class ElgamalParameters (G : Type) extends
+class PublicParameters (G : Type) extends
   Fintype G, Group G, IsCyclic G where
   [decidable_G : DecidableEq G]
   q : ℕ
@@ -63,7 +63,7 @@ class ElgamalParameters (G : Type) extends
   G_card_q : Fintype.card G = q
 
 -- Make instances available
-variable {G : Type} [params : ElgamalParameters G]
+variable {G : Type} [params : PublicParameters G]
 instance : DecidableEq G := params.decidable_G
 instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
 
@@ -80,12 +80,11 @@ do
 def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 :=
   if c = ⟨params.g^o.val, h^o.val * m⟩ then 1 else 0
 
-noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G :=
-{
-  setup := setup,
-  commit := commit,
+noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G where
+  setup := setup
+  commit := commit
   verify := verify
-}
+
 /-
   -----------------------------------------------------------
   Proof of correctness of ElGamal

From d46a3d8801b37f5489d7218ec79646457e6e0bc0 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Wed, 25 Feb 2026 20:31:36 -0800
Subject: [PATCH 2/2] feat: add proof of elgamal binding

---
 VerifiedCommitments/ElgamalCommitments.lean | 40 +++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index 4807bb3..3767892 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -389,4 +389,44 @@ theorem computational_hiding_from_ddh (ε : ENNReal)
   exact DDH_hard (D_from_adversary hA)
 
 
+/- ========================================
+   BINDING PROPERTY
+   ======================================== -/
+
+lemma ordg_eq_q : orderOf params.g = params.q := by
+  have h_card_zpow : Fintype.card (Subgroup.zpowers params.g) = orderOf params.g := Fintype.card_zpowers
+  have h_card_eq : Fintype.card (Subgroup.zpowers params.g) = Fintype.card G := by
+    have : Function.Bijective (Subtype.val : Subgroup.zpowers params.g → G) := by
+      constructor
+      · exact Subtype.val_injective
+      · intro x
+        use ⟨x, params.g_gen_G x⟩
+    exact Fintype.card_of_bijective this
+  rw [← h_card_zpow, h_card_eq, params.card_eq]
+
+
+theorem perfect_binding : Commitment.perfect_binding (@scheme G params) := by
+  unfold Commitment.perfect_binding
+  intro h c m m' o o'
+  unfold scheme verify
+  simp only [ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
+  intro hc
+  simp [hc]
+  congr! with hc₁ hc₂
+
+
+  have h_congr : o.val ≡ o'.val [MOD params.q] := by
+      simpa [ordg_eq_q] using (pow_eq_pow_iff_modEq.mp hc₁)
+
+  have o_eq : o = o' := by
+    have eq_cast : ((o.val : ℕ) : ZMod params.q) = ((o'.val : ℕ) : ZMod params.q) :=
+      ZMod.natCast_eq_natCast_iff o.val o'.val params.q |>.mpr h_congr
+    simp at eq_cast
+    exact eq_cast
+
+  subst o_eq
+  simp at hc₂
+  exact hc₂
+
+
 end Elgamal