Curve group orders via the Hasse bound, for prime-order curves and for Pallas/Vesta; includes fast SWPoint scalar mul

CompElliptic.lean

@@ -5,11 +5,14 @@ as described in the files LICENSE-APACHE and LICENSE-MIT.
 Authors: Daira-Emma Hopwood
 -/
 import CompElliptic.Basic
+import CompElliptic.ScalarMul
 import CompElliptic.CoordinateSystem
 import CompElliptic.Encoding
 import CompElliptic.Encodings.Common
 import CompElliptic.Encodings.Pasta
 import CompElliptic.Fields.Pasta
 import CompElliptic.Fields.Sqrt
 import CompElliptic.CurveForms.ShortWeierstrass
+import CompElliptic.CurveOrder
 import CompElliptic.Curves.Pasta
+import CompElliptic.Curves.PastaOrder

CompElliptic/CoordinateSystem.lean

@@ -6,6 +6,7 @@ Authors: Daira-Emma Hopwood
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.Group.Basic
+import CompElliptic.ScalarMul
 
 /-!
 # Coordinate systems
@@ -86,7 +87,12 @@ instance : AddCommGroup P.Quot where
   add := (· + ·)
   zero := 0
   neg := (- ·)
-  nsmul := nsmulRec
+  nsmul := binNsmul (· + ·) 0
+  nsmul_zero x := binNsmul_zero _ _ x
+  nsmul_succ n x := by
+    refine binNsmul_succ ?_ ?_ n x
+    · exact fun a b c => Quotient.inductionOn₃ a b c (fun p q r => Quotient.sound (P.add_assoc p.2 q.2 r.2))
+    · exact fun a => Quotient.inductionOn a (fun p => Quotient.sound (P.add_zero p.2))
   zsmul := zsmulRec
   add_assoc := by
     rintro x y z

CompElliptic/CurveForms/ShortWeierstrass.lean

@@ -21,6 +21,11 @@ One module for the short-Weierstrass curve form `y² = x³ + A x + B`, layered:
 3. **Rich bundled types** — `SWCurve` (bundles ellipticity and `B ≠ 0`) and `SWPoint E`
    (correct-by-construction: on the curve or `𝒪`). This is the correct-by-construction interface
    used to express the group structure and circuit gadgets.
+4. **Fast scalar multiplication** — the group action `n • _` on `SWPoint E` is the generic binary
+   double-and-add `CompElliptic.binNsmul` (`ScalarMul.lean`), so `n • P` computes in `O(log n)` and
+   is `native_decide`-friendly for cryptographic-size scalars, while remaining the genuine scalar
+   action (every Mathlib `n • _` lemma still applies, since they follow from `nsmul_zero` /
+   `nsmul_succ`).
 
 The field assumption is a generic `[Field F]`: `SWCurve.IsElliptic` excludes characteristic 2
 (`sw_Δ = 0` there), so binary fields are gracefully excluded, but without precluding any future
@@ -398,14 +403,34 @@ instance (E : SWCurve F) : Zero (SWPoint E) := ⟨SWPoint.zero E⟩
 instance (E : SWCurve F) : Add (SWPoint E) := ⟨sw_add⟩
 instance (E : SWCurve F) : Neg (SWPoint E) := ⟨sw_neg⟩
 
+/-! ### Fast (logarithmic) scalar multiplication
+
+The spec-level `smul` is linear (`n` additions), so it cannot be evaluated by `decide` or
+`native_decide` for cryptographic-size scalars (`≈ 2^254`). The group action `n • _` on `SWPoint E`
+(the `nsmul` field of the `AddCommGroup` instance below) is instead the generic binary
+double-and-add `CompElliptic.binNsmul` over the raw `sw_add` / `SWPoint.zero`. So `n • P` computes in
+`O(log n)` and is `native_decide`-friendly, while remaining the genuine scalar action: every Mathlib
+`n • _` lemma still applies, since they follow from `nsmul_zero` and `nsmul_succ`. -/
+
+/-- `SWPoint E` has decidable equality (the `onCurve` field is a `Prop`, so equality reduces to the
+coordinate pair); needed for `native_decide` on `n • P = Q`. -/
+instance instDecidableEqSWPoint {E : SWCurve F} : DecidableEq (SWPoint E) := fun P Q =>
+  decidable_of_iff ((P.x, P.y) = (Q.x, Q.y)) ⟨SWPoint.ext_pair, fun h => by rw [h]⟩
+
 /-- The abelian group of representable points on `E`: identity laws and inverses are immediate;
