diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean
index 046ae87..d918a01 100644
--- a/VerifiedCommitments/CommitmentScheme.lean
+++ b/VerifiedCommitments/CommitmentScheme.lean
@@ -4,76 +4,99 @@ import Mathlib.Probability.ProbabilityMassFunction.Constructions
 import Mathlib.Probability.Distributions.Uniform
 import Mathlib.Data.ZMod.Defs
 
+/-- A CommitmentScheme is a structure over four spaces:
+M: Message space
+C: Commitment space
+O: Opening value space
+K: Key space
+
+And that contains three algorithms:
+setup: returns a public parameter and associated randomness
+commit: given the public parameter and a message produces a commitment and an opening value
+verify: given the public parameter, message and associated commit and opening value returns 1 when the commit opens to the given message and 0 otherwise.-/
 structure CommitmentScheme (M C O K : Type) where
   setup : PMF (K × O)
   commit : K → M → PMF (C × O)
   verify : K → M → C → O → ZMod 2
 
+
+/-- The structure of binding adversary guesses for use in the computational binding game.-/
 structure BindingGuess (M C O : Type) where
   c : C
   m : M
   m' : M
   o : O
-  o': O
+  o' : O
 
+/-- The structure of the hiding adversary for use in the computational hiding game.-/
 structure TwoStageAdversary (K M C : Type) where
-  State : Type
-  stage1 : K → PMF ((M × M) × State)
-  stage2 : C → State → PMF (ZMod 2)
+  state : Type
+  stage1 : K → PMF ((M × M) × state)
+  stage2 : C → state → PMF (ZMod 2)
 
 namespace Commitment
 
-noncomputable section
 variable {M C O K : Type}
-variable (scheme : CommitmentScheme M C O K)
 
+/-- For any public parameters `h` and any message `m` if `commit` outputs a commitment `c` and opening value `o`, then `verify h m c o` accepts with probability 1.-/
 def correctness (scheme : CommitmentScheme M C O K) : Prop :=
-  ∀ (h : K) (m : M),
-  PMF.bind (scheme.commit h m) (fun (commit, opening_val) => pure $ scheme.verify h m commit opening_val) = pure 1
+  ∀ (h : K) (m : M), (scheme.commit h m |>.bind fun (c, o) =>
+    pure <| scheme.verify h m c o) = pure 1
 
--- Perfect binding
+/-- A commitment scheme with public parameter `h` is perfectly binding if no commitment `c` can be opened to two different messages. For two purported openings `(m,o)` and `(m',o')` both verifying for the same `c`, the messages must be equal (`m = m'`). -/
 def perfect_binding (scheme : CommitmentScheme M C O K) : Prop :=
   ∀ (h : K) (c : C) (m m' : M) (o o' : O),
     scheme.verify h m c o = 1 →
