From 77668f85b3cb22b1325695cc7227ceb0d8e986e0 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 25 Nov 2025 20:57:15 -0800 Subject: [PATCH 01/15] wip: add bijection equiv to get access to inverse --- VerifiedCommitments/PedersenHiding.lean | 44 +++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index d680f60..9bf3b72 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -53,6 +53,48 @@ lemma exp_bij (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod q rw [←ZMod.cast_eq_val] at h_pow -- Transfer ↑ and .val back to .cast exact Exists.intro (r) h_pow +lemma exp_bij' (a : ZMod q) (ha : (a.val : ZMod q) ≠ 0) (m : ZMod q) : Function.Bijective fun (r : ZMod q) => g^((m + a.val * r : ZMod q).val : ℤ) := by + apply (Fintype.bijective_iff_surjective_and_card _).mpr + simp [G_card_q] + intro c --So take any cc ∈ GG + obtain ⟨k, hk⟩ := g_gen_G c + simp only at hk + simp only + + let z : ZMod q := (k : ZMod q) -- Since g is a generator we have c = g^z for some z ∈ Zq + have hk' : g ^ (z.val : ℤ) = c := by + rw [←hk] + simp only [ZMod.natCast_val] + rw [ZMod.coe_intCast] + rw [← G_card_q] + rw [@zpow_mod_card] + + -- we need g^m+a^r = g^z + -- This is the case iff m + ar ≡ z (mod q) + -- This is the case iff t ≡ a^−1 * (z − m) (mod q) + let a_unit := Units.mk0 (a.val : ZMod q) ha + let r : ZMod q := (a_unit⁻¹ : ZMod q) * (z - m) + have h_mod : (m + a_unit * r) = z := by + subst r + rw [IsUnit.mul_inv_cancel_left (Exists.intro a_unit rfl) (z - m)] + simp + + have h_pow : g^((m + a_unit * r).val : ℤ) = c := by + rw [←hk'] + subst r + rw [h_mod] + + rw [←ZMod.cast_eq_val] at h_pow -- Transfer ↑ and .val back to .cast + sorry + --exact Exists.intro (r) h_pow + + +noncomputable def expEquiv (a : ZMod q) (ha : (a.val : ZMod q) ≠ 0) (m : ZMod q) : ZMod q ≃ G := +Equiv.ofBijective (fun (r : ZMod q) => g^((m + (a.val) * r : ZMod q).val : ℤ)) (exp_bij' q G_card_q g g_gen_G a ha m) + +variable (a' : ZMod q) (ha' : (a'.val : ZMod q) ≠ 0) (m' : ZMod q) +#check (expEquiv q G_card_q g g_gen_G a' ha' m').invFun + lemma pedersen_uniform_for_fixed_a {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) : (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c }) / (Finset.card ( (⊤ : Finset G) ) : ℚ) @@ -76,6 +118,8 @@ lemma pedersen_uniform_for_fixed_a rw [h_card] exact rfl + + lemma pedersen_uniform_for_fixed_a' {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) : Finset.card { r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val } = 1 := by From aca2b33789ac9ae5fd3a5e3e4d15b7a3ed136dc4 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 25 Nov 2025 21:49:20 -0800 Subject: [PATCH 02/15] wip: refactor fixed_a proofs to use Equiv --- VerifiedCommitments/PedersenHiding.lean | 141 ++++++++++-------------- 1 file changed, 61 insertions(+), 80 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 9bf3b72..e98f1d5 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -22,38 +22,8 @@ lemma ordg_eq_q : orderOf g = q := by exact Fintype.card_of_bijective this rw [← h_card_zpow, h_card_eq, G_card_q] -lemma exp_bij (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ) := by - apply (Fintype.bijective_iff_surjective_and_card _).mpr - simp [G_card_q] - intro y - obtain ⟨k, hk⟩ := g_gen_G y - simp only at hk - simp only - let k' : ZMod q := (k : ZMod q) - have hk' : g ^ (k'.val : ℤ) = y := by - rw [←hk] - simp only [ZMod.natCast_val] - rw [ZMod.coe_intCast] - rw [← G_card_q] - rw [@zpow_mod_card] - - let a_unit := Units.mk0 (a.val : ZMod q) a.2 - let r : ZMod q := (a_unit⁻¹ : ZMod q) * (k' - m) - have h_mod : (m + a_unit * r) = k' := by - subst r - rw [IsUnit.mul_inv_cancel_left (Exists.intro a_unit rfl) (k' - m)] - simp - - have h_pow : g^((m + a_unit * r).val : ℤ) = y := by - rw [←hk'] - subst r - rw [h_mod] - - rw [←ZMod.cast_eq_val] at h_pow -- Transfer ↑ and .val back to .cast - exact Exists.intro (r) h_pow - -lemma exp_bij' (a : ZMod q) (ha : (a.val : ZMod q) ≠ 0) (m : ZMod q) : Function.Bijective fun (r : ZMod q) => g^((m + a.val * r : ZMod q).val : ℤ) := by +lemma exp_bij' (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ) := by apply (Fintype.bijective_iff_surjective_and_card _).mpr simp [G_card_q] intro c --So take any cc ∈ GG @@ -72,7 +42,7 @@ lemma exp_bij' (a : ZMod q) (ha : (a.val : ZMod q) ≠ 0) (m : ZMod q) : Functio -- we need g^m+a^r = g^z -- This is the case iff m + ar ≡ z (mod q) -- This is the case iff t ≡ a^−1 * (z − m) (mod q) - let a_unit := Units.mk0 (a.val : ZMod q) ha + let a_unit := Units.mk0 (a.val : ZMod q) a.2 let r : ZMod q := (a_unit⁻¹ : ZMod q) * (z - m) have h_mod : (m + a_unit * r) = z := by subst r @@ -85,77 +55,88 @@ lemma exp_bij' (a : ZMod q) (ha : (a.val : ZMod q) ≠ 0) (m : ZMod q) : Functio rw [h_mod] rw [←ZMod.cast_eq_val] at h_pow -- Transfer ↑ and .val back to .cast - sorry - --exact Exists.intro (r) h_pow + exact Exists.intro (r) h_pow -noncomputable def expEquiv (a : ZMod q) (ha : (a.val : ZMod q) ≠ 0) (m : ZMod q) : ZMod q ≃ G := -Equiv.ofBijective (fun (r : ZMod q) => g^((m + (a.val) * r : ZMod q).val : ℤ)) (exp_bij' q G_card_q g g_gen_G a ha m) +noncomputable def expEquiv (a : ZModMult q) (m : ZMod q) : ZMod q ≃ G := +Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) (exp_bij' q G_card_q g g_gen_G a m) variable (a' : ZMod q) (ha' : (a'.val : ZMod q) ≠ 0) (m' : ZMod q) -#check (expEquiv q G_card_q g g_gen_G a' ha' m').invFun +variable (az : ZModMult q) (mz : ZMod q) +#check (expEquiv q G_card_q g g_gen_G az mz).invFun + lemma pedersen_uniform_for_fixed_a {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) : (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c }) / (Finset.card ( (⊤ : Finset G) ) : ℚ) = 1 / (Fintype.card G) := by - have h_bij := exp_bij q G_card_q g g_gen_G ⟨a, ha⟩ m + let a_mult : ZModMult q := ⟨a, ha⟩ + let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G a_mult m have h_card : Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } = 1 := by rw [Finset.card_eq_one] - obtain ⟨r, hr⟩ := h_bij.surjective c - use r + use equiv.symm c ext t simp only [Finset.mem_singleton, Finset.mem_filter, Finset.mem_univ, true_and] + have h_equiv_def : ∀ r, equiv r = g^((m + (val a_mult) * r : ZMod q).val : ℤ) := fun r => rfl + have h_val_eq : val a_mult = a := rfl constructor · intro ht - have : g ^ ((m + a * t : ZMod q).val : ℤ) = g ^ ((m + a * r : ZMod q).val : ℤ) := by - rw [ht, ← hr] - simp only [val] - exact h_bij.injective this + have : equiv t = c := by rw [h_equiv_def, h_val_eq, ht] + rw [← this, Equiv.eq_symm_apply] · intro ht - rw [ht, ← hr] - simp only [val] + subst ht + have : equiv (equiv.symm c) = c := Equiv.apply_symm_apply equiv c + rw [h_equiv_def, h_val_eq] at this + exact this rw [h_card] exact rfl - - lemma pedersen_uniform_for_fixed_a' {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) : Finset.card { r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val } = 1 := by - have h_ratio := pedersen_uniform_for_fixed_a q G_card_q g g_gen_G ha m c - have h_card : Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } = 1 := by - have h_pos : (0 : ℚ) < Finset.card (⊤ : Finset G) := by simp; exact Fintype.card_pos - have h_eq : (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } : ℚ) = - (Finset.card (⊤ : Finset G) : ℚ) / (Fintype.card G : ℚ) := by - grind --only [= Finset.card_univ, usr Finset.card_filter_le, cases Or] - have h_top : Finset.card (⊤ : Finset G) = Fintype.card G := by rfl - have : (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } : ℚ) = (1 : ℚ) := by - grind - exact Nat.cast_injective (R := ℚ) this - convert h_card using 2 + let a_mult : ZModMult q := ⟨a, ha⟩ + let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G a_mult m + have h_equiv_def : ∀ r, equiv r = g^((m + (val a_mult) * r : ZMod q).val : ℤ) := fun r => rfl + have h_val_eq : val a_mult = a := rfl + -- Show the goal using equiv + suffices Finset.card { r : ZMod q | g ^ ((m + a * r : ZMod q).val : ℤ) = c } = 1 by + convert this using 2 + ext t + simp only [Finset.mem_filter, Finset.mem_univ, true_and] + have key : g ^ ((m + a * t).val : ℤ) = g ^ m.val * (g ^ a.val) ^ t.val := by + have : (g ^ m.val * (g ^ a.val) ^ t.val : G) = g ^ m.val * g ^ (a.val * t.val) := by + rw [← pow_mul] + rw [this, ← pow_add] + have h_order : orderOf g = q := ordg_eq_q q G_card_q g g_gen_G + have h_val_eq_local : (m + a * t).val = (m.val + a.val * t.val) % q := by + have h_eq : (m + a * t : ZMod q) = ((m.val + a.val * t.val) : ℕ) := by + simp only [Nat.cast_add, ZMod.natCast_val, ZMod.cast_id', id_eq, Nat.cast_mul] + rw [h_eq, ZMod.val_natCast] + rw [h_val_eq_local] + show g ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ (m.val + a.val * t.val : ℕ) + rw [← zpow_natCast] + have : (g : G) ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ ((m.val + a.val * t.val : ℕ) : ℤ) := by + have : ((m.val + a.val * t.val : ℕ) : ℤ) % (orderOf g : ℤ) = ((m.val + a.val * t.val) % q : ℕ) := by + grind + rw [← this, zpow_mod_orderOf] + assumption + constructor + · intro h; rw [key, h] + · intro h; rw [← key, h] + -- Now prove the suffices goal + rw [Finset.card_eq_one] + use equiv.symm c ext t - simp only [Finset.mem_filter, Finset.mem_univ, true_and] - have key : g ^ ((m + a * t).val : ℤ) = g ^ m.val * (g ^ a.val) ^ t.val := by - have : (g ^ m.val * (g ^ a.val) ^ t.val : G) = g ^ m.val * g ^ (a.val * t.val) := by - rw [← pow_mul] - rw [this] - rw [← pow_add] - have h_order : orderOf g = q := by - · expose_names; exact ordg_eq_q q G_card_q g g_gen_G - have h_val_eq : (m + a * t).val = (m.val + a.val * t.val) % q := by - have h_eq : (m + a * t : ZMod q) = ((m.val + a.val * t.val) : ℕ) := by - simp only [Nat.cast_add, ZMod.natCast_val, ZMod.cast_id', id_eq, Nat.cast_mul] - rw [h_eq, ZMod.val_natCast] - rw [h_val_eq] - show g ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ (m.val + a.val * t.val : ℕ) - rw [← zpow_natCast] - have : (g : G) ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ ((m.val + a.val * t.val : ℕ) : ℤ) := by - have : ((m.val + a.val * t.val : ℕ) : ℤ) % (orderOf g : ℤ) = ((m.val + a.val * t.val) % q : ℕ) := by - grind - rw [← this, zpow_mod_orderOf] - assumption - rw [key, eq_comm] + simp only [Finset.mem_singleton, Finset.mem_filter, Finset.mem_univ, true_and] + constructor + · intro ht + have : equiv t = c := by rw [h_equiv_def, h_val_eq, ht] + rw [← this, Equiv.eq_symm_apply] + · intro ht + subst ht + have : equiv (equiv.symm c) = c := Equiv.apply_symm_apply equiv c + rw [h_equiv_def, h_val_eq] at this + exact this -- Temporary? From d5e3a034415f43748c99675301e0d9cbd3f81fa4 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 26 Nov 2025 10:32:31 -0800 Subject: [PATCH 03/15] wip: add commented alternative to setup def using bind rather than do --- VerifiedCommitments/PedersenScheme.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index cfa503c..65bf778 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -7,7 +7,7 @@ namespace Pedersen (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 q hq 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, From 9098950ca91baf4aef04e4eb63a8ef61c4ad3918 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 29 Nov 2025 11:53:18 -0800 Subject: [PATCH 04/15] feat: add mapping uniform PMF bijection proof from formalmethods.io --- VerifiedCommitments/PedersenHiding.lean | 53 ++++++++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index e98f1d5..3207f55 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -63,7 +63,58 @@ Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) variable (a' : ZMod q) (ha' : (a'.val : ZMod q) ≠ 0) (m' : ZMod q) variable (az : ZModMult q) (mz : ZMod q) -#check (expEquiv q G_card_q g g_gen_G az mz).invFun +#check (expEquiv q G_card_q g g_gen_G az mz).toFun + + +open Classical -- needed here or α must be DecidableEq +/-! ### 2. Mapping a uniform PMF through a bijection stays uniform -------------/ +-- Courtesy of formalmethods.io +lemma map_uniformOfFintype_equiv + {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] + (e : α ≃ β) : + PMF.map e (PMF.uniformOfFintype α) = PMF.uniformOfFintype β := by + -- Prove equality of PMFs by showing they assign the same probability to each element + ext b + -- Goal: (PMF.map e (uniformOfFintype α)) b = (uniformOfFintype β) b + + -- Step 1: Simplify the LHS using PMF.map_apply + rw [PMF.map_apply] + -- This gives us: ∑' (a : α), if b = e a then (uniformOfFintype α) a else 0 + + -- Step 2: Simplify the uniform distribution on α + simp only [PMF.uniformOfFintype_apply] + -- Goal: ∑' (a : α), if b = e a then (↑(card α))⁻¹ else 0 = (↑(card β))⁻¹ + + -- Step 3: The sum has exactly one non-zero term when a = e.symm b + -- We can rewrite this as a sum over the singleton {e.symm b} + have h_equiv : (∑' (a : α), if b = e a then (↑(Fintype.card α : ENNReal))⁻¹ else 0) = + (∑' (a : α), if a = e.symm b then (↑(Fintype.card α))⁻¹ else 0) := by + congr 1 + ext a + -- Show: (if b = e a then (↑(card α))⁻¹ else 0) = (if a = e.symm b then (↑(card α))⁻¹ else 0) + by_cases h : b = e a + · -- Case: b = e a + rw [if_pos h, if_pos] + -- Need to show a = e.symm b + rw [←Equiv.symm_apply_apply e a] + rw [h] + · -- Case: b ≠ e a + rw [if_neg h, if_neg] + -- Need to show a ≠ e.symm b + intro contra + subst contra + rw [Equiv.apply_symm_apply e] at h + apply h + rfl + + -- Step 4: Apply the equivalence and simplify + rw [h_equiv] + rw [tsum_ite_eq] + -- Goal: (↑(card α))⁻¹ = (↑(card β))⁻¹ + + -- Step 5: Use the fact that equivalent finite types have the same cardinality + congr 1 + rw [Fintype.card_congr e] lemma pedersen_uniform_for_fixed_a From cad159f0c04c4d3fdfeac06db9bcd247ebf1fb74 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 29 Nov 2025 11:55:19 -0800 Subject: [PATCH 05/15] feat: add proof of equivalence of PMF bind and map --- VerifiedCommitments/PedersenHiding.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 3207f55..96a82f5 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -341,6 +341,11 @@ lemma pedersen_commitment_uniform (m : ZMod q) [DecidableEq G] (c : G) : return g^m.val * (g^a.val)^r.val : PMF G) c = 1 / Fintype.card G := by sorry +lemma bind_eq_map + {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] + (e : α ≃ β) : + PMF.map e (PMF.uniformOfFintype α) = PMF.bind (PMF.uniformOfFintype α) (fun a => pure (e a)) := by + rfl theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q), From 2bbe3f042f09269bf13f867cea3af37bb9d1be20 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 29 Nov 2025 11:56:52 -0800 Subject: [PATCH 06/15] wip: add alternative formulation for pedersen_commitment_uniform --- VerifiedCommitments/PedersenHiding.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 96a82f5..a7ed9bd 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -347,6 +347,15 @@ lemma bind_eq_map PMF.map e (PMF.uniformOfFintype α) = PMF.bind (PMF.uniformOfFintype α) (fun a => pure (e a)) := by rfl + +lemma pedersen_commitment_uniform'' (m : ZMod q) [DecidableEq G] (c : G) : + (PMF.bind (generate_a q hq_prime) + (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q)) + (fun r => PMF.pure (g^m.val * (g^a.val)^r.val)))) c = 1 / Fintype.card G := by + conv_lhs => arg 1; arg 2; ext a; rw [←@bind_eq_map _ _ (fun r ↦ PMF.pure (g ^ m.val * (g ^ a.val) ^ r.val))] + + 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 From e06ac86f974d3889d0274e42bbc5182a949ffa03 Mon Sep 17 00:00:00 2001 From: Ashley Blacquiere Date: Sat, 29 Nov 2025 12:08:10 -0800 Subject: [PATCH 07/15] wip: add probablistitc definitions for hiding property (#3) --- VerifiedCommitments/PedersenHiding.lean | 120 +++++++++++++++++++++++- 1 file changed, 117 insertions(+), 3 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index a7ed9bd..425982b 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -2,6 +2,10 @@ 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) @@ -9,6 +13,9 @@ variable (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g) include G_card_q include g_gen_G +-- Temporary? +variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) + lemma ordg_eq_q : orderOf g = q := by have h_card_zpow : Fintype.card (Subgroup.zpowers g) = orderOf g := Fintype.card_zpowers -- zpowers g has the same cardinality as G since g generates G @@ -58,6 +65,15 @@ lemma exp_bij' (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod exact Exists.intro (r) h_pow +-- Fintype instance for commit +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⟩ + left_inv := fun _ => rfl + right_inv := fun x => by cases x; rfl + } + noncomputable def expEquiv (a : ZModMult q) (m : ZMod q) : ZMod q ≃ G := Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) (exp_bij' q G_card_q g g_gen_G a m) @@ -189,6 +205,107 @@ lemma pedersen_uniform_for_fixed_a' rw [h_equiv_def, h_val_eq] at this exact this +-- 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 +lemma pedersen_uniform_for_fixed_a_probablistic + (a : ZMod q) (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c' : G) : + (PMF.map commit.c ((Pedersen.scheme G g q hq_prime).commit (g^a.val) m)) c' = 1 / (Fintype.card G) := by -- Should be using ZModUtils? + unfold Pedersen.scheme + rw [G_card_q] + simp only [bind_pure_comp, one_div] + have h_bij := exp_bij q G_card_q g g_gen_G ⟨a, ha⟩ m + obtain ⟨r, hr⟩ := h_bij.surjective c' + --subst hr + --simp only [ne_eq, ZMod.natCast_val] + rw [@PMF.monad_map_eq_map] -- PMF.map_apply (fun a_1 ↦ { c := g ^ m.val * (g ^ a.val) ^ a_1.val, o := a_1 })] + conv_lhs => arg 1; rw [PMF.map, PMF.bind] + simp only [Function.comp_apply, PMF.pure_apply, mul_ite, mul_one, mul_zero] + have key : ∀ r, g ^ m.val * (g ^ a.val) ^ r.val = g^((m + a * r).val : ℤ) := by + intro r + -- This is the same calculation as in pedersen_uniform_for_fixed_a' line 129-147 + rw [← pow_mul] + rw [← pow_add] + have h_order : orderOf g = q := by + · expose_names; exact ordg_eq_q q G_card_q g g_gen_G + have h_val_eq : (m + a * r).val = (m.val + a.val * r.val) % q := by + have h_eq : (m + a * r : ZMod q) = ((m.val + a.val * r.val) : ℕ) := by + simp only [Nat.cast_add, ZMod.natCast_val, ZMod.cast_id', id_eq, Nat.cast_mul] + rw [h_eq, ZMod.val_natCast] + rw [h_val_eq] + show g ^ (m.val + a.val * r.val : ℕ) = g ^ (((m.val + a.val * r.val) % q : ℕ) : ℤ) + rw [← zpow_natCast] + have : (g : G) ^ (((m.val + a.val * r.val) % q : ℕ) : ℤ) = g ^ ((m.val + a.val * r.val : ℕ) : ℤ) := by + have : ((m.val + a.val * r.val : ℕ) : ℤ) % (orderOf g : ℤ) = ((m.val + a.val * r.val) % q : ℕ) := by + grind + rw [← this, zpow_mod_orderOf] + grind + simp only [PMF.map_apply, PMF.uniformOfFintype_apply, ZMod.card] + -- Apply the PMF to c' + simp only [PMF.instFunLike] + -- Simplify the outer tsum + rw [tsum_fintype] + -- Convert inner tsums + simp_rw [tsum_fintype] + -- Use Finset.sum_ite to separate the outer sum + rw [Finset.sum_ite] + simp only [Finset.sum_const_zero, add_zero] + -- Now we have: sum over {x | c' = x.c} of (sum over a_1 of ...) + -- Swap the summation order + rw [Finset.sum_comm] + + + + -- For each a_1, the inner sum has at most one non-zero term + -- It's non-zero when x = commit.mk (g^...) a_1 AND c' = x.c + classical + have h_simplify : ∀ a_1 : ZMod q, + (∑ x ∈ Finset.filter (fun (x : commit G (ZMod q)) => c' = x.c) Finset.univ, + if x = { c := g^m.val * (g^a.val)^a_1.val, o := a_1 } then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = + (if c' = g^m.val * (g^a.val)^a_1.val then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by + intro a_1 + rw [Finset.sum_ite_eq'] + simp only [Finset.mem_filter, Finset.mem_univ, true_and] + have h_rewrite : (∑ a_1 : ZMod q, ∑ x ∈ Finset.filter (fun (x : commit G (ZMod q)) => c' = x.c) Finset.univ, + if x = ({ c := g^m.val * (g^a.val)^a_1.val, o := a_1 } : commit G (ZMod q)) then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = + (∑ a_1 : ZMod q, if c' = g^m.val * (g^a.val)^a_1.val then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by + congr 1; ext a_1; exact h_simplify a_1 + rw [h_rewrite] + -- Use the key lemma to rewrite + have h_key_rewrite : (∑ a_1 : ZMod q, if c' = g^m.val * (g^a.val)^a_1.val then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = + (∑ a_1 : ZMod q, if c' = g^((m + a * a_1).val : ℤ) then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by + congr 1; ext a_1; congr 1; rw [key] + rw [h_key_rewrite] + -- Now we have: sum over a_1 of (if c' = g^((m + a*a_1).val) then (↑q)⁻¹ else 0) + -- By the bijection, exactly one a_1 satisfies this (namely r) + -- First simplify hr - note that val ⟨a, ha⟩ = a by definition + have hr_simplified : c' = g^((m + a * r).val : ℤ) := by + have step1 : (fun r => g ^ ((m + val ⟨a, ha⟩ * r).val : ℤ)) r = g^((m + val ⟨a, ha⟩ * r).val : ℤ) := rfl + have step2 : g^((m + val ⟨a, ha⟩ * r).val : ℤ) = g^((m + a * r).val : ℤ) := by simp only [val] + rw [← step2, ← step1] + exact hr.symm + -- We need to show that exactly one value (r) makes the condition true + have h_unique : ∀ a_1 : ZMod q, (c' = g^((m + a * a_1).val : ℤ)) ↔ a_1 = r := by + intro a_1 + constructor + · intro h + have eq1 : g^((m + a * a_1).val : ℤ) = g^((m + a * r).val : ℤ) := by rw [← h, ← hr_simplified] + have eq2 : g^((m + val ⟨a, ha⟩ * a_1).val : ℤ) = g^((m + val ⟨a, ha⟩ * r).val : ℤ) := by + have : val ⟨a, ha⟩ = a := by simp only [val] + simp only [this] + exact eq1 + apply h_bij.injective + exact eq2 + · intro h + rw [h] + exact hr_simplified + -- Rewrite the sum using this unique characterization + have h_sum_unique : (∑ a_1 : ZMod q, if c' = g^((m + a * a_1).val : ℤ) then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = + (∑ a_1 : ZMod q, if a_1 = r then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by + congr 1; ext a_1; congr 1; rw [h_unique] + rw [h_sum_unique] + rw [Finset.sum_ite_eq'] + simp only [Finset.mem_univ, ite_true] + -- Temporary? variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) @@ -369,6 +486,3 @@ theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic sorry - --- Collection of uniform distrbutions and need to choose uniformly among them --- Seems that this is the work of a bind to map across two distributions From 4aba83e7176fa5c4b8caafce650e0151afd0a2b8 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 29 Nov 2025 14:27:30 -0800 Subject: [PATCH 08/15] fix: add missing typeclasses and correct lemma call following merge --- VerifiedCommitments/PedersenHiding.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 425982b..ac1349c 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -138,7 +138,7 @@ lemma pedersen_uniform_for_fixed_a (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c }) / (Finset.card ( (⊤ : Finset G) ) : ℚ) = 1 / (Fintype.card G) := by let a_mult : ZModMult q := ⟨a, ha⟩ - let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G a_mult m + let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G _ _ a_mult m have h_card : Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } = 1 := by rw [Finset.card_eq_one] use equiv.symm c @@ -162,7 +162,7 @@ lemma pedersen_uniform_for_fixed_a' {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) : Finset.card { r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val } = 1 := by let a_mult : ZModMult q := ⟨a, ha⟩ - let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G a_mult m + let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G _ _ a_mult m have h_equiv_def : ∀ r, equiv r = g^((m + (val a_mult) * r : ZMod q).val : ℤ) := fun r => rfl have h_val_eq : val a_mult = a := rfl -- Show the goal using equiv @@ -213,7 +213,7 @@ lemma pedersen_uniform_for_fixed_a_probablistic unfold Pedersen.scheme rw [G_card_q] simp only [bind_pure_comp, one_div] - have h_bij := exp_bij q G_card_q g g_gen_G ⟨a, ha⟩ m + have h_bij := exp_bij' q G_card_q g g_gen_G ⟨a, ha⟩ m obtain ⟨r, hr⟩ := h_bij.surjective c' --subst hr --simp only [ne_eq, ZMod.natCast_val] From 02cd6b8893c4d75e9ec726aca53c0bfd9f2abc4d Mon Sep 17 00:00:00 2001 From: ashandoak Date: Sat, 29 Nov 2025 14:28:41 -0800 Subject: [PATCH 09/15] feat: add equivalence between PMF bind and map for expEquiv --- VerifiedCommitments/PedersenHiding.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index ac1349c..a648160 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -464,7 +464,14 @@ lemma bind_eq_map PMF.map e (PMF.uniformOfFintype α) = PMF.bind (PMF.uniformOfFintype α) (fun a => pure (e a)) := by rfl - +lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), + PMF.map (expEquiv q G_card_q g g_gen_G fixed_a fixed_m) (PMF.uniformOfFintype (ZMod q)) = + PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun a => pure (expEquiv q G_card_q g g_gen_G fixed_a fixed_m a)) + := by + intros + exact rfl + + -- let a_mult : ZModMult q := ⟨a, ha⟩ lemma pedersen_commitment_uniform'' (m : ZMod q) [DecidableEq G] (c : G) : (PMF.bind (generate_a q hq_prime) (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q)) From 779fb1966d169ee6eb69c73e6f249c1cb5b9938d Mon Sep 17 00:00:00 2001 From: ashandoak Date: Mon, 1 Dec 2025 18:59:38 -0800 Subject: [PATCH 10/15] wip: add fintype and nonempty instances for ZModMult --- VerifiedCommitments/ZModUtil.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/VerifiedCommitments/ZModUtil.lean b/VerifiedCommitments/ZModUtil.lean index 8467efb..3d4fa04 100644 --- a/VerifiedCommitments/ZModUtil.lean +++ b/VerifiedCommitments/ZModUtil.lean @@ -18,3 +18,9 @@ def ZModMult (q : ℕ) [NeZero q] := {a : ZMod q // a ≠ 0} -- Helper function to extract the value from ZModMult def val {q : ℕ} [NeZero q] (a : ZModMult q) : ZMod q := a.val + +-- Fintype instance for ZModMult +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 From 917aa3d38b301a9abf846e3f4a78320920dac3d6 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Mon, 1 Dec 2025 19:02:34 -0800 Subject: [PATCH 11/15] wip: cleanup code to reduce extraneous context --- VerifiedCommitments/PedersenHiding.lean | 384 +++--------------------- 1 file changed, 47 insertions(+), 337 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index a648160..9e9e63e 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -77,9 +77,12 @@ instance {C O : Type} [Fintype C] [Fintype O] : Fintype (commit C O) := noncomputable def expEquiv (a : ZModMult q) (m : ZMod q) : ZMod q ≃ G := Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) (exp_bij' q G_card_q g g_gen_G a m) -variable (a' : ZMod q) (ha' : (a'.val : ZMod q) ≠ 0) (m' : ZMod q) -variable (az : ZModMult q) (mz : ZMod q) -#check (expEquiv q G_card_q g g_gen_G az mz).toFun + +#check expEquiv q G_card_q g g_gen_G + +lemma expEquiv_unfold (a : ZModMult q) (m r : ZMod q) : + expEquiv q G_card_q g g_gen_G a m r = g^m.val * (g^(val a).val)^r.val := by + open Classical -- needed here or α must be DecidableEq @@ -132,332 +135,6 @@ lemma map_uniformOfFintype_equiv congr 1 rw [Fintype.card_congr e] - -lemma pedersen_uniform_for_fixed_a - {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) : - (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c }) / (Finset.card ( (⊤ : Finset G) ) : ℚ) - = 1 / (Fintype.card G) := by - let a_mult : ZModMult q := ⟨a, ha⟩ - let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G _ _ a_mult m - have h_card : Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } = 1 := by - rw [Finset.card_eq_one] - use equiv.symm c - ext t - simp only [Finset.mem_singleton, Finset.mem_filter, Finset.mem_univ, true_and] - have h_equiv_def : ∀ r, equiv r = g^((m + (val a_mult) * r : ZMod q).val : ℤ) := fun r => rfl - have h_val_eq : val a_mult = a := rfl - constructor - · intro ht - have : equiv t = c := by rw [h_equiv_def, h_val_eq, ht] - rw [← this, Equiv.eq_symm_apply] - · intro ht - subst ht - have : equiv (equiv.symm c) = c := Equiv.apply_symm_apply equiv c - rw [h_equiv_def, h_val_eq] at this - exact this - rw [h_card] - exact rfl - -lemma pedersen_uniform_for_fixed_a' - {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) : - Finset.card { r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val } = 1 := by - let a_mult : ZModMult q := ⟨a, ha⟩ - let equiv := @expEquiv G _ _ q _ G_card_q g g_gen_G _ _ a_mult m - have h_equiv_def : ∀ r, equiv r = g^((m + (val a_mult) * r : ZMod q).val : ℤ) := fun r => rfl - have h_val_eq : val a_mult = a := rfl - -- Show the goal using equiv - suffices Finset.card { r : ZMod q | g ^ ((m + a * r : ZMod q).val : ℤ) = c } = 1 by - convert this using 2 - ext t - simp only [Finset.mem_filter, Finset.mem_univ, true_and] - have key : g ^ ((m + a * t).val : ℤ) = g ^ m.val * (g ^ a.val) ^ t.val := by - have : (g ^ m.val * (g ^ a.val) ^ t.val : G) = g ^ m.val * g ^ (a.val * t.val) := by - rw [← pow_mul] - rw [this, ← pow_add] - have h_order : orderOf g = q := ordg_eq_q q G_card_q g g_gen_G - have h_val_eq_local : (m + a * t).val = (m.val + a.val * t.val) % q := by - have h_eq : (m + a * t : ZMod q) = ((m.val + a.val * t.val) : ℕ) := by - simp only [Nat.cast_add, ZMod.natCast_val, ZMod.cast_id', id_eq, Nat.cast_mul] - rw [h_eq, ZMod.val_natCast] - rw [h_val_eq_local] - show g ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ (m.val + a.val * t.val : ℕ) - rw [← zpow_natCast] - have : (g : G) ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ ((m.val + a.val * t.val : ℕ) : ℤ) := by - have : ((m.val + a.val * t.val : ℕ) : ℤ) % (orderOf g : ℤ) = ((m.val + a.val * t.val) % q : ℕ) := by - grind - rw [← this, zpow_mod_orderOf] - assumption - constructor - · intro h; rw [key, h] - · intro h; rw [← key, h] - -- Now prove the suffices goal - rw [Finset.card_eq_one] - use equiv.symm c - ext t - simp only [Finset.mem_singleton, Finset.mem_filter, Finset.mem_univ, true_and] - constructor - · intro ht - have : equiv t = c := by rw [h_equiv_def, h_val_eq, ht] - rw [← this, Equiv.eq_symm_apply] - · intro ht - subst ht - have : equiv (equiv.symm c) = c := Equiv.apply_symm_apply equiv c - rw [h_equiv_def, h_val_eq] at this - exact this - --- 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 -lemma pedersen_uniform_for_fixed_a_probablistic - (a : ZMod q) (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c' : G) : - (PMF.map commit.c ((Pedersen.scheme G g q hq_prime).commit (g^a.val) m)) c' = 1 / (Fintype.card G) := by -- Should be using ZModUtils? - unfold Pedersen.scheme - rw [G_card_q] - simp only [bind_pure_comp, one_div] - have h_bij := exp_bij' q G_card_q g g_gen_G ⟨a, ha⟩ m - obtain ⟨r, hr⟩ := h_bij.surjective c' - --subst hr - --simp only [ne_eq, ZMod.natCast_val] - rw [@PMF.monad_map_eq_map] -- PMF.map_apply (fun a_1 ↦ { c := g ^ m.val * (g ^ a.val) ^ a_1.val, o := a_1 })] - conv_lhs => arg 1; rw [PMF.map, PMF.bind] - simp only [Function.comp_apply, PMF.pure_apply, mul_ite, mul_one, mul_zero] - have key : ∀ r, g ^ m.val * (g ^ a.val) ^ r.val = g^((m + a * r).val : ℤ) := by - intro r - -- This is the same calculation as in pedersen_uniform_for_fixed_a' line 129-147 - rw [← pow_mul] - rw [← pow_add] - have h_order : orderOf g = q := by - · expose_names; exact ordg_eq_q q G_card_q g g_gen_G - have h_val_eq : (m + a * r).val = (m.val + a.val * r.val) % q := by - have h_eq : (m + a * r : ZMod q) = ((m.val + a.val * r.val) : ℕ) := by - simp only [Nat.cast_add, ZMod.natCast_val, ZMod.cast_id', id_eq, Nat.cast_mul] - rw [h_eq, ZMod.val_natCast] - rw [h_val_eq] - show g ^ (m.val + a.val * r.val : ℕ) = g ^ (((m.val + a.val * r.val) % q : ℕ) : ℤ) - rw [← zpow_natCast] - have : (g : G) ^ (((m.val + a.val * r.val) % q : ℕ) : ℤ) = g ^ ((m.val + a.val * r.val : ℕ) : ℤ) := by - have : ((m.val + a.val * r.val : ℕ) : ℤ) % (orderOf g : ℤ) = ((m.val + a.val * r.val) % q : ℕ) := by - grind - rw [← this, zpow_mod_orderOf] - grind - simp only [PMF.map_apply, PMF.uniformOfFintype_apply, ZMod.card] - -- Apply the PMF to c' - simp only [PMF.instFunLike] - -- Simplify the outer tsum - rw [tsum_fintype] - -- Convert inner tsums - simp_rw [tsum_fintype] - -- Use Finset.sum_ite to separate the outer sum - rw [Finset.sum_ite] - simp only [Finset.sum_const_zero, add_zero] - -- Now we have: sum over {x | c' = x.c} of (sum over a_1 of ...) - -- Swap the summation order - rw [Finset.sum_comm] - - - - -- For each a_1, the inner sum has at most one non-zero term - -- It's non-zero when x = commit.mk (g^...) a_1 AND c' = x.c - classical - have h_simplify : ∀ a_1 : ZMod q, - (∑ x ∈ Finset.filter (fun (x : commit G (ZMod q)) => c' = x.c) Finset.univ, - if x = { c := g^m.val * (g^a.val)^a_1.val, o := a_1 } then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = - (if c' = g^m.val * (g^a.val)^a_1.val then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by - intro a_1 - rw [Finset.sum_ite_eq'] - simp only [Finset.mem_filter, Finset.mem_univ, true_and] - have h_rewrite : (∑ a_1 : ZMod q, ∑ x ∈ Finset.filter (fun (x : commit G (ZMod q)) => c' = x.c) Finset.univ, - if x = ({ c := g^m.val * (g^a.val)^a_1.val, o := a_1 } : commit G (ZMod q)) then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = - (∑ a_1 : ZMod q, if c' = g^m.val * (g^a.val)^a_1.val then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by - congr 1; ext a_1; exact h_simplify a_1 - rw [h_rewrite] - -- Use the key lemma to rewrite - have h_key_rewrite : (∑ a_1 : ZMod q, if c' = g^m.val * (g^a.val)^a_1.val then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = - (∑ a_1 : ZMod q, if c' = g^((m + a * a_1).val : ℤ) then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by - congr 1; ext a_1; congr 1; rw [key] - rw [h_key_rewrite] - -- Now we have: sum over a_1 of (if c' = g^((m + a*a_1).val) then (↑q)⁻¹ else 0) - -- By the bijection, exactly one a_1 satisfies this (namely r) - -- First simplify hr - note that val ⟨a, ha⟩ = a by definition - have hr_simplified : c' = g^((m + a * r).val : ℤ) := by - have step1 : (fun r => g ^ ((m + val ⟨a, ha⟩ * r).val : ℤ)) r = g^((m + val ⟨a, ha⟩ * r).val : ℤ) := rfl - have step2 : g^((m + val ⟨a, ha⟩ * r).val : ℤ) = g^((m + a * r).val : ℤ) := by simp only [val] - rw [← step2, ← step1] - exact hr.symm - -- We need to show that exactly one value (r) makes the condition true - have h_unique : ∀ a_1 : ZMod q, (c' = g^((m + a * a_1).val : ℤ)) ↔ a_1 = r := by - intro a_1 - constructor - · intro h - have eq1 : g^((m + a * a_1).val : ℤ) = g^((m + a * r).val : ℤ) := by rw [← h, ← hr_simplified] - have eq2 : g^((m + val ⟨a, ha⟩ * a_1).val : ℤ) = g^((m + val ⟨a, ha⟩ * r).val : ℤ) := by - have : val ⟨a, ha⟩ = a := by simp only [val] - simp only [this] - exact eq1 - apply h_bij.injective - exact eq2 - · intro h - rw [h] - exact hr_simplified - -- Rewrite the sum using this unique characterization - have h_sum_unique : (∑ a_1 : ZMod q, if c' = g^((m + a * a_1).val : ℤ) then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) = - (∑ a_1 : ZMod q, if a_1 = r then ((↑q : ENNReal)⁻¹) else (0 : ENNReal)) := by - congr 1; ext a_1; congr 1; rw [h_unique] - rw [h_sum_unique] - rw [Finset.sum_ite_eq'] - simp only [Finset.mem_univ, ite_true] - - --- Temporary? -variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) - --- This is presumably a more convenient approach rather than including the do-block directly in a the type of pedersen_commitment_uniform -noncomputable def generate_a : PMF $ ZMod q := - do - let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2 - return a - --- lemma sum_indicator_uniform {α : Type} [Fintype α] (p : α → Prop) [DecidablePred p] (h : (Finset.filter p Finset.univ).card = 1) : --- ∑' (x : α), if p x then (↑(Fintype.card α))⁻¹ else 0 = (↑(Fintype.card α))⁻¹ := by --- sorry - -lemma pedersen_commitment_uniform' (m : ZMod q) [DecidableEq G] (c : G) : - (PMF.bind (generate_a q hq_prime) - (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.pure (g^m.val * (g^a.val)^r.val)))) c = 1 / Fintype.card G := by - -- The key insight: for each non-zero a, the inner distribution is uniform over G - -- We'll show that the result doesn't depend on which a we sample - have h_uniform_inner : ∀ (a : ZMod q), a ≠ 0 → - (PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.pure (g^m.val * (g^a.val)^r.val))) c = 1 / Fintype.card G := by - intro a ha - rw [PMF.bind_apply] - conv_lhs => arg 1; ext r; rw [PMF.pure_apply] - simp only [PMF.uniformOfFintype_apply, ZMod.card] - -- Need to show: ∑' r, (1/q) * (if c = g^m.val * (g^a.val)^r.val then 1 else 0) = 1 / |G| - -- Since |G| = q, this reduces to showing the sum of indicators equals 1 - rw [ENNReal.tsum_mul_left, G_card_q, one_div] - -- Now need to show: q^{-1} * (sum of indicators) = q^{-1} - -- Equivalently: sum of indicators = 1 - -- Convert to finset sum - rw [tsum_eq_sum (s := {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset)] - swap - · simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and, - ite_eq_right_iff, one_ne_zero, imp_false, imp_self, implies_true]--intro r hr - -- The sum equals the cardinality - trans ((q : ENNReal)⁻¹ * ↑{r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset.card) - · congr 1 - trans (∑ b ∈ {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset, (1 : ENNReal)) - · apply Finset.sum_congr rfl - intro b hb - simp only [Set.mem_toFinset, Set.mem_setOf_eq] at hb - simp [hb] - · rw [Finset.sum_const, nsmul_eq_mul, mul_one] - rw [Set.toFinset_card] - -- Now use pedersen_uniform_for_fixed_a to show the cardinality is 1 - -- The cardinality of the set is 1, so q^{-1} * 1 = q^{-1} - have h_card : Fintype.card {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} = 1 := by - have h_finset : ({r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card = 1 := by - convert pedersen_uniform_for_fixed_a' q G_card_q g g_gen_G ha m c using 2 - ext r - simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] - have : Fintype.card {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} = - ({r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card := by - simp only [Set.toFinset_card] - grind only - simp_all - - -- Now use bind_skip_const' since the inner bind always gives the same distribution - have h_uniform_inner_gen : ∀ (a : ZMod q) (c' : G), a ≠ 0 → - (PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.pure (g^m.val * (g^a.val)^r.val))) c' = 1 / Fintype.card G := by - intro a c' ha - -- This is the same proof as h_uniform_inner but for c' instead of c - rw [PMF.bind_apply] - conv_lhs => arg 1; ext r; rw [PMF.pure_apply] - simp only [PMF.uniformOfFintype_apply, ZMod.card] - rw [ENNReal.tsum_mul_left, G_card_q, one_div] - rw [tsum_eq_sum (s := {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset)] - swap - · intro r hr - simp only [Set.mem_toFinset, Set.mem_setOf_eq] at hr - simp [hr] - trans ((q : ENNReal)⁻¹ * ↑{r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset.card) - · congr 1 - trans (∑ b ∈ {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset, (1 : ENNReal)) - · apply Finset.sum_congr rfl - intro b hb - simp only [Set.mem_toFinset, Set.mem_setOf_eq] at hb - simp [hb] - · rw [Finset.sum_const, nsmul_eq_mul, mul_one] - rw [Set.toFinset_card] - have h_card : Fintype.card {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} = 1 := by - have h_finset : ({r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card = 1 := by - convert pedersen_uniform_for_fixed_a' q G_card_q g g_gen_G ha m c' using 2 - ext r - simp [Set.mem_toFinset] - have : Fintype.card {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} = - ({r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card := by - simp only [Set.toFinset_card] - rw [this, h_finset] - rw [h_card] - simp - have h_const : ∀ a, a ∈ ((Finset.univ : Finset (ZMod q)).erase 0) → - (PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.pure (g^m.val * (g^a.val)^r.val))) = PMF.uniformOfFintype G := by - intro a ha - ext c' - simp [Finset.mem_erase] at ha - rw [h_uniform_inner_gen a c' ha] - simp [PMF.uniformOfFintype_apply] - rw [generate_a] - rw [bind_pure_comp] - rw [id_map'] - - have : (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2).bind - (fun a => (PMF.uniformOfFintype (ZMod q)).bind fun r => PMF.pure (g^m.val * (g^a.val)^r.val)) = - PMF.uniformOfFintype G := by - ext x - rw [PMF.bind_apply] - simp only [PMF.uniformOfFinset_apply] - trans (∑' a, (if a ∈ (nonzeroElements hq_prime).1 then ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (PMF.uniformOfFintype G) x else 0)) - · apply tsum_congr - intro a - by_cases ha : a ∈ (nonzeroElements hq_prime).1 - · simp only [ha, ite_true] - rw [h_const a ha] - · simp only [ha, ite_false, zero_mul] - · rw [tsum_eq_sum (s := (nonzeroElements hq_prime).1)] - · have : ∑ b ∈ (nonzeroElements hq_prime).1, (if b ∈ (nonzeroElements hq_prime).1 then ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (PMF.uniformOfFintype G) x else 0) = - ∑ b ∈ (nonzeroElements hq_prime).1, ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (PMF.uniformOfFintype G) x := by - apply Finset.sum_congr rfl - intro b hb - simp only [hb, ite_true] - rw [this, Finset.sum_const, nsmul_eq_mul, PMF.uniformOfFintype_apply] - -- Goal: (nonzeroElements hq_prime).1.card * (((nonzeroElements hq_prime).1.card)⁻¹ * (Fintype.card G)⁻¹) = (Fintype.card G)⁻¹ - calc ((nonzeroElements hq_prime).1.card : ENNReal) * (((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (Fintype.card G : ENNReal)⁻¹) - _ = (((nonzeroElements hq_prime).1.card : ENNReal) * ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹) * (Fintype.card G : ENNReal)⁻¹ := by - ring_nf - _ = 1 * (Fintype.card G : ENNReal)⁻¹ := by - congr 1 - apply ENNReal.mul_inv_cancel - · simp - exact Finset.Nonempty.ne_empty (nonzeroElements hq_prime).2 - · exact ENNReal.natCast_ne_top _ - _ = (Fintype.card G : ENNReal)⁻¹ := by rw [one_mul] - · intro a ha - simp [ha] - conv_lhs => rw [this] - simp [PMF.uniformOfFintype_apply] - - - -lemma pedersen_commitment_uniform (m : ZMod q) [DecidableEq G] (c : G) : - (do - let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2 - let r ← PMF.uniformOfFintype (ZMod q) - return g^m.val * (g^a.val)^r.val : PMF G) c = 1 / Fintype.card G := by - sorry - lemma bind_eq_map {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] (e : α ≃ β) : @@ -466,20 +143,54 @@ lemma bind_eq_map lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), PMF.map (expEquiv q G_card_q g g_gen_G fixed_a fixed_m) (PMF.uniformOfFintype (ZMod q)) = - PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun a => pure (expEquiv q G_card_q g g_gen_G fixed_a fixed_m a)) + PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun a => PMF.pure (expEquiv q G_card_q g g_gen_G fixed_a fixed_m a)) := by intros exact rfl - -- let a_mult : ZModMult q := ⟨a, ha⟩ -lemma pedersen_commitment_uniform'' (m : ZMod q) [DecidableEq G] (c : G) : - (PMF.bind (generate_a q hq_prime) - (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.pure (g^m.val * (g^a.val)^r.val)))) c = 1 / Fintype.card G := by - conv_lhs => arg 1; arg 2; ext a; rw [←@bind_eq_map _ _ (fun r ↦ PMF.pure (g ^ m.val * (g ^ a.val) ^ r.val))] +-- Temporary? +variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) +noncomputable def generate_a : PMF (ZMod q) := + PMF.uniformOfFintype (ZMod q) + + + +lemma pedersen_uniform_for_fixed_a_probablistic (a : ZModMult q) (m : ZMod q) : + PMF.map commit.c ((Pedersen.scheme G g q hq_prime).commit (g^(val a).val) m) = + PMF.uniformOfFintype G := by + -- Unfold commit definition + -- Use expEquiv_unfold to rewrite as map through expEquiv + -- Apply bind_eq_map' + -- Apply map_uniformOfFintype_equiv + -- Use G_card_q to get the right cardinality + 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 -- Should be using ZModUtils? sorry + + + +-- 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 @@ -492,4 +203,3 @@ theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic rw [Monad.toBind, PMF.instMonad] sorry - From 9d52566aed0b53a6c0cbbf427914a4c63c1a82d4 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Mon, 1 Dec 2025 19:05:56 -0800 Subject: [PATCH 12/15] wip: typo fixes --- VerifiedCommitments/PedersenHiding.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 9e9e63e..2ad7220 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -82,6 +82,7 @@ Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) lemma expEquiv_unfold (a : ZModMult q) (m r : ZMod q) : expEquiv q G_card_q g g_gen_G a m r = g^m.val * (g^(val a).val)^r.val := by + sorry @@ -156,7 +157,7 @@ noncomputable def generate_a : PMF (ZMod q) := -lemma pedersen_uniform_for_fixed_a_probablistic (a : ZModMult q) (m : ZMod q) : +lemma pedersen_uniform_for_fixed_a_probablistic' (a : ZModMult q) (m : ZMod q) : PMF.map commit.c ((Pedersen.scheme G g q hq_prime).commit (g^(val a).val) m) = PMF.uniformOfFintype G := by -- Unfold commit definition @@ -172,8 +173,7 @@ lemma pedersen_uniform_for_fixed_a_probablistic (a : ZModMult q) (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 -- Should be using ZModUtils? - 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 ddf0e930e54097d3942deb0153e63709c9ce4669 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 9 Dec 2025 22:43:42 -0800 Subject: [PATCH 13/15] fix: correct type for generate_a --- VerifiedCommitments/PedersenHiding.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 2ad7220..8a26022 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -152,8 +152,9 @@ lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), -- Temporary? variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) -noncomputable def generate_a : PMF (ZMod q) := - PMF.uniformOfFintype (ZMod q) + +noncomputable def generate_a : PMF (ZModMult q) := + PMF.uniformOfFintype (ZModMult q) From 6d777b65d20a82e50666c8e4c4e3b196276e6415 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 9 Dec 2025 22:44:03 -0800 Subject: [PATCH 14/15] wip: add expEquiv_unfold --- VerifiedCommitments/PedersenHiding.lean | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 8a26022..879c429 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -82,8 +82,27 @@ Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) lemma expEquiv_unfold (a : ZModMult q) (m r : ZMod q) : expEquiv q G_card_q g g_gen_G a m r = g^m.val * (g^(val a).val)^r.val := by - sorry + unfold expEquiv + simp only [Equiv.ofBijective, Equiv.coe_fn_mk] + + have h_pow : (g^(val a).val)^r.val = g^((val a).val * r.val) := (pow_mul g (val a).val r.val).symm + rw [h_pow] + + simp only [← zpow_natCast] + rw [← zpow_add] + + have hord : orderOf g = q := ordg_eq_q q G_card_q g g_gen_G + conv_lhs => rw [← zpow_mod_orderOf, hord] + + suffices h : (((m + (val a) * r).val : ℤ) % ↑q) = ((m.val : ℤ) + ((val a).val * r.val : ℤ)) % ↑q by + conv_rhs => rw [← zpow_mod_orderOf, hord] + rw [h] + congr 1 + conv_lhs => rw [ZMod.val_add, ZMod.val_mul] + norm_cast + rw [Nat.add_mod, Nat.mul_mod] + simp open Classical -- needed here or α must be DecidableEq From 14620032b31a2b2f8dd99808094c322e0d09ccff Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 9 Dec 2025 22:45:21 -0800 Subject: [PATCH 15/15] wip: clean up equiv proofs and add new Pedersen scheme defs --- VerifiedCommitments/PedersenHiding.lean | 45 +++++++++++++++++++++---- VerifiedCommitments/PedersenScheme.lean | 10 ++++++ 2 files changed, 48 insertions(+), 7 deletions(-) diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean index 879c429..9b325a9 100644 --- a/VerifiedCommitments/PedersenHiding.lean +++ b/VerifiedCommitments/PedersenHiding.lean @@ -175,17 +175,48 @@ variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) noncomputable def generate_a : PMF (ZModMult q) := PMF.uniformOfFintype (ZModMult q) +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) + +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 + unfold generate_a + apply bind_skip_const' + 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) : - PMF.map commit.c ((Pedersen.scheme G g q hq_prime).commit (g^(val a).val) m) = + (Pedersen.commit G g q hq_prime (g^(val a).val) m) = PMF.uniformOfFintype G := by - -- Unfold commit definition - -- Use expEquiv_unfold to rewrite as map through expEquiv - -- Apply bind_eq_map' - -- Apply map_uniformOfFintype_equiv - -- Use G_card_q to get the right cardinality - sorry + 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 + + +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 + 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] + + +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 + congr 1 + funext a + exact bij_fixed_a_equiv_pedersen_commit q G_card_q g g_gen_G hq_prime m a -- for fixed aa ∈ {1, ... , q − 1}, and for any m ∈ Zq, if t ← Zq, then g^m*h^r is uniformly distributed over G diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean index 65bf778..7d6d2ea 100644 --- a/VerifiedCommitments/PedersenScheme.lean +++ b/VerifiedCommitments/PedersenScheme.lean @@ -18,4 +18,14 @@ namespace Pedersen 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) + + 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 + end Pedersen