diff --git a/CompElliptic.lean b/CompElliptic.lean index 56e9a59..513c96c 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -5,6 +5,7 @@ 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 @@ -12,4 +13,6 @@ 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 diff --git a/CompElliptic/CoordinateSystem.lean b/CompElliptic/CoordinateSystem.lean index c9f43c2..d9261bc 100644 --- a/CompElliptic/CoordinateSystem.lean +++ b/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 diff --git a/CompElliptic/CurveForms/ShortWeierstrass.lean b/CompElliptic/CurveForms/ShortWeierstrass.lean index 7a1d49d..d7eb6f5 100644 --- a/CompElliptic/CurveForms/ShortWeierstrass.lean +++ b/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) diff --git a/CompElliptic/CurveOrder.lean b/CompElliptic/CurveOrder.lean new file mode 100644 index 0000000..1b3ed03 --- /dev/null +++ b/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 diff --git a/CompElliptic/Curves/PastaOrder.lean b/CompElliptic/Curves/PastaOrder.lean new file mode 100644 index 0000000..ed0d2af --- /dev/null +++ b/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 diff --git a/CompElliptic/ScalarMul.lean b/CompElliptic/ScalarMul.lean new file mode 100644 index 0000000..27c3795 --- /dev/null +++ b/CompElliptic/ScalarMul.lean @@ -0,0 +1,92 @@ +/- +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 Mathlib.Data.Nat.Init + +/-! +# Scalar multiplication by binary double-and-add + +`binNsmul add zero n x` computes `[n] x` (`n`-fold `add` from `zero`) by binary double-and-add: +`O(log n)` applications of `add`, via a single shared recursive call. It is stated over a *raw* +binary operation `add : M → M → M` and identity `zero : M` —not an `AddMonoid`— precisely so it +can supply the `nsmul` field *of* an `AddMonoid` / `AddCommGroup` instance (a field cannot refer to +the structure it is defining). + +It is proven equal (`binNsmul_eq_linNsmul`) to the linear fold `linNsmul`, giving the `nsmul_zero` / +`nsmul_succ` obligations (`binNsmul_zero`, `binNsmul_succ`) any such instance needs. The only +algebraic facts required are associativity of `add` and right-identity of `zero`. +-/ + +namespace CompElliptic + +variable {M : Type*} + +/-- Linear scalar multiplication: the left fold `add (... add (add zero x) x ...) x` of `n` copies. -/ +def linNsmul (add : M → M → M) (zero : M) : ℕ → M → M + | 0, _ => zero + | n + 1, x => add (linNsmul add zero n x) x + +/-- Binary double-and-add scalar multiplication: `O(log n)` applications of `add` (the recursive +value is shared via `let`, so there is exactly one recursive call), hence evaluable by +`native_decide` for large `n`. Proven equal to `linNsmul` by `binNsmul_eq_linNsmul`. -/ +def binNsmul (add : M → M → M) (zero : M) (n : ℕ) (x : M) : M := + if h : n = 0 then zero + else + let q := binNsmul add zero (n / 2) x + let d := add q q + if n % 2 = 1 then add d x else d + decreasing_by exact Nat.div_lt_self (Nat.pos_of_ne_zero h) (by decide) + +theorem binNsmul_zero (add : M → M → M) (zero : M) (x : M) : binNsmul add zero 0 x = zero := by + rw [binNsmul]; rfl + +variable {add : M → M → M} {zero : M} + (hassoc : ∀ a b c : M, add (add a b) c = add a (add b c)) (hzero : ∀ a : M, add a zero = a) + +include hassoc hzero + +/-- Additivity of `linNsmul` in the scalar: `[m + n] x = [m] x + [n] x`. -/ +theorem linNsmul_add (m n : ℕ) (x : M) : + linNsmul add zero (m + n) x = add (linNsmul add zero m x) (linNsmul add zero n x) := by + induction n with + | zero => + show linNsmul add zero m x = add (linNsmul add zero m x) zero + rw [hzero] + | succ k ih => + show add (linNsmul add zero (m + k) x) x + = add (linNsmul add zero m x) (add (linNsmul add zero k x) x) + rw [ih, hassoc] + +/-- The binary form computes the same value as the linear fold. -/ +theorem binNsmul_eq_linNsmul (n : ℕ) (x : M) : + binNsmul add zero n x = linNsmul add zero n x := by + induction n using Nat.strong_induction_on with + | _ n ih => + rw [binNsmul] + split + · rename_i h; subst h; rfl + · rename_i h + have hlt : n / 2 < n := Nat.div_lt_self (Nat.pos_of_ne_zero h) (by decide) + simp only [ih (n / 2) hlt] + split + · rename_i hodd + rw [(linNsmul_add hassoc hzero (n / 2) (n / 2) x).symm] + have hn : n / 2 + n / 2 + 1 = n := by omega + have hstep : add (linNsmul add zero (n / 2 + n / 2) x) x + = linNsmul add zero (n / 2 + n / 2 + 1) x := rfl + rw [hstep, hn] + · rename_i heven + rw [(linNsmul_add hassoc hzero (n / 2) (n / 2) x).symm] + have hn : n / 2 + n / 2 = n := by omega + rw [hn] + +/-- The double-and-add recurrence: `[n+1] x = [n] x + x`. Supplies the `nsmul_succ` instance field. -/ +theorem binNsmul_succ (n : ℕ) (x : M) : + binNsmul add zero (n + 1) x = add (binNsmul add zero n x) x := by + rw [binNsmul_eq_linNsmul hassoc hzero (n + 1) x, binNsmul_eq_linNsmul hassoc hzero n x] + rfl + +end CompElliptic diff --git a/TODO.md b/TODO.md index 8675f54..943b4ef 100644 --- a/TODO.md +++ b/TODO.md @@ -111,6 +111,10 @@ types + transport) has been consolidated into these and removed. `SWPoint E` for any `SWCurve`. - [x] closure of the raw `smul` (`valid_smul`, induction on `valid_add`) and `coords_nsmul` relating the group action `n • P` to the spec-level `smul` on the underlying coordinates. + - [x] Fast `•` (generic `binNsmul`, `ScalarMul.lean`): the `SWPoint E` `nsmul` field is the binary + double-and-add `binNsmul`, so `n • P` itself computes in `O(log n)` and is `native_decide`-friendly + for `≈ 2^254` scalars while staying the genuine group action (all Mathlib `n • _` lemmas still + apply). `DecidableEq (SWPoint E)` added (for `native_decide` on point equality). - [x] Non-residue `five_not_isSquare` (Euler's criterion `ZMod.euler_criterion`: `5 ^ (p / 2) = -1 ≠ 1`) ⟹ no Pallas point has `x = 0` (`no_onCurve_x_zero`), in `Curves/Pasta.lean` — the spec §5.4.9.7 property the `(0,0) ≡ 𝒪` representation relies on. The power is evaluated by @@ -121,15 +125,37 @@ types + transport) has been consolidated into these and removed. `isUnit_iff_ne_zero` + `decide` (Pallas `sw_Δ = -10800 ≠ 0`), `B ≠ 0` by `decide`. - [x] Vesta `SWCurve` instance (identical, over the Vesta base field), with its own `five_not_isSquare` / `no_onCurve_x_zero` (`5` is a non-residue in the Vesta base field too). -- [ ] A windowed / double-and-add `smul` matching the circuit's scalar decomposition. (The - iterated-add `smul` is adequate for *stating* soundness; the circuit's structure is what the - gadget proofs reduce to.) +- [ ] A windowed / double-and-add `smul` matching the **circuit's** scalar decomposition — distinct + from the generic computational `binNsmul` above (the group action `n • _`). The iterated-add `smul` + is adequate for *stating* soundness; the circuit's structure is what the gadget proofs reduce to. + +## CompElliptic — group order (`CurveOrder.lean`, `Curves/PastaOrder.lean`) + +- [x] Prime-order pinning without point-counting (`CurveOrder.lean`): `card_eq_of_prime_witness` + (pure finite-group theory — a non-identity point killed by prime `r`, with `#G < 2r`, forces + `#G = r`); the sqrt-free Hasse bound as `hasseInterval` / `HasseBound`, taken as a hypothesis + (Mathlib has no Hasse theorem for `WeierstrassCurve`; cited to Hasse, Crelle 175 (1936), + §3.1/§4.2); capstones `card_eq_of_hasse` (explicit gap) and `card_eq_of_hasse_of_field_ge_37` + (`37 ≤ #F` plus `r` in the Hasse interval). No `sorry`/`axiom`/`native_decide`; standard axioms. +- [x] Pallas/Vesta orders (`Curves/PastaOrder.lean`): assuming `HasseBound`, `Pallas.card_eq` + (`= PALLAS_SCALAR_CARD`) and `Vesta.card_eq` (`= PALLAS_BASE_CARD`) — the Pasta cycle — with witness + `G = (-1, 2)` and `[order] G = 𝒪` discharged by a one-line `native_decide` (fast `•`). +- [ ] Small-cofactor variant (`#G = h·r` for known `h`): a straightforward Layer-1 generalization, + deferred. Needed for Jubjub (cofactor 8), which also needs the Edwards form first. ## CompElliptic — other forms & the group abstraction (later) - [x] Coordinate-system abstraction (`CoordinateSystem.lean`): carrier + `Valid` + `Rel` + ops → derived `AddCommGroup` on the quotient. The locus of generality; the setoid/quotient that - non-injective coordinate systems need lives here. Affine is the `Rel = Eq` instance. + non-injective coordinate systems need lives here. Affine is the `Rel = Eq` instance + (`affineCoordinateSystem`, in `ShortWeierstrass.lean`). Its `nsmul` is the generic `binNsmul` too, + so `n • _` on the quotient (e.g. `affineCoordinateSystem`) is `O(log n)`. +- [ ] Decide whether to fold `SWPoint E` into `affineCoordinateSystem.Quot` (dropping the redundant + affine API). **Defer until there is an actual projective/Jacobian coordinate system** (a + non-trivial `Rel`) to judge against — only with a real second instance is the ergonomics tradeoff + concrete. Foundationally a wash either way (both rest on `propext` / `Classical.choice` / + `Quot.sound`, and `Quot.sound` is already in the footprint everywhere), so it's purely an + ergonomics call. - [ ] Projective (and/or Jacobian) coordinate system with inversion-free complete formulas, transported to Mathlib's `Projective.Point` group, designated the canonical efficient group element (`Point`); explicit `toAffine` / `fromAffine` conversions. (Per the efficiency criterion.)