From 18356e2e54611e069a5ac9b19d2df361e8d4ec7b Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 12:28:59 -0800 Subject: [PATCH 01/23] refactor: modify statements for clarity --- VerifiedCommitments/CommitmentScheme.lean | 2 +- VerifiedCommitments/Pedersen.lean | 36 +++++++++++++---------- 2 files changed, 22 insertions(+), 16 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 046ae87..28a9e00 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -29,7 +29,7 @@ variable (scheme : CommitmentScheme M C O 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 + (scheme.commit h m).bind (fun (commit, opening_val) => pure <| scheme.verify h m commit opening_val) = pure 1 -- Perfect binding def perfect_binding (scheme : CommitmentScheme M C O K) : Prop := diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 8cd41b9..e8bfe0c 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -50,20 +50,23 @@ lemma ordg_eq_q : orderOf params.g = params.q := by ======================================== -/ 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, +noncomputable def scheme : + CommitmentScheme (ZMod params.q) G (ZMod params.q) G where + setup := setup + commit := commit verify := verify - } theorem pedersen_correctness : Commitment.correctness (@scheme G params) := by @@ -130,18 +133,21 @@ noncomputable def generate_a : PMF (ZModMult params.q) := PMF.uniformOfFintype ( 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 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 => + PMF.bind (A h) fun guess => if guess.o ≠ guess.o' then - return ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹) + return (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ else - PMF.uniformOfFintype (ZMod params.q)) + PMF.uniformOfFintype (ZMod params.q) end DLog From 4624e6be8d05993b4ee7ed28a4f5e926fcf1ac3f Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 12:29:38 -0800 Subject: [PATCH 02/23] refactor: modify name of public parameters class --- VerifiedCommitments/Pedersen.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index e8bfe0c..8a69421 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,7 +25,7 @@ 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⟩ From 6b288b52ef4f626766b6a7f80cefb616360f9422 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 12:30:14 -0800 Subject: [PATCH 03/23] refactor: change order of core lemmas and defs --- VerifiedCommitments/Pedersen.lean | 39 ++++++++++++++++--------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 8a69421..f3788d9 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -29,22 +29,6 @@ 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 ======================================== -/ @@ -68,6 +52,9 @@ noncomputable def scheme : commit := commit verify := verify +/- ======================================== + CORRECTNESS + ======================================== -/ theorem pedersen_correctness : Commitment.correctness (@scheme G params) := by unfold Commitment.correctness @@ -124,9 +111,6 @@ 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 ======================================== -/ @@ -151,6 +135,23 @@ noncomputable def constructDlogAdversary 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 ======================================== -/ From 12dfdc4c2c8095a3ef7730100560c0ec46752cb4 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 12:31:21 -0800 Subject: [PATCH 04/23] refactor: change name of dlogadv def --- VerifiedCommitments/Pedersen.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index f3788d9..0c62e4c 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -124,7 +124,7 @@ noncomputable def DLogExperiment (A h).bind fun x' => pure <| if params.g^x'.val = params.g^(x).val then 1 else 0 -noncomputable def constructDlogAdversary +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 => @@ -338,8 +338,8 @@ lemma binding_implies_dlog (a : ZMod params.q) (guess : BindingGuess (ZMod param lemma binding_as_hard_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] From 8fb6a51bc657a8c0d5c81525578411855e259877 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 12:32:27 -0800 Subject: [PATCH 05/23] refactor: modify lemma to mathlib style; update associated proof --- VerifiedCommitments/Pedersen.lean | 32 +++++++++++++++---------------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 0c62e4c..be2b856 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -292,17 +292,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 binding_implies_dlog + (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] @@ -320,7 +323,7 @@ lemma binding_implies_dlog (a : ZMod params.q) (guess : BindingGuess (ZMod param 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) + 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) @@ -397,13 +400,8 @@ lemma binding_as_hard_dlog have h_o_ne : guess.o ≠ guess.o' := h₂ 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 [binding_implies_dlog] -- The RHS is a sum over a single-element distribution (pure x') -- The sum includes the term for x = x', which equals 1 From b413d21125839a3e4f87791b7f17f01d14b36fa7 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 12:32:53 -0800 Subject: [PATCH 06/23] fix: missed adding dlogadv name change --- VerifiedCommitments/Pedersen.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index be2b856..12ea551 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -458,7 +458,7 @@ theorem computational_binding : (∀ (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_as_hard_dlog A) (A' (constructDLogAdversary A)) end Binding From 2f5ef5abe7541063294ff71b3f8cd03249a0d2bf Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 13:18:59 -0800 Subject: [PATCH 07/23] refactor: rename binding lemmas for clarity --- VerifiedCommitments/Pedersen.lean | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 12ea551..70ea4cb 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -50,7 +50,7 @@ noncomputable def scheme : CommitmentScheme (ZMod params.q) G (ZMod params.q) G where setup := setup commit := commit - verify := verify + verify := verify /- ======================================== CORRECTNESS @@ -125,12 +125,12 @@ noncomputable def DLogExperiment 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) := + (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 + if guess.o ≠ guess.o' then return (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ - else + else PMF.uniformOfFintype (ZMod params.q) end DLog @@ -292,7 +292,7 @@ end Hiding section Binding -lemma binding_implies_dlog +lemma gpow_eq_of_two_valid_openings (a : ZMod params.q) (guess : BindingGuess (ZMod params.q) G (ZMod params.q)) (h₁ : @@ -339,9 +339,10 @@ lemma binding_implies_dlog 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 + 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] @@ -396,12 +397,12 @@ 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 + -- This is the main case where we use gpow_eq_of_two_valid_openings have h_o_ne : guess.o ≠ guess.o' := h₂ let x' := (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ have h_dlog : params.g^x'.val = params.g^a.val := by - grind only [binding_implies_dlog] + 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 @@ -458,7 +459,7 @@ theorem computational_binding : (∀ (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 From 8db1669c866c721f5537c66cca5a71db16ae1384 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 21:30:21 -0800 Subject: [PATCH 08/23] refactor: remove unnecessary hypothesis --- VerifiedCommitments/Pedersen.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 70ea4cb..c7a6c00 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -398,7 +398,6 @@ lemma binding_reduction_to_dlog · -- Case 2: Binding collision (h₁) AND o ≠ o' (¬h₂) -- This is the main case where we use gpow_eq_of_two_valid_openings - have h_o_ne : guess.o ≠ guess.o' := h₂ let x' := (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ have h_dlog : params.g^x'.val = params.g^a.val := by From 9038e832e663e9ba0841e54d4ac990a7728c26bb Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sun, 22 Feb 2026 21:30:50 -0800 Subject: [PATCH 09/23] refactor: remove unnecessary parentheses --- VerifiedCommitments/Pedersen.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index c7a6c00..efe44c0 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -455,8 +455,8 @@ lemma binding_reduction_to_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_reduction_to_dlog A) (A' (constructDLogAdversary A)) From 7f688973dad0174ac04dc14e1ca00c1277cb4f19 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Mon, 23 Feb 2026 17:39:05 -0800 Subject: [PATCH 10/23] refactor: clean up lemma statements and have blocks --- VerifiedCommitments/Pedersen.lean | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index efe44c0..b761517 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -158,7 +158,8 @@ noncomputable def generate_a : PMF (ZModMult params.q) := PMF.uniformOfFintype ( 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] @@ -215,29 +216,29 @@ 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 + (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 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 + have h_eq : generate_a.bind fun (a : ZModMult params.q) => + PMF.uniformOfFintype (ZMod params.q)|>.bind (fun r => + PMF.pure (params.g^m.val * (params.g^(val a).val)^r.val)) = + generate_a.bind fun (a : ZModMult params.q) => + PMF.uniformOfFintype (ZMod params.q)|>.map (expEquiv a m) := by apply bind_skip' intro a ext x From 1bbbce54f1747d11bae3a8cf5688c05ea14f75bc Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 24 Feb 2026 21:13:47 -0800 Subject: [PATCH 11/23] refactor: update proof of pedersen uniformity to use commit directly --- VerifiedCommitments/Pedersen.lean | 58 ++++++++++++++++++++++++------- 1 file changed, 46 insertions(+), 12 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index b761517..b84fbd4 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -232,28 +232,62 @@ lemma pedersen_commitment_uniform (m : ZMod params.q) (c : G) : (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 - unfold commit - simp only [PMF.map_bind, pure, PMF.pure_map] - have h_eq : generate_a.bind fun (a : ZModMult params.q) => - PMF.uniformOfFintype (ZMod params.q)|>.bind (fun r => - PMF.pure (params.g^m.val * (params.g^(val a).val)^r.val)) = + 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] From 527885bd9645a93ba7c7037eebabd06e879434dc Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 28 Feb 2026 11:17:26 -0800 Subject: [PATCH 12/23] Add commitment scheme docstrings and clean up definitions; update pedersen as necessary --- VerifiedCommitments/CommitmentScheme.lean | 112 +++++++++++++--------- VerifiedCommitments/Pedersen.lean | 8 +- 2 files changed, 73 insertions(+), 47 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 28a9e00..577f5f2 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -4,76 +4,102 @@ 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) - -namespace Commitment + state : Type + stage1 : K → PMF ((M × M) × state) + stage2 : C → state → PMF (ZMod 2) noncomputable section + variable {M C O K : Type} -variable (scheme : CommitmentScheme M C O K) +namespace Commitment + +/-- 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), - (scheme.commit h m).bind (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 is perfectly binding if for any public parameters `h`, any commits `c`, and any messages `m m'` and any opening values `o o'` if `verify h m c o = verify h m' c o'` then `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 ≤ ε + scheme.verify h m' c o' = 1 → + m = m' +/-- A commitment scheme is perfectly hiding if for any messages `m m'` and any commitment `c`, the distributions on commitments induced by first running `setup` and then running `commit` on `m` or `m'` are identical. -/ +def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop := + ∀ (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'`). -/ +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 ≤ ε --- 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)) -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 -/ --- 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')))))) +/-- 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`. -/ +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 - end Commitment + +end diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index b84fbd4..0030c13 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -295,7 +295,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] @@ -319,6 +319,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 /- ======================================== @@ -382,7 +383,7 @@ lemma binding_reduction_to_dlog 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⟩ @@ -394,7 +395,7 @@ lemma binding_reduction_to_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 @@ -402,7 +403,6 @@ lemma binding_reduction_to_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') From 911b86e8d4067d8cd9b5fbb31ff6132ee8fd07f8 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 28 Feb 2026 12:27:40 -0800 Subject: [PATCH 13/23] Tweak language for perfect hiding and binding --- VerifiedCommitments/CommitmentScheme.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 577f5f2..5558225 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -45,14 +45,14 @@ def correctness (scheme : CommitmentScheme M C O K) : Prop := ∀ (h : K) (m : M), (scheme.commit h m).bind (fun (c, o) => pure <| scheme.verify h m c o) = pure 1 -/-- A commitment scheme is perfectly binding if for any public parameters `h`, any commits `c`, and any messages `m m'` and any opening values `o o'` if `verify h m c o = verify h m' c o'` then `m = m'`.-/ +/-- 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' -/-- A commitment scheme is perfectly hiding if for any messages `m m'` and any commitment `c`, the distributions on commitments induced by first running `setup` and then running `commit` on `m` or `m'` are identical. -/ +/-- 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), PMF.bind scheme.setup (fun (h, _) => From 886a573f7e699486031c989fa1715be4bc55201b Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 28 Feb 2026 12:30:28 -0800 Subject: [PATCH 14/23] Reorder noncomputable section --- VerifiedCommitments/CommitmentScheme.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 5558225..e810082 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -34,12 +34,10 @@ structure TwoStageAdversary (K M C : Type) where stage1 : K → PMF ((M × M) × state) stage2 : C → state → PMF (ZMod 2) -noncomputable section +namespace Commitment variable {M C O K : Type} -namespace Commitment - /-- 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), (scheme.commit h m).bind (fun (c, o) => @@ -63,6 +61,8 @@ def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop := PMF.bind (scheme.commit h m') (fun (c, _) => pure c)) c +noncomputable section + /- 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'`). -/ @@ -100,6 +100,6 @@ 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 - end + +end Commitment From c460ba87cd375a108f621f7af722f334adcb118f Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 28 Feb 2026 17:28:48 -0800 Subject: [PATCH 15/23] Reconfigure some aspects of commitment spec --- VerifiedCommitments/CommitmentScheme.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index e810082..95ed1f1 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -40,7 +40,7 @@ variable {M C O K : Type} /-- 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), (scheme.commit h m).bind (fun (c, o) => + ∀ (h : K) (m : M), (scheme.commit h m |>.bind fun (c, o) => pure <| scheme.verify h m c o) = pure 1 /-- 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'`). -/ @@ -61,12 +61,11 @@ def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop := PMF.bind (scheme.commit h m') (fun (c, _) => pure c)) c -noncomputable section - /- 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'`). -/ -def comp_binding_game [DecidableEq M] (scheme : CommitmentScheme M C O K) +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 @@ -81,11 +80,10 @@ 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 ≤ ε - /- 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`. -/ -def comp_hiding_game +noncomputable def comp_hiding_game (scheme : CommitmentScheme M C O K) (A : TwoStageAdversary K M C) := do let (h, _) ← scheme.setup @@ -100,6 +98,4 @@ 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 - end Commitment From 5e564eb1b9609940c33959704ebf29823baed0b4 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 28 Feb 2026 17:30:21 -0800 Subject: [PATCH 16/23] refactor: reorder elgamal definitions --- VerifiedCommitments/ElgamalCommitments.lean | 104 +++++++++----------- 1 file changed, 48 insertions(+), 56 deletions(-) diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean index 24fb2d8..cc2d959 100644 --- a/VerifiedCommitments/ElgamalCommitments.lean +++ b/VerifiedCommitments/ElgamalCommitments.lean @@ -1,56 +1,16 @@ -- 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 -class ElgamalParameters (G : Type) extends +class PublicParameters (G : Type) extends Fintype G, Group G, IsCyclic G where [decidable_G : DecidableEq G] q : ℕ @@ -63,11 +23,15 @@ class ElgamalParameters (G : Type) extends G_card_q : Fintype.card G = q -- Make instances available -variable {G : Type} [params : ElgamalParameters G] +variable {G : Type} [params : PublicParameters G] instance : DecidableEq G := params.decidable_G instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩ -noncomputable def setup : PMF (G × ZMod params.q) := -- Need to include x to match CommitmentScheme spec +/- ======================================== + SCHEME DEFINITION + ======================================== -/ + +noncomputable def setup : PMF (G × ZMod params.q) := do let x ← PMF.uniformOfFintype (ZMod params.q) return (params.g^x.val, x) @@ -80,17 +44,14 @@ do def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 := if c = ⟨params.g^o.val, h^o.val * m⟩ then 1 else 0 -noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G := -{ - setup := setup, - commit := commit, +noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G where + setup := setup + commit := commit verify := verify -} -/- - ----------------------------------------------------------- - Proof of correctness of ElGamal - ----------------------------------------------------------- --/ + +/- ======================================== + CORRECTNESS + ======================================== -/ theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G params) := by intro h m @@ -99,6 +60,37 @@ 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] +/- ======================================== + DDH EXPERIMENT + ======================================== -/ + +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 + +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 + +def Assumption (ε : ENNReal) : Prop := (Game0 G g q D 1) - (Game1 G g q D 1) ≤ ε + +end DDH /- ----------------------------------------------------------- From 87a3900fea368fd6eaba009fafd865a32df89cf2 Mon Sep 17 00:00:00 2001 From: Ashley Blacquiere Date: Sat, 28 Feb 2026 19:17:41 -0800 Subject: [PATCH 17/23] feat: add proof of elgamal binding * refactor: rename parameters * feat: add proof of elgamal binding --- VerifiedCommitments/ElgamalCommitments.lean | 40 +++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean index cc2d959..5072162 100644 --- a/VerifiedCommitments/ElgamalCommitments.lean +++ b/VerifiedCommitments/ElgamalCommitments.lean @@ -382,4 +382,44 @@ theorem computational_hiding_from_ddh (ε : ENNReal) exact DDH_hard (D_from_adversary hA) +/- ======================================== + BINDING PROPERTY + ======================================== -/ + +lemma ordg_eq_q : orderOf params.g = params.q := by + have h_card_zpow : Fintype.card (Subgroup.zpowers params.g) = orderOf params.g := Fintype.card_zpowers + have h_card_eq : Fintype.card (Subgroup.zpowers params.g) = Fintype.card G := by + have : Function.Bijective (Subtype.val : Subgroup.zpowers params.g → G) := by + constructor + · exact Subtype.val_injective + · intro x + use ⟨x, params.g_gen_G x⟩ + exact Fintype.card_of_bijective this + rw [← h_card_zpow, h_card_eq, params.card_eq] + + +theorem perfect_binding : Commitment.perfect_binding (@scheme G params) := by + unfold Commitment.perfect_binding + intro h c m m' o o' + unfold scheme verify + simp only [ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not] + intro hc + simp [hc] + congr! with hc₁ hc₂ + + + have h_congr : o.val ≡ o'.val [MOD params.q] := by + simpa [ordg_eq_q] using (pow_eq_pow_iff_modEq.mp hc₁) + + have o_eq : o = o' := by + have eq_cast : ((o.val : ℕ) : ZMod params.q) = ((o'.val : ℕ) : ZMod params.q) := + ZMod.natCast_eq_natCast_iff o.val o'.val params.q |>.mpr h_congr + simp at eq_cast + exact eq_cast + + subst o_eq + simp at hc₂ + exact hc₂ + + end Elgamal From c9751cd735410c77fd6cb7d446828964e47b910b Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 28 Feb 2026 19:40:54 -0800 Subject: [PATCH 18/23] refactor: remove unnecessary elements --- VerifiedCommitments/ElgamalCommitments.lean | 22 +++++++++------------ 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean index 5072162..8864b9a 100644 --- a/VerifiedCommitments/ElgamalCommitments.lean +++ b/VerifiedCommitments/ElgamalCommitments.lean @@ -15,12 +15,10 @@ 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] @@ -31,15 +29,13 @@ instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩ SCHEME DEFINITION ======================================== -/ -noncomputable def setup : PMF (G × ZMod params.q) := -do +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 @@ -67,11 +63,11 @@ theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G param 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) + (g : G) (gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g) + (q : ℕ) [NeZero q] [Fact (0 < q)] (card_eq : Fintype.card G = q) (D : G → G → G → PMF (ZMod 2)) -include g_gen_G G_card_q +include gen_G card_eq noncomputable def Game0 : PMF (ZMod 2) := do @@ -184,7 +180,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] @@ -393,7 +389,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] From 705fb7afaffea4b57437c5adf03d84669fa53067 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 28 Feb 2026 20:17:43 -0800 Subject: [PATCH 19/23] refactor: fix line break in defs --- VerifiedCommitments/ElgamalCommitments.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean index 8864b9a..9885b6c 100644 --- a/VerifiedCommitments/ElgamalCommitments.lean +++ b/VerifiedCommitments/ElgamalCommitments.lean @@ -49,7 +49,8 @@ noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G where 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] From f8f86eceb4616adff7285926c53519691761c2f3 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 10 Mar 2026 17:25:57 -0700 Subject: [PATCH 20/23] wip: minor refactoring --- VerifiedCommitments/Pedersen.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 0030c13..b3daadf 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -140,9 +140,12 @@ end DLog ======================================== -/ 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 + 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 @@ -150,7 +153,8 @@ lemma ordg_eq_q : orderOf params.g = params.q := by 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) +noncomputable def generate_a : PMF (ZModMult params.q) := + PMF.uniformOfFintype (ZModMult params.q) /- ======================================== HIDING PROPERTY @@ -383,7 +387,7 @@ lemma binding_reduction_to_dlog simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify] - rw [PMF.bind_apply ] + rw [PMF.bind_apply] apply ENNReal.tsum_le_tsum intro ⟨h, a⟩ From 4ab2133b887c7e5e614bcde5b5ce0716f55388ba Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 10 Mar 2026 17:27:04 -0700 Subject: [PATCH 21/23] wip: remove coprime hypothesis from binding lemma (grind handles it) --- VerifiedCommitments/Pedersen.lean | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index b3daadf..4cacd65 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -353,17 +353,17 @@ lemma gpow_eq_of_two_valid_openings 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 ho_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) From 616d2c14f20f9c57608815b51c3281b409a28ab6 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 10 Mar 2026 17:27:36 -0700 Subject: [PATCH 22/23] wip: minor refactoring --- VerifiedCommitments/CommitmentScheme.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 95ed1f1..d918a01 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -95,7 +95,8 @@ noncomputable def comp_hiding_game /-- 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 := +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 From 60e4ddd3ee27cfcd69df34a8d84ffc3a1f0a1059 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 10 Mar 2026 17:28:37 -0700 Subject: [PATCH 23/23] wip: refactor some defs --- VerifiedCommitments/ElgamalCommitments.lean | 118 ++++++++++---------- 1 file changed, 56 insertions(+), 62 deletions(-) diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean index 9885b6c..3fbf5d4 100644 --- a/VerifiedCommitments/ElgamalCommitments.lean +++ b/VerifiedCommitments/ElgamalCommitments.lean @@ -63,68 +63,41 @@ theorem elgamal_commitment_correctness : namespace DDH -variable (G : Type) [Fintype G] [Group G] - (g : G) (gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g) - (q : ℕ) [NeZero q] [Fact (0 < q)] (card_eq : Fintype.card G = q) - (D : G → G → G → PMF (ZMod 2)) - -include gen_G card_eq - -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 - -def Assumption (ε : ENNReal) : Prop := (Game0 G g q D 1) - (Game1 G g q D 1) ≤ ε +variable (D : 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 -/- - ----------------------------------------------------------- - Proof of semantic security of ElGamal - ----------------------------------------------------------- --/ +/- ======================================== + HIDING PROPERTY + ======================================== -/ -noncomputable def D_from_adversary (A : TwoStageAdversary G G (G × G)) : G → G → G → PMF (ZMod 2) := +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') + 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 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] - -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) @@ -134,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) @@ -146,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 @@ -358,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] @@ -371,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 @@ -404,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₁)