1/-2 WP34 — Abstract signature correctness in an axiomatised cyclic group (no Mathlib).34 `CyclicGroup G` bundles an additively written commutative group with scalar multiplication by5 naturals, a distinguished generator `gen` of order `order`, and an `xcoord` map invariant under6 negation (the model of a prime-order elliptic-curve group such as secp256k1 with the7 x-coordinate projection). EVERY FIELD OF THE STRUCTURE IS AN AXIOM OF THE MODEL; everything8 stated with `theorem` below is derived from those fields and Lean-core arithmetic on `Nat`.9-/1011namespace Wp341213structure CyclicGroup (G : Type) where14 zero : G15 add : G → G → G16 neg : G → G17 nsmul : Nat → G → G18 xcoord : G → Nat19 gen : G20 order : Nat21 -- axioms: commutative group22 add_assoc : ∀ a b c, add (add a b) c = add a (add b c)23 add_comm : ∀ a b, add a b = add b a24 zero_add : ∀ a, add zero a = a25 add_neg : ∀ a, add a (neg a) = zero26 -- axioms: scalar multiplication by naturals (recursive definition, as fields)27 nsmul_zero : ∀ a, nsmul 0 a = zero28 nsmul_succ : ∀ k a, nsmul (k + 1) a = add (nsmul k a) a29 -- axioms: the generator has order `order` (> 1)30 one_lt_order : 1 < order31 nsmul_order : nsmul order gen = zero32 -- axiom: the x-coordinate does not see the sign of a point33 xcoord_neg : ∀ P, xcoord (neg P) = xcoord P3435namespace CyclicGroup3637variable {G : Type} (C : CyclicGroup G)3839/-! ### Derived group facts (theorems, not axioms) -/4041theorem add_zero (a : G) : C.add a C.zero = a := by42 rw [C.add_comm, C.zero_add]4344theorem neg_add (a : G) : C.add (C.neg a) a = C.zero := by45 rw [C.add_comm, C.add_neg]4647/-- Uniqueness of inverses: `a + b = 0 → a = −b`. -/48theorem eq_neg_of_add_eq_zero {a b : G} (h : C.add a b = C.zero) : a = C.neg b := by49 calc a = C.add a C.zero := (C.add_zero a).symm50 _ = C.add a (C.add b (C.neg b)) := by rw [C.add_neg]51 _ = C.add (C.add a b) (C.neg b) := by rw [C.add_assoc]52 _ = C.add C.zero (C.neg b) := by rw [h]53 _ = C.neg b := C.zero_add _5455theorem neg_add_rev (a b : G) : C.neg (C.add a b) = C.add (C.neg a) (C.neg b) := by56 symm57 apply C.eq_neg_of_add_eq_zero58 calc C.add (C.add (C.neg a) (C.neg b)) (C.add a b)59 = C.add (C.neg a) (C.add (C.neg b) (C.add b a)) := by60 rw [C.add_assoc, C.add_comm a b]61 _ = C.add (C.neg a) (C.add (C.add (C.neg b) b) a) := by rw [C.add_assoc]62 _ = C.add (C.neg a) a := by rw [C.neg_add, C.zero_add]63 _ = C.zero := C.neg_add a6465theorem nsmul_add (m k : Nat) (a : G) : C.nsmul (m + k) a = C.add (C.nsmul m a) (C.nsmul k a) := by66 induction k with67 | zero => rw [Nat.add_zero, C.nsmul_zero, C.add_zero]68 | succ k ih => rw [← Nat.add_assoc, C.nsmul_succ, ih, C.nsmul_succ, C.add_assoc]6970theorem nsmul_zero_point (k : Nat) : C.nsmul k C.zero = C.zero := by71 induction k with72 | zero => exact C.nsmul_zero _73 | succ k ih => rw [C.nsmul_succ, ih, C.zero_add]7475theorem nsmul_mul (m k : Nat) (a : G) : C.nsmul (m * k) a = C.nsmul m (C.nsmul k a) := by76 induction m with77 | zero => rw [Nat.zero_mul, C.nsmul_zero, C.nsmul_zero]78 | succ m ih => rw [Nat.succ_mul, C.nsmul_add, ih, C.nsmul_succ]7980theorem add_add_add_comm (a b c d : G) :81 C.add (C.add a b) (C.add c d) = C.add (C.add a c) (C.add b d) := by82 calc C.add (C.add a b) (C.add c d) = C.add a (C.add b (C.add c d)) := C.add_assoc _ _ _83 _ = C.add a (C.add (C.add b c) d) := by rw [C.add_assoc b c d]84 _ = C.add a (C.add (C.add c b) d) := by rw [C.add_comm b c]85 _ = C.add a (C.add c (C.add b d)) := by rw [C.add_assoc c b d]86 _ = C.add (C.add a c) (C.add b d) := (C.add_assoc _ _ _).symm8788theorem nsmul_add_point (k : Nat) (a b : G) :89 C.nsmul k (C.add a b) = C.add (C.nsmul k a) (C.nsmul k b) := by90 induction k with91 | zero => rw [C.nsmul_zero, C.nsmul_zero, C.nsmul_zero, C.zero_add]92 | succ k ih => rw [C.nsmul_succ, C.nsmul_succ, C.nsmul_succ, ih, C.add_add_add_comm]9394theorem nsmul_neg (k : Nat) (a : G) : C.nsmul k (C.neg a) = C.neg (C.nsmul k a) := by95 apply C.eq_neg_of_add_eq_zero96 rw [← C.nsmul_add_point, C.neg_add, C.nsmul_zero_point]9798/-- Membership in the cyclic subgroup generated by `gen` (`P = d•G` for some `d`). -/99def InSubgroup (P : G) : Prop := ∃ d, P = C.nsmul d C.gen100101theorem nsmul_one (a : G) : C.nsmul 1 a = a := by102 rw [show (1 : Nat) = 0 + 1 from rfl, C.nsmul_succ, C.nsmul_zero, C.zero_add]103104theorem gen_inSubgroup : C.InSubgroup C.gen := ⟨1, (C.nsmul_one _).symm⟩105106theorem nsmul_inSubgroup (k : Nat) (P : G) (hP : C.InSubgroup P) : C.InSubgroup (C.nsmul k P) := by107 obtain ⟨d, rfl⟩ := hP108 exact ⟨k * d, (C.nsmul_mul k d C.gen).symm⟩109110/-- Every point of the subgroup is killed by `order`. -/111theorem nsmul_order_of_mem (P : G) (hP : C.InSubgroup P) : C.nsmul C.order P = C.zero := by112 obtain ⟨d, rfl⟩ := hP113 rw [← C.nsmul_mul, Nat.mul_comm, C.nsmul_mul, C.nsmul_order, C.nsmul_zero_point]114115/-- Scalars act modulo `order` on the subgroup. -/116theorem nsmul_mod (k : Nat) (P : G) (hP : C.InSubgroup P) :117 C.nsmul (k % C.order) P = C.nsmul k P := by118 conv => rhs; rw [← Nat.div_add_mod k C.order]119 rw [C.nsmul_add, Nat.mul_comm C.order (k / C.order), C.nsmul_mul, C.nsmul_order_of_mem P hP,120 C.nsmul_zero_point, C.zero_add]121122theorem nsmul_congr_mod (k k' : Nat) (P : G) (hP : C.InSubgroup P) (h : k % C.order = k' % C.order) :123 C.nsmul k P = C.nsmul k' P := by124 rw [← C.nsmul_mod k P hP, h, C.nsmul_mod k' P hP]125126/-- `(order − u)•P = −(u•P)` for `u ≤ order` and `P` in the subgroup. -/127theorem nsmul_order_sub (u : Nat) (hu : u ≤ C.order) (P : G) (hP : C.InSubgroup P) :128 C.nsmul (C.order - u) P = C.neg (C.nsmul u P) := by129 apply C.eq_neg_of_add_eq_zero130 rw [← C.nsmul_add, Nat.sub_add_cancel hu, C.nsmul_order_of_mem P hP]131132/-! ### Schnorr signatures (BIP340-style, abstract)133134Key pair `(d, P = d•G)`, nonce `k` with commitment `R = k•G`, challenge `e` (any natural — in135BIP340 it is `H(R ‖ P ‖ m)`), response `s = (k + e·d) mod n`.136Verification: `s•G = R + e•P`. -/137138/-- Schnorr verification equation. -/139def schnorrVerify (P R : G) (e s : Nat) : Prop :=140 C.nsmul s C.gen = C.add R (C.nsmul e P)141142/-- **Schnorr correctness**: an honestly generated signature verifies. -/143theorem schnorr_correct (d k e : Nat) :144 C.schnorrVerify (C.nsmul d C.gen) (C.nsmul k C.gen) e ((k + e * d) % C.order) := by145 unfold schnorrVerify146 rw [C.nsmul_mod _ _ C.gen_inSubgroup, C.nsmul_add, C.nsmul_mul]147148/-- Variant without the final reduction (`s = k + e·d` as a natural number). -/149theorem schnorr_correct_nat (d k e : Nat) :150 C.schnorrVerify (C.nsmul d C.gen) (C.nsmul k C.gen) e (k + e * d) := by151 unfold schnorrVerify152 rw [C.nsmul_add, C.nsmul_mul]153154/-! ### ECDSA (abstract)155156Signature `(r, s)` on hash `e` under public key `P`. Verification computes `w = s⁻¹ mod n`,157`u₁ = e·w`, `u₂ = r·w`, `R' = u₁•G + u₂•P` and checks `x(R') mod n = r`. The modular inverse is158given as a witness `w` with `s·w ≡ 1 (mod n)`; scalars `e·w`, `r·w` need not be reduced because159`nsmul_mod` shows scalars act modulo `n` on the subgroup. -/160161/-- ECDSA verification predicate (`0 < r, s < n` as in the standard). -/162def ecdsaVerify (P : G) (e r s : Nat) : Prop :=163 0 < r ∧ r < C.order ∧ 0 < s ∧ s < C.order ∧164 ∃ w, (s * w) % C.order = 1 ∧165 (C.xcoord (C.add (C.nsmul (e * w) C.gen) (C.nsmul (r * w) P))) % C.order = r166167/-- Helper: `(n − s)(n − w) ≡ s·w (mod n)` for `s, w ≤ n` (pure `Nat` arithmetic). -/168theorem sub_mul_sub_mod (n s w : Nat) (hs : s ≤ n) (hw : w ≤ n) :169 ((n - s) * (n - w)) % n = (s * w) % n := by170 obtain ⟨p, hp⟩ := Nat.exists_eq_add_of_le hs171 obtain ⟨q, hq⟩ := Nat.exists_eq_add_of_le hw172 have h1 : n - s = p := by omega173 have h2 : n - w = q := by omega174 rw [h1, h2]175 -- p*q + n*(w + s) = s*w + n*n, hence p*q ≡ s*w (mod n)176 have key : p * q + n * (w + s) = s * w + n * n := by177 have e1 : n * n = n * w + s * q + p * q := by178 calc n * n = n * (w + q) := by rw [← hq]179 _ = n * w + n * q := Nat.mul_add _ _ _180 _ = n * w + (s + p) * q := by rw [← hp]181 _ = n * w + (s * q + p * q) := by rw [Nat.add_mul]182 _ = n * w + s * q + p * q := by rw [Nat.add_assoc]183 have e2 : n * (w + s) = n * w + s * q + s * w := by184 calc n * (w + s) = n * w + n * s := Nat.mul_add _ _ _185 _ = n * w + s * n := by rw [Nat.mul_comm n s]186 _ = n * w + s * (w + q) := by rw [← hq]187 _ = n * w + (s * w + s * q) := by rw [Nat.mul_add]188 _ = n * w + s * q + s * w := by omega189 rw [e1, e2]; omega190 have : (p * q + n * (w + s)) % n = (s * w + n * n) % n := by rw [key]191 rwa [Nat.add_mul_mod_self_left, Nat.add_mul_mod_self_left] at this192193/-- **ECDSA malleability**: if `(r, s)` verifies then so does `(r, n − s)`, using only the194group axioms and `xcoord (−Q) = xcoord Q`. -/195theorem ecdsa_malleable (P : G) (hP : C.InSubgroup P) (e r s : Nat)196 (h : C.ecdsaVerify P e r s) : C.ecdsaVerify P e r (C.order - s) := by197 obtain ⟨hr0, hrn, hs0, hsn, w, hw, hx⟩ := h198 have hn : 0 < C.order := Nat.lt_trans Nat.zero_lt_one C.one_lt_order199 have hG : C.InSubgroup C.gen := C.gen_inSubgroup200 -- reduce the inverse witness modulo n: w0 = w mod n, 0 < w0 < n, s·w0 ≡ 1201 obtain ⟨w0, hw0def⟩ : ∃ w0, w % C.order = w0 := ⟨_, rfl⟩202 have hw0n : w0 < C.order := hw0def ▸ Nat.mod_lt _ hn203 have hw0 : (s * w0) % C.order = 1 := by204 rw [Nat.mul_mod, ← hw0def, Nat.mod_mod, ← Nat.mul_mod, hw]205 have hw0pos : 0 < w0 := by206 rcases Nat.eq_zero_or_pos w0 with h0 | h0207 · rw [h0, Nat.mul_zero, Nat.zero_mod] at hw0; omega208 · exact h0209 -- (n − w0) + w is a multiple of n210 have hsum : C.order - w0 + w = C.order * (w / C.order + 1) := by211 have := Nat.div_add_mod w C.order212 rw [hw0def] at this213 rw [Nat.mul_add, Nat.mul_one]; omega214 -- u•(n − w0) + u•w = 0 for every u and every Q in the subgroup215 have hneg : ∀ (u : Nat) (Q : G), C.InSubgroup Q →216 C.nsmul (u * (C.order - w0)) Q = C.neg (C.nsmul (u * w) Q) := by217 intro u Q hQ218 apply C.eq_neg_of_add_eq_zero219 have h1 : u * (C.order - w0) + u * w = C.order * ((w / C.order + 1) * u) := by220 rw [← Nat.mul_add, hsum]; ac_rfl221 rw [← C.nsmul_add, h1, C.nsmul_mul, C.nsmul_order_of_mem _ (C.nsmul_inSubgroup _ _ hQ)]222 refine ⟨hr0, hrn, by omega, by omega, C.order - w0, ?_, ?_⟩223 · -- (n − s)(n − w0) ≡ s·w0 ≡ 1224 rw [sub_mul_sub_mod _ _ _ (Nat.le_of_lt hsn) (Nat.le_of_lt hw0n), hw0]225 · -- the verification point is negated, so its x-coordinate is unchanged226 rw [hneg e C.gen hG, hneg r P hP, ← C.neg_add_rev, C.xcoord_neg]227 exact hx228229/-- **ECDSA correctness**: an honestly generated signature verifies. Hypotheses encode230`r = x(k•G) mod n` and `s ≡ k⁻¹(e + r·d)`, i.e. `k·s ≡ e + r·d (mod n)`, with a witness `w` for231`s⁻¹`. -/232theorem ecdsa_correct (d k e r s w : Nat)233 (hr0 : 0 < r) (hrn : r < C.order) (hs0 : 0 < s) (hsn : s < C.order)234 (hr : (C.xcoord (C.nsmul k C.gen)) % C.order = r)235 (hs : (k * s) % C.order = (e + r * d) % C.order)236 (hw : (s * w) % C.order = 1) :237 C.ecdsaVerify (C.nsmul d C.gen) e r s := by238 refine ⟨hr0, hrn, hs0, hsn, w, hw, ?_⟩239 have hG : C.InSubgroup C.gen := C.gen_inSubgroup240 have hpt : C.add (C.nsmul (e * w) C.gen) (C.nsmul (r * w) (C.nsmul d C.gen)) =241 C.nsmul k C.gen := by242 rw [← C.nsmul_mul, ← C.nsmul_add]243 apply C.nsmul_congr_mod _ _ _ hG244 -- e·w + r·w·d = w·(e + r·d) ≡ w·k·s = k·(s·w) ≡ k245 have e1 : e * w + r * w * d = w * (e + r * d) := by rw [Nat.mul_add]; ac_rfl246 have e2 : w * (k * s) = k * (s * w) := by ac_rfl247 rw [e1, Nat.mul_mod, ← hs, ← Nat.mul_mod, e2, Nat.mul_mod, hw, Nat.mul_one, Nat.mod_mod]248 rw [hpt, hr]249250end CyclicGroup251252end Wp34253