-    scheme.verify h m' c o' = 1 →
-    m = m'
-    -- Equivalent to:
-    --if scheme.verify h m c o = scheme.verify h m' c o' then true else false
-
--- Computational binding game
--- Security depends on generating the parameters correctly, but at this level probably alright to have the group and generator fixed
--- h should be inside the game, because its unique to a specific run
-def comp_binding_game (scheme : CommitmentScheme M C O K)
-  (A' : K → PMF (BindingGuess M C O)) : PMF $ ZMod 2 :=
-  open scoped Classical in
-  PMF.bind scheme.setup (fun (h, _) =>
-    PMF.bind (A' h) (fun guess =>
-      if scheme.verify h guess.m guess.c guess.o = 1 ∧ scheme.verify h guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0 ))
-
-def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
-  ∀ (A' : K → PMF (BindingGuess M C O )), comp_binding_game scheme A' 1 ≤ ε
-
-
--- Perfect hiding
-def do_commit (scheme: CommitmentScheme M C O K) (m : M) : PMF C :=
-PMF.bind scheme.setup (fun (h, _) =>
-  PMF.bind (scheme.commit h m) (fun (c, _) => pure c))
+      scheme.verify h m' c o' = 1 →
+        m = m'
 
+/-- A commitment scheme is perfectly hiding if for any messages `m` and `m'`, the induced distribution on commitments is the same. Sampling `h ← setup` and then committing to `m` or `m'` under `h` yields identical commitment distributions. -/
 def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop :=
-  ∀ (m m' : M) (c : C), (do_commit scheme m) c = (do_commit scheme m') c
-
--- Computational hiding game
-def comp_hiding_game (scheme : CommitmentScheme M C O K) (A : TwoStageAdversary K M C) :=
-  PMF.bind scheme.setup (fun (h, _) =>
-    PMF.bind (A.stage1 h) (fun ((m₀, m₁), state) =>
-      PMF.bind (PMF.uniformOfFintype (ZMod 2)) (fun b =>
-        PMF.bind (scheme.commit h (if b = 0 then m₀ else m₁)) (fun (c, _) =>
-          PMF.bind (A.stage2 c state) (fun b' =>
-            pure (1 + b + b'))))))
-
-def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
-  ∀ (A : TwoStageAdversary K M C), comp_hiding_game scheme A 1 - 1/2 ≤ ε
+  ∀ (m m' : M) (c : C),
+    PMF.bind scheme.setup (fun (h, _) =>
+      PMF.bind (scheme.commit h m) (fun (c, _) =>
+        pure c)) c
+    =
+    PMF.bind scheme.setup (fun (h, _) =>
+      PMF.bind (scheme.commit h m') (fun (c, _) =>
+        pure c)) c
+
+/- Computational Binding -/
+
+/-- For any adversary `A` that accepts `h ← setup` and outputs a single commitment `c` together with two purported openings `(m,o)` and `(m',o')`, the computational binding game outputs `1` if `c` opens to both `(m,o)` and `(m',o') and the messages differ (`m ≠ m'`). -/
+noncomputable def comp_binding_game
+    [DecidableEq M] (scheme : CommitmentScheme M C O K)
+    (A : K → PMF (BindingGuess M C O)) : PMF (ZMod 2) := do
+  let (h, _) ← scheme.setup
+  let guess ← A h
+  pure (
+    if scheme.verify h guess.m guess.c guess.o = 1 ∧
+      scheme.verify h guess.m' guess.c guess.o' = 1 ∧
+        guess.m ≠ guess.m'
+          then 1 else 0 )
+
+/-- A commitment scheme is computationally binding if every adversary’s probability of winning the computational binding game is at most `ε`. -/
+def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K)
+    (ε : ENNReal) : Prop :=
+  ∀ (A' : K → PMF (BindingGuess M C O )), comp_binding_game scheme A' 1 ≤ ε
 
-end
+/- Computational Hiding -/
+
+/-- For any `TwoStageAdversary` `A`, sample `h ← setup` and give `h` to the adversary’s first stage to produce two challenge messages `m₀, m₁. The computational hiding game samples a uniform bit `b`, computes a commitment to `m_b`, and gives the commitment `c` to the adversary’s second stage. The game outputs a bit indicating whether the adversary’s guess matches `b`. -/
+noncomputable def comp_hiding_game
+    (scheme : CommitmentScheme M C O K)
+    (A : TwoStageAdversary K M C) := do
+  let (h, _) ← scheme.setup
+  let ((m₀, m₁), state) ← A.stage1 h
+  let b ← PMF.uniformOfFintype (ZMod 2)
+  let (c, _) ← scheme.commit h (if b = 0 then m₀ else m₁)
+  let b' ← A.stage2 c state
+  pure (1 + b + b')
+
+/-- A commitment scheme is computationally hiding if every adversary’s advantage
+over random guessing in the hiding game is at most `ε`. -/
+def computational_hiding (scheme : CommitmentScheme M C O K)
+    (ε : ENNReal) : Prop :=
+  ∀ (A : TwoStageAdversary K M C), comp_hiding_game scheme A 1 - 1/2 ≤ ε
 
 end Commitment
diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index 3767892..3fbf5d4 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -1,52 +1,12 @@
 -- From cryptolib licensed under Apache 2.0
 -- https://github.com/joeylupo/cryptolib
 
-/-
- -----------------------------------------------------------
-  Correctness and semantic security of ElGamal public-key
-  encryption scheme
- -----------------------------------------------------------
--/
-
-import Mathlib
 import VerifiedCommitments.cryptolib
 import VerifiedCommitments.CommitmentScheme
 
-namespace DDH
-
-variable (G : Type) [Fintype G] [Group G]
-          (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
-          (q : ℕ) [NeZero q] [Fact (0 < q)] (G_card_q : Fintype.card G = q)
-          (D : G → G → G → PMF (ZMod 2))
-
-include g_gen_G G_card_q
-
-instance : Fintype (ZMod q) := ZMod.fintype q
-
-noncomputable def Game0 : PMF (ZMod 2) :=
-do
-  let x ← PMF.uniformOfFintype (ZMod q)
-  let y ← PMF.uniformOfFintype (ZMod q)
-  let b ← D (g^x.val) (g^y.val) (g^(x.val * y.val))
-  pure b
-
-noncomputable def Game1 : PMF (ZMod 2) :=
-do
-  let x ← PMF.uniformOfFintype (ZMod q)
-  let y ← PMF.uniformOfFintype (ZMod q)
-  let z ← PMF.uniformOfFintype (ZMod q)
-  let b ← D (g^x.val) (g^y.val) (g^z.val)
-  pure b
-
--- DDH0(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^(xy))
--- local notation `Pr[DDH0(D)]` := (DDH0 G g g_gen_G q G_card_q D 1 : ℝ)
-
--- DDH1(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^z)
--- local notation `Pr[DDH1(D)]` := (DDH1 G g g_gen_G q G_card_q D 1 : ℝ)
-
-def Assumption (ε : ENNReal) : Prop := (Game0 G g q D 1) - (Game1 G g q D 1) ≤ ε
-
-end DDH
+/- ========================================
+   PUBLIC PARAMETERS
+   ======================================== -/
 
 namespace Elgamal
 
@@ -55,27 +15,27 @@ class PublicParameters (G : Type) extends
   [decidable_G : DecidableEq G]
   q : ℕ
   [neZero_q : NeZero q]
-  -- [fact (0 < params.q)]
   prime_q : Nat.Prime q
   g : G
   card_eq : Fintype.card G = q
-  g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g
-  G_card_q : Fintype.card G = q
+  gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g
 
 -- Make instances available
 variable {G : Type} [params : PublicParameters G]
 instance : DecidableEq G := params.decidable_G
 instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
 
-noncomputable def setup : PMF (G × ZMod params.q) := -- Need to include x to match CommitmentScheme spec
-do
+/- ========================================
+   SCHEME DEFINITION
+   ======================================== -/
+
+noncomputable def setup : PMF (G × ZMod params.q) := do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   return (params.g^x.val, x)
 
-noncomputable def commit (h m : G) : PMF ((G × G) × ZMod params.q) :=
-do
+noncomputable def commit (h m : G) : PMF ((G × G) × ZMod params.q) := do
   let r ← PMF.uniformOfFintype (ZMod params.q)
-  pure ((params.g^r.val, h^r.val * m), r)
+  return ((params.g^r.val, h^r.val * m), r)
 
 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
@@ -85,56 +45,59 @@ noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G where
   commit := commit
   verify := verify
 
-/-
-  -----------------------------------------------------------
-  Proof of correctness of ElGamal
-  -----------------------------------------------------------
--/
+/- ========================================
+   CORRECTNESS
+   ======================================== -/
 
-theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G params) := by
+theorem elgamal_commitment_correctness :
+    Commitment.correctness (@scheme G params) := by
   intro h m
   show PMF.bind (scheme.commit h m) _ = _
   simp only [scheme]
   unfold commit verify
   simp only [bind_pure_comp, Functor.map, PMF.bind_bind, Function.comp_apply, PMF.pure_bind, ↓reduceIte, PMF.bind_const]
 
+/- ========================================
+   DDH EXPERIMENT
+   ======================================== -/
+
+namespace DDH
 
-/-
-  -----------------------------------------------------------
-  Proof of semantic security of ElGamal
-  -----------------------------------------------------------
--/
+variable (D : G → G → G → PMF (ZMod 2))
 
-noncomputable def D_from_adversary (A : TwoStageAdversary G G (G × G)) : G → G → G → PMF (ZMod 2) :=
+noncomputable def experiment0 : PMF (ZMod 2) := do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  let y ← PMF.uniformOfFintype (ZMod params.q)
+  let z := x.val * y.val
+  let b ← D (params.g^x.val) (params.g^y.val) (params.g^z)
+  return b
+
+noncomputable def experiment1 : PMF (ZMod 2) := do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  let y ← PMF.uniformOfFintype (ZMod params.q)
+  let z ← PMF.uniformOfFintype (ZMod params.q)
+  let b ← D (params.g^x.val) (params.g^y.val) (params.g^z.val)
+  return b
+
+def Assumption (ε : ENNReal) : Prop := (experiment0 D 1) - (experiment1 D 1) ≤ ε
+
+end DDH
+
+/- ========================================
+   HIDING PROPERTY
+   ======================================== -/
+
+noncomputable def D_from_adversary
+    (A : TwoStageAdversary G G (G × G)) : G → G → G → PMF (ZMod 2) :=
   fun gx gy gz => do
     let ((m₀, m₁), state) ← A.stage1 gx
     let b ← PMF.uniformOfFintype (ZMod 2)
     let mb := if b = 0 then m₀ else m₁
     let b' ← A.stage2 ⟨gy, gz * mb⟩ state
-    pure (1 + b + b')
-
-/-
-  The probability of the attacker (i.e. the composition of A1 and A2)
-  winning the semantic security game (i.e. guessing the correct bit),
-  w.r.t. ElGamal is equal to the probability of D winning the game DDH0.
--/
-theorem ComputationalHiding_DDH0 (A : TwoStageAdversary G G (G × G)) : Commitment.comp_hiding_game scheme A =  DDH.Game0 G params.g params.q (D_from_adversary A) := by
-  simp only [Commitment.comp_hiding_game, DDH.Game0, bind, scheme, setup, commit, D_from_adversary]
-  simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
-  apply bind_skip'
-  intro x
-  simp [pure]
-  simp_rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
-  apply bind_skip'
-  intro m
-  apply bind_skip'
-  intro b
-  apply bind_skip'
-  intro y
-  rw [pow_mul params.g x.val y.val]
+    return (1 + b + b')
 
-noncomputable def Game1 (A : TwoStageAdversary G G (G × G)) : PMF (ZMod 2) :=
-do
+noncomputable def Game1
+    (A : TwoStageAdversary G G (G × G)) : PMF (ZMod 2) := do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   let y ← PMF.uniformOfFintype (ZMod params.q)
   let ((m₀, m₁), a_state) ← A.stage1 (params.g^x.val)
@@ -144,10 +107,10 @@ do
     let mb ← pure (if b = 0 then m₀ else m₁)
     pure (params.g^z.val * mb))
   let b' ← A.stage2 ⟨(params.g^y.val), ζ⟩ a_state
-  pure (1 + b + b')
+  return (1 + b + b')
 
-noncomputable def Game2 (A : TwoStageAdversary G G (G × G)) : PMF (ZMod 2) :=
-do
+noncomputable def Game2
+    (A : TwoStageAdversary G G (G × G)) : PMF (ZMod 2) := do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   let y ← PMF.uniformOfFintype (ZMod params.q)
   let (_, a_state) ← A.stage1 (params.g^x.val)
@@ -156,16 +119,38 @@ do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     pure (params.g^z.val))
   let b' ← A.stage2 ⟨(params.g^y.val), ζ⟩ a_state
-  pure (1 + b + b')
+  return (1 + b + b')
 
+/-
+  The probability of the attacker (i.e. the composition of A1 and A2)
+  winning the semantic security game (i.e. guessing the correct bit),
+  w.r.t. ElGamal is equal to the probability of D winning the game DDH0.
+-/
+theorem ComputationalHidingGame_DDH0
+    (A : TwoStageAdversary G G (G × G)) :
+    Commitment.comp_hiding_game scheme A =
+    DDH.experiment0 (D_from_adversary A) := by
+  simp only [Commitment.comp_hiding_game, DDH.experiment0, bind, scheme, setup, commit, D_from_adversary]
+  simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
+  apply bind_skip'
+  intro x
+  simp [pure]
+  simp_rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
+  apply bind_skip'
+  intro m
+  apply bind_skip'
+  intro b
+  apply bind_skip'
+  intro y
+  rw [pow_mul params.g x.val y.val]
 
 /-
   The probability of the attacker (i.e. the composition of A1 and A2)
   winning Game1 (i.e. guessing the correct bit) is equal to the
   probability of D winning the game DDH1.
 -/
-theorem Game1_DDH1 (A : TwoStageAdversary G G (G × G)) : @Game1 G params A = DDH.Game1 G params.g params.q (D_from_adversary A):= by
-  simp only [DDH.Game1, Game1, bind, D_from_adversary]
+theorem Game1_DDH1 (A : TwoStageAdversary G G (G × G)) : @Game1 G params A = DDH.experiment1 (D_from_adversary A) := by
+  simp only [DDH.experiment1, Game1, bind, D_from_adversary]
   simp only [PMF.bind_bind, mul_ite]
   apply bind_skip'
   intro x
@@ -191,7 +176,7 @@ lemma exp_bij : Function.Bijective (fun (z : ZMod params.q) => params.g ^ z.val)
   apply (Fintype.bijective_iff_surjective_and_card _).mpr
   simp [params.card_eq]
   intro y
-  obtain ⟨k, hk⟩ := params.g_gen_G y
+  obtain ⟨k, hk⟩ := params.gen_G y
   use (k : ZMod params.q)
   simp only at hk ⊢
   rw [← hk]
@@ -368,9 +353,9 @@ variable (ε : ENNReal)
 
 theorem hiding_from_ddh_single_adversary
     (A : TwoStageAdversary G G (G × G))
-    (DDH_assumption : DDH.Assumption G params.g params.q (D_from_adversary A) ε) :
+    (DDH_assumption : DDH.Assumption (D_from_adversary A) ε) :
     Commitment.comp_hiding_game scheme A 1 - 1/2 ≤ ε := by
-  rw [ComputationalHiding_DDH0]
+  rw [ComputationalHidingGame_DDH0]
   have h : ((PMF.uniformOfFintype (ZMod 2)) 1) = 1/2 := by
     simp only [PMF.uniformOfFintype_apply, ZMod.card, Nat.cast_ofNat, one_div]
   rw [← h]
@@ -381,7 +366,7 @@ theorem hiding_from_ddh_single_adversary
 
 
 theorem computational_hiding_from_ddh (ε : ENNReal)
-    (DDH_hard : ∀ (D : G → G → G → PMF (ZMod 2)), DDH.Assumption G params.g params.q D ε) :
+    (DDH_hard : ∀ (D : G → G → G → PMF (ZMod 2)), DDH.Assumption D ε) :
     Commitment.computational_hiding (@scheme G params) ε := by
   unfold Commitment.computational_hiding
   intro hA
@@ -400,7 +385,7 @@ lemma ordg_eq_q : orderOf params.g = params.q := by
       constructor
       · exact Subtype.val_injective
       · intro x
-        use ⟨x, params.g_gen_G x⟩
+        use ⟨x, params.gen_G x⟩
     exact Fintype.card_of_bijective this
   rw [← h_card_zpow, h_card_eq, params.card_eq]
 
@@ -414,7 +399,6 @@ theorem perfect_binding : Commitment.perfect_binding (@scheme G params) := by
   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₁)
 
diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean
index 8cd41b9..4cacd65 100644
--- a/VerifiedCommitments/Pedersen.lean
+++ b/VerifiedCommitments/Pedersen.lean
@@ -14,7 +14,7 @@ namespace Pedersen
    PUBLIC PARAMETERS
    ======================================== -/
 
-class PedersenScheme (G : Type) extends
+class PublicParameters (G : Type) extends
   Fintype G, Group G, IsCyclic G where
   [decidable_G : DecidableEq G]
   q : ℕ
@@ -25,46 +25,36 @@ class PedersenScheme (G : Type) extends
   gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g
 
 -- Make instances available
-variable {G : Type} [params : PedersenScheme G]
+variable {G : Type} [params : PublicParameters G]
 instance : DecidableEq G := params.decidable_G
 instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
 
-/- ========================================
-   CORE LEMMAS
-   ======================================== -/
-
-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.gen_G x⟩
-    exact Fintype.card_of_bijective this
-  rw [← h_card_zpow, h_card_eq, params.card_eq]
-
-
 /- ========================================
    SCHEME DEFINITION
    ======================================== -/
 
 noncomputable def setup : PMF (G × (ZMod params.q)) :=
-  PMF.bind (PMF.uniformOfFintype (ZModMult params.q)) (fun a => return ⟨params.g^(val a).val, val a⟩)
+  PMF.uniformOfFintype (ZModMult params.q)|>.bind fun a =>
+    return ⟨params.g^(val a).val, val a⟩
 
-noncomputable def commit (h : G) (m : ZMod params.q) : PMF (G × (ZMod params.q)) :=
-  PMF.bind (PMF.uniformOfFintype (ZMod params.q)) (fun r => return ⟨params.g^m.val * h^r.val, r⟩)
+noncomputable def commit
+    (h : G) (m : ZMod params.q) : PMF (G × (ZMod params.q)) :=
+  PMF.uniformOfFintype (ZMod params.q)|>.bind fun r =>
+    return ⟨params.g^m.val * h^r.val, r⟩
 
-def verify (h : G) (m : ZMod params.q) (c : G) (o : ZMod params.q) : ZMod 2 :=
+def verify
+    (h : G) (m : ZMod params.q) (c : G) (o : ZMod params.q) : ZMod 2 :=
   if c = params.g^m.val * h^o.val then 1 else 0
 
-noncomputable def scheme : CommitmentScheme (ZMod params.q) G (ZMod params.q) G :=
-  {
-    setup := setup,
-    commit := commit,
-    verify := verify
-  }
+noncomputable def scheme :
+    CommitmentScheme (ZMod params.q) G (ZMod params.q) G where
+  setup := setup
+  commit := commit
+  verify := verify
 
+/- ========================================
+   CORRECTNESS
+   ======================================== -/
 
 theorem pedersen_correctness : Commitment.correctness (@scheme G params) := by
   unfold Commitment.correctness
@@ -121,37 +111,59 @@ theorem pedersen_correctness : Commitment.correctness (@scheme G params) := by
     · simp [ENNReal.natCast_ne_top]
   · simp [hb]
 
-
-noncomputable def generate_a : PMF (ZModMult params.q) := PMF.uniformOfFintype (ZModMult params.q)
-
 /- ========================================
    DLOG EXPERIMENT
    ======================================== -/
 
 section DLog
 
-noncomputable def DLogExperiment (A : G → PMF (ZMod params.q)) : PMF (ZMod 2) :=
-  PMF.bind scheme.setup (fun h =>
-  PMF.bind (A h.1) (fun x' => pure (if params.g^x'.val = params.g^(h.2).val then 1 else 0)))
-
-noncomputable def constructDlogAdversary
-      (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q)))
-      (h : G) : PMF (ZMod params.q) :=
-    PMF.bind (A h) (fun guess =>
-      if guess.o ≠ guess.o' then
-        return ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹)
-      else
-        PMF.uniformOfFintype (ZMod params.q))
+noncomputable def DLogExperiment
+    (A : G → PMF (ZMod params.q)) :
+    PMF (ZMod 2) :=
+  scheme.setup.bind fun (h, x) =>
+    (A h).bind fun x' =>
+      pure <| if params.g^x'.val = params.g^(x).val then 1 else 0
+
+noncomputable def constructDLogAdversary
+    (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q)))
+    (h : G) : PMF (ZMod params.q) :=
+  PMF.bind (A h) fun guess =>
+    if guess.o ≠ guess.o' then
+      return (guess.m - guess.m') * (guess.o' - guess.o)⁻¹
+    else
+      PMF.uniformOfFintype (ZMod params.q)
 
 end DLog
 
+/- ========================================
+   CORE LEMMAS AND DEFINITIONS
+   ======================================== -/
+
+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.gen_G x⟩
+    exact Fintype.card_of_bijective this
+  rw [← h_card_zpow, h_card_eq, params.card_eq]
+
+noncomputable def generate_a : PMF (ZModMult params.q) :=
+    PMF.uniformOfFintype (ZModMult params.q)
+
 /- ========================================
    HIDING PROPERTY
    ======================================== -/
 
 section Hiding
 
-lemma exp_bij (a : ZModMult params.q) (m : ZMod params.q) : Function.Bijective fun (r : ZMod params.q) =>
+lemma exp_bij (a : ZModMult params.q) (m : ZMod params.q) :
+    Function.Bijective fun (r : ZMod params.q) =>
     params.g^((m + (val a) * r : ZMod params.q).val : ℤ) := by
   apply (Fintype.bijective_iff_surjective_and_card _).mpr
   simp [params.card_eq]
@@ -208,44 +220,78 @@ lemma expEquiv_unfold (a : ZModMult params.q) (m r : ZMod params.q) :
   simp
 
 lemma bij_uniform_for_fixed_a (a : ZModMult params.q) (m : ZMod params.q) :
-    PMF.map (expEquiv a m) (PMF.uniformOfFintype (ZMod params.q)) = (PMF.uniformOfFintype G) := by
-  · expose_names;
+    (PMF.uniformOfFintype (ZMod params.q)).map (expEquiv a m) =
+      PMF.uniformOfFintype G := by
     exact map_uniformOfFintype_equiv (expEquiv a m)
 
 lemma bij_uniform_for_uniform_a (m : ZMod params.q) :
-    (PMF.bind (generate_a)
-    (fun a => PMF.map (expEquiv a m) (PMF.uniformOfFintype (ZMod params.q)))) = (PMF.uniformOfFintype G) := by
-  unfold generate_a
+    generate_a.bind (fun a =>
+      (PMF.uniformOfFintype (ZMod params.q)).map (expEquiv a m)) =
+        PMF.uniformOfFintype G := by
   apply bind_skip_const'
   intro a
-  · expose_names; exact bij_uniform_for_fixed_a a m
+  exact bij_uniform_for_fixed_a a m
 
 lemma pedersen_commitment_uniform (m : ZMod params.q) (c : G) :
-    (PMF.map Prod.fst (PMF.bind (generate_a : PMF (ZModMult params.q))
-    (fun a => commit (params.g^(val a).val) m )) c) =
-    ((1 : ENNReal) / (Fintype.card G)) := by
-  unfold commit
-  simp only [PMF.map_bind, pure, PMF.pure_map]
-  have h_eq : (PMF.bind (generate_a : PMF (ZModMult params.q))
-                (fun a => PMF.bind (PMF.uniformOfFintype (ZMod params.q))
-                  (fun r => PMF.pure (params.g^m.val * (params.g^(val a).val)^r.val)))) =
-              (PMF.bind (generate_a : PMF (ZModMult params.q))
-                (fun a => PMF.map (expEquiv a m) (PMF.uniformOfFintype (ZMod params.q)))) := by
+    (generate_a.bind fun (a : ZModMult params.q) =>
+      commit (params.g^(val a).val) m ).map Prod.fst c =
+        (1 : ENNReal) / Fintype.card G := by
+  have h_eq : (generate_a.bind fun (a : ZModMult params.q) =>
+        commit (params.g^(val a).val) m).map Prod.fst  =
+          generate_a.bind fun (a : ZModMult params.q) =>
+            PMF.uniformOfFintype (ZMod params.q)|>.map (expEquiv a m) := by
+    unfold commit PMF.map
+    simp only [PMF.bind_bind]
     apply bind_skip'
     intro a
     ext x
-    simp only [PMF.bind_apply, PMF.map_apply, PMF.pure_apply, PMF.uniformOfFintype_apply]
+    simp only [PMF.bind_apply, PMF.uniformOfFintype_apply]
     congr 1; ext r
     by_cases h : x = params.g^m.val * (params.g^(val a).val)^r.val
-    · simp only [h, ↓reduceIte]
+    · simp only [h, ZMod.card, Function.comp_apply, PMF.pure_apply, mul_ite, mul_one, mul_zero, tsum_fintype]
       rw [← expEquiv_unfold a m r]
-      simp
-    · simp only [h, ↓reduceIte]
+      have hs :
+          (∑ a_1 : G × ZMod params.q,
+            if (expEquiv a m) r = a_1.1 then
+              (pure ((expEquiv a m) r, r) :
+                PMF (G × ZMod params.q)) a_1 else 0) = (1 : ENNReal) := by
+        have hs_pure:
+            (∑ a_1 : G × ZMod params.q,
+              if (expEquiv a m) r = a_1.1 then
+                (pure ((expEquiv a m) r, r) :
+                  PMF (G × ZMod params.q)) a_1 else 0) =
+                    ∑ a_1 : G × ZMod params.q, (pure ((expEquiv a m) r, r) :
+                      PMF (G × ZMod params.q)) a_1 := by
+          refine Finset.sum_congr rfl ?_
+          intro y hy
+          by_cases hyEq : y = ((expEquiv a m) r, r)
+          · subst hyEq
+            simp
+          · have hp : (pure ((expEquiv a m) r, r) :
+                PMF (G × ZMod params.q)) y = 0 := by
+              exact PMF.pure_apply_of_ne (a := ((expEquiv a m) r, r)) (a' := y) hyEq
+            by_cases hy1 : (expEquiv a m) r = y.1
+            · simp [hy1]
+            · simp [hy1, hp]
+        have h_pure_one :
+            (∑ a_1 : G × ZMod params.q, (pure ((expEquiv a m) r, r) :
+              PMF (G × ZMod params.q)) a_1) = (1 : ENNReal) := by
+          simpa [tsum_fintype] using (PMF.tsum_coe
+            (pure ((expEquiv a m) r, r) : PMF (G × ZMod params.q)))
+        rw [hs_pure, h_pure_one]
+      simp [hs]
+    · simp only [ZMod.card, Function.comp_apply, PMF.pure_apply, mul_ite, mul_one, mul_zero, tsum_fintype]
       have : x ≠ expEquiv a m r := by
-        intro contra
-        rw [expEquiv_unfold a m r] at contra
-        exact h contra
+        grind only [expEquiv_unfold]
       simp [this]
+      intro a₁ b hx
+      subst hx
+      have hneq :
+          (x, b) ≠ (params.g ^ m.val *
+            (params.g ^ (val a).val) ^ r.val, r) := by grind only
+      exact PMF.pure_apply_of_ne
+        (a := (params.g ^ m.val * (params.g ^ (val a).val) ^ r.val, r))
+          (a' := (x, b)) hneq
   rw [h_eq]
   rw [bij_uniform_for_uniform_a m]
   simp [PMF.uniformOfFintype_apply]
@@ -253,7 +299,7 @@ lemma pedersen_commitment_uniform (m : ZMod params.q) (c : G) :
 theorem perfect_hiding : Commitment.perfect_hiding (@scheme G params) := by
   unfold Commitment.perfect_hiding
   intros m m' c
-  unfold Commitment.do_commit Pedersen.scheme
+  unfold Pedersen.scheme
   simp only []
   unfold Pedersen.setup Pedersen.commit
   simp only [PMF.bind_bind]
@@ -277,6 +323,7 @@ theorem perfect_hiding : Commitment.perfect_hiding (@scheme G params) := by
     simp only [PMF.map_bind, pure, PMF.pure_map]
   rw [h_lhs, h_rhs]
 
+
 end Hiding
 
 /- ========================================
@@ -285,17 +332,20 @@ end Hiding
 
 section Binding
 
-lemma binding_implies_dlog (a : ZMod params.q) (guess : BindingGuess (ZMod params.q) G (ZMod params.q)) :
-    let h := params.g ^ a.val
-    let verify := fun (m : ZMod params.q) (c : G) (o : ZMod params.q) => if c = params.g^m.val * h^o.val then (1 : ZMod 2) else 0
-    (verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') →
-    (guess.o ≠ guess.o' → params.g^(((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val) = h) := by
-  intro h verify ⟨h1, h2, m_ne⟩ o_ne
-  simp only [verify] at h1 h2
-  split at h1 <;> split at h2
+lemma gpow_eq_of_two_valid_openings
+    (a : ZMod params.q)
+    (guess : BindingGuess (ZMod params.q) G (ZMod params.q))
+    (h₁ :
+      (if guess.c = params.g ^ guess.m.val * (params.g ^ a.val) ^ guess.o.val
+        then (1 : ZMod 2) else 0) = 1)
+    (h₂ :
+      (if guess.c = params.g ^ guess.m'.val * (params.g ^ a.val) ^ guess.o'.val
+        then (1 : ZMod 2) else 0) = 1)
+    (ho_ne : guess.o ≠ guess.o') :
+    params.g^((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val =
+      params.g ^ a.val := by
+  split at h₁ <;> split at h₂
   case' isTrue.isTrue c_eq1 c_eq2 =>
-    simp only [h] at c_eq1 c_eq2
-
     have collision : params.g^guess.m.val * (params.g^a.val)^guess.o.val = params.g^guess.m'.val * (params.g^a.val)^guess.o'.val := by
       rw [← c_eq1, c_eq2]
 
@@ -303,17 +353,17 @@ lemma binding_implies_dlog (a : ZMod params.q) (guess : BindingGuess (ZMod param
     conv_rhs at collision => arg 2; rw [← pow_mul]
     rw [← pow_add, ← pow_add] at collision
 
-    have h_coprime : (guess.o' - guess.o).val.Coprime params.q := by
-      cases Nat.coprime_or_dvd_of_prime params.prime_q (guess.o' - guess.o).val with
-      | inl h_cop => exact Nat.coprime_comm.mp h_cop
-      | inr h_dvd =>
-        exfalso
-        have h_zero : guess.o' - guess.o = 0 := by
-          rw [← ZMod.val_eq_zero]
-          have h_mod_zero : (guess.o' - guess.o).val % params.q = 0 := Nat.mod_eq_zero_of_dvd h_dvd
-          have h_val_bound : (guess.o' - guess.o).val < params.q := ZMod.val_lt (guess.o' - guess.o)
-          exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound
-        exact o_ne.symm (eq_of_sub_eq_zero h_zero)
+    -- have h_coprime : (guess.o' - guess.o).val.Coprime params.q := by
+    --   cases Nat.coprime_or_dvd_of_prime params.prime_q (guess.o' - guess.o).val with
+    --   | inl h_cop => exact Nat.coprime_comm.mp h_cop
+    --   | inr h_dvd =>
+    --     exfalso
+    --     have h_zero : guess.o' - guess.o = 0 := by
+    --       rw [← ZMod.val_eq_zero]
+    --       have h_mod_zero : (guess.o' - guess.o).val % params.q = 0 := Nat.mod_eq_zero_of_dvd h_dvd
+    --       have h_val_bound : (guess.o' - guess.o).val < params.q := ZMod.val_lt (guess.o' - guess.o)
+    --       exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound
+    --     exact ho_ne.symm (eq_of_sub_eq_zero h_zero)
 
     have h_congr_nat : guess.m.val + a.val * guess.o.val ≡ guess.m'.val + a.val * guess.o'.val [MOD params.q] := by
       simpa [ordg_eq_q] using (pow_eq_pow_iff_modEq.mp collision)
@@ -329,14 +379,15 @@ lemma binding_implies_dlog (a : ZMod params.q) (guess : BindingGuess (ZMod param
   all_goals contradiction
 
 
-lemma binding_as_hard_dlog
+lemma binding_reduction_to_dlog
     (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))) : -- Pedersen adversary
-    Commitment.comp_binding_game (scheme) A 1 ≤ DLogExperiment (constructDlogAdversary A) 1 := by
-  unfold Commitment.comp_binding_game DLogExperiment constructDlogAdversary
+  Commitment.comp_binding_game (scheme) A 1 ≤
+    DLogExperiment (constructDLogAdversary A) 1 := by
+  unfold Commitment.comp_binding_game DLogExperiment constructDLogAdversary
 
   simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify]
 
-  rw [PMF.bind_apply, PMF.bind_apply]
+  rw [PMF.bind_apply]
   apply ENNReal.tsum_le_tsum
   intro ⟨h, a⟩
 
@@ -348,7 +399,7 @@ lemma binding_as_hard_dlog
     conv_rhs => rw [PMF.bind_bind]
 
     -- Same structure as above
-    rw [PMF.bind_apply, PMF.bind_apply]
+    rw [PMF.bind_apply ]
     apply ENNReal.tsum_le_tsum
     intro guess
 
@@ -356,7 +407,6 @@ lemma binding_as_hard_dlog
 
     simp only [ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not, ne_eq, ite_not,
       PMF.bind_apply, tsum_fintype]
-    rw [@DFunLike.ite_apply]
     split_ifs with h₁ h₂
 
     · -- Case 1: h₁ binding collision AND h₂ (o = o')
@@ -386,17 +436,11 @@ lemma binding_as_hard_dlog
       exact m_ne m_eq
 
     · -- Case 2: Binding collision (h₁) AND o ≠ o' (¬h₂)
-      -- This is the main case where we use binding_implies_dlog
-      have h_o_ne : guess.o ≠ guess.o' := h₂
+      -- This is the main case where we use gpow_eq_of_two_valid_openings
       let x' := (guess.m - guess.m') * (guess.o' - guess.o)⁻¹
 
-      have h₁' : (let h := params.g^a.val;
-                  let verify := fun m c o => if c = params.g^m.val * h^o.val then (1 : ZMod 2) else 0;
-                  verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') := by
-        grind only
-
       have h_dlog : params.g^x'.val = params.g^a.val := by
-        apply binding_implies_dlog a guess h₁' h_o_ne
+        grind only [gpow_eq_of_two_valid_openings]
 
       -- The RHS is a sum over a single-element distribution (pure x')
       -- The sum includes the term for x = x', which equals 1
@@ -450,10 +494,10 @@ lemma binding_as_hard_dlog
 theorem computational_binding :
     ∀ (ε : ENNReal),
     (∀ (A' : G → PMF (ZMod params.q)), DLogExperiment A' 1 ≤ ε) →
-    (∀ (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))),
-    Commitment.comp_binding_game (@scheme G params) A 1 ≤ ε) := by
+    ∀ (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))),
+    Commitment.comp_binding_game (@scheme G params) A 1 ≤ ε := by
   intro ε A' A
-  exact le_trans (binding_as_hard_dlog A) (A' (constructDlogAdversary A))
+  exact le_trans (binding_reduction_to_dlog A) (A' (constructDLogAdversary A))
 
 end Binding