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