From 668726ce9bb6800918639e317321604c08100d44 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Mon, 26 Jan 2026 22:02:17 -0800
Subject: [PATCH 01/11] wip: early defs - but not complete

---
 VerifiedCommitments/BindingEncryption.lean | 32 ++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 VerifiedCommitments/BindingEncryption.lean

diff --git a/VerifiedCommitments/BindingEncryption.lean b/VerifiedCommitments/BindingEncryption.lean
new file mode 100644
index 0000000..5280df4
--- /dev/null
+++ b/VerifiedCommitments/BindingEncryption.lean
@@ -0,0 +1,32 @@
+import VerifiedCommitments.elgamal
+
+variable {X Y L R : Type}
+
+structure BindingEncryptionScheme (X Y L R : Type) where
+  gen : PMF (L × L)
+  enc : L → X → R → Y
+  dec : L → Y → X
+
+
+def correctness (scheme : BindingEncryptionScheme X Y L R) : Prop :=
+  ∀ (m : X) (r : R) (sk pk : L), scheme.dec sk (scheme.enc pk m r) = m
+
+variable {G : Type} [params : Elgamal.ElgamalParameters G]
+instance : DecidableEq G := params.decidable_G
+instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
+
+noncomputable def setup : PMF (ZMod params.q × G) := --Elgamal.keygen
+  PMF.uniformOfFintype (ZMod params.q) |>.bind (fun x => pure (x, params.g^x.val))
+
+noncomputable def commit (h m : G) : PMF (G × ZMod params.q) := --(Elgamal.encrypt h m).map (fun (_, b) => b)
+  PMF.uniformOfFintype (ZMod params.q) |>.bind (fun r => pure (h^r.val * m, r))
+
+def verify (h m c : G) (o : ZMod params.q) : ZMod 2 := --if c = Elgamal.encrypt h m
+  if c = h^o.val * m then 1 else 0
+
+noncomputable def scheme : BindingEncryptionScheme G G G (ZMod params.q) :=
+  {
+    gen := setup,
+    enc := commit,
+    dec := verify
+  }

From 5f37bdaae6759c2645c00852dcafde0d0c3f9a9a Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Fri, 30 Jan 2026 21:11:36 -0800
Subject: [PATCH 02/11] wip: convert all pke ddh and elgamal defs to commit
 scheme