-commutativity and associativity transport from the raw `add` lemmas, whose hypotheses `E`'s bundled
-fields (`IsElliptic`, `B_nonzero`) discharge. -/
+commutativity and associativity transport from the raw `add` lemmas, whose hypotheses are discharged
+by `E`'s bundled fields (`IsElliptic` and `B_nonzero`). -/
 instance (E : SWCurve F) : AddCommGroup (SWPoint E) where
   add := sw_add
   zero := SWPoint.zero E
   neg := sw_neg
-  nsmul := nsmulRec
+  nsmul := binNsmul sw_add (SWPoint.zero E)
+  nsmul_zero P := binNsmul_zero _ _ P
+  nsmul_succ n P := by
+    haveI := instIsElliptic E
+    refine binNsmul_succ ?_ ?_ n P
+    · exact fun a b c => SWPoint.ext_pair (add_assoc E.B_nonzero a.onCurve b.onCurve c.onCurve)
+    · exact fun a => SWPoint.ext_pair (ShortWeierstrass.add_zero E.A (a.x, a.y))
   zsmul := zsmulRec
   add_assoc P Q R := by
     haveI := instIsElliptic E
@@ -418,12 +443,12 @@ instance (E : SWCurve F) : AddCommGroup (SWPoint E) where
     rw [add_comm (valid_neg P.onCurve) P.onCurve]
     exact add_neg E.A (P.x, P.y))
 
-/-- The group action `n • P` on `SWPoint E` is the spec-level `smul` on the underlying coordinates,
-so the two notions of scalar multiplication agree. -/
+/-- The group action `n • P` on `SWPoint E` is equivalent to the spec-level `smul` on the underlying
+coordinates, so the two notions of scalar multiplication agree. -/
 theorem coords_nsmul {E : SWCurve F} (n : ℕ) (P : SWPoint E) :
     ((n • P).x, (n • P).y) = smul E.A n (P.x, P.y) := by
   induction n with
-  | zero => rfl
+  | zero => rw [zero_nsmul]; rfl
   | succ k ih =>
     rw [succ_nsmul]
     show add E.A ((k • P).x, (k • P).y) (P.x, P.y) = smul E.A (k + 1) (P.x, P.y)

