wip: refactor bijection equiv

VerifiedCommitments/PedersenHiding.lean

@@ -2,13 +2,20 @@ 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)
 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