From 539abba96243d1bd80fc30bd816e6084555e5c9e Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 16 Dec 2025 21:27:50 -0800 Subject: [PATCH 01/24] refactor: break pedersen scheme into separate defs --- VerifiedCommitments/PedersenScheme.lean | 44 ++++++++++++++----------- 1 file changed, 24 insertions(+), 20 deletions(-) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 7d6d2ea..a81baac 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -3,29 +3,33 @@ import VerifiedCommitments.dlog namespace Pedersen - noncomputable def scheme - (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : - CommitmentScheme (ZMod q) G (ZMod q) G := { - setup := -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val), --setup q hq g, - do - let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2 - return g^a.val, - commit := fun h m => --commit h m g, - do - let r ← PMF.uniformOfFintype (ZMod q) - return ⟨g^m.val * h^r.val, r⟩, - verify := fun h m c o => if c = g^m.val * h^o.val then 1 else 0 --verify h m c o g - } + -- noncomputable def scheme + -- (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) + -- (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : + -- CommitmentScheme (ZMod q) G (ZMod q) G := { + -- setup := -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val), --setup q hq g, + -- do + -- let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2 + -- return g^a.val, + -- commit := fun h m => --commit h m g, + -- do + -- let r ← PMF.uniformOfFintype (ZMod q) + -- return ⟨g^m.val * h^r.val, r⟩, + -- verify := fun h m c o => if c = g^m.val * h^o.val then 1 else 0 --verify h m c o g + -- } noncomputable def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : PMF G := - PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) + (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : PMF G := + PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) noncomputable def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) (h : G) (m : ZMod q) : PMF G := - do - let r ← PMF.uniformOfFintype (ZMod q) - return g^m.val * h^r.val + (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF G := + do + let r ← PMF.uniformOfFintype (ZMod q) + return g^m.val * h^r.val + + noncomputable def verify (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) + (q : ℕ) [NeZero q] (h : G) (m : ZMod q) (c : G) (o : ZMod q): ZMod 2 := + if c = g^m.val * h^o.val then 1 else 0 end Pedersen From 3699a6f88bd02118bc2ff3d8916d146795f1de91 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 16 Dec 2025 21:52:08 -0800 Subject: [PATCH 02/24] chore: bump to 4.27 --- lake-manifest.json | 22 +++++++++++----------- lean-toolchain | 2 +- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 294bf9b..f4ce7bb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a778305ec3a679802f7dcfa64e2b903d4679ee21", + "rev": "6c8fd6fb284ad384ef49513a1d0515b2441799a5", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9f492660e9837df43fd885a2ad05c520da9ff9f5", + "rev": "e2a2ee109182182dd0e347e8149d312d72bfbfb2", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "90f3b0f429411beeeb29bbc248d799c18a2d520d", + "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "556caed0eadb7901e068131d1be208dd907d07a2", + "rev": "ef8377f31b5535430b6753a974d685b0019d0681", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.74", + "inputRev": "v0.0.84", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "14d8accc7513f8a85ae142201907f49f518ae0ec", + "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2e582a44b0150db152bff1c8484eb557fb5340da", + "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9c1ad6d93126e346c859d4a17d71b010e7951f92", + "rev": "78129e1913fe4988ac238156ec5f223ec02d286c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "b62fd39acc32da6fb8bb160c82d1bbc3cb3c186e", + "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.27.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "«verified-commitments»", diff --git a/lean-toolchain b/lean-toolchain index 66a6d41..fb18a7f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.24.0-rc1 \ No newline at end of file +leanprover/lean4:v4.27.0-rc1 \ No newline at end of file From 3b97cfce1a7a1f0a55cf497e988c54064110d018 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 17 Dec 2025 08:30:33 -0800 Subject: [PATCH 03/24] fix: rename commit to Commit --- VerifiedCommitments/CommitmentScheme.lean | 4 ++-- VerifiedCommitments/PedersenHiding.lean | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 6264201..78cebd0 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -4,13 +4,13 @@ import Mathlib.Probability.ProbabilityMassFunction.Constructions import Mathlib.Data.ZMod.Defs -structure commit (C O : Type) where +structure Commit (C O : Type) where c : C o : O structure CommitmentScheme (M C O K : Type) where setup : PMF K - commit : K → M → PMF (commit C O) + commit : K → M → PMF (Commit C O) verify : K → M → C → O → ZMod 2 namespace Adversary diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 9b325a9..412defc 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -66,7 +66,7 @@ lemma exp_bij' (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod -- Fintype instance for commit -instance {C O : Type} [Fintype C] [Fintype O] : Fintype (commit C O) := +instance {C O : Type} [Fintype C] [Fintype O] : Fintype (Commit C O) := Fintype.ofEquiv (C × O) { toFun := fun ⟨c, o⟩ => ⟨c, o⟩ invFun := fun ⟨c, o⟩ => ⟨c, o⟩ @@ -191,7 +191,7 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) : lemma pedersen_uniform_for_fixed_a_probablistic' (a : ZModMult q) (m : ZMod q) : (Pedersen.commit G g q hq_prime (g^(val a).val) m) = - PMF.uniformOfFintype G := by + PMF.uniformOfFintype (Commit G (ZMod q)) := by rw [← bij_uniform_for_fixed_a q G_card_q g g_gen_G a m] -- Unfold Pedersen.commit unfold Pedersen.commit @@ -224,7 +224,7 @@ lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) : -- g^((m + (val a) * r : ZMod q).val : ℤ) lemma pedersen_uniform_for_fixed_a_probablistic (a : ZModMult q) (m : ZMod q) [DecidableEq G] (c' : G) : - PMF.map commit.c ((Pedersen.scheme G g q hq_prime).commit (g^(val a).val) m) c' = 1 / (Fintype.card G) := by sorry + PMF.map Commit.c ((Pedersen.scheme G g q hq_prime).commit (g^(val a).val) m) c' = 1 / (Fintype.card G) := by sorry From af79045c28b9b38d325139450716cbe1420755a6 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 17 Dec 2025 08:31:18 -0800 Subject: [PATCH 04/24] fix: remove unnecessary hypothesis form hiding proofs --- VerifiedCommitments/PedersenHiding.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 412defc..24ce747 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -190,7 +190,7 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) : lemma pedersen_uniform_for_fixed_a_probablistic' (a : ZModMult q) (m : ZMod q) : - (Pedersen.commit G g q hq_prime (g^(val a).val) m) = + (Pedersen.commit G g q (g^(val a).val) m) = PMF.uniformOfFintype (Commit G (ZMod q)) := by rw [← bij_uniform_for_fixed_a q G_card_q g g_gen_G a m] -- Unfold Pedersen.commit @@ -204,7 +204,7 @@ lemma pedersen_uniform_for_fixed_a_probablistic' (a : ZModMult q) (m : ZMod q) : lemma bij_fixed_a_equiv_pedersen_commit (m : ZMod q) (a : ZModMult q) : PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = - (Pedersen.commit G g q hq_prime (g^(val a).val) m) := by + (Pedersen.commit G g q (g^(val a).val) m) := by rw [bij_uniform_for_fixed_a q G_card_q g g_gen_G a m] rw [← pedersen_uniform_for_fixed_a_probablistic' q G_card_q g g_gen_G hq_prime a m] @@ -213,7 +213,7 @@ lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) : PMF.bind (generate_a q) (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = PMF.bind (generate_a q) - (fun a => (Pedersen.commit G g q hq_prime (g^(val a).val) m)) := by + (fun a => (Pedersen.commit G g q g^(val a).val) m)) := by congr 1 funext a exact bij_fixed_a_equiv_pedersen_commit q G_card_q g g_gen_G hq_prime m a From 7a842b3f78303ac2f8637a10c2a4ee87aa001adc Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 17 Dec 2025 08:32:05 -0800 Subject: [PATCH 05/24] fix: add pedersen scheme back in --- VerifiedCommitments/PedersenScheme.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index a81baac..a750ebb 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -32,4 +32,14 @@ namespace Pedersen (q : ℕ) [NeZero q] (h : G) (m : ZMod q) (c : G) (o : ZMod q): ZMod 2 := if c = g^m.val * h^o.val then 1 else 0 + + noncomputable def scheme + (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) + (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : + CommitmentScheme (ZMod q) G (ZMod q) G := { + setup := setup G g q hq_prime, + commit (h : G) (m : ZMod q) := commit G g q h m, + verify (h : G) (m : ZMod q) (c : G) (o : ZMod q):= verify G g q h m c o + } + end Pedersen From a0f1d48395a0a867edfe12fdfddab4cf6a621598 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 17 Dec 2025 08:32:33 -0800 Subject: [PATCH 06/24] fix: add nonempty instance for Pedersen Commit --- VerifiedCommitments/PedersenScheme.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index a750ebb..0ed9f16 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -43,3 +43,5 @@ namespace Pedersen } end Pedersen + +instance {G : Type} {q : ℕ} [NeZero q] : Nonempty (Commit G (ZMod q)) := sorry From c619477b44ec04245ccdaed04f5cbde42f0a7028 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 17 Dec 2025 08:34:38 -0800 Subject: [PATCH 07/24] wip: modify commit output to include opening value --- VerifiedCommitments/PedersenScheme.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 0ed9f16..995a4fe 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -23,10 +23,10 @@ namespace Pedersen PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) noncomputable def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF G := + (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (Commit G (ZMod q)) := do let r ← PMF.uniformOfFintype (ZMod q) - return g^m.val * h^r.val + return ⟨g^m.val * h^r.val, r⟩ noncomputable def verify (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (h : G) (m : ZMod q) (c : G) (o : ZMod q): ZMod 2 := From e8fea566615c84df4127fd5ec762fa7f1e12d8ee Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 31 Dec 2025 10:49:53 -0800 Subject: [PATCH 08/24] wip: add Commitment namespace; remove Commit structure; add Pedersen noncomputable section --- VerifiedCommitments/CommitmentScheme.lean | 26 +++++++++++++------ VerifiedCommitments/PedersenBinding.lean | 8 +++--- VerifiedCommitments/PedersenHiding.lean | 6 ++--- VerifiedCommitments/PedersenScheme.lean | 31 +++++++---------------- 4 files changed, 33 insertions(+), 38 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 78cebd0..b0c1f11 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -4,13 +4,14 @@ import Mathlib.Probability.ProbabilityMassFunction.Constructions import Mathlib.Data.ZMod.Defs -structure Commit (C O : Type) where - c : C - o : O +-- namespace Crypto - or similar? +-- structure Commit (C O : Type) where +-- c : C +-- o : O structure CommitmentScheme (M C O K : Type) where setup : PMF K - commit : K → M → PMF (Commit C O) + commit : K → M → PMF (C × O) verify : K → M → C → O → ZMod 2 namespace Adversary @@ -22,13 +23,18 @@ structure guess (M C O : Type) where o': O end Adversary -variable {M C O K : Type} + +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 => pure $ scheme.verify h m commit.c commit.o) = pure 1 + PMF.bind (scheme.commit h m) (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 := @@ -72,7 +78,7 @@ def do_commit (scheme: CommitmentScheme M C O K) (m : M) : PMF C := do let h ← scheme.setup let commit ← scheme.commit h m - return commit.c + return commit.1 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 @@ -84,9 +90,13 @@ def comp_hiding_game (scheme : CommitmentScheme M C O K) do let h ← scheme.setup -- As above with comp_binding_game let commit ← scheme.commit h m - A h commit.c + A h commit.1 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 ≤ ε + +end + +end Commitment diff --git a/VerifiedCommitments/PedersenBinding.lean b/VerifiedCommitments/PedersenBinding.lean index 59225cb..fc6cfc6 100644 --- a/VerifiedCommitments/PedersenBinding.lean +++ b/VerifiedCommitments/PedersenBinding.lean @@ -5,12 +5,12 @@ namespace Pedersen lemma binding_as_hard_dlog (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) (ε : ENNReal) + (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) (G_card_q : Fintype.card G = q) (hg_gen : orderOf g = Fintype.card G) (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) : - comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q hq_prime (DLog.adversary' G q A) 1 := by - simp only [DLog.experiment, comp_binding_game', Pedersen.scheme, DLog.adversary'] + Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q hq_prime (DLog.adversary' G q A) 1 := by + simp only [DLog.experiment, Commitment.comp_binding_game', Pedersen.scheme, DLog.adversary'] simp only [bind_pure_comp, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not, ne_eq, bind_map_left, ite_not, map_bind] congr! 5 with x ⟨c, m, m', o, o'⟩ @@ -94,7 +94,7 @@ theorem Pedersen.computational_binding : (hg_gen : orderOf g = Fintype.card G), (∀ (A : G → PMF (ZMod q)), DLog.experiment G g q hq_prime A 1 ≤ ε) → (∀ (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))), - comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by + Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by intro G _ _ _ _ g q _ _ hq_prime ε G_card_q hg_gen hdlog A exact le_trans (binding_as_hard_dlog G g q hq_prime ε G_card_q hg_gen A) (hdlog (DLog.adversary' G q A)) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 24ce747..e57771d 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -1,11 +1,9 @@ import VerifiedCommitments.PedersenScheme import VerifiedCommitments.ZModUtil -import Mathlib -- Would like to trim down this import but the Units.mk0 (a.val : ZMod q) a.2 line is a problem -- Temporary import VerifiedCommitments.«scratch-skip-bind» - variable {G: Type} [Fintype G] [Group G] variable (q : ℕ) [Fact (Nat.Prime q)] variable (G_card_q : Fintype.card G = q) @@ -66,7 +64,7 @@ lemma exp_bij' (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod -- Fintype instance for commit -instance {C O : Type} [Fintype C] [Fintype O] : Fintype (Commit C O) := +instance {C O : Type} [Fintype C] [Fintype O] : Fintype (C × O) := Fintype.ofEquiv (C × O) { toFun := fun ⟨c, o⟩ => ⟨c, o⟩ invFun := fun ⟨c, o⟩ => ⟨c, o⟩ @@ -170,7 +168,7 @@ lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), -- Temporary? -variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) +-- variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) noncomputable def generate_a : PMF (ZModMult q) := PMF.uniformOfFintype (ZModMult q) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 995a4fe..9b3d841 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -3,37 +3,23 @@ import VerifiedCommitments.dlog namespace Pedersen - -- noncomputable def scheme - -- (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - -- (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : - -- CommitmentScheme (ZMod q) G (ZMod q) G := { - -- setup := -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val), --setup q hq g, - -- do - -- let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2 - -- return g^a.val, - -- commit := fun h m => --commit h m g, - -- do - -- let r ← PMF.uniformOfFintype (ZMod q) - -- return ⟨g^m.val * h^r.val, r⟩, - -- verify := fun h m c o => if c = g^m.val * h^o.val then 1 else 0 --verify h m c o g - -- } - - noncomputable def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) +noncomputable section + + def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : PMF G := PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) - noncomputable def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (Commit G (ZMod q)) := + def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) + (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (G × (ZMod q)) := do let r ← PMF.uniformOfFintype (ZMod q) return ⟨g^m.val * h^r.val, r⟩ - noncomputable def verify (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) + def verify (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (h : G) (m : ZMod q) (c : G) (o : ZMod q): ZMod 2 := if c = g^m.val * h^o.val then 1 else 0 - - noncomputable def scheme + def scheme (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : CommitmentScheme (ZMod q) G (ZMod q) G := { @@ -42,6 +28,7 @@ namespace Pedersen verify (h : G) (m : ZMod q) (c : G) (o : ZMod q):= verify G g q h m c o } +end end Pedersen -instance {G : Type} {q : ℕ} [NeZero q] : Nonempty (Commit G (ZMod q)) := sorry +instance {G : Type} {q : ℕ} [NeZero q] : Nonempty (G × (ZMod q)) := sorry From 3025e7181977e0fbdd19f932e2e2b64356425f13 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 31 Dec 2025 10:50:49 -0800 Subject: [PATCH 09/24] wip: mapping logic in hiding; fix hiding def --- VerifiedCommitments/PedersenHiding.lean | 89 +++++++++++++------------ 1 file changed, 47 insertions(+), 42 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index e57771d..f801d29 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -173,11 +173,14 @@ lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), noncomputable def generate_a : PMF (ZModMult q) := PMF.uniformOfFintype (ZModMult q) +-- 1 lemma bij_uniform_for_fixed_a (a : ZModMult q) (m : ZMod q) : PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = (PMF.uniformOfFintype G) := by · expose_names; exact map_uniformOfFintype_equiv q G_card_q g g_gen_G (expEquiv q G_card_q g g_gen_G a m) +-- 2 +-- 1 -> 2 lemma bij_uniform_for_uniform_a (m : ZMod q) : (PMF.bind (generate_a q) (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)))) = (PMF.uniformOfFintype G) := by @@ -186,69 +189,71 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) : intro a · expose_names; exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m - -lemma pedersen_uniform_for_fixed_a_probablistic' (a : ZModMult q) (m : ZMod q) : - (Pedersen.commit G g q (g^(val a).val) m) = - PMF.uniformOfFintype (Commit G (ZMod q)) := by +-- 3 +-- 1 -> 3 +lemma pedersen_uniform_for_fixed_a_probablistic (a : ZModMult q) (m : ZMod q) : + PMF.map Prod.fst (Pedersen.commit G g q (g^(val a).val) m) = + PMF.uniformOfFintype G := by rw [← bij_uniform_for_fixed_a q G_card_q g g_gen_G a m] -- Unfold Pedersen.commit unfold Pedersen.commit simp only [bind_pure_comp] -- Now both sides are PMF.map over uniformOfFintype (ZMod q) congr 1 - funext r - exact (expEquiv_unfold q G_card_q g g_gen_G a m r).symm - - + · sorry + · sorry + · sorry + -- funext r + -- exact (expEquiv_unfold q G_card_q g g_gen_G a m r).symm + +-- 4 +-- 1, 3 -> 4 lemma bij_fixed_a_equiv_pedersen_commit (m : ZMod q) (a : ZModMult q) : PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = - (Pedersen.commit G g q (g^(val a).val) m) := by + PMF.map Prod.fst (Pedersen.commit G g q (g^(val a).val) m) := by rw [bij_uniform_for_fixed_a q G_card_q g g_gen_G a m] - rw [← pedersen_uniform_for_fixed_a_probablistic' q G_card_q g g_gen_G hq_prime a m] + rw [← pedersen_uniform_for_fixed_a_probablistic q G_card_q g g_gen_G a m] +-- 5 lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) : PMF.bind (generate_a q) - (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = - PMF.bind (generate_a q) - (fun a => (Pedersen.commit G g q g^(val a).val) m)) := by + (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = -- this line = PMF.uniformOfFintype G by (2) bij_uniform_for_uniform_a + PMF.map Prod.fst (PMF.bind (generate_a q) + (fun a => (Pedersen.commit G g q (g^(val a).val) m))) := by congr 1 - funext a - exact bij_fixed_a_equiv_pedersen_commit q G_card_q g g_gen_G hq_prime m a + · sorry + · sorry + · sorry --- for fixed aa ∈ {1, ... , q − 1}, and for any m ∈ Zq, if t ← Zq, then g^m*h^r is uniformly distributed over G --- We can do this by proving t ↦ g^m*h^r is a bijection - see exp_bij above --- g^((m + (val a) * r : ZMod q).val : ℤ) -lemma pedersen_uniform_for_fixed_a_probablistic - (a : ZModMult q) (m : ZMod q) [DecidableEq G] (c' : G) : - PMF.map Commit.c ((Pedersen.scheme G g q hq_prime).commit (g^(val a).val) m) c' = 1 / (Fintype.card G) := by sorry +-- 6 +-- 5, 2 -> 6 +lemma pedersen_commitment_uniform (m : ZMod q) (c : G) : + (PMF.map Prod.fst ((PMF.bind (generate_a q) + (fun a => Pedersen.commit G g q (g^(val a).val) m ))) c) = + ((1 : ENNReal) / (Fintype.card G)) := by + rw [← bij_random_a_equiv_pedersen_commit q G_card_q g g_gen_G m] + rw [bij_uniform_for_uniform_a q G_card_q g g_gen_G m] + simp [PMF.uniformOfFintype_apply] +-- Express the marginal probability equals the PMF on G +-- (PMF.map Prod.fst (Pedersen.commit G g q h m)) +-- = +-- (PMF.uniformOfFintype G) +-- This could be used above to solve the intermediate lemmas, so that I don't need to compare to PMF (G × ZMod q) --- lemma pedersen_commitment_uniform'' (m : ZMod q) [DecidableEq G] (c : G) : --- (PMF.bind (generate_a q) --- (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q)) --- (fun r => PMF.pure (g^m.val * (g^((val a).val))^r.val)))) c = 1 / Fintype.card G := by --- --have h_expEquiv : PMF.uniformOfFintype (ZMod q)).bind fun r ↦ PMF.pure (g ^ m.val * (g ^ (val a).val) ^ r.val --- unfold generate_a --- simp [PMF.bind_apply] --- rw [tsum_fintype] --- simp_rw [tsum_fintype] --- conv_lhs => arg 1; arg 2; rw [←bind_eq_map' q G_card_q g g_gen_G a m] --do I need to first get a version of expEquiv and unfold to match the def? - --- sorry - theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q), - perfect_hiding (Pedersen.scheme G g q hq_prime) := by + Commitment.perfect_hiding (Pedersen.scheme G g q hq_prime) := by intros G _ _ _ _ g q _ hq_prime - simp only [Pedersen.scheme, _root_.perfect_hiding, do_commit] - simp only [bind_pure_comp, Functor.map_map, bind_map_left] - intro m m' c - rw [bind, Functor.map] - simp only [PMF] - rw [Monad.toBind, PMF.instMonad] - + have : Fact (Nat.Prime q) := ⟨hq_prime⟩ + unfold Commitment.perfect_hiding + intros m m' c + unfold Commitment.do_commit + unfold Pedersen.scheme + simp only + --apply pedersen_commitment_uniform sorry From e60922c4f1a676f81ba757a0610321712d4c5d0c Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 31 Dec 2025 13:53:24 -0800 Subject: [PATCH 10/24] wip: completed hiding lemmas; partial proof of perfect hiding, but need to reconsider some structural elements? --- VerifiedCommitments/PedersenHiding.lean | 78 +++++++++++-------------- 1 file changed, 34 insertions(+), 44 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index f801d29..59782a2 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -4,6 +4,8 @@ import VerifiedCommitments.ZModUtil -- Temporary import VerifiedCommitments.«scratch-skip-bind» +namespace Pedersen + variable {G: Type} [Fintype G] [Group G] variable (q : ℕ) [Fact (Nat.Prime q)] variable (G_card_q : Fintype.card G = q) @@ -166,10 +168,6 @@ lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), intros exact rfl - --- Temporary? --- variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) - noncomputable def generate_a : PMF (ZModMult q) := PMF.uniformOfFintype (ZModMult q) @@ -189,42 +187,32 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) : intro a · expose_names; exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m --- 3 --- 1 -> 3 -lemma pedersen_uniform_for_fixed_a_probablistic (a : ZModMult q) (m : ZMod q) : - PMF.map Prod.fst (Pedersen.commit G g q (g^(val a).val) m) = - PMF.uniformOfFintype G := by - rw [← bij_uniform_for_fixed_a q G_card_q g g_gen_G a m] - -- Unfold Pedersen.commit - unfold Pedersen.commit - simp only [bind_pure_comp] - -- Now both sides are PMF.map over uniformOfFintype (ZMod q) - congr 1 - · sorry - · sorry - · sorry - -- funext r - -- exact (expEquiv_unfold q G_card_q g g_gen_G a m r).symm - --- 4 --- 1, 3 -> 4 -lemma bij_fixed_a_equiv_pedersen_commit (m : ZMod q) (a : ZModMult q) : - PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = - PMF.map Prod.fst (Pedersen.commit G g q (g^(val a).val) m) := by - rw [bij_uniform_for_fixed_a q G_card_q g g_gen_G a m] - rw [← pedersen_uniform_for_fixed_a_probablistic q G_card_q g g_gen_G a m] - - -- 5 +-- 1, 2 -> 5 lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) : PMF.bind (generate_a q) (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = -- this line = PMF.uniformOfFintype G by (2) bij_uniform_for_uniform_a PMF.map Prod.fst (PMF.bind (generate_a q) (fun a => (Pedersen.commit G g q (g^(val a).val) m))) := by - congr 1 - · sorry - · sorry - · sorry + simp only [bij_uniform_for_uniform_a q G_card_q g g_gen_G m] + unfold Pedersen.commit generate_a + simp only [PMF.map_bind] + simp only [bind_pure_comp] + ext c + rw [bind_skip_const'] + intro a + conv_lhs => + arg 2 + arg 1 + ext r + rw [← expEquiv_unfold q G_card_q g g_gen_G a m r] + + rw [← PMF.monad_map_eq_map] + simp only [Functor.map_map] + + show PMF.map (fun r ↦ Prod.fst ((expEquiv q G_card_q g g_gen_G a m) r, r)) (PMF.uniformOfFintype (ZMod q)) = PMF.uniformOfFintype G + simp only + exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m -- 6 @@ -238,22 +226,24 @@ lemma pedersen_commitment_uniform (m : ZMod q) (c : G) : simp [PMF.uniformOfFintype_apply] --- Express the marginal probability equals the PMF on G --- (PMF.map Prod.fst (Pedersen.commit G g q h m)) --- = --- (PMF.uniformOfFintype G) --- This could be used above to solve the intermediate lemmas, so that I don't need to compare to PMF (G × ZMod q) - +end Pedersen theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q), + (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) + (G_card_q : Fintype.card G = q) + (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g), Commitment.perfect_hiding (Pedersen.scheme G g q hq_prime) := by - intros G _ _ _ _ g q _ hq_prime + intros G _ _ _ _ g q _ hq_prime G_card_q g_gen_G have : Fact (Nat.Prime q) := ⟨hq_prime⟩ unfold Commitment.perfect_hiding intros m m' c unfold Commitment.do_commit unfold Pedersen.scheme - simp only - --apply pedersen_commitment_uniform + simp + unfold Pedersen.setup Pedersen.commit + simp only [bind_pure_comp, Functor.map_map] + change (PMF.bind _ _) c = (PMF.bind _ _) c + simp only [PMF.bind_apply] + + rw [Pedersen.pedersen_commitment_uniform q G_card_q g g_gen_G m c] sorry From 8ec70dabc230c7250698e0554bf965acee8ce0f0 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 31 Dec 2025 17:41:23 -0800 Subject: [PATCH 11/24] wip: move generate_a to pedersenscheme --- VerifiedCommitments/PedersenHiding.lean | 3 --- VerifiedCommitments/PedersenScheme.lean | 11 ++++++++++- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 59782a2..cac1380 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -168,9 +168,6 @@ lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), intros exact rfl -noncomputable def generate_a : PMF (ZModMult q) := - PMF.uniformOfFintype (ZModMult q) - -- 1 lemma bij_uniform_for_fixed_a (a : ZModMult q) (m : ZMod q) : PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = (PMF.uniformOfFintype G) := by diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 9b3d841..5378c8a 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -1,13 +1,22 @@ import VerifiedCommitments.CommitmentScheme import VerifiedCommitments.dlog +import VerifiedCommitments.ZModUtil namespace Pedersen +-- TODO: I'm not sure this should be here, or that +-- Setup should definitely return h, but should there be another def hanging around that computes an a independently? + +noncomputable def generate_a (q : ℕ) [NeZero q] : PMF (ZModMult q) := + PMF.uniformOfFintype (ZModMult q) + + noncomputable section def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : PMF G := - PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) + PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun a => return g^(val a).val) + --PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (G × (ZMod q)) := From dc08d1e932986904854b97a9bd499680e6156277 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 3 Jan 2026 11:46:59 -0800 Subject: [PATCH 12/24] wip: minor update to spec notes and pedersen setup --- VerifiedCommitments/PedersenScheme.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 5378c8a..c137f97 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -6,6 +6,7 @@ namespace Pedersen -- TODO: I'm not sure this should be here, or that -- Setup should definitely return h, but should there be another def hanging around that computes an a independently? +-- The two alternatives below for bind in setup may have some bearing on how the binding proof progresses, unless I change the dlog definitions to match... noncomputable def generate_a (q : ℕ) [NeZero q] : PMF (ZModMult q) := PMF.uniformOfFintype (ZModMult q) @@ -16,7 +17,7 @@ noncomputable section def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : PMF G := PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun a => return g^(val a).val) - --PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) + -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (G × (ZMod q)) := From a9ff6178f1a154458b67397d61599de9ac225204 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 3 Jan 2026 19:07:59 -0800 Subject: [PATCH 13/24] wip: commitmentscheme to bind defs --- VerifiedCommitments/CommitmentScheme.lean | 28 ++++++++--------------- 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index b0c1f11..e9206c7 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -51,23 +51,20 @@ def perfect_binding (scheme : CommitmentScheme M C O K) : Prop := def comp_binding_game (scheme : CommitmentScheme M C O K) (A : K → PMF (C × M × M × O × O)) : PMF $ ZMod 2 := open scoped Classical in - do - let h ← scheme.setup - let (c, m, m', o, o') ← A h - if scheme.verify h m c o = 1 ∧ scheme.verify h m' c o' = 1 ∧ m ≠ m' then pure 1 else pure 0 + PMF.bind scheme.setup (fun h => + PMF.bind (A h) (fun (c, m , m', o, o') => + if scheme.verify h m c o = 1 ∧ scheme.verify h m' c o' = 1 ∧ m ≠ m' then pure 1 else pure 0 )) def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop := ∀ (A : K → PMF (C × M × M × O × O)), comp_binding_game scheme A 1 ≤ ε - -- With Adversary namespace def comp_binding_game' (scheme : CommitmentScheme M C O K) (A' : K → PMF (Adversary.guess M C O)) : PMF $ ZMod 2 := open scoped Classical in - do - let h ← scheme.setup - let guess ← A' h - 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 + 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 (Adversary.guess M C O )), comp_binding_game' scheme A' 1 ≤ ε @@ -75,22 +72,17 @@ 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 := -do - let h ← scheme.setup - let commit ← scheme.commit h m - return commit.1 +PMF.bind scheme.setup (fun h => + PMF.bind (scheme.commit h m) (fun commit => pure commit.1)) 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) := - do - let h ← scheme.setup -- As above with comp_binding_game - let commit ← scheme.commit h m - A h 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 ca159b43bafcf1b38cdb3ff441292fe33f9e9286 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 3 Jan 2026 19:10:04 -0800 Subject: [PATCH 14/24] wip: pedersen scheme to bind --- VerifiedCommitments/PedersenScheme.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index c137f97..4957160 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -21,9 +21,7 @@ noncomputable section def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (G × (ZMod q)) := - do - let r ← PMF.uniformOfFintype (ZMod q) - return ⟨g^m.val * h^r.val, r⟩ + PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun r => return ⟨g^m.val * h^r.val, r⟩) def verify (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (h : G) (m : ZMod q) (c : G) (o : ZMod q): ZMod 2 := From dd7bd97f2c6ac869259120a50d7fd5381171ec25 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 3 Jan 2026 19:17:06 -0800 Subject: [PATCH 15/24] wip: dlog switch to bind --- VerifiedCommitments/dlog.lean | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/VerifiedCommitments/dlog.lean b/VerifiedCommitments/dlog.lean index 04b7b39..4bbb827 100644 --- a/VerifiedCommitments/dlog.lean +++ b/VerifiedCommitments/dlog.lean @@ -11,10 +11,8 @@ noncomputable section -- Modification of Attack game and advantage as specified in Boneh 10.4 to account for check between generated x and x' def attack_game (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF (ZMod q)) : PMF (ZMod 2) := -do - let x ← PMF.uniformOfFintype (ZMod q) - let x' ← A (g^x.val) - pure (if x = x' then 1 else 0) +PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun x => + PMF.bind (A (g^x.val)) (fun x' => pure (if x = x' then 1 else 0))) -- The advantage of an attacker A in the DLog problem -- attack_game returns a PMF () @@ -24,34 +22,31 @@ noncomputable def experiment (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) (A' : G → PMF (ZMod q)) : PMF (ZMod 2) := - do - let x ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2 - let h := g^x.val - let x' ← A' h - pure (if g^x'.val = h then 1 else 0) + PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun x => + PMF.bind (A' (g^x.val)) (fun x' => pure (if g^x'.val = g^x.val then 1 else 0))) noncomputable def adversary (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (q : ℕ) [NeZero q] (A : G → PMF (G × ZMod q × ZMod q × ZMod q × ZMod q)) (h : G) : PMF (ZMod q) := - do - let (_c, m, m', o, o') ← A h - if o ≠ o' then + PMF.bind (A h) (fun (_c, m, m', o, o') => + if o ≠ o' then return ((m - m') * (o' - o)⁻¹) else PMF.uniformOfFintype (ZMod q) + ) noncomputable def adversary' (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (q : ℕ) [NeZero q] (A' : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) (h : G) : PMF (ZMod q) := - do - let guess ← A' h + PMF.bind (A' h) (fun guess => if guess.o ≠ guess.o' then return ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹) else PMF.uniformOfFintype (ZMod q) + ) end end DLog From b3f90595277bc039bf0248a80f8d67eadead2325 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 3 Jan 2026 19:51:46 -0800 Subject: [PATCH 16/24] wip: change dlog to fintype rather than finset; complete nonempty instance for ZModMult --- VerifiedCommitments/ZModUtil.lean | 2 +- VerifiedCommitments/dlog.lean | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/VerifiedCommitments/ZModUtil.lean b/VerifiedCommitments/ZModUtil.lean index 3d4fa04..def9da1 100644 --- a/VerifiedCommitments/ZModUtil.lean +++ b/VerifiedCommitments/ZModUtil.lean @@ -23,4 +23,4 @@ def val {q : ℕ} [NeZero q] (a : ZModMult q) : ZMod q := a.val instance {q : ℕ} [NeZero q] : Fintype (ZModMult q) := Fintype.subtype ((Finset.univ : Finset (ZMod q)).erase 0) (by simp [Finset.mem_erase]) -instance {q : ℕ} [NeZero q] : Nonempty (ZModMult q) := sorry +instance {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] : Nonempty (ZModMult q) := ⟨⟨1, one_ne_zero⟩⟩ diff --git a/VerifiedCommitments/dlog.lean b/VerifiedCommitments/dlog.lean index 4bbb827..bdc96b0 100644 --- a/VerifiedCommitments/dlog.lean +++ b/VerifiedCommitments/dlog.lean @@ -4,6 +4,7 @@ import Mathlib.Probability.Distributions.Uniform import Mathlib.Data.ZMod.Basic import VerifiedCommitments.ProofUtils import VerifiedCommitments.CommitmentScheme +import VerifiedCommitments.ZModUtil namespace DLog @@ -20,10 +21,10 @@ def advantage (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF ( noncomputable def experiment (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) + (q : ℕ) [NeZero q] (A' : G → PMF (ZMod q)) : PMF (ZMod 2) := - PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun x => - PMF.bind (A' (g^x.val)) (fun x' => pure (if g^x'.val = g^x.val then 1 else 0))) + PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun x => + PMF.bind (A' (g^(val x).val)) (fun x' => pure (if g^x'.val = g^(val x).val then 1 else 0))) noncomputable def adversary (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] From 4b0d84df33424eda654ad1f32e2863bcbbf0bc58 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 3 Jan 2026 20:05:31 -0800 Subject: [PATCH 17/24] wip: add Fact Nat.Prime q back in where necessary --- VerifiedCommitments/PedersenScheme.lean | 6 +++--- VerifiedCommitments/dlog.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 4957160..6c28a73 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -8,14 +8,14 @@ namespace Pedersen -- Setup should definitely return h, but should there be another def hanging around that computes an a independently? -- The two alternatives below for bind in setup may have some bearing on how the binding proof progresses, unless I change the dlog definitions to match... -noncomputable def generate_a (q : ℕ) [NeZero q] : PMF (ZModMult q) := +noncomputable def generate_a (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] : PMF (ZModMult q) := PMF.uniformOfFintype (ZModMult q) noncomputable section def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : PMF G := + (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) : PMF G := PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun a => return g^(val a).val) -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) @@ -29,7 +29,7 @@ noncomputable section def scheme (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : + (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) : CommitmentScheme (ZMod q) G (ZMod q) G := { setup := setup G g q hq_prime, commit (h : G) (m : ZMod q) := commit G g q h m, diff --git a/VerifiedCommitments/dlog.lean b/VerifiedCommitments/dlog.lean index bdc96b0..6924aeb 100644 --- a/VerifiedCommitments/dlog.lean +++ b/VerifiedCommitments/dlog.lean @@ -21,7 +21,7 @@ def advantage (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF ( noncomputable def experiment (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] + (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (A' : G → PMF (ZMod q)) : PMF (ZMod 2) := PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun x => PMF.bind (A' (g^(val x).val)) (fun x' => pure (if g^x'.val = g^(val x).val then 1 else 0))) From 082f8475193404a4c7bed60c184e6308475b9bbe Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 3 Jan 2026 22:05:21 -0800 Subject: [PATCH 18/24] wip: most of a fix for pedersen binding - need to equate dlog and comp binding game distributions --- VerifiedCommitments/PedersenBinding.lean | 228 ++++++++++++++--------- 1 file changed, 144 insertions(+), 84 deletions(-) diff --git a/VerifiedCommitments/PedersenBinding.lean b/VerifiedCommitments/PedersenBinding.lean index fc6cfc6..0923615 100644 --- a/VerifiedCommitments/PedersenBinding.lean +++ b/VerifiedCommitments/PedersenBinding.lean @@ -3,99 +3,159 @@ import Mathlib.Tactic namespace Pedersen +-- Helper lemma: if binding succeeds, then either o = o' or we can extract the discrete log +lemma binding_implies_dlog + (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) + (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) + (G_card_q : Fintype.card G = q) + (hg_gen : orderOf g = Fintype.card G) + (a : ZMod q) (guess : Adversary.guess (ZMod q) G (ZMod q)) : + let h := g ^ a.val + let verify := fun (m : ZMod q) (c : G) (o : ZMod q) => if c = 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' → g^(((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val) = h) := by + intro h verify ⟨h1, h2, m_ne⟩ o_ne + -- From h1: guess.c = g^(guess.m).val * h^(guess.o).val + -- From h2: guess.c = g^(guess.m').val * h^(guess.o').val + simp only [verify] at h1 h2 + split at h1 <;> split at h2 + case' isTrue.isTrue c_eq1 c_eq2 => + -- We have: g^m.val * h^o.val = g^m'.val * h^o'.val + -- Substituting h = g^a.val: + -- g^m.val * g^(a.val * o.val) = g^m'.val * g^(a.val * o'.val) + -- g^(m.val + a.val * o.val) = g^(m'.val + a.val * o'.val) + + simp only [h] at c_eq1 c_eq2 + -- c_eq1: guess.c = g ^ guess.m.val * (g ^ a.val) ^ guess.o.val + -- c_eq2: guess.c = g ^ guess.m'.val * (g ^ a.val) ^ guess.o'.val + + have collision : g^guess.m.val * (g^a.val)^guess.o.val = g^guess.m'.val * (g^a.val)^guess.o'.val := by + rw [← c_eq1, c_eq2] + + -- Simplify (g^a.val)^o.val to g^(a.val * o.val) + conv_lhs at collision => arg 2; rw [← pow_mul] + conv_rhs at collision => arg 2; rw [← pow_mul] + -- Combine: g^m.val * g^(a.val * o.val) = g^(m + a*o).val + rw [← pow_add, ← pow_add] at collision + + -- From collision: g^(m.val + a.val*o.val) = g^(m'.val + a.val*o'.val) + -- We need to extract a from this equation + -- Strategy: show that a = (m - m') / (o' - o) + + -- First, rearrange the equation algebraically in ZMod q: + -- m + a*o = m' + a*o' (as elements of ZMod q when viewed mod q) + -- m - m' = a*o' - a*o + -- m - m' = a*(o' - o) + -- Therefore: a = (m - m') / (o' - o) = (m - m') * (o' - o)⁻¹ + + -- Now we need to show g^(((m - m') * (o' - o)⁻¹).val) = g^a.val + + -- this is o_ne + -- have h_noo' : o' ≠ o := by exact fun a ↦ ho (id (Eq.symm a)) + have h_coprime : (guess.o - guess.o').val.Coprime q := by + cases' Nat.coprime_or_dvd_of_prime hq_prime (o' - o).val with h_cop h_dvd + · exact Nat.coprime_comm.mp h_cop + · exfalso + have h_zero : guess.o - guess.o' = 0 := by + rw [← ZMod.val_eq_zero] + have h_mod_zero : (guess.o - guess.o').val % q = 0 := Nat.mod_eq_zero_of_dvd h_dvd + have h_val_bound : (guess.o - guess.o').val < q := ZMod.val_lt (guess.o - guess.o') + exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound + exact o_ne (eq_of_sub_eq_zero h_zero) + + have h_ex_inv : ∃ y, ↑(guess.o - guess.o').val * y ≡ 1 [ZMOD q] := by apply Int.mod_coprime h_coprime + + have h_ord : orderOf g = q := by + rw [← G_card_q]; exact hg_gen + + -- this is collision + -- have h_pow : g ^ (m.val + x.val * o.val) = g ^ (m'.val + x.val * o'.val) := by + -- simp [←pow_mul, ←pow_add] at h2 + -- exact h2 + + have h_congr_nat : guess.m.val + a.val * guess.o.val ≡ guess.m'.val + a.val * guess.o'.val [MOD q] := by + simpa [h_ord] using (pow_eq_pow_iff_modEq.mp collision) + + have h_zmod : (guess.m + a * guess.o : ZMod q) = (guess.m' + a * guess.o' : ZMod q) := by + have eq_cast : ((guess.m.val + a.val * guess.o.val : ℕ) : ZMod q) = + ((guess.m'.val + a.val * guess.o'.val : ℕ) : ZMod q) := + (ZMod.eq_iff_modEq_nat _).mpr h_congr_nat + simp at eq_cast + exact eq_cast + + have h_lin : a * (guess.o' - guess.o) = guess.m - guess.m' := by grind + + have h_unit : guess.o' - guess.o ≠ 0 := sub_ne_zero.mpr o_ne.symm + + have h_solve_x : a = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ := by + calc a = a * 1 := by rw [mul_one] + _ = a * ((guess.o' - guess.o) * (guess.o' - guess.o)⁻¹) := by + haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ + rw [← one_mul a] + congr 1 + have h_field_inv : (guess.o' - guess.o) * (guess.o' - guess.o)⁻¹ = 1 := by + apply Field.mul_inv_cancel + exact h_unit + exact h_field_inv.symm + _ = (a * (guess.o' - guess.o)) * (guess.o' - guess.o)⁻¹ := by rw [mul_assoc] + _ = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ := by rw [h_lin] + + have h_congr_final : ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val ≡ a.val [MOD q] := by + have h1 : (((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val : ZMod q) = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ := + ZMod.natCast_zmod_val ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹) + have h2 : (a.val : ZMod q) = a := ZMod.natCast_zmod_val a + rw [← ZMod.eq_iff_modEq_nat] + rw [h1, h2] + exact h_solve_x.symm + + have h_eq : g ^ ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val = g ^ a.val := + (pow_eq_pow_iff_modEq.mpr (by rwa [h_ord])) + + rw [h_eq] + all_goals contradiction + lemma binding_as_hard_dlog (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) (G_card_q : Fintype.card G = q) (hg_gen : orderOf g = Fintype.card G) (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) : - Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q hq_prime (DLog.adversary' G q A) 1 := by - simp only [DLog.experiment, Commitment.comp_binding_game', Pedersen.scheme, DLog.adversary'] - simp only [bind_pure_comp, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not, ne_eq, - bind_map_left, ite_not, map_bind] - congr! 5 with x ⟨c, m, m', o, o'⟩ - simp - split_ifs - · sorry -- this is a case I want to skip - rename_i ho - rename_i h - obtain ⟨h1, h2, h3⟩ := h - rw [h1] at h2 - simp only [map_pure] - have h_noo' : o' ≠ o := by exact fun a ↦ ho (id (Eq.symm a)) - have h_coprime : (o' - o).val.Coprime q := by - cases' Nat.coprime_or_dvd_of_prime hq_prime (o' - o).val with h_cop h_dvd - · exact Nat.coprime_comm.mp h_cop - · exfalso - have h_zero : o' - o = 0 := by - rw [← ZMod.val_eq_zero] - have h_mod_zero : (o' - o).val % q = 0 := Nat.mod_eq_zero_of_dvd h_dvd - have h_val_bound : (o' - o).val < q := ZMod.val_lt (o' - o) - exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound - exact h_noo' (eq_of_sub_eq_zero h_zero) - - have h_ex_inv : ∃ y, ↑(o' - o).val * y ≡ 1 [ZMOD q] := by apply Int.mod_coprime h_coprime - - have h_ord : orderOf g = q := by - rw [← G_card_q]; exact hg_gen - - have h_pow : g ^ (m.val + x.val * o.val) = g ^ (m'.val + x.val * o'.val) := by - simp [←pow_mul, ←pow_add] at h2 - exact h2 - - have h_congr_nat : m.val + x.val * o.val ≡ m'.val + x.val * o'.val [MOD q] := by - simpa [h_ord] using (pow_eq_pow_iff_modEq.mp h_pow) - - have h_zmod : (m + x * o : ZMod q) = (m' + x * o' : ZMod q) := by - have eq_cast : ((m.val + x.val * o.val : ℕ) : ZMod q) = - ((m'.val + x.val * o'.val : ℕ) : ZMod q) := - (ZMod.eq_iff_modEq_nat _).mpr h_congr_nat - simp at eq_cast - exact eq_cast - - have h_lin : x * (o' - o) = m - m' := by grind - - have h_unit : o' - o ≠ 0 := sub_ne_zero.mpr h_noo' - - have h_solve_x : x = (m - m') * (o' - o)⁻¹ := by - calc x = x * 1 := by rw [mul_one] - _ = x * ((o' - o) * (o' - o)⁻¹) := by - haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ - rw [← one_mul x] - congr 1 - have h_field_inv : (o' - o) * (o' - o)⁻¹ = 1 := by - apply Field.mul_inv_cancel - exact h_unit - exact h_field_inv.symm - _ = (x * (o' - o)) * (o' - o)⁻¹ := by rw [mul_assoc] - _ = (m - m') * (o' - o)⁻¹ := by rw [h_lin] - - have h_congr_final : ((m - m') * (o' - o)⁻¹).val ≡ x.val [MOD q] := by - have h1 : (((m - m') * (o' - o)⁻¹).val : ZMod q) = (m - m') * (o' - o)⁻¹ := - ZMod.natCast_zmod_val ((m - m') * (o' - o)⁻¹) - have h2 : (x.val : ZMod q) = x := ZMod.natCast_zmod_val x - rw [← ZMod.eq_iff_modEq_nat] - rw [h1, h2] - exact h_solve_x.symm - - have h_eq : g ^ ((m - m') * (o' - o)⁻¹).val = g ^ x.val := - (pow_eq_pow_iff_modEq.mpr (by rwa [h_ord])) - - rw [h_eq] - simp only [↓reduceIte] - · sorry -- cases I want to skip - · sorry - - -theorem Pedersen.computational_binding : + haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩; + Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q (DLog.adversary' G q A) 1 := by + haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ + -- Unfold definitions + unfold Commitment.comp_binding_game' DLog.experiment DLog.adversary' + simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify] + + -- Both games now sample from PMF.uniformOfFintype (ZModMult q) + -- LHS: Pr[a ← ZModMult q; guess ← A(g^a); binding succeeds] + -- RHS: Pr[a ← ZModMult q; guess ← A(g^a); adversary' extracts a correctly] + + -- The LHS sums over G, but only elements of the form g^a for a ∈ ZModMult q have nonzero weight + -- The RHS sums over ZModMult q directly + + -- Strategy: Show that for each a ∈ ZModMult q and each guess from A(g^a): + -- if binding succeeds with o ≠ o', then adversary' extracts a correctly + -- if binding succeeds with o = o', we get a contradiction (m = m') + -- Therefore: Pr[binding succeeds] ≤ Pr[adversary' extracts a] + + -- The key challenge is that we need to massage the LHS to sum over ZModMult q + -- instead of G, using the fact that only g^a values have nonzero probability. + + sorry + + +theorem computational_binding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) (ε : ENNReal) + (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] [Fact (Nat.Prime q)] (ε : ENNReal) (G_card_q : Fintype.card G = q) (hg_gen : orderOf g = Fintype.card G), - (∀ (A : G → PMF (ZMod q)), DLog.experiment G g q hq_prime A 1 ≤ ε) → + (∀ (A : G → PMF (ZMod q)), DLog.experiment G g q A 1 ≤ ε) → (∀ (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))), - Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by - intro G _ _ _ _ g q _ _ hq_prime ε G_card_q hg_gen hdlog A - exact le_trans (binding_as_hard_dlog G g q hq_prime ε G_card_q hg_gen A) (hdlog (DLog.adversary' G q A)) + ∃ hq_prime : Nat.Prime q, Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by + intro G _ _ _ _ g q _ _ _ ε G_card_q hg_gen hdlog A + have hq_prime := Fact.out (p := Nat.Prime q) + use hq_prime + exact le_trans (binding_as_hard_dlog G g q hq_prime G_card_q hg_gen A) (hdlog (DLog.adversary' G q A)) end Pedersen From c9e47699bcaf7647b896549c2b37cb0e40c812c8 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Mon, 5 Jan 2026 16:22:59 -0800 Subject: [PATCH 19/24] fix: import fix --- VerifiedCommitments/PedersenScheme.lean | 2 +- VerifiedCommitments/dlog.lean | 8 +------- 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 6c28a73..0eda1de 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -1,5 +1,5 @@ import VerifiedCommitments.CommitmentScheme -import VerifiedCommitments.dlog +import Mathlib.Probability.Distributions.Uniform import VerifiedCommitments.ZModUtil namespace Pedersen diff --git a/VerifiedCommitments/dlog.lean b/VerifiedCommitments/dlog.lean index 6924aeb..de002a0 100644 --- a/VerifiedCommitments/dlog.lean +++ b/VerifiedCommitments/dlog.lean @@ -1,10 +1,4 @@ -import Mathlib.Probability.ProbabilityMassFunction.Basic -import Mathlib.Probability.ProbabilityMassFunction.Monad -import Mathlib.Probability.Distributions.Uniform -import Mathlib.Data.ZMod.Basic -import VerifiedCommitments.ProofUtils -import VerifiedCommitments.CommitmentScheme -import VerifiedCommitments.ZModUtil +import VerifiedCommitments.PedersenScheme namespace DLog From 9cad454bf3e3653fc5e6cf3c12c7642a33e213ea Mon Sep 17 00:00:00 2001 From: ashandoak Date: Mon, 5 Jan 2026 17:19:33 -0800 Subject: [PATCH 20/24] wip: change setup from PMF K to PMF K O --- VerifiedCommitments/CommitmentScheme.lean | 14 ++++++------ VerifiedCommitments/PedersenBinding.lean | 28 +++++++++++------------ VerifiedCommitments/PedersenScheme.lean | 4 ++-- VerifiedCommitments/dlog.lean | 9 +++++--- 4 files changed, 28 insertions(+), 27 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index e9206c7..45596e7 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -10,7 +10,7 @@ import Mathlib.Data.ZMod.Defs -- o : O structure CommitmentScheme (M C O K : Type) where - setup : PMF K + setup : PMF (K × O) commit : K → M → PMF (C × O) verify : K → M → C → O → ZMod 2 @@ -52,8 +52,8 @@ def comp_binding_game (scheme : CommitmentScheme M C O K) (A : K → PMF (C × M × M × O × O)) : PMF $ ZMod 2 := open scoped Classical in PMF.bind scheme.setup (fun h => - PMF.bind (A h) (fun (c, m , m', o, o') => - if scheme.verify h m c o = 1 ∧ scheme.verify h m' c o' = 1 ∧ m ≠ m' then pure 1 else pure 0 )) + PMF.bind (A h.1) (fun (c, m , m', o, o') => + if scheme.verify h.1 m c o = 1 ∧ scheme.verify h.1 m' c o' = 1 ∧ m ≠ m' then pure 1 else pure 0 )) def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop := ∀ (A : K → PMF (C × M × M × O × O)), comp_binding_game scheme A 1 ≤ ε @@ -63,8 +63,8 @@ def comp_binding_game' (scheme : CommitmentScheme M C O K) (A' : K → PMF (Adversary.guess 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 )) + 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 )) def computational_binding' [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop := ∀ (A' : K → PMF (Adversary.guess M C O )), comp_binding_game' scheme A' 1 ≤ ε @@ -73,7 +73,7 @@ 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 m) (fun commit => pure commit.1)) + PMF.bind (scheme.commit h.1 m) (fun commit => pure commit.1)) 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 @@ -82,7 +82,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.1 m) (fun commit => A h.1 commit.1)) def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop := ∀ (A : K → C → PMF (ZMod 2)) (m₀ m₁ : M), diff --git a/VerifiedCommitments/PedersenBinding.lean b/VerifiedCommitments/PedersenBinding.lean index 0923615..8b359ff 100644 --- a/VerifiedCommitments/PedersenBinding.lean +++ b/VerifiedCommitments/PedersenBinding.lean @@ -1,4 +1,5 @@ import VerifiedCommitments.PedersenScheme +import VerifiedCommitments.dlog import Mathlib.Tactic namespace Pedersen @@ -52,18 +53,18 @@ lemma binding_implies_dlog -- this is o_ne -- have h_noo' : o' ≠ o := by exact fun a ↦ ho (id (Eq.symm a)) - have h_coprime : (guess.o - guess.o').val.Coprime q := by - cases' Nat.coprime_or_dvd_of_prime hq_prime (o' - o).val with h_cop h_dvd + have h_coprime : (guess.o' - guess.o).val.Coprime q := by + cases' Nat.coprime_or_dvd_of_prime hq_prime (guess.o' - guess.o).val with h_cop h_dvd · exact Nat.coprime_comm.mp h_cop · exfalso - have h_zero : guess.o - guess.o' = 0 := by + have h_zero : guess.o' - guess.o = 0 := by rw [← ZMod.val_eq_zero] - have h_mod_zero : (guess.o - guess.o').val % q = 0 := Nat.mod_eq_zero_of_dvd h_dvd - have h_val_bound : (guess.o - guess.o').val < q := ZMod.val_lt (guess.o - guess.o') + have h_mod_zero : (guess.o' - guess.o).val % q = 0 := Nat.mod_eq_zero_of_dvd h_dvd + have h_val_bound : (guess.o' - guess.o).val < q := ZMod.val_lt (guess.o' - guess.o) exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound - exact o_ne (eq_of_sub_eq_zero h_zero) + exact o_ne.symm (eq_of_sub_eq_zero h_zero) - have h_ex_inv : ∃ y, ↑(guess.o - guess.o').val * y ≡ 1 [ZMOD q] := by apply Int.mod_coprime h_coprime + have h_ex_inv : ∃ y, ↑(guess.o' - guess.o).val * y ≡ 1 [ZMOD q] := by apply Int.mod_coprime h_coprime have h_ord : orderOf g = q := by rw [← G_card_q]; exact hg_gen @@ -119,9 +120,9 @@ lemma binding_as_hard_dlog (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) (G_card_q : Fintype.card G = q) (hg_gen : orderOf g = Fintype.card G) - (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) : + (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) : -- Pedersen adversary haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩; - Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q (DLog.adversary' G q A) 1 := by + Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q hq_prime (DLog.adversary' G q A) 1 := by haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ -- Unfold definitions unfold Commitment.comp_binding_game' DLog.experiment DLog.adversary' @@ -147,15 +148,12 @@ lemma binding_as_hard_dlog theorem computational_binding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] [Fact (Nat.Prime q)] (ε : ENNReal) + (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] [Fact (Nat.Prime q)] (hq_prime : (Nat.Prime q)) (ε : ENNReal) (G_card_q : Fintype.card G = q) (hg_gen : orderOf g = Fintype.card G), - (∀ (A : G → PMF (ZMod q)), DLog.experiment G g q A 1 ≤ ε) → + (∀ (A : G → PMF (ZMod q)), DLog.experiment G g q hq_prime A 1 ≤ ε) → (∀ (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))), ∃ hq_prime : Nat.Prime q, Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by - intro G _ _ _ _ g q _ _ _ ε G_card_q hg_gen hdlog A - have hq_prime := Fact.out (p := Nat.Prime q) - use hq_prime + intro G _ _ _ _ g q _ _ _ hq_prime ε G_card_q hg_gen hdlog A exact le_trans (binding_as_hard_dlog G g q hq_prime G_card_q hg_gen A) (hdlog (DLog.adversary' G q A)) - end Pedersen diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 0eda1de..f78a6e0 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -15,8 +15,8 @@ noncomputable def generate_a (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] : PMF (ZM noncomputable section def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) : PMF G := - PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun a => return g^(val a).val) + (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) : PMF (G × (ZMod q)) := + PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun a => return ⟨g^(val a).val, val a⟩) -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) diff --git a/VerifiedCommitments/dlog.lean b/VerifiedCommitments/dlog.lean index de002a0..60fe676 100644 --- a/VerifiedCommitments/dlog.lean +++ b/VerifiedCommitments/dlog.lean @@ -13,12 +13,15 @@ PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun x => -- attack_game returns a PMF () def advantage (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF (ZMod q)) : ENNReal := attack_game G q g A 1 +#check Pedersen.scheme noncomputable def experiment (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] + (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) (A' : G → PMF (ZMod q)) : PMF (ZMod 2) := - PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun x => - PMF.bind (A' (g^(val x).val)) (fun x' => pure (if g^x'.val = g^(val x).val then 1 else 0))) + PMF.bind (Pedersen.scheme G g q hq_prime).setup (fun h => + PMF.bind (A' h.1) (fun x' => pure (if g^x'.val = g^(h.2).val then 1 else 0))) + -- PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun x => + -- PMF.bind (A' (g^(val x).val)) (fun x' => pure (if g^x'.val = g^(val x).val then 1 else 0))) noncomputable def adversary (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] From 7d2b97e6083c45ccc3d222d276fc494ca25eca65 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 6 Jan 2026 21:30:24 -0800 Subject: [PATCH 21/24] feat: fix binding --- VerifiedCommitments/PedersenBinding.lean | 186 ++++++++++++++++++----- 1 file changed, 144 insertions(+), 42 deletions(-) diff --git a/VerifiedCommitments/PedersenBinding.lean b/VerifiedCommitments/PedersenBinding.lean index 8b359ff..aaee00e 100644 --- a/VerifiedCommitments/PedersenBinding.lean +++ b/VerifiedCommitments/PedersenBinding.lean @@ -1,6 +1,7 @@ import VerifiedCommitments.PedersenScheme import VerifiedCommitments.dlog import Mathlib.Tactic +import VerifiedCommitments.«scratch-skip-bind» namespace Pedersen @@ -21,38 +22,15 @@ lemma binding_implies_dlog simp only [verify] at h1 h2 split at h1 <;> split at h2 case' isTrue.isTrue c_eq1 c_eq2 => - -- We have: g^m.val * h^o.val = g^m'.val * h^o'.val - -- Substituting h = g^a.val: - -- g^m.val * g^(a.val * o.val) = g^m'.val * g^(a.val * o'.val) - -- g^(m.val + a.val * o.val) = g^(m'.val + a.val * o'.val) - simp only [h] at c_eq1 c_eq2 - -- c_eq1: guess.c = g ^ guess.m.val * (g ^ a.val) ^ guess.o.val - -- c_eq2: guess.c = g ^ guess.m'.val * (g ^ a.val) ^ guess.o'.val have collision : g^guess.m.val * (g^a.val)^guess.o.val = g^guess.m'.val * (g^a.val)^guess.o'.val := by rw [← c_eq1, c_eq2] - -- Simplify (g^a.val)^o.val to g^(a.val * o.val) conv_lhs at collision => arg 2; rw [← pow_mul] conv_rhs at collision => arg 2; rw [← pow_mul] - -- Combine: g^m.val * g^(a.val * o.val) = g^(m + a*o).val rw [← pow_add, ← pow_add] at collision - -- From collision: g^(m.val + a.val*o.val) = g^(m'.val + a.val*o'.val) - -- We need to extract a from this equation - -- Strategy: show that a = (m - m') / (o' - o) - - -- First, rearrange the equation algebraically in ZMod q: - -- m + a*o = m' + a*o' (as elements of ZMod q when viewed mod q) - -- m - m' = a*o' - a*o - -- m - m' = a*(o' - o) - -- Therefore: a = (m - m') / (o' - o) = (m - m') * (o' - o)⁻¹ - - -- Now we need to show g^(((m - m') * (o' - o)⁻¹).val) = g^a.val - - -- this is o_ne - -- have h_noo' : o' ≠ o := by exact fun a ↦ ho (id (Eq.symm a)) have h_coprime : (guess.o' - guess.o).val.Coprime q := by cases' Nat.coprime_or_dvd_of_prime hq_prime (guess.o' - guess.o).val with h_cop h_dvd · exact Nat.coprime_comm.mp h_cop @@ -64,16 +42,9 @@ lemma binding_implies_dlog exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound exact o_ne.symm (eq_of_sub_eq_zero h_zero) - have h_ex_inv : ∃ y, ↑(guess.o' - guess.o).val * y ≡ 1 [ZMOD q] := by apply Int.mod_coprime h_coprime - have h_ord : orderOf g = q := by rw [← G_card_q]; exact hg_gen - -- this is collision - -- have h_pow : g ^ (m.val + x.val * o.val) = g ^ (m'.val + x.val * o'.val) := by - -- simp [←pow_mul, ←pow_add] at h2 - -- exact h2 - have h_congr_nat : guess.m.val + a.val * guess.o.val ≡ guess.m'.val + a.val * guess.o'.val [MOD q] := by simpa [h_ord] using (pow_eq_pow_iff_modEq.mp collision) @@ -128,22 +99,152 @@ lemma binding_as_hard_dlog unfold Commitment.comp_binding_game' DLog.experiment DLog.adversary' simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify] - -- Both games now sample from PMF.uniformOfFintype (ZModMult q) - -- LHS: Pr[a ← ZModMult q; guess ← A(g^a); binding succeeds] - -- RHS: Pr[a ← ZModMult q; guess ← A(g^a); adversary' extracts a correctly] + -- Expand the bind applications + rw [PMF.bind_apply, PMF.bind_apply] + + -- Both sum over the same type: G × ZMod q (the pairs from setup) + -- We need pointwise inequality + apply ENNReal.tsum_le_tsum + intro ⟨h, a⟩ + + -- Key observation: setup only returns pairs (g^x.val, x) + -- So if h ≠ g^a.val, the probability of this pair is 0 and inequality holds trivially + by_cases h_case : h = g^a.val + + · -- Case: h = g^a.val (pair is in support of setup) + subst h_case -- Replace h with g^a.val everywhere + + -- Now we have h = g^a.val as needed! + apply mul_le_mul_right + + -- Now compare the inner probabilities + -- Continue with the proof that was already working + -- First, use bind associativity on RHS to flatten the nested binds + conv_rhs => rw [PMF.bind_bind] + + -- Now both have structure: (A (g^a.val)).bind (fun guess => ...) 1 + -- Expand the bind application + rw [PMF.bind_apply, PMF.bind_apply] + + -- Now both are sums over Adversary.guess + apply ENNReal.tsum_le_tsum + intro guess + + apply mul_le_mul_right + + -- For each guess, show: + -- (if [binding succeeds] then pure 1 else pure 0) 1 ≤ + -- ((if o≠o' then pure x' else uniform).bind (λ x'. pure (if g^x'=g^a then 1 else 0))) 1 + + 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) AND h₂ (o = o') + -- This is the contradiction case: o = o' but binding succeeds + exfalso + obtain ⟨eq1, eq2, m_ne⟩ := h₁ + -- Since h₂: o = o', we have (g^a.val)^o.val = (g^a.val)^o'.val + have ho_eq : (g^a.val)^guess.o.val = (g^a.val)^guess.o'.val := by + rw [h₂] + -- So: g^m.val * (g^a.val)^o.val = g^m'.val * (g^a.val)^o.val + have collision : g^guess.m.val * (g^a.val)^guess.o.val = g^guess.m'.val * (g^a.val)^guess.o.val := by + calc g^guess.m.val * (g^a.val)^guess.o.val + = guess.c := eq1.symm + _ = g^guess.m'.val * (g^a.val)^guess.o'.val := eq2 + _ = g^guess.m'.val * (g^a.val)^guess.o.val := by rw [← ho_eq] + -- Cancel (g^a.val)^o.val from both sides + have g_eq : g^guess.m.val = g^guess.m'.val := mul_right_cancel collision + -- Since g is a generator, this means m.val ≡ m'.val (mod q) + have h_ord : orderOf g = q := by rw [← G_card_q]; exact hg_gen + have h_congr : guess.m.val ≡ guess.m'.val [MOD q] := by + simpa [h_ord] using (pow_eq_pow_iff_modEq.mp g_eq) + -- Therefore m = m' in ZMod q + have m_eq : guess.m = guess.m' := by + have eq_cast : ((guess.m.val : ℕ) : ZMod q) = ((guess.m'.val : ℕ) : ZMod q) := + ZMod.natCast_eq_natCast_iff guess.m.val guess.m'.val q |>.mpr h_congr + simp at eq_cast + exact eq_cast + exact m_ne m_eq + + · -- Case 2: Binding succeeds (h₁) AND o ≠ o' (¬h₂) + -- This is the main case where we use binding_implies_dlog + have h_o_ne : guess.o ≠ guess.o' := h₂ + let x' := (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ + + -- Convert h₁ to the form expected by binding_implies_dlog + have h₁' : (let h := g^a.val; + let verify := fun m c o => if c = 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 + obtain ⟨eq1, eq2, m_ne⟩ := h₁ + simp only [] + refine ⟨?_, ?_, m_ne⟩ + · split + · rfl + · contradiction + · split + · rfl + · contradiction + + -- By binding_implies_dlog, g^x'.val = g^a.val + have h_dlog : g^x'.val = g^a.val := by + apply binding_implies_dlog G g q hq_prime G_card_q hg_gen a guess h₁' h_o_ne - -- The LHS sums over G, but only elements of the form g^a for a ∈ ZModMult q have nonzero weight - -- The RHS sums over ZModMult q directly + -- The RHS is a sum over a single-element distribution (pure x') + -- The sum includes the term for x = x', which equals 1 + have h_term : (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 1 := by + rw [PMF.pure_apply, PMF.pure_apply] + simp only [h_dlog] + norm_num + have h_zero : ∀ x ∈ Finset.univ, x ∉ ({x'} : Finset (ZMod q)) → + (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 0 := by + intros x _ hx + rw [PMF.pure_apply] + simp only [Finset.mem_singleton] at hx + simp [hx] + have h_sum_ge : (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) ≤ + ∑ x, (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := by + rw [← Finset.sum_subset (Finset.subset_univ {x'}) h_zero] + simp only [Finset.sum_singleton] + rfl + calc (PMF.pure (1 : ZMod 2)) (1 : ZMod 2) + = 1 := by rw [PMF.pure_apply]; norm_num + _ = (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_term.symm + _ ≤ ∑ x, (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_sum_ge - -- Strategy: Show that for each a ∈ ZModMult q and each guess from A(g^a): - -- if binding succeeds with o ≠ o', then adversary' extracts a correctly - -- if binding succeeds with o = o', we get a contradiction (m = m') - -- Therefore: Pr[binding succeeds] ≤ Pr[adversary' extracts a] + · -- Case 3: Binding fails (¬h₁) AND o = o' (h✝) + show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _ + rw [PMF.pure_apply] + norm_num - -- The key challenge is that we need to massage the LHS to sum over ZModMult q - -- instead of G, using the fact that only g^a values have nonzero probability. + · -- Case 4: Binding fails (¬h₁) AND o ≠ o' (¬h✝) + show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _ + rw [PMF.pure_apply] + norm_num - sorry + · -- Case neg: h ≠ g^a.val (pair is NOT in support) + -- Setup only returns pairs of the form (g^x.val, x) + -- So if h ≠ g^a.val, then (h, a) has probability 0 in the setup distribution + -- Therefore both sides are 0 * something = 0, and 0 ≤ 0 + have h_prob_zero : ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) = 0 := by + rw [PMF.bind_apply, tsum_fintype] + apply Finset.sum_eq_zero + intros a_mult _ + rw [PMF.pure_apply, PMF.uniformOfFintype_apply] + split_ifs with h_eq + · -- If (h, a) = (g^(val a_mult).val, val a_mult) + -- Then h = g^(val a_mult).val and a = val a_mult + exfalso + have eq_h : h = g^(val a_mult).val := (Prod.mk.injEq _ _ _ _).mp h_eq |>.1 + have eq_a : a = val a_mult := (Prod.mk.injEq _ _ _ _).mp h_eq |>.2 + rw [← eq_a] at eq_h + exact h_case eq_h + · simp + change ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) * _ ≤ + ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) * _ + rw [h_prob_zero] + simp only [zero_mul, le_refl] theorem computational_binding : @@ -155,5 +256,6 @@ theorem computational_binding : (∀ (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))), ∃ hq_prime : Nat.Prime q, Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by intro G _ _ _ _ g q _ _ _ hq_prime ε G_card_q hg_gen hdlog A + use hq_prime exact le_trans (binding_as_hard_dlog G g q hq_prime G_card_q hg_gen A) (hdlog (DLog.adversary' G q A)) end Pedersen From a51a84ba3f80388e5539918b5c07999c8c55c3fd Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 6 Jan 2026 21:30:41 -0800 Subject: [PATCH 22/24] wip: hiding in progress - but cycle? --- VerifiedCommitments/PedersenHiding.lean | 40 +++++++++++++------------ 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index cac1380..cad7feb 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -184,36 +184,37 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) : intro a · expose_names; exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m --- 5 --- 1, 2 -> 5 +-- 3 +-- 1, 2 -> 3 lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) : PMF.bind (generate_a q) - (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = -- this line = PMF.uniformOfFintype G by (2) bij_uniform_for_uniform_a + (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = PMF.map Prod.fst (PMF.bind (generate_a q) (fun a => (Pedersen.commit G g q (g^(val a).val) m))) := by simp only [bij_uniform_for_uniform_a q G_card_q g g_gen_G m] unfold Pedersen.commit generate_a simp only [PMF.map_bind] - simp only [bind_pure_comp] - ext c rw [bind_skip_const'] intro a + have h_bind_eq : PMF.bind (PMF.uniformOfFintype (ZMod q)) + (fun r => PMF.map Prod.fst (pure (g^m.val * (g^(val a).val)^r.val, r))) = + PMF.bind (PMF.uniformOfFintype (ZMod q)) + (fun r => PMF.pure (g^m.val * (g^(val a).val)^r.val)) := by + apply bind_skip' + intro r + simp only [pure, PMF.pure_map] + rw [h_bind_eq] conv_lhs => arg 2 - arg 1 ext r + arg 1 rw [← expEquiv_unfold q G_card_q g g_gen_G a m r] - - rw [← PMF.monad_map_eq_map] - simp only [Functor.map_map] - - show PMF.map (fun r ↦ Prod.fst ((expEquiv q G_card_q g g_gen_G a m) r, r)) (PMF.uniformOfFintype (ZMod q)) = PMF.uniformOfFintype G - simp only + rw [← bind_eq_map'] exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m --- 6 --- 5, 2 -> 6 +-- 4 +-- 3, 2 -> 6 lemma pedersen_commitment_uniform (m : ZMod q) (c : G) : (PMF.map Prod.fst ((PMF.bind (generate_a q) (fun a => Pedersen.commit G g q (g^(val a).val) m ))) c) = @@ -229,18 +230,19 @@ theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) (G_card_q : Fintype.card G = q) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g), - Commitment.perfect_hiding (Pedersen.scheme G g q hq_prime) := by + haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩; Commitment.perfect_hiding (Pedersen.scheme G g q hq_prime) := by intros G _ _ _ _ g q _ hq_prime G_card_q g_gen_G - have : Fact (Nat.Prime q) := ⟨hq_prime⟩ + haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ unfold Commitment.perfect_hiding intros m m' c unfold Commitment.do_commit unfold Pedersen.scheme simp unfold Pedersen.setup Pedersen.commit - simp only [bind_pure_comp, Functor.map_map] - change (PMF.bind _ _) c = (PMF.bind _ _) c + -- simp only [bind_pure_comp, Functor.map_map] -- no longer makes progress + -- change (PMF.bind _ _) c = (PMF.bind _ _) c -- goal structure changed slightly simp only [PMF.bind_apply] - rw [Pedersen.pedersen_commitment_uniform q G_card_q g g_gen_G m c] + -- rw [Pedersen.pedersen_commitment_uniform q G_card_q g g_gen_G m c] -- goal structure changed + -- The proof would continue to show both sides are uniform, hence equal sorry From 981abb82bd5a180b86b5520fb82f2f9a38a598f2 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 6 Jan 2026 21:43:22 -0800 Subject: [PATCH 23/24] wip: all hiding lemma proved --- VerifiedCommitments/PedersenHiding.lean | 41 +++++++++++++------------ 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index cad7feb..38a8c04 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -185,40 +185,42 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) : · expose_names; exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m -- 3 --- 1, 2 -> 3 +-- Direct proof without using bij_uniform_for_uniform_a lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) : PMF.bind (generate_a q) (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = PMF.map Prod.fst (PMF.bind (generate_a q) (fun a => (Pedersen.commit G g q (g^(val a).val) m))) := by - simp only [bij_uniform_for_uniform_a q G_card_q g g_gen_G m] unfold Pedersen.commit generate_a simp only [PMF.map_bind] - rw [bind_skip_const'] + -- Goal: bind uniform_a (λ a. map expEquiv uniform_r) = bind uniform_a (λ a. bind uniform_r (λ r. map Prod.fst (pure (g^..., r)))) + apply bind_skip' intro a - have h_bind_eq : PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.map Prod.fst (pure (g^m.val * (g^(val a).val)^r.val, r))) = - PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.pure (g^m.val * (g^(val a).val)^r.val)) := by - apply bind_skip' - intro r - simp only [pure, PMF.pure_map] - rw [h_bind_eq] - conv_lhs => - arg 2 - ext r - arg 1 - rw [← expEquiv_unfold q G_card_q g g_gen_G a m r] - rw [← bind_eq_map'] - exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m + -- Goal: map expEquiv uniform_r = bind uniform_r (λ r. map Prod.fst (pure (g^..., r))) + ext c + simp only [PMF.map_apply, PMF.bind_apply, pure, PMF.pure_apply, PMF.pure_map] + -- Both sides are sums, show they're equal + congr 1 + ext r + by_cases h : c = (expEquiv q G_card_q g g_gen_G a m) r + · simp only [h, ↓reduceIte] + rw [expEquiv_unfold q G_card_q g g_gen_G a m r] + simp + · simp only [h, ↓reduceIte] + have : ¬(c = g ^ m.val * (g ^ (val a).val) ^ r.val) := by + intro contra + rw [← expEquiv_unfold q G_card_q g g_gen_G a m r] at contra + exact h contra + simp [this] -- 4 --- 3, 2 -> 6 +-- 2, 3 -> 4 lemma pedersen_commitment_uniform (m : ZMod q) (c : G) : (PMF.map Prod.fst ((PMF.bind (generate_a q) (fun a => Pedersen.commit G g q (g^(val a).val) m ))) c) = ((1 : ENNReal) / (Fintype.card G)) := by + -- Rewrite using bij_random_a_equiv_pedersen_commit, then apply bij_uniform_for_uniform_a rw [← bij_random_a_equiv_pedersen_commit q G_card_q g g_gen_G m] rw [bij_uniform_for_uniform_a q G_card_q g g_gen_G m] simp [PMF.uniformOfFintype_apply] @@ -245,4 +247,5 @@ theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic -- rw [Pedersen.pedersen_commitment_uniform q G_card_q g g_gen_G m c] -- goal structure changed -- The proof would continue to show both sides are uniform, hence equal + sorry From f9b317bef2b1ed860e31717467c7cfa6fa607910 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 6 Jan 2026 21:55:59 -0800 Subject: [PATCH 24/24] feat: hiding complete --- VerifiedCommitments/PedersenHiding.lean | 93 ++++++++++++------------- 1 file changed, 45 insertions(+), 48 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 38a8c04..5657287 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -168,14 +168,11 @@ lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), intros exact rfl --- 1 lemma bij_uniform_for_fixed_a (a : ZModMult q) (m : ZMod q) : PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = (PMF.uniformOfFintype G) := by · expose_names; exact map_uniformOfFintype_equiv q G_card_q g g_gen_G (expEquiv q G_card_q g g_gen_G a m) --- 2 --- 1 -> 2 lemma bij_uniform_for_uniform_a (m : ZMod q) : (PMF.bind (generate_a q) (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)))) = (PMF.uniformOfFintype G) := by @@ -184,44 +181,33 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) : intro a · expose_names; exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m --- 3 --- Direct proof without using bij_uniform_for_uniform_a -lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) : - PMF.bind (generate_a q) - (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) = - PMF.map Prod.fst (PMF.bind (generate_a q) - (fun a => (Pedersen.commit G g q (g^(val a).val) m))) := by - unfold Pedersen.commit generate_a - simp only [PMF.map_bind] - -- Goal: bind uniform_a (λ a. map expEquiv uniform_r) = bind uniform_a (λ a. bind uniform_r (λ r. map Prod.fst (pure (g^..., r)))) - apply bind_skip' - intro a - -- Goal: map expEquiv uniform_r = bind uniform_r (λ r. map Prod.fst (pure (g^..., r))) - ext c - simp only [PMF.map_apply, PMF.bind_apply, pure, PMF.pure_apply, PMF.pure_map] - -- Both sides are sums, show they're equal - congr 1 - ext r - by_cases h : c = (expEquiv q G_card_q g g_gen_G a m) r - · simp only [h, ↓reduceIte] - rw [expEquiv_unfold q G_card_q g g_gen_G a m r] - simp - · simp only [h, ↓reduceIte] - have : ¬(c = g ^ m.val * (g ^ (val a).val) ^ r.val) := by - intro contra - rw [← expEquiv_unfold q G_card_q g g_gen_G a m r] at contra - exact h contra - simp [this] - - --- 4 --- 2, 3 -> 4 lemma pedersen_commitment_uniform (m : ZMod q) (c : G) : (PMF.map Prod.fst ((PMF.bind (generate_a q) (fun a => Pedersen.commit G g q (g^(val a).val) m ))) c) = ((1 : ENNReal) / (Fintype.card G)) := by - -- Rewrite using bij_random_a_equiv_pedersen_commit, then apply bij_uniform_for_uniform_a - rw [← bij_random_a_equiv_pedersen_commit q G_card_q g g_gen_G m] + unfold Pedersen.commit + simp only [PMF.map_bind, pure, PMF.pure_map] + have h_eq : (PMF.bind (generate_a q) + (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q)) + (fun r => PMF.pure (g^m.val * (g^(val a).val)^r.val)))) = + (PMF.bind (generate_a q) + (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)))) := by + apply bind_skip' + intro a + ext x + simp only [PMF.bind_apply, PMF.map_apply, PMF.pure_apply, PMF.uniformOfFintype_apply] + congr 1; ext r + by_cases h : x = g^m.val * (g^(val a).val)^r.val + · simp only [h, ↓reduceIte] + rw [← expEquiv_unfold q G_card_q g g_gen_G a m r] + simp + · simp only [h, ↓reduceIte] + have : x ≠ expEquiv q G_card_q g g_gen_G a m r := by + intro contra + rw [expEquiv_unfold q G_card_q g g_gen_G a m r] at contra + exact h contra + simp [this] + rw [h_eq] rw [bij_uniform_for_uniform_a q G_card_q g g_gen_G m] simp [PMF.uniformOfFintype_apply] @@ -237,15 +223,26 @@ theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ unfold Commitment.perfect_hiding intros m m' c - unfold Commitment.do_commit - unfold Pedersen.scheme - simp + unfold Commitment.do_commit Pedersen.scheme + simp only [] unfold Pedersen.setup Pedersen.commit - -- simp only [bind_pure_comp, Functor.map_map] -- no longer makes progress - -- change (PMF.bind _ _) c = (PMF.bind _ _) c -- goal structure changed slightly - simp only [PMF.bind_apply] - - -- rw [Pedersen.pedersen_commitment_uniform q G_card_q g g_gen_G m c] -- goal structure changed - -- The proof would continue to show both sides are uniform, hence equal - - sorry + simp only [PMF.bind_bind] + have h_lhs : ((PMF.uniformOfFintype (ZModMult q)).bind fun a => + PMF.bind (pure (g^(val a).val, val a)) fun h => + (PMF.uniformOfFintype (ZMod q)).bind fun r => + PMF.bind (pure (g^m.val * h.1^r.val, r)) fun commit => + pure commit.1) c = 1 / Fintype.card G := by + simp only [pure, PMF.pure_bind] + convert pedersen_commitment_uniform q G_card_q g g_gen_G m c using 2 + unfold generate_a Pedersen.commit + simp only [PMF.map_bind, pure, PMF.pure_map] + have h_rhs : ((PMF.uniformOfFintype (ZModMult q)).bind fun a => + PMF.bind (pure (g^(val a).val, val a)) fun h => + (PMF.uniformOfFintype (ZMod q)).bind fun r => + PMF.bind (pure (g^m'.val * h.1^r.val, r)) fun commit => + pure commit.1) c = 1 / Fintype.card G := by + simp only [pure, PMF.pure_bind] + convert pedersen_commitment_uniform q G_card_q g g_gen_G m' c using 2 + unfold generate_a Pedersen.commit + simp only [PMF.map_bind, pure, PMF.pure_map] + rw [h_lhs, h_rhs]