---
 VerifiedCommitments/ElgamalCommitments.lean | 454 ++++++++++++++++++++
 1 file changed, 454 insertions(+)
 create mode 100644 VerifiedCommitments/ElgamalCommitments.lean

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
new file mode 100644
index 0000000..6f891c5
--- /dev/null
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -0,0 +1,454 @@
+-- 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 : ℕ) [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 {q : ℕ} : Fintype (ZMod q) := sorry
+
+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
+
+namespace PKE
+variable {K M C O A_state: Type} [DecidableEq M]
+          (setup : PMF (K × O))
+          (commit : K → M → PMF (C × O))
+          (verify : K → M → C → O → ZMod 2)
+          (A1 : K → PMF (M × M × A_state))
+          (A2 : C → A_state → PMF (ZMod 2))
+
+/-
+  Executes the a public-key protocol defined by keygen,
+  encrypt, and decrypt
+-/
+noncomputable def commit_verify (m : M) : PMF (ZMod 2) :=
+do
+  let (h, _) ← setup
+  let c ← commit h m
+  pure (verify h m c.1 c.2)
+
+/-
+  A public-key encryption protocol is correct if decryption undoes
+  encryption with probability 1
+-/
+def pke_correctness : Prop := ∀ (m : M), commit_verify setup commit verify m = pure 1
+
+/-
+  The semantic security game.
+  Returns 1 if the attacker A2 guesses the correct bit
+-/
+noncomputable def ComputationalHidingGame : PMF (ZMod 2):=
+do
+  let (h, _) ← setup
+  let (m, m', a_state) ← A1 h
+  let b ← PMF.uniformOfFintype (ZMod 2)
+  let (c, _) ← commit h (if b = 0 then m else m')
+  let b' ← A2 c a_state
+  pure (1 + b + b')
+
+
+-- SSG(A) denotes the event that A wins the semantic security game
+--local notation `Pr[SSG(A)]` := (SSG keygen encrypt A1 A2 1 : ℝ)
+
+def pke_semantic_security (ε : ENNReal) : Prop :=  (ComputationalHidingGame setup commit A1 A2 1) - 1/2 ≤ ε
+
+end PKE
+
+namespace Elgamal
+
+class ElgamalParameters (G : Type) extends
+  Fintype G, Group G, IsCyclic G where
+  [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
+  A_state : Type
+  A1 : G → PMF (G × G × A_state)
+  A2 : G → G → A_state → PMF (ZMod 2)
+
+-- Make instances available
+variable {G : Type} [params : ElgamalParameters G]
+instance : DecidableEq G := params.decidable_G
+instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
+
+-- noncomputable section
+
+
+def A2' : G × G → params.A_state → PMF (ZMod 2) := fun (gg : G × G) => params.A2 gg.1 gg.2
+
+-- generates a public key `g^x.val`, and private key `x`
+noncomputable def setup : PMF (G × ZMod params.q) := -- Need to include x to match CommitmentScheme spec
+do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  return (params.g^x.val, x)
+
+-- encrypt takes a pair (public key, message)
+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)
+
+-- def verify (h m c : G) (o : ZMod params.q) : ZMod 2 :=
+--   (commit h m).bind (fun (x, _, _) => if x = c then 1 else 0)
+
+def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 :=
+  if c.2 = h^o.val * m then 1 else 0
+
+noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G :=
+{
+  setup := setup,
+  commit := commit,
+  verify := verify
+}
+
+/-
+  -----------------------------------------------------------
+  Proof of correctness of ElGamal
+  -----------------------------------------------------------
+-/
+
+
+def elgamal_commitment_correctness_prop : Prop :=
+  ∀ (m : G), PKE.commit_verify setup commit verify m = pure 1
+
+
+theorem elgamal_commitment_correctness : @elgamal_commitment_correctness_prop G params := by
+  simp [elgamal_commitment_correctness_prop]
+  intro m
+  unfold setup commit verify PKE.commit_verify
+  simp only [bind_pure_comp, Functor.map_map, bind_map_left]
+  apply bind_skip_const'
+  intro x
+  apply bind_skip_const'
+  intro y
+  simp only [Function.comp_apply]
+  rfl
+
+
+
+/-
+  -----------------------------------------------------------
+  Proof of semantic security of ElGamal
+  -----------------------------------------------------------
+-/
+
+noncomputable def D (gx gy gz : G) : PMF (ZMod 2) :=
+do
+  let m ← params.A1 gx
+  let b ← PMF.uniformOfFintype (ZMod 2)
+  let mb ← pure (if b = 0 then m.1 else m.2.1)
+  let b' ← params.A2 gy (gz * mb) m.2.2
+  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 SSG_DDH0 : PKE.SSG keygen encrypt params.A1 A2' =  DDH.Game0 G params.g params.q D := by
+  simp only [PKE.SSG, DDH.Game0, bind, keygen, encrypt, D]
+  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
+  simp only [A2']
+  rw [pow_mul params.g x.val y.val]
+
+noncomputable def Game1 : PMF (ZMod 2) :=
+do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  let y ← PMF.uniformOfFintype (ZMod params.q)
+  let m ← params.A1 (params.g^x.val)
+  let b ← PMF.uniformOfFintype (ZMod 2)
+  let ζ ← (do
+    let z ← PMF.uniformOfFintype (ZMod params.q)
+    let mb ← pure (if b = 0 then m.1 else m.2.1)
+    pure (params.g^z.val * mb))
+  let b' ← params.A2 (params.g^y.val) ζ m.2.2
+  pure (1 + b + b')
+
+noncomputable def Game2 : PMF (ZMod 2) :=
+do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  let y ← PMF.uniformOfFintype (ZMod params.q)
+  let m ← params.A1 (params.g^x.val)
+  let b ← PMF.uniformOfFintype (ZMod 2)
+  let ζ ← (do
+    let z ← PMF.uniformOfFintype (ZMod params.q)
+    pure (params.g^z.val))
+  let b' ← params.A2 (params.g^y.val) ζ m.2.2
+  pure (1 + b + b')
+
+
+
+/-
+  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 : @Game1 G params = DDH.Game1 G params.g params.q D := by
+  simp only [DDH.Game1, Game1, bind, D]
+  apply bind_skip'
+  intro x
+  apply bind_skip'
+  intro y
+  simp_rw [PMF.bind_bind (params.A1 _)]
+  conv_rhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
+  apply bind_skip'
+  intro m
+  simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
+  conv_lhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod 2))]
+  apply bind_skip'
+  intro z
+  conv_rhs => rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod 2))]
+  apply bind_skip'
+  intro b
+  simp_rw [PMF.bind_bind]
+  apply bind_skip'
+  intro mb
+  simp [pure]
+
+
+lemma exp_bij : Function.Bijective (fun (z : ZMod params.q) => params.g ^ z.val) := by
+  apply (Fintype.bijective_iff_surjective_and_card _).mpr
+  simp [params.card_eq]
+  intro y
+  obtain ⟨k, hk⟩ := params.g_gen_G y
+  use (k : ZMod params.q)
+  simp only at hk ⊢
+  rw [← hk]
+  suffices params.g ^ ((k : ZMod params.q).val : ℤ) = params.g ^ k by exact_mod_cast this
+  simp only [ZMod.val_intCast, ← params.card_eq]
+  exact zpow_mod_card params.g k
+
+
+lemma exp_mb_bij (mb : G) : Function.Bijective (fun (z : ZMod params.q) => params.g ^ z.val * mb) := by
+  have h : (fun (z : ZMod params.q) => params.g ^ z.val * mb) =
+    (fun (m : G) => m * mb) ∘ (fun (z : ZMod params.q) => params.g ^ z.val) := by rfl
+  rw [h]
+  apply Function.Bijective.comp
+  · -- (λ (m : G), (m * mb)) bijective
+    refine (Fintype.bijective_iff_injective_and_card _).mpr ⟨?_, rfl⟩
+    intros x y hxy
+    exact mul_right_cancel hxy
+  · -- (λ (z : ZMod params.q), g ^ z.val) bijective
+    exact exp_bij
+
+
+lemma G1_G2_lemma1 (x : G) (exp : ZMod params.q → G) (exp_bij : Function.Bijective exp) :
+    ∑' (z : ZMod params.q), ite (x = exp z) (1 : ENNReal) 0 = 1 := by
+  obtain ⟨exp_inv, hinv_left, hinv_right⟩ := Function.bijective_iff_has_inverse.mp exp_bij
+  have bij_eq : ∀ (z : ZMod params.q), (x = exp z) ↔ (z = exp_inv x) := by
+    intro z
+    constructor
+    · -- (x = exp z) → (z = exp_inv x)
+      intro h
+      have h1 : exp_inv x = exp_inv (exp z) := congrArg exp_inv h
+      rw [hinv_left z] at h1
+      exact h1.symm
+    · -- (z = exp_inv x) → (x = exp z)
+      intro h
+      have h2 : exp z = exp (exp_inv x) := congrArg exp h
+      rw [hinv_right x] at h2
+      exact h2.symm
+  simp_rw [bij_eq]
+  simp
+
+
+lemma G1_G2_lemma2 (mb : G) :
+    (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val * mb)) =
+    (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val)) := by
+  ext x
+  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, Pure.pure]
+  have lhs_eq : ∑' (z : ZMod params.q), ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * (PMF.pure (params.g ^ z.val * mb)) x =
+                ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * ∑' (z : ZMod params.q), ite (x = params.g ^ z.val * mb) 1 0 := by
+    rw [ENNReal.tsum_mul_left]
+    congr
+    funext z
+    simp only [PMF.pure_apply]
+    split_ifs <;> ring
+  have rhs_eq : ∑' (z : ZMod params.q), ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * (PMF.pure (params.g ^ z.val)) x =
+                ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * ∑' (z : ZMod params.q), ite (x = params.g ^ z.val) 1 0 := by
+    rw [ENNReal.tsum_mul_left]
+    congr
+    funext z
+    simp only [PMF.pure_apply]
+    split_ifs <;> ring
+  rw [lhs_eq, rhs_eq]
+  rw [G1_G2_lemma1 x (fun z => params.g ^ z.val * mb) (exp_mb_bij mb)]
+  rw [G1_G2_lemma1 x (fun z => params.g ^ z.val) exp_bij]
+
+
+
+lemma G1_G2_lemma3 (m : PMF G) :
+    m.bind (fun (mb : G) => (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val * mb))) =
+    (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val)) := by
+  simp_rw [G1_G2_lemma2 _]
+  apply bind_skip_const'
+  intro m
+  congr
+
+/-
+  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 the attacker winning Game2.
+-/
+theorem Game1_Game2 : @Game1 G params = @Game2 G params := by
+  simp only [Game1, Game2]
+  apply bind_skip'
+  intro x
+  apply bind_skip'
+  intro y
+  apply bind_skip'
+  intro m
+  apply bind_skip'
+  intro b
+  simp [bind, -PMF.bind_pure, -PMF.bind_bind]
+  simp_rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
+  rw [G1_G2_lemma3]
+
+lemma G2_uniform_lemma (b' : ZMod 2) : (PMF.uniformOfFintype (ZMod 2)).bind (fun (b : ZMod 2) => pure (1 + b + b')) = PMF.uniformOfFintype (ZMod 2) := by
+  -- The function (b ↦ 1 + b + b') is a bijection on ZMod 2
+  have bij : Function.Bijective (fun b : ZMod 2 => 1 + b + b') := by
+    constructor
+    · intro x y hxy
+      have : x + b' = y + b' := by linear_combination hxy
+      linear_combination this
+    · intro y
+      use y - b' - 1
+      ring
+  -- Use the same argument as G1_G2_lemma2
+  ext a
+  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, Pure.pure, PMF.pure_apply]
+  rw [tsum_fintype]
+  simp only [mul_ite, mul_one, mul_zero]
+  have card_eq : Fintype.card (ZMod 2) = 2 := by norm_num
+  simp only [card_eq]
+  norm_num
+  -- Exactly one value of b makes a = 1 + b + b', namely b = a - b' - 1
+  have : ∃! b : ZMod 2, a = 1 + b + b' := by
+    use a - b' - 1
+    constructor
+    · ring
+    · intro y hy
+      calc y = y + 0 := by ring
+        _ = y + (b' + (a - b' - 1) - (a - 1)) := by ring
+        _ = (y + b') + (a - b' - 1) - (a - 1) := by ring
+        _ = (1 + y + b') + (a - b' - 1) - (1 + a - 1) := by ring
+        _ = a + (a - b' - 1) - a := by rw [← hy]; ring
+        _ = a - b' - 1 := by ring
+  obtain ⟨b₀, hb₀, huniq⟩ := this
+  have sum_eq : ∑ x : ZMod 2, (if a = 1 + x + b' then (2⁻¹ : ENNReal) else 0) = 2⁻¹ := by
+    have : ∑ x : ZMod 2, (if a = 1 + x + b' then (2⁻¹ : ENNReal) else 0) =
+           ∑ x : ZMod 2, (if x = b₀ then (2⁻¹ : ENNReal) else 0) := by
+      congr 1
+      ext x
+      by_cases h : a = 1 + x + b'
+      · simp [h, huniq x h]
+      · simp [h]
+        by_cases hx : x = b₀
+        · subst hx
+          contradiction
+        · simp [hx]
+    rw [this, Finset.sum_ite_eq']
+    simp
+  exact sum_eq
+
+
+/-
+  The probability of the attacker (i.e. the composition of A1 and A2)
+  winning Game2 (i.e. guessing the correct bit) is equal to a coin flip.
+-/
+theorem Game2_uniform : @Game2 G params = PMF.uniformOfFintype (ZMod 2) := by
+  simp [Game2, bind]
+  apply bind_skip_const'
+  intro x
+  apply bind_skip_const'
+  intro m
+  apply bind_skip_const'
+  intro y
+  rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod 2))]
+  simp_rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod 2))]
+  apply bind_skip_const'
+  intro z
+  apply bind_skip_const'
+  intro ζ
+  apply bind_skip_const'
+  intro b'
+  exact G2_uniform_lemma b'
+
+-- parameters (ε : nnreal)
+variable (ε : ENNReal)
+/-
+  The advantage of the attacker (i.e. the composition of A1 and A2) in
+  the semantic security game `ε` is exactly equal to the advantage of D in
+  the Diffie-Hellman game. Therefore, assumining the decisional Diffie-Hellman
+  assumption holds for the group `G`, we conclude `ε` is negligble, and
+  therefore ElGamal is, by definition, semantically secure.
+-/
+theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D ε) :
+    PKE.pke_semantic_security keygen encrypt params.A1 A2' ε := by
+  simp only [PKE.pke_semantic_security]
+  rw [SSG_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]
+  rw [← @Game2_uniform G params]
+  rw [← Game1_Game2]
+  rw [Game1_DDH1]
+  exact DDH_G
+
+
+
+end Elgamal