CompElliptic/CurveOrder.lean

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2026 CompElliptic Contributors. All rights reserved.
+Released under the Apache License, Version 2.0, or the MIT license, at your option,
+as described in the files LICENSE-APACHE and LICENSE-MIT.
+Authors: Daira-Emma Hopwood
+-/
+import CompElliptic.CurveForms.ShortWeierstrass
+import Mathlib.GroupTheory.OrderOfElement
+
+/-!
+# Pinning a prime-order curve group's order without point-counting
+
+For a curve whose group is *known to have prime order* r, fixing the order to exactly r needs
+no point-counting algorithm (no Schoof, no proof of a counting algorithm's correctness).
+It needs only:
+
+1. a non-identity point P killed by r (so r ∣ #G, since r is prime); and
+2. an *upper* bound #G < 2r, which can be provided by the Hasse bound for elliptic curves.
+
+This module is the curve-agnostic core of that argument, in two layers.
+
+* **Layer 1 — pure finite-group theory.** `card_eq_of_prime_witness` holds for *any* finite
+  additive group, with no reference to elliptic curves. A witness of r • P = 0 forces r ∣ #G,
+  and #G < 2r then forces #G = r.
+
+* **Layer 2 — the Hasse bound.** If G is any elliptic curve E(F) over any finite field F of
+  order q ≥ 37, Hasse's theorem |#E(F) - (q+1)| ≤ 2·√q supplies the #G < 2r premiss provided
+  that r also satisfies the Hasse bound. For a prime-order cryptographic curve r ≈ q, so 2r
+  sits far above the Hasse upper bound. Mathlib does not yet have Hasse's theorem for
+  `WeierstrassCurve`, so we state it as a predicate (`HasseBound`) and take it as a hypothesis.
+
+This is an application of the *Independently re-checkable trust* principle: the one piece
+of trust beyond the kernel + standard axioms is a single *named general theorem* (Hasse),
+flagged as an explicit hypothesis. It is separated from the concrete *closed numeric* fact
+4q < (2r - (q+1))² (`hgap`), or alternatively the Hasse bound on r (`hr`), either of which
+can be verified by any independent tool.
+-/
+
+namespace CompElliptic.CurveOrder
+
+open CompElliptic.CurveForms.ShortWeierstrass
+
+/-! ## Layer 1: pin the order from a prime-order witness (any finite additive group) -/
+
+/-- If `r` is prime, the finite additive group `G` has a non-identity element `P` killed by `r`
+(`r • P = 0`), and `#G < 2r`, then `#G = r`.
+
+`r • P = 0` gives `addOrderOf P ∣ r`; primality and `P ≠ 0` upgrade this to `addOrderOf P = r`,
+so `r ∣ #G` by Lagrange. With `0 < #G < 2r` the only multiple of `r` available is `r` itself. -/
+theorem card_eq_of_prime_witness {G : Type*} [AddGroup G] [Finite G] {r : ℕ}
+    (hr : r.Prime) {P : G} (hP : P ≠ 0) (hPr : r • P = 0)
+    (hlt : Nat.card G < 2 * r) : Nat.card G = r := by
+  have hdvd : addOrderOf P ∣ r := addOrderOf_dvd_iff_nsmul_eq_zero.mpr hPr
+  have hne1 : addOrderOf P ≠ 1 := by simp [hP]
+  have hord : addOrderOf P = r := (hr.eq_one_or_self_of_dvd _ hdvd).resolve_left hne1
+  have hrdvd : r ∣ Nat.card G := hord ▸ addOrderOf_dvd_natCard P
+  have hne0 : Nat.card G ≠ 0 := Nat.card_ne_zero.mpr ⟨⟨P⟩, inferInstance⟩
+  exact Nat.eq_of_dvd_of_lt_two_mul hne0 hrdvd hlt
+
+/-! ## Layer 2: the Hasse bound (assumed; not yet in Mathlib) discharges `#G < 2r` -/
+
+/-- The Hasse interval for a field of size `q`: the cardinalities `n` within `2√q` of `q + 1`,
+written sqrt-free over `ℤ` as `(n - (q+1))² ≤ 4·q` (equivalently `|n - (q+1)| ≤ 2√q`). By Hasse's
+theorem every point count `#E(F)` lies in it (with `q = #F`); we use the same interval to constrain
+a candidate prime order. -/
+def hasseInterval (q : ℕ) : Set ℕ := { n | ((n : ℤ) - (q+1))^2 ≤ 4*q }
+
+/-- The arithmetic step from Hasse to the layer-1 premiss, purely over `ℕ`/`ℤ` and independent of
+any particular curve. From the sqrt-free Hasse inequality on `N` relative to the field size `q`
+(`(N - (q+1))² ≤ 4·q`), the concrete gap `4·q < (2r - (q+1))²`, and `q + 1 ≤ 2r`, conclude `N < 2r`.
+(Only the *upper* Hasse bound is used; the gap and `q + 1 ≤ 2r` are closed facts about the two
+relevant numbers, true here because `r ≈ q` so `2r` clears the upper bound with room.) -/
+theorem lt_two_mul_of_hasse {N q r : ℕ}
+    (hHasse : N ∈ hasseInterval q)
+    (hgap : 4*(q : ℤ) < (2*r - (q+1))^2)
+    (hle : (q : ℤ) + 1 ≤ 2*r) :
+    N < 2*r := by
+  simp only [hasseInterval, Set.mem_setOf_eq] at hHasse
+  by_contra hcon
+  rw [not_lt] at hcon
+  have hN : (2*r : ℤ) ≤ (N : ℤ) := by exact_mod_cast hcon
+  have h0 : (0 : ℤ) ≤ 2*r - (q+1) := by linarith
+  have h1 : 2*(r : ℤ) - (q+1) ≤ (N : ℤ) - (q+1) := by linarith
+  have hmono : (2*(r : ℤ) - (q+1))^2 ≤ ((N : ℤ) - (q+1))^2 := pow_le_pow_left₀ h0 h1 2
+  linarith
+
+/-- The Hasse bound for a short-Weierstrass elliptic curve `E` over a finite field `F` with
+`q = #F`: `|#E(F) - (q+1)| ≤ 2·√q`, written sqrt-free over `ℤ` as `(#E(F) - (q+1))² ≤ 4·q`,
+where `#E(F) = Nat.card (SWPoint E)`.
+
+This is Hasse's theorem, the "Riemann hypothesis for elliptic function fields":
+
+> H. Hasse, *Zur Theorie der abstrakten elliptischen Funktionenkörper III: Die Struktur des
+> Meromorphismenrings; Die Riemannsche Vermutung*, Journal für die reine und angewandte
+> Mathematik (Crelle's Journal) *175* (1936), 193–208. doi:10.1515/crll.1936.175.193.
+
+The point-count form used here is §4.2 (p. 206): for `N₁` the number of degree-one prime divisors
+(`= #E(F)`, the `F`-rational places including `𝒪`) and `q = #F`, `(q + 1 - N₁)² ≤ 4q`. It rests on
+§3.1 (p. 203), where the Frobenius meromorphism `π : (x, y) ↦ (x^q, y^q)` satisfies
+`Q(π) = π² - lπ + q = 0` with `l² ≤ 4q`. A scan of part III is available at
+https://download.uni-mainz.de/mathematik/Algebraische%20Geometrie/Lehre/WS23.Padische.Hasse.III.pdf
+
+Mathlib does not yet carry this for `WeierstrassCurve`, so we define the statement and take it
+as a hypothesis where needed. -/
+def HasseBound {F : Type*} [Field F] [Fintype F] (E : SWCurve F) : Prop :=
+  Nat.card (SWPoint E) ∈ hasseInterval (Fintype.card F)
+
+/-- `SWPoint E` is finite whenever the base field is, by the injection into `F × F`. -/
+instance instFiniteSWPoint {F : Type*} [Field F] [DecidableEq F] [Fintype F] (E : SWCurve F) :
+    Finite (SWPoint E) :=
+  Finite.of_injective (fun P => (P.x, P.y)) (fun _ _ h => SWPoint.ext_pair h)
+
+/-- **Order of a prime-order short-Weierstrass curve group, via Hasse.** Given Hasse's bound
+(assumed), a prime `r`, a non-identity point `P` with `r • P = 0`, and the concrete gap
+`4q < (2r - (q+1))²` together with `q + 1 ≤ 2r`, the curve group has exactly `r` points. -/
+theorem card_eq_of_hasse {F : Type*} [Field F] [DecidableEq F] [Fintype F] (E : SWCurve F)
+    {r : ℕ} (hrPrime : r.Prime) {P : SWPoint E} (hP : P ≠ 0) (hPr : r • P = 0)
+    (hHasse : HasseBound E)
+    (hgap : 4*(Fintype.card F : ℤ) < (2*r - (Fintype.card F + 1))^2)
+    (hle : (Fintype.card F : ℤ) + 1 ≤ 2*r) :
+    Nat.card (SWPoint E) = r :=
+  card_eq_of_prime_witness hrPrime hP hPr (lt_two_mul_of_hasse hHasse hgap hle)
+
+/-! ## Alternative approach that reaches the same conclusion -/
+
+/-- Convenience form of `lt_two_mul_of_hasse` for callers who already hold the two-sided Hasse
+bound. For `37 ≤ q` (the least prime power for which `2·(q + 1 - 2√q) > q + 1 + 2√q`), the
+explicit gap inequalities are implied by the Hasse bound on `r` itself: a `r` in the Hasse interval
+`[q + 1 - 2√q, q + 1 + 2√q]` has `2r ≥ 2·(q + 1 - 2√q) > q + 1 + 2√q ≥ N`, so `N < 2r`.
+
+The Hasse bound on `r` (`hr`) is essential — `37 ≤ q` alone is unsound. A witness of small prime
+order (e.g. an order-2 point on a group of composite order in the interval) would otherwise force a
+wrong conclusion; `hr` pins `r` to the interval from below, ruling that out. -/
+theorem lt_two_mul_of_hasse_of_field_ge_37 {N q r : ℕ}
+    (hN : N ∈ hasseInterval q)
+    (hr : r ∈ hasseInterval q)
+    (hq : 37 ≤ q) :
+    N < 2*r := by
+  simp only [hasseInterval, Set.mem_setOf_eq] at hN hr
+  have hq' : (36 : ℤ) < q := by exact_mod_cast hq
+  by_contra hcon
+  rw [not_lt] at hcon
+  have hcon' : 2 * (r : ℤ) ≤ (N : ℤ) := by exact_mod_cast hcon
+  -- Writing `n = N - (q+1)`, `m = r - (q+1)`: from `hN`/`hr`, `(n - 2m)² ≤ 3n² + 6m² ≤ 36·q`
+  -- (the `sq_nonneg (n+m)` hint supplies `-4nm ≤ 2(n² + m²)`); but `N ≥ 2r` gives `n - 2m ≥ q+1`,
+  -- so `(q+1)² ≤ (n-2m)² ≤ 36·q`, contradicting `37 ≤ q` (where `(q+1)² > 36·q`).
+  nlinarith [hN, hr, hq', hcon',
+    sq_nonneg ((N : ℤ) - (q+1) + ((r : ℤ) - (q+1))),
+    mul_nonneg (show (0 : ℤ) ≤ (N : ℤ) - 2*r by linarith)
+               (show (0 : ℤ) ≤ (N : ℤ) - 2*r + 2*((q : ℤ)+1) by linarith)]
+
+/-- Curve-level capstone of the `37 ≤ #F` route: combine `HasseBound` (assumed) with `37 ≤ #F` and
+the Hasse bound on the prime `r` to conclude the curve group has exactly `r` points, without the
+caller having to supply the explicit gap inequalities `hgap` and `hle`.
+
+`hHasse` is definitionally the two-sided bound on `#E(F)` that `lt_two_mul_of_hasse_of_field_ge_37`
+needs; see there for why `hr` is needed. -/
+theorem card_eq_of_hasse_of_field_ge_37 {F : Type*} [Field F] [DecidableEq F] [Fintype F]
+    (E : SWCurve F) {r : ℕ} (hrPrime : r.Prime) {P : SWPoint E} (hP : P ≠ 0) (hPr : r • P = 0)
+    (hHasse : HasseBound E)
+    (hr : r ∈ hasseInterval (Fintype.card F))
+    (hq : 37 ≤ Fintype.card F) :
+    Nat.card (SWPoint E) = r :=
+  card_eq_of_prime_witness hrPrime hP hPr (lt_two_mul_of_hasse_of_field_ge_37 hHasse hr hq)
+
+end CompElliptic.CurveOrder

CompElliptic/Curves/PastaOrder.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2026 CompElliptic Contributors. All rights reserved.
+Released under the Apache License, Version 2.0, or the MIT license, at your option,
+as described in the files LICENSE-APACHE and LICENSE-MIT.
+Authors: Daira-Emma Hopwood
+-/
+import CompElliptic.Curves.Pasta
+import CompElliptic.CurveOrder
+
+/-!
+# Orders of the Pasta curve groups (Pallas and Vesta)
+
+Instantiates `CompElliptic.CurveOrder.card_eq_of_hasse_of_field_ge_37` at the two Pasta curves:
+assuming Hasse's bound (`HasseBound`, the one irreducible hypothesis — Mathlib lacks Hasse's
+theorem), the Pallas group has order `PALLAS_SCALAR_CARD` and the Vesta group has order
+`PALLAS_BASE_CARD` (the Pasta cycle: each curve's order is the other's base-field size).
+
+Everything else is discharged outright. The test point `G = (-1, 2)` is the prime-order witness,
+and the witness fact `[order] G = 𝒪` (a `≈ 2^254` scalar multiplication) is a one-line
+`native_decide` now that the `SWPoint` scalar action `•` itself computes in `O(log n)`. The
+field-size facts (`order ∈ hasseInterval (#F)`, `37 ≤ #F`) are concrete closed facts.
+-/
+
+namespace CompElliptic.Curves.Pasta
+
+open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder CompElliptic.Fields.Pasta
+
+namespace Pallas
+
+/-- The test point `(-1, 2)` as a point of the Pallas curve — the prime-order witness. -/
+def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by native_decide)⟩
+
+theorem Gpt_ne_zero : Gpt ≠ 0 := by native_decide
+
+/-- `[q] G = 𝒪`, where `q = PALLAS_SCALAR_CARD` is the Pallas group order. -/
+theorem scalarCard_nsmul_Gpt : PALLAS_SCALAR_CARD • Gpt = 0 := by native_decide
+
+/-- **The Pallas curve group has order `PALLAS_SCALAR_CARD`**, assuming Hasse's bound. -/
+theorem card_eq (hHasse : HasseBound curve) :
+    Nat.card (SWPoint curve) = PALLAS_SCALAR_CARD := by
+  refine card_eq_of_hasse_of_field_ge_37 curve PALLAS_SCALAR_is_prime Gpt_ne_zero
+    scalarCard_nsmul_Gpt hHasse ?_ ?_
+  · rw [show Fintype.card PallasBaseField = PALLAS_BASE_CARD from ZMod.card _]
+    simp only [hasseInterval, Set.mem_setOf_eq]; native_decide
+  · rw [show Fintype.card PallasBaseField = PALLAS_BASE_CARD from ZMod.card _]; decide
+
+end Pallas
+
+namespace Vesta
+
+/-- The test point `(-1, 2)` as a point of the Vesta curve — the prime-order witness. -/
+def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by native_decide)⟩
+
+theorem Gpt_ne_zero : Gpt ≠ 0 := by native_decide
+
+/-- `[p] G = 𝒪`, where `p = PALLAS_BASE_CARD` is the Vesta group order. -/
+theorem baseCard_nsmul_Gpt : PALLAS_BASE_CARD • Gpt = 0 := by native_decide
+
+/-- **The Vesta curve group has order `PALLAS_BASE_CARD`**, assuming Hasse's bound. -/
+theorem card_eq (hHasse : HasseBound curve) :
+    Nat.card (SWPoint curve) = PALLAS_BASE_CARD := by
+  refine card_eq_of_hasse_of_field_ge_37 curve PALLAS_BASE_is_prime Gpt_ne_zero
+    baseCard_nsmul_Gpt hHasse ?_ ?_
+  · rw [show Fintype.card VestaBaseField = PALLAS_SCALAR_CARD from ZMod.card _]
+    simp only [hasseInterval, Set.mem_setOf_eq]; native_decide
+  · rw [show Fintype.card VestaBaseField = PALLAS_SCALAR_CARD from ZMod.card _]; decide
+
+end Vesta
+
+end CompElliptic.Curves.Pasta