From f5403d8f04615cad320a9fb8a359b3e3db2c9c42 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Mon, 2 Feb 2026 21:14:54 -0800
Subject: [PATCH 03/11] wip: stray parameter changes, add commitmentscheme
 correctness

---
 VerifiedCommitments/ElgamalCommitments.lean | 73 +++++++++++----------
 1 file changed, 39 insertions(+), 34 deletions(-)

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index 6f891c5..f32da23 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -16,12 +16,12 @@ namespace DDH
 
 variable (G : Type) [Fintype G] [Group G]
           (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
-          (q : ℕ) [Fact (0 < q)] (G_card_q : Fintype.card G = q)
+          (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 {q : ℕ} : Fintype (ZMod q) := sorry
+instance : Fintype (ZMod q) := ZMod.fintype q
 
 noncomputable def Game0 : PMF (ZMod 2) :=
 do
@@ -52,8 +52,8 @@ namespace PKE
 variable {K M C O A_state: Type} [DecidableEq M]
           (setup : PMF (K × O))
           (commit : K → M → PMF (C × O))
-          (verify : K → M → C → O → ZMod 2)
-          (A1 : K → PMF (M × M × A_state))
+          (verify : K → M → C → O → ZMod 2) -- This confusing C is (G × G), but also just G?
+          (A1 : K → PMF ((M × M) × A_state))
           (A2 : C → A_state → PMF (ZMod 2))
 
 /-
@@ -63,8 +63,8 @@ variable {K M C O A_state: Type} [DecidableEq M]
 noncomputable def commit_verify (m : M) : PMF (ZMod 2) :=
 do
   let (h, _) ← setup
-  let c ← commit h m
-  pure (verify h m c.1 c.2)
+  let (c, o) ← commit h m
+  pure (verify h m c o)
 
 /-
   A public-key encryption protocol is correct if decryption undoes
@@ -79,7 +79,7 @@ def pke_correctness : Prop := ∀ (m : M), commit_verify setup commit verify m =
 noncomputable def ComputationalHidingGame : PMF (ZMod 2):=
 do
   let (h, _) ← setup
-  let (m, m', a_state) ← A1 h
+  let ((m, m'), a_state) ← A1 h
   let b ← PMF.uniformOfFintype (ZMod 2)
   let (c, _) ← commit h (if b = 0 then m else m')
   let b' ← A2 c a_state
@@ -107,17 +107,15 @@ class ElgamalParameters (G : Type) extends
   g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g
   G_card_q : Fintype.card G = q
   A_state : Type
-  A1 : G → PMF (G × G × A_state)
-  A2 : G → G → A_state → PMF (ZMod 2)
+  A1 : G → PMF ((G × G) × A_state)
+  A2 : G → G → A_state → PMF (ZMod 2) -- what deoes this need to be? Has to match what the distinguisher needs...
 
 -- Make instances available
 variable {G : Type} [params : ElgamalParameters G]
 instance : DecidableEq G := params.decidable_G
 instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
 
--- noncomputable section
-
-
+-- Should this match the A' := A from Bruce's notes?
 def A2' : G × G → params.A_state → PMF (ZMod 2) := fun (gg : G × G) => params.A2 gg.1 gg.2
 
 -- generates a public key `g^x.val`, and private key `x`
@@ -132,8 +130,8 @@ do
   let r ← PMF.uniformOfFintype (ZMod params.q)
   pure ((params.g^r.val, h^r.val * m), r)
 
--- def verify (h m c : G) (o : ZMod params.q) : ZMod 2 :=
---   (commit h m).bind (fun (x, _, _) => if x = c then 1 else 0)
+-- def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 := -- verify shouldn't run commit directly, correct? Verify is only ever passed the deterministic values - if we need to run both we have commit_verify above
+--   (commit h m).bind (fun (c', _) => if c' = c then 1 else 0)
 
 def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 :=
   if c.2 = h^o.val * m then 1 else 0
@@ -151,13 +149,7 @@ noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G :=
   -----------------------------------------------------------
 -/
 
-
-def elgamal_commitment_correctness_prop : Prop :=
-  ∀ (m : G), PKE.commit_verify setup commit verify m = pure 1
-
-
-theorem elgamal_commitment_correctness : @elgamal_commitment_correctness_prop G params := by
-  simp [elgamal_commitment_correctness_prop]
+theorem elgamal_pke_correctness : @PKE.pke_correctness G G (G × G) (ZMod params.q) setup commit verify := by
   intro m
   unfold setup commit verify PKE.commit_verify
   simp only [bind_pure_comp, Functor.map_map, bind_map_left]
@@ -168,6 +160,20 @@ theorem elgamal_commitment_correctness : @elgamal_commitment_correctness_prop G
   simp only [Function.comp_apply]
   rfl
 
+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]
+
+/-
+  -----------------------------------------------------------
+  Computational Hiding
+  -----------------------------------------------------------
+-/
+theorem computational_hiding : ∀ (ε : ENNReal), Commitment.computational_hiding (@scheme G params) ε := by
+  sorry
 
 
 /-
@@ -178,10 +184,10 @@ theorem elgamal_commitment_correctness : @elgamal_commitment_correctness_prop G
 
 noncomputable def D (gx gy gz : G) : PMF (ZMod 2) :=
 do
-  let m ← params.A1 gx
+  let ((m₀, m₁), a_state) ← params.A1 gx
   let b ← PMF.uniformOfFintype (ZMod 2)
-  let mb ← pure (if b = 0 then m.1 else m.2.1)
-  let b' ← params.A2 gy (gz * mb) m.2.2
+  let mb ← pure (if b = 0 then m₀ else m₁)
+  let b' ← params.A2 gy (gz * mb) a_state
   pure (1 + b + b')
 
 /-
@@ -189,8 +195,8 @@ do
   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 SSG_DDH0 : PKE.SSG keygen encrypt params.A1 A2' =  DDH.Game0 G params.g params.q D := by
-  simp only [PKE.SSG, DDH.Game0, bind, keygen, encrypt, D]
+theorem ComputationalHiding_DDH0 : PKE.ComputationalHidingGame setup commit params.A1 A2' =  DDH.Game0 G params.g params.q D := by
+  simp only [PKE.ComputationalHidingGame, DDH.Game0, bind, setup, commit, D]
   simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
   apply bind_skip'
   intro x
@@ -209,29 +215,28 @@ noncomputable def Game1 : PMF (ZMod 2) :=
 do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   let y ← PMF.uniformOfFintype (ZMod params.q)
-  let m ← params.A1 (params.g^x.val)
+  let ((m₀, m₁), a_state) ← params.A1 (params.g^x.val)
   let b ← PMF.uniformOfFintype (ZMod 2)
   let ζ ← (do
     let z ← PMF.uniformOfFintype (ZMod params.q)
-    let mb ← pure (if b = 0 then m.1 else m.2.1)
+    let mb ← pure (if b = 0 then m₀ else m₁)
     pure (params.g^z.val * mb))
-  let b' ← params.A2 (params.g^y.val) ζ m.2.2
+  let b' ← params.A2 (params.g^y.val) ζ a_state
   pure (1 + b + b')
 
 noncomputable def Game2 : PMF (ZMod 2) :=
 do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   let y ← PMF.uniformOfFintype (ZMod params.q)
-  let m ← params.A1 (params.g^x.val)
+  let (_, a_state) ← params.A1 (params.g^x.val)
   let b ← PMF.uniformOfFintype (ZMod 2)
   let ζ ← (do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     pure (params.g^z.val))
-  let b' ← params.A2 (params.g^y.val) ζ m.2.2
+  let b' ← params.A2 (params.g^y.val) ζ a_state
   pure (1 + b + b')
 
 
-
 /-
   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
@@ -438,9 +443,9 @@ variable (ε : ENNReal)
   therefore ElGamal is, by definition, semantically secure.
 -/
 theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D ε) :
-    PKE.pke_semantic_security keygen encrypt params.A1 A2' ε := by
+    PKE.pke_semantic_security setup commit params.A1 A2' ε := by
   simp only [PKE.pke_semantic_security]
-  rw [SSG_DDH0]
+  rw [ComputationalHiding_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]

From 7cc8e741aa005e3d96ab4ea0918ef5db35acf2cc Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Fri, 6 Feb 2026 21:14:36 -0800
Subject: [PATCH 04/11] wip: remove unncessary A2 def

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

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index f32da23..7cc803b 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -108,33 +108,25 @@ class ElgamalParameters (G : Type) extends
   G_card_q : Fintype.card G = q
   A_state : Type
   A1 : G → PMF ((G × G) × A_state)
-  A2 : G → G → A_state → PMF (ZMod 2) -- what deoes this need to be? Has to match what the distinguisher needs...
+  A2 : (G × G) → A_state → PMF (ZMod 2) -- what deoes this need to be? Has to match what the distinguisher needs...
 
 -- Make instances available
 variable {G : Type} [params : ElgamalParameters G]
 instance : DecidableEq G := params.decidable_G
 instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
 
--- Should this match the A' := A from Bruce's notes?
-def A2' : G × G → params.A_state → PMF (ZMod 2) := fun (gg : G × G) => params.A2 gg.1 gg.2
-
--- generates a public key `g^x.val`, and private key `x`
 noncomputable def setup : PMF (G × ZMod params.q) := -- Need to include x to match CommitmentScheme spec
 do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   return (params.g^x.val, x)
 
--- encrypt takes a pair (public key, message)
 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)
 
--- def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 := -- verify shouldn't run commit directly, correct? Verify is only ever passed the deterministic values - if we need to run both we have commit_verify above
---   (commit h m).bind (fun (c', _) => if c' = c then 1 else 0)
-
 def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 :=
-  if c.2 = h^o.val * m then 1 else 0
+  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 :=
 {
@@ -187,7 +179,7 @@ do
   let ((m₀, m₁), a_state) ← params.A1 gx
   let b ← PMF.uniformOfFintype (ZMod 2)
   let mb ← pure (if b = 0 then m₀ else m₁)
-  let b' ← params.A2 gy (gz * mb) a_state
+  let b' ← params.A2 ⟨gy, (gz * mb)⟩ a_state
   pure (1 + b + b')
 
 /-
@@ -195,7 +187,7 @@ do
   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 : PKE.ComputationalHidingGame setup commit params.A1 A2' =  DDH.Game0 G params.g params.q D := by
+theorem ComputationalHiding_DDH0 : PKE.ComputationalHidingGame setup commit params.A1 params.A2 =  DDH.Game0 G params.g params.q D := by
   simp only [PKE.ComputationalHidingGame, DDH.Game0, bind, setup, commit, D]
   simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
   apply bind_skip'
@@ -208,7 +200,6 @@ theorem ComputationalHiding_DDH0 : PKE.ComputationalHidingGame setup commit para
   intro b
   apply bind_skip'
   intro y
-  simp only [A2']
   rw [pow_mul params.g x.val y.val]
 
 noncomputable def Game1 : PMF (ZMod 2) :=
@@ -221,7 +212,7 @@ do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     let mb ← pure (if b = 0 then m₀ else m₁)
     pure (params.g^z.val * mb))
-  let b' ← params.A2 (params.g^y.val) ζ a_state
+  let b' ← params.A2 ⟨(params.g^y.val), ζ⟩ a_state
   pure (1 + b + b')
 
 noncomputable def Game2 : PMF (ZMod 2) :=
@@ -233,7 +224,7 @@ do
   let ζ ← (do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     pure (params.g^z.val))
-  let b' ← params.A2 (params.g^y.val) ζ a_state
+  let b' ← params.A2 ⟨(params.g^y.val), ζ⟩ a_state
   pure (1 + b + b')
 
 
@@ -443,7 +434,7 @@ variable (ε : ENNReal)
   therefore ElGamal is, by definition, semantically secure.
 -/
 theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D ε) :
-    PKE.pke_semantic_security setup commit params.A1 A2' ε := by
+    PKE.pke_semantic_security setup commit params.A1 params.A2 ε := by
   simp only [PKE.pke_semantic_security]
   rw [ComputationalHiding_DDH0]
   have h : ((PMF.uniformOfFintype (ZMod 2)) 1) = 1/2 := by

From 5b2581c84fe0856b462d27b67fde234cbad9d974 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Fri, 6 Feb 2026 21:20:23 -0800
Subject: [PATCH 05/11] wip: change commitmentscheme defs to multiparameter
 projections

---
 VerifiedCommitments/CommitmentScheme.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean
index 6a0ac0e..cd51c8f 100644
--- a/VerifiedCommitments/CommitmentScheme.lean
+++ b/VerifiedCommitments/CommitmentScheme.lean
@@ -42,9 +42,9 @@ def perfect_binding (scheme : CommitmentScheme M C O K) : Prop :=
 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.1) (fun guess =>
-      if scheme.verify h.1 guess.m guess.c guess.o = 1 ∧ scheme.verify h.1 guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0 ))
+  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 ≤ ε
@@ -52,8 +52,8 @@ def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (
 
 -- 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.1 m) (fun commit => pure commit.1))
+PMF.bind scheme.setup (fun (h, _) =>
+  PMF.bind (scheme.commit h m) (fun (c, _) => pure c))
 
 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
@@ -61,8 +61,8 @@ def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop :=
 -- Computational hiding game
 def comp_hiding_game (scheme : CommitmentScheme M C O K)
   (A : K → C → PMF (ZMod 2)) (m : M) : PMF (ZMod 2) :=
-  PMF.bind scheme.setup (fun h =>
-    PMF.bind (scheme.commit h.1 m) (fun commit => A h.1 commit.1))
+  PMF.bind scheme.setup (fun (h, _) =>
+    PMF.bind (scheme.commit h m) (fun commit => A h commit.1))
 
 def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
   ∀ (A : K → C → PMF (ZMod 2)) (m₀ m₁ : M),

From cf84db2e5b9f65b3e2deea8790db91f044929bbd Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Fri, 6 Feb 2026 21:21:31 -0800
Subject: [PATCH 06/11] wip: missed one projection

---
 VerifiedCommitments/CommitmentScheme.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean
index cd51c8f..fc6b9a0 100644
--- a/VerifiedCommitments/CommitmentScheme.lean
+++ b/VerifiedCommitments/CommitmentScheme.lean
@@ -62,7 +62,7 @@ def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop :=
 def comp_hiding_game (scheme : CommitmentScheme M C O K)
   (A : K → C → PMF (ZMod 2)) (m : M) : PMF (ZMod 2) :=
   PMF.bind scheme.setup (fun (h, _) =>
-    PMF.bind (scheme.commit h m) (fun commit => A h commit.1))
+    PMF.bind (scheme.commit h m) (fun (c, _) => A h c))
 
 def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
   ∀ (A : K → C → PMF (ZMod 2)) (m₀ m₁ : M),

From b6255091b19d131c2521cba2be744fbfa8c68091 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Fri, 6 Feb 2026 21:25:13 -0800
Subject: [PATCH 07/11] wip: change computational_hiding to use max

---
 VerifiedCommitments/CommitmentScheme.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean
index fc6b9a0..81b30f4 100644
--- a/VerifiedCommitments/CommitmentScheme.lean
+++ b/VerifiedCommitments/CommitmentScheme.lean
@@ -66,8 +66,8 @@ def comp_hiding_game (scheme : CommitmentScheme M C O K)
 
 def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
   ∀ (A : K → C → PMF (ZMod 2)) (m₀ m₁ : M),
-  comp_hiding_game scheme A m₀ 1 - comp_hiding_game scheme A m₁ 1 ≤ ε ||
-  comp_hiding_game scheme A m₁ 1 - comp_hiding_game scheme A m₀ 1 ≤ ε
+  max (comp_hiding_game scheme A m₀ 1 - comp_hiding_game scheme A m₁ 1)
+      (comp_hiding_game scheme A m₁ 1 - comp_hiding_game scheme A m₀ 1) ≤ ε
 
 end
 

From d82fafc7df03e8437a6c5f0e9c02eb4152c7468b Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Sat, 7 Feb 2026 15:22:58 -0800
Subject: [PATCH 08/11] wip: refactor computational hiding game to match cpa
 approach; refactored adversary into structure

---
 VerifiedCommitments/CommitmentScheme.lean   | 21 +++++----
 VerifiedCommitments/ElgamalCommitments.lean | 47 +++++++++------------
 2 files changed, 34 insertions(+), 34 deletions(-)

diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean
index 81b30f4..046ae87 100644
--- a/VerifiedCommitments/CommitmentScheme.lean
+++ b/VerifiedCommitments/CommitmentScheme.lean
@@ -1,6 +1,7 @@
 import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Monad
 import Mathlib.Probability.ProbabilityMassFunction.Constructions
+import Mathlib.Probability.Distributions.Uniform
 import Mathlib.Data.ZMod.Defs
 
 structure CommitmentScheme (M C O K : Type) where
@@ -15,14 +16,17 @@ structure BindingGuess (M C O : Type) where
   o : O
   o': O
 
+structure TwoStageAdversary (K M C : Type) where
+  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)
 
-variable (h : K)
-
 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
@@ -59,15 +63,16 @@ 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 : K → C → PMF (ZMod 2)) (m : M) : PMF (ZMod 2) :=
+def comp_hiding_game (scheme : CommitmentScheme M C O K) (A : TwoStageAdversary K M C) :=
   PMF.bind scheme.setup (fun (h, _) =>
-    PMF.bind (scheme.commit h m) (fun (c, _) => A h c))
+    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 : K → C → PMF (ZMod 2)) (m₀ m₁ : M),
-  max (comp_hiding_game scheme A m₀ 1 - comp_hiding_game scheme A m₁ 1)
-      (comp_hiding_game scheme A m₁ 1 - comp_hiding_game scheme A m₀ 1) ≤ ε
+  ∀ (A : TwoStageAdversary K M C), comp_hiding_game scheme A 1 - 1/2 ≤ ε
 
 end
 
diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index 7cc803b..2bb85e8 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -52,9 +52,8 @@ namespace PKE
 variable {K M C O A_state: Type} [DecidableEq M]
           (setup : PMF (K × O))
           (commit : K → M → PMF (C × O))
-          (verify : K → M → C → O → ZMod 2) -- This confusing C is (G × G), but also just G?
-          (A1 : K → PMF ((M × M) × A_state))
-          (A2 : C → A_state → PMF (ZMod 2))
+          (verify : K → M → C → O → ZMod 2)
+          (adversary : TwoStageAdversary K M C)
 
 /-
   Executes the a public-key protocol defined by keygen,
@@ -79,17 +78,17 @@ def pke_correctness : Prop := ∀ (m : M), commit_verify setup commit verify m =
 noncomputable def ComputationalHidingGame : PMF (ZMod 2):=
 do
   let (h, _) ← setup
-  let ((m, m'), a_state) ← A1 h
+  let ((m, m'), a_state) ← adversary.stage1 h
   let b ← PMF.uniformOfFintype (ZMod 2)
   let (c, _) ← commit h (if b = 0 then m else m')
-  let b' ← A2 c a_state
+  let b' ← adversary.stage2 c a_state
   pure (1 + b + b')
 
 
 -- SSG(A) denotes the event that A wins the semantic security game
 --local notation `Pr[SSG(A)]` := (SSG keygen encrypt A1 A2 1 : ℝ)
 
-def pke_semantic_security (ε : ENNReal) : Prop :=  (ComputationalHidingGame setup commit A1 A2 1) - 1/2 ≤ ε
+def pke_semantic_security (ε : ENNReal) : Prop :=  (ComputationalHidingGame setup commit adversary 1) - 1/2 ≤ ε
 
 end PKE
 
@@ -106,9 +105,7 @@ class ElgamalParameters (G : Type) extends
   card_eq : Fintype.card G = q
   g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g
   G_card_q : Fintype.card G = q
-  A_state : Type
-  A1 : G → PMF ((G × G) × A_state)
-  A2 : (G × G) → A_state → PMF (ZMod 2) -- what deoes this need to be? Has to match what the distinguisher needs...
+  adversary : TwoStageAdversary G G (G × G)
 
 -- Make instances available
 variable {G : Type} [params : ElgamalParameters G]
@@ -159,14 +156,6 @@ theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G param
   unfold commit verify
   simp only [bind_pure_comp, Functor.map, PMF.bind_bind, Function.comp_apply, PMF.pure_bind, ↓reduceIte, PMF.bind_const]
 
-/-
-  -----------------------------------------------------------
-  Computational Hiding
-  -----------------------------------------------------------
--/
-theorem computational_hiding : ∀ (ε : ENNReal), Commitment.computational_hiding (@scheme G params) ε := by
-  sorry
-
 
 /-
   -----------------------------------------------------------
@@ -176,10 +165,10 @@ theorem computational_hiding : ∀ (ε : ENNReal), Commitment.computational_hidi
 
 noncomputable def D (gx gy gz : G) : PMF (ZMod 2) :=
 do
-  let ((m₀, m₁), a_state) ← params.A1 gx
+  let ((m₀, m₁), a_state) ← params.adversary.stage1 gx
   let b ← PMF.uniformOfFintype (ZMod 2)
   let mb ← pure (if b = 0 then m₀ else m₁)
-  let b' ← params.A2 ⟨gy, (gz * mb)⟩ a_state
+  let b' ← params.adversary.stage2 ⟨gy, (gz * mb)⟩ a_state
   pure (1 + b + b')
 
 /-
@@ -187,7 +176,7 @@ do
   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 : PKE.ComputationalHidingGame setup commit params.A1 params.A2 =  DDH.Game0 G params.g params.q D := by
+theorem ComputationalHiding_DDH0 : PKE.ComputationalHidingGame setup commit params.adversary =  DDH.Game0 G params.g params.q D := by
   simp only [PKE.ComputationalHidingGame, DDH.Game0, bind, setup, commit, D]
   simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
   apply bind_skip'
@@ -206,25 +195,25 @@ noncomputable def Game1 : PMF (ZMod 2) :=
 do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   let y ← PMF.uniformOfFintype (ZMod params.q)
-  let ((m₀, m₁), a_state) ← params.A1 (params.g^x.val)
+  let ((m₀, m₁), a_state) ← params.adversary.stage1 (params.g^x.val)
   let b ← PMF.uniformOfFintype (ZMod 2)
   let ζ ← (do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     let mb ← pure (if b = 0 then m₀ else m₁)
     pure (params.g^z.val * mb))
-  let b' ← params.A2 ⟨(params.g^y.val), ζ⟩ a_state
+  let b' ← params.adversary.stage2 ⟨(params.g^y.val), ζ⟩ a_state
   pure (1 + b + b')
 
 noncomputable def Game2 : PMF (ZMod 2) :=
 do
   let x ← PMF.uniformOfFintype (ZMod params.q)
   let y ← PMF.uniformOfFintype (ZMod params.q)
-  let (_, a_state) ← params.A1 (params.g^x.val)
+  let (_, a_state) ← params.adversary.stage1 (params.g^x.val)
   let b ← PMF.uniformOfFintype (ZMod 2)
   let ζ ← (do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     pure (params.g^z.val))
-  let b' ← params.A2 ⟨(params.g^y.val), ζ⟩ a_state
+  let b' ← params.adversary.stage2 ⟨(params.g^y.val), ζ⟩ a_state
   pure (1 + b + b')
 
 
@@ -239,7 +228,7 @@ theorem Game1_DDH1 : @Game1 G params = DDH.Game1 G params.g params.q D := by
   intro x
   apply bind_skip'
   intro y
-  simp_rw [PMF.bind_bind (params.A1 _)]
+  simp_rw [PMF.bind_bind (params.adversary.stage1 _)]
   conv_rhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
   apply bind_skip'
   intro m
@@ -434,7 +423,7 @@ variable (ε : ENNReal)
   therefore ElGamal is, by definition, semantically secure.
 -/
 theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D ε) :
-    PKE.pke_semantic_security setup commit params.A1 params.A2 ε := by
+    PKE.pke_semantic_security setup commit params.adversary ε := by
   simp only [PKE.pke_semantic_security]
   rw [ComputationalHiding_DDH0]
   have h : ((PMF.uniformOfFintype (ZMod 2)) 1) = 1/2 := by
@@ -447,4 +436,10 @@ theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D
 
 
 
+theorem computational_hiding_from_ddh
+    (DDH_assumption : ∀ (D : G → G → G → PMF (ZMod 2)), ∃ ε, DDH.Assumption G params.g params.q D ε) :
+    ∃ ε, Commitment.computational_hiding (@scheme G params) ε := by
+
+  sorry
+
 end Elgamal

From 0dc4b4083842b6ece7ae02ac4c0f125731daf2d1 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Sat, 7 Feb 2026 16:22:04 -0800
Subject: [PATCH 09/11] wip: employ Commitments.comp_hiding_game, rather than
 bespoke version in Elgamal - update lemmas

---
 VerifiedCommitments/ElgamalCommitments.lean | 42 +++++++++++++--------
 1 file changed, 27 insertions(+), 15 deletions(-)

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index 2bb85e8..e03f8d3 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -75,20 +75,20 @@ def pke_correctness : Prop := ∀ (m : M), commit_verify setup commit verify m =
   The semantic security game.
   Returns 1 if the attacker A2 guesses the correct bit
 -/
-noncomputable def ComputationalHidingGame : PMF (ZMod 2):=
-do
-  let (h, _) ← setup
-  let ((m, m'), a_state) ← adversary.stage1 h
-  let b ← PMF.uniformOfFintype (ZMod 2)
-  let (c, _) ← commit h (if b = 0 then m else m')
-  let b' ← adversary.stage2 c a_state
-  pure (1 + b + b')
+-- noncomputable def ComputationalHidingGame : PMF (ZMod 2):=
+-- do
+--   let (h, _) ← setup
+--   let ((m, m'), a_state) ← adversary.stage1 h
+--   let b ← PMF.uniformOfFintype (ZMod 2)
+--   let (c, _) ← commit h (if b = 0 then m else m')
+--   let b' ← adversary.stage2 c a_state
+--   pure (1 + b + b')
 
 
 -- SSG(A) denotes the event that A wins the semantic security game
 --local notation `Pr[SSG(A)]` := (SSG keygen encrypt A1 A2 1 : ℝ)
 
-def pke_semantic_security (ε : ENNReal) : Prop :=  (ComputationalHidingGame setup commit adversary 1) - 1/2 ≤ ε
+-- def pke_semantic_security (ε : ENNReal) : Prop :=  (ComputationalHidingGame setup commit adversary 1) - 1/2 ≤ ε
 
 end PKE
 
@@ -132,6 +132,9 @@ noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G :=
   verify := verify
 }
 
+def pke_semantic_security' (ε : ENNReal) : Prop := (Commitment.comp_hiding_game scheme params.adversary 1) - 1/2 ≤ ε
+
+
 /-
   -----------------------------------------------------------
   Proof of correctness of ElGamal
@@ -176,8 +179,8 @@ do
   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 : PKE.ComputationalHidingGame setup commit params.adversary =  DDH.Game0 G params.g params.q D := by
-  simp only [PKE.ComputationalHidingGame, DDH.Game0, bind, setup, commit, D]
+theorem ComputationalHiding_DDH0 : Commitment.comp_hiding_game scheme params.adversary =  DDH.Game0 G params.g params.q D := by
+  simp only [Commitment.comp_hiding_game, DDH.Game0, bind, scheme, setup, commit, D]
   simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
   apply bind_skip'
   intro x
@@ -422,9 +425,11 @@ variable (ε : ENNReal)
   assumption holds for the group `G`, we conclude `ε` is negligble, and
   therefore ElGamal is, by definition, semantically secure.
 -/
+
+#check pke_semantic_security'
 theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D ε) :
-    PKE.pke_semantic_security setup commit params.adversary ε := by
-  simp only [PKE.pke_semantic_security]
+    @pke_semantic_security' G params ε := by
+  simp only [pke_semantic_security']
   rw [ComputationalHiding_DDH0]
   have h : ((PMF.uniformOfFintype (ZMod 2)) 1) = 1/2 := by
     simp only [PMF.uniformOfFintype_apply, ZMod.card, Nat.cast_ofNat, one_div]
@@ -434,11 +439,18 @@ theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D
   rw [Game1_DDH1]
   exact DDH_G
 
+-- lemma semantic_security_eq_computational_hiding : ∀ (ε : ENNReal),
+--     PKE.pke_semantic_security setup commit params.adversary ε = Commitment.computational_hiding (@scheme G params) ε := by
+--   intro ε
+--   unfold PKE.pke_semantic_security Commitment.computational_hiding
+
 
+include ε
 
 theorem computational_hiding_from_ddh
-    (DDH_assumption : ∀ (D : G → G → G → PMF (ZMod 2)), ∃ ε, DDH.Assumption G params.g params.q D ε) :
-    ∃ ε, Commitment.computational_hiding (@scheme G params) ε := by
+    (DDH_assumption : ∀ (D : G → G → G → PMF (ZMod 2)), ∃ ε', DDH.Assumption G params.g params.q D ε') :
+    ∃ ε', Commitment.computational_hiding (@scheme G params) ε' := by
+  use ε
 
   sorry
 

From aad79791e10ab11af9517265226f2be80cc888e3 Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Sat, 7 Feb 2026 19:51:00 -0800
Subject: [PATCH 10/11] wip: add D_from_adversary

---
 VerifiedCommitments/ElgamalCommitments.lean | 38 +++++++++++++++------
 1 file changed, 27 insertions(+), 11 deletions(-)

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index e03f8d3..114867f 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -132,7 +132,7 @@ noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G :=
   verify := verify
 }
 
-def pke_semantic_security' (ε : ENNReal) : Prop := (Commitment.comp_hiding_game scheme params.adversary 1) - 1/2 ≤ ε
+def pke_semantic_security' (ε : ENNReal) : Prop := (Commitment.comp_hiding_game scheme params.adversary) 1 - 1/2 ≤ ε
 
 
 /-
@@ -174,6 +174,14 @@ do
   let b' ← params.adversary.stage2 ⟨gy, (gz * mb)⟩ a_state
   pure (1 + b + b')
 
+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),
@@ -426,7 +434,7 @@ variable (ε : ENNReal)
   therefore ElGamal is, by definition, semantically secure.
 -/
 
-#check pke_semantic_security'
+
 theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D ε) :
     @pke_semantic_security' G params ε := by
   simp only [pke_semantic_security']
@@ -439,19 +447,27 @@ theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D
   rw [Game1_DDH1]
   exact DDH_G
 
--- lemma semantic_security_eq_computational_hiding : ∀ (ε : ENNReal),
---     PKE.pke_semantic_security setup commit params.adversary ε = Commitment.computational_hiding (@scheme G params) ε := by
---   intro ε
---   unfold PKE.pke_semantic_security Commitment.computational_hiding
 
 
-include ε
+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) ε) :
+    Commitment.comp_hiding_game scheme A 1 - 1/2 ≤ ε := by
+  simp only [Commitment.comp_hiding_game]
+  -- unfold Commitment.comp_hiding_game
+  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, ZMod.card, Nat.cast_ofNat, tsum_fintype,
+    one_div, tsub_le_iff_right]
 
-theorem computational_hiding_from_ddh
-    (DDH_assumption : ∀ (D : G → G → G → PMF (ZMod 2)), ∃ ε', DDH.Assumption G params.g params.q D ε') :
-    ∃ ε', Commitment.computational_hiding (@scheme G params) ε' := by
-  use ε
+  sorry
 
+theorem computational_hiding_from_ddh (ε : ENNReal)
+    (DDH_hard : ∀ (D : G → G → G → PMF (ZMod 2)), DDH.Assumption G params.g params.q D ε) :
+    Commitment.computational_hiding (@scheme G params) ε := by
+  unfold Commitment.computational_hiding
+  intro hA
+  apply hiding_from_ddh_single_adversary
   sorry
+  -- exact DDH_hard D
+
 
 end Elgamal

From dba6b2d6d368ee4c3330fe55a75314df4daba55b Mon Sep 17 00:00:00 2001
From: ashandoak <ash.blacquiere@pm.me>
Date: Sat, 7 Feb 2026 20:30:24 -0800
Subject: [PATCH 11/11] feat: computational hiding complete

---
 VerifiedCommitments/ElgamalCommitments.lean | 130 ++++----------------
 1 file changed, 25 insertions(+), 105 deletions(-)

diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
index 114867f..24fb2d8 100644
--- a/VerifiedCommitments/ElgamalCommitments.lean
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -48,50 +48,6 @@ def Assumption (ε : ENNReal) : Prop := (Game0 G g q D 1) - (Game1 G g q D 1) 
 
 end DDH
 
-namespace PKE
-variable {K M C O A_state: Type} [DecidableEq M]
-          (setup : PMF (K × O))
-          (commit : K → M → PMF (C × O))
-          (verify : K → M → C → O → ZMod 2)
-          (adversary : TwoStageAdversary K M C)
-
-/-
-  Executes the a public-key protocol defined by keygen,
-  encrypt, and decrypt
--/
-noncomputable def commit_verify (m : M) : PMF (ZMod 2) :=
-do
-  let (h, _) ← setup
-  let (c, o) ← commit h m
-  pure (verify h m c o)
-
-/-
-  A public-key encryption protocol is correct if decryption undoes
-  encryption with probability 1
--/
-def pke_correctness : Prop := ∀ (m : M), commit_verify setup commit verify m = pure 1
-
-/-
-  The semantic security game.
-  Returns 1 if the attacker A2 guesses the correct bit
--/
--- noncomputable def ComputationalHidingGame : PMF (ZMod 2):=
--- do
---   let (h, _) ← setup
---   let ((m, m'), a_state) ← adversary.stage1 h
---   let b ← PMF.uniformOfFintype (ZMod 2)
---   let (c, _) ← commit h (if b = 0 then m else m')
---   let b' ← adversary.stage2 c a_state
---   pure (1 + b + b')
-
-
--- SSG(A) denotes the event that A wins the semantic security game
---local notation `Pr[SSG(A)]` := (SSG keygen encrypt A1 A2 1 : ℝ)
-
--- def pke_semantic_security (ε : ENNReal) : Prop :=  (ComputationalHidingGame setup commit adversary 1) - 1/2 ≤ ε
-
-end PKE
-
 namespace Elgamal
 
 class ElgamalParameters (G : Type) extends
@@ -105,7 +61,6 @@ class ElgamalParameters (G : Type) extends
   card_eq : Fintype.card G = q
   g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g
   G_card_q : Fintype.card G = q
-  adversary : TwoStageAdversary G G (G × G)
 
 -- Make instances available
 variable {G : Type} [params : ElgamalParameters G]
@@ -131,27 +86,12 @@ noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G :=
   commit := commit,
   verify := verify
 }
-
-def pke_semantic_security' (ε : ENNReal) : Prop := (Commitment.comp_hiding_game scheme params.adversary) 1 - 1/2 ≤ ε
-
-
 /-
   -----------------------------------------------------------
   Proof of correctness of ElGamal
   -----------------------------------------------------------
 -/
 
-theorem elgamal_pke_correctness : @PKE.pke_correctness G G (G × G) (ZMod params.q) setup commit verify := by
-  intro m
-  unfold setup commit verify PKE.commit_verify
-  simp only [bind_pure_comp, Functor.map_map, bind_map_left]
-  apply bind_skip_const'
-  intro x
-  apply bind_skip_const'
-  intro y
-  simp only [Function.comp_apply]
-  rfl
-
 theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G params) := by
   intro h m
   show PMF.bind (scheme.commit h m) _ = _
@@ -166,14 +106,6 @@ theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G param
   -----------------------------------------------------------
 -/
 
-noncomputable def D (gx gy gz : G) : PMF (ZMod 2) :=
-do
-  let ((m₀, m₁), a_state) ← params.adversary.stage1 gx
-  let b ← PMF.uniformOfFintype (ZMod 2)
-  let mb ← pure (if b = 0 then m₀ else m₁)
-  let b' ← params.adversary.stage2 ⟨gy, (gz * mb)⟩ a_state
-  pure (1 + b + b')
-
 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
@@ -187,8 +119,8 @@ noncomputable def D_from_adversary (A : TwoStageAdversary G G (G × G)) : G →
   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 : Commitment.comp_hiding_game scheme params.adversary =  DDH.Game0 G params.g params.q D := by
-  simp only [Commitment.comp_hiding_game, DDH.Game0, bind, scheme, setup, commit, D]
+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
@@ -202,29 +134,29 @@ theorem ComputationalHiding_DDH0 : Commitment.comp_hiding_game scheme params.adv
   intro y
   rw [pow_mul params.g x.val y.val]
 
-noncomputable def Game1 : PMF (ZMod 2) :=
+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) ← params.adversary.stage1 (params.g^x.val)
+  let ((m₀, m₁), a_state) ← A.stage1 (params.g^x.val)
   let b ← PMF.uniformOfFintype (ZMod 2)
   let ζ ← (do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     let mb ← pure (if b = 0 then m₀ else m₁)
     pure (params.g^z.val * mb))
-  let b' ← params.adversary.stage2 ⟨(params.g^y.val), ζ⟩ a_state
+  let b' ← A.stage2 ⟨(params.g^y.val), ζ⟩ a_state
   pure (1 + b + b')
 
-noncomputable def Game2 : PMF (ZMod 2) :=
+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) ← params.adversary.stage1 (params.g^x.val)
+  let (_, a_state) ← A.stage1 (params.g^x.val)
   let b ← PMF.uniformOfFintype (ZMod 2)
   let ζ ← (do
     let z ← PMF.uniformOfFintype (ZMod params.q)
     pure (params.g^z.val))
-  let b' ← params.adversary.stage2 ⟨(params.g^y.val), ζ⟩ a_state
+  let b' ← A.stage2 ⟨(params.g^y.val), ζ⟩ a_state
   pure (1 + b + b')
 
 
@@ -233,29 +165,29 @@ do
   winning Game1 (i.e. guessing the correct bit) is equal to the
   probability of D winning the game DDH1.
 -/
-theorem Game1_DDH1 : @Game1 G params = DDH.Game1 G params.g params.q D := by
-  simp only [DDH.Game1, Game1, bind, D]
+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]
+  simp only [PMF.bind_bind, mul_ite]
   apply bind_skip'
   intro x
   apply bind_skip'
   intro y
-  simp_rw [PMF.bind_bind (params.adversary.stage1 _)]
+  -- simp_rw [PMF.bind_bind (A.stage1 _)]
   conv_rhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
   apply bind_skip'
   intro m
-  simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
+  -- simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
   conv_lhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod 2))]
   apply bind_skip'
   intro z
-  conv_rhs => rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod 2))]
+  -- conv_rhs => rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod 2))]
   apply bind_skip'
   intro b
-  simp_rw [PMF.bind_bind]
-  apply bind_skip'
-  intro mb
+  -- simp_rw [PMF.bind_bind]
+  -- apply bind_skip'
+  -- intro mb
   simp [pure]
 
-
 lemma exp_bij : Function.Bijective (fun (z : ZMod params.q) => params.g ^ z.val) := by
   apply (Fintype.bijective_iff_surjective_and_card _).mpr
   simp [params.card_eq]
@@ -340,7 +272,7 @@ lemma G1_G2_lemma3 (m : PMF G) :
   winning Game1 (i.e. guessing the correct bit) is equal to the
   probability of the attacker winning Game2.
 -/
-theorem Game1_Game2 : @Game1 G params = @Game2 G params := by
+theorem Game1_Game2 (A : TwoStageAdversary G G (G × G)) : @Game1 G params A = @Game2 G params A := by
   simp only [Game1, Game2]
   apply bind_skip'
   intro x
@@ -406,7 +338,7 @@ lemma G2_uniform_lemma (b' : ZMod 2) : (PMF.uniformOfFintype (ZMod 2)).bind (fun
   The probability of the attacker (i.e. the composition of A1 and A2)
   winning Game2 (i.e. guessing the correct bit) is equal to a coin flip.
 -/
-theorem Game2_uniform : @Game2 G params = PMF.uniformOfFintype (ZMod 2) := by
+theorem Game2_uniform (A : TwoStageAdversary G G (G × G)) : @Game2 G params A = PMF.uniformOfFintype (ZMod 2) := by
   simp [Game2, bind]
   apply bind_skip_const'
   intro x
@@ -435,9 +367,10 @@ variable (ε : ENNReal)
 -/
 
 
-theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D ε) :
-    @pke_semantic_security' G params ε := by
-  simp only [pke_semantic_security']
+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) ε) :
+    Commitment.comp_hiding_game scheme A 1 - 1/2 ≤ ε := by
   rw [ComputationalHiding_DDH0]
   have h : ((PMF.uniformOfFintype (ZMod 2)) 1) = 1/2 := by
     simp only [PMF.uniformOfFintype_apply, ZMod.card, Nat.cast_ofNat, one_div]
@@ -445,20 +378,8 @@ theorem elgamal_semantic_security (DDH_G : DDH.Assumption G params.g params.q D
   rw [← @Game2_uniform G params]
   rw [← Game1_Game2]
   rw [Game1_DDH1]
-  exact DDH_G
-
-
-
-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) ε) :
-    Commitment.comp_hiding_game scheme A 1 - 1/2 ≤ ε := by
-  simp only [Commitment.comp_hiding_game]
-  -- unfold Commitment.comp_hiding_game
-  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, ZMod.card, Nat.cast_ofNat, tsum_fintype,
-    one_div, tsub_le_iff_right]
+  exact le_of_eq_of_le rfl DDH_assumption
 
-  sorry
 
 theorem computational_hiding_from_ddh (ε : ENNReal)
     (DDH_hard : ∀ (D : G → G → G → PMF (ZMod 2)), DDH.Assumption G params.g params.q D ε) :
@@ -466,8 +387,7 @@ theorem computational_hiding_from_ddh (ε : ENNReal)
   unfold Commitment.computational_hiding
   intro hA
   apply hiding_from_ddh_single_adversary
-  sorry
-  -- exact DDH_hard D
+  exact DDH_hard (D_from_adversary hA)
 
 
 end Elgamal