Sync with upstream: unconditional Pasta group orders (daira/CompElliptic#6)

CompElliptic.lean

@@ -11,6 +11,7 @@ import CompElliptic.Encoding
 import CompElliptic.Encodings.Common
 import CompElliptic.Encodings.Pasta
 import CompElliptic.Fields.Pasta
+import CompElliptic.Fields.Residue
 import CompElliptic.Fields.Sqrt
 import CompElliptic.CurveForms.ShortWeierstrass
 import CompElliptic.CurveOrder

CompElliptic/CurveForms/ShortWeierstrass.lean

@@ -46,6 +46,11 @@ instance (a b : F) (p : F × F) : Decidable (OnCurve a b p) := by unfold OnCurve
 /-- A representable point: on the curve, or the `(0, 0)` identity sentinel `𝒪`. -/
 def Valid (a b : F) (p : F × F) : Prop := OnCurve a b p ∨ p = (0, 0)
 
+/-- Representability is decidable too: being on the curve is, and so is the `(0, 0)` sentinel test.
+This is what lets a representable point be exhibited by `decide`, and `SWPoint E` be counted as a
+subtype of `F × F`. -/
+instance (a b : F) (p : F × F) : Decidable (Valid a b p) := by unfold Valid; infer_instance
+
 omit [DecidableEq F] in
 /-- The `(0, 0)` sentinel is off the curve exactly when `b ≠ 0` (which holds for any elliptic
 curve: `a = b = 0` is the singular cusp `y² = x³`). This is what makes `(0, 0) ≡ 𝒪` unambiguous. -/
@@ -389,6 +394,15 @@ theorem SWPoint.ext_pair {E : SWCurve F} {P Q : SWPoint E}
   injection h with hx hy
   subst hx; subst hy; rfl
 
+/-- Points on `E` are exactly the valid coordinate pairs: the carried `onCurve` proof is a `Prop`,
+so nothing is lost by passing to the subtype. This is the bridge to anything `F × F` already knows —
+decidable equality, finiteness, and counting `SWPoint E` as a `Finset` of pairs. -/
+def SWPoint.equivSubtype (E : SWCurve F) : SWPoint E ≃ { pr : F × F // Valid E.A E.B pr } where
+  toFun P := ⟨(P.x, P.y), P.onCurve⟩
+  invFun pr := ⟨pr.1.1, pr.1.2, pr.2⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
 /-- Addition lifted to `SWPoint E`; closure from `valid_add`. -/
 def sw_add {E : SWCurve F} (P Q : SWPoint E) : SWPoint E :=
   haveI := instIsElliptic E
@@ -403,6 +417,15 @@ 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⟩
 
+omit [DecidableEq F] in
+/-- Negation fixes the `x`-coordinate. True by `rfl` (`sw_neg` is `neg` on the coordinates), but
+worth naming: without it every caller re-derives it inline. -/
+@[simp] theorem SWPoint.neg_x {E : SWCurve F} (P : SWPoint E) : (-P).x = P.x := rfl
+
+omit [DecidableEq F] in
+/-- Negation negates the `y`-coordinate — the one fact that makes `2 • P = 0` say `P.y = -P.y`. -/
+@[simp] theorem SWPoint.neg_y {E : SWCurve F} (P : SWPoint E) : (-P).y = -P.y := rfl
+
 /-! ### Fast (logarithmic) scalar multiplication
 
 The spec-level `smul` is linear (`n` additions), so it cannot be evaluated by `decide` or
@@ -413,9 +436,9 @@ double-and-add `CompElliptic.binNsmul` over the raw `sw_add` / `SWPoint.zero`. S
 `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]⟩
+coordinate pair, via `SWPoint.equivSubtype`); needed for `native_decide` on `n • P = Q`. -/
+instance instDecidableEqSWPoint {E : SWCurve F} : DecidableEq (SWPoint E) :=
+  (SWPoint.equivSubtype E).decidableEq
 
 /-- 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 are discharged

CompElliptic/Curves/Pasta.lean

@@ -6,6 +6,7 @@ Authors: Daira-Emma Hopwood
 -/
 import CompElliptic.CurveForms.ShortWeierstrass
 import CompElliptic.Fields.Pasta
+import CompElliptic.Fields.Residue
 import Mathlib.NumberTheory.LegendreSymbol.Basic
 
 /-!
@@ -27,18 +28,18 @@ open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.Fields.Pasta
 namespace Pallas
 
 /-- Pallas: `y² = x³ + 5` over the Pallas base field (`A = 0`, `B = 5`). -/
-def a : PallasBaseField := 0
-def b : PallasBaseField := 5
+def a : Fp := 0
+def b : Fp := 5
 
 /-- A convenient prime-order point `(-1, 2)` for testing (just a test point, not a
 protocol-specified base). -/
-def G : PallasBaseField × PallasBaseField := (-1, 2)
+def G : Fp × Fp := (-1, 2)
 
 theorem b_ne_zero : b ≠ 0 := by decide
 
 /-- The Pallas curve as a rich `SWCurve`: ellipticity (`sw_Δ 0 5 = -10800 ≠ 0`, so `IsUnit`) and
 `B ≠ 0` discharged by computation. -/
-def curve : SWCurve PallasBaseField where
+def curve : SWCurve Fp where
   A := a
   B := b
   IsElliptic := by rw [isUnit_iff_ne_zero]; decide
@@ -54,14 +55,14 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) :=
 Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (p / 2) ≠ 1`. The LHS (`-1`) is
 evaluated by `reduce_mod_char` (fast modular exponentiation via `NormNum.PowMod`), the same
 machinery the `PrattPartList.prime` legs use for their `a ^ k ≠ 1` conditions. -/
-theorem five_not_isSquare : ¬ IsSquare (5 : PallasBaseField) := by
-  rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (5 : PallasBaseField) ≠ 0)]
+theorem five_not_isSquare : ¬ IsSquare (5 : Fp) := by
+  rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (5 : Fp) ≠ 0)]
   reduce_mod_char
   decide
 
 /-- Consequently no point on the Pallas curve has `x`-coordinate `0`, so `x = 0` denotes `𝒪`
 unambiguously. -/
-theorem no_onCurve_x_zero (y : PallasBaseField) : ¬ OnCurve a b (0, y) := by
+theorem no_onCurve_x_zero (y : Fp) : ¬ OnCurve a b (0, y) := by
   intro h
   have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h
   exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩
@@ -90,19 +91,19 @@ end Pallas
 
 namespace Vesta
 
-/-- Vesta: `y² = x³ + 5` over the Vesta base field (`= PallasScalarField`; `A = 0`, `B = 5`). -/
-def a : VestaBaseField := 0
-def b : VestaBaseField := 5
+/-- Vesta: `y² = x³ + 5` over the Vesta base field (`= Fq`; `A = 0`, `B = 5`). -/
+def a : Fq := 0
+def b : Fq := 5
 
 /-- A convenient prime-order point `(-1, 2)` for testing (just a test point, not a
 protocol-specified base). -/
-def G : VestaBaseField × VestaBaseField := (-1, 2)
+def G : Fq × Fq := (-1, 2)
 
 theorem b_ne_zero : b ≠ 0 := by decide
 
 /-- The Vesta curve as a rich `SWCurve`: ellipticity (`sw_Δ 0 5 = -10800 ≠ 0`, so `IsUnit`) and
 `B ≠ 0` discharged by computation. -/
-def curve : SWCurve VestaBaseField where
+def curve : SWCurve Fq where
   A := a
   B := b
   IsElliptic := by rw [isUnit_iff_ne_zero]; decide
@@ -117,18 +118,42 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) :=
 
 As for Pallas: Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (q / 2) ≠ 1`, and
 `reduce_mod_char` (fast modular exponentiation) evaluates the power to `-1`. -/
-theorem five_not_isSquare : ¬ IsSquare (5 : VestaBaseField) := by
-  rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (5 : VestaBaseField) ≠ 0)]
+theorem five_not_isSquare : ¬ IsSquare (5 : Fq) := by
+  rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (5 : Fq) ≠ 0)]
   reduce_mod_char
   decide
 
 /-- Consequently no point on the Vesta curve has `x`-coordinate `0`, so `x = 0` denotes `𝒪`
 unambiguously. -/
-theorem no_onCurve_x_zero (y : VestaBaseField) : ¬ OnCurve a b (0, y) := by
+theorem no_onCurve_x_zero (y : Fq) : ¬ OnCurve a b (0, y) := by
   intro h
   have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h
   exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩
 
+/-- `-5` is not a cube in the Vesta base field — the cubic analogue of `five_not_isSquare`, and
+what rules out 2-torsion on the Vesta curve.
+
+`3 ∣ q - 1`, so `not_exists_pow_eq_of_pow_ne_one` reduces this to the single power
+`(-5)^((q-1)/3)`, which is not `1`. As for `five_not_isSquare`, `reduce_mod_char` (fast modular
+exponentiation) evaluates it and the kernel re-checks the result. -/
+theorem neg_five_not_isCube : ¬ ∃ x : Fq, x ^ 3 = -(5 : Fq) := by
+  have hcard : Fintype.card Fq = PALLAS_SCALAR_CARD := ZMod.card _
+  refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) (by decide) ?_
+  rw [hcard]
+  -- `reduce_mod_char` keys on the `ZMod` spelling of the type, which the `Fq` abbrev hides;
+  -- `show` re-exposes it. (The `Field` instances agree — `(inferInstance : Field Fq) =
+  -- ZMod.instField _` is `rfl` — so this is only about how the goal is written.)
+  show (-(5 : ZMod PALLAS_SCALAR_CARD)) ^ ((PALLAS_SCALAR_CARD - 1) / 3) ≠ 1
+  reduce_mod_char
+  decide
+
+/-- No point on the Vesta curve has `y`-coordinate `0`: that would need `x³ = -5`, and `-5` is not
+a cube (`neg_five_not_isCube`). Equivalently, the Vesta group has no 2-torsion. -/
+theorem no_onCurve_y_zero (x : Fq) : ¬ OnCurve a b (x, 0) := by
+  intro h
+  have hsum : x ^ 3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm
+  exact neg_five_not_isCube ⟨x, by linear_combination hsum⟩
+
 -- `(-1, 2)` is on the curve: `2² = 4 = (-1)³ + 5`.
 example : OnCurve a b G := by native_decide
 

CompElliptic/Curves/PastaOrder.lean

@@ -2,23 +2,34 @@
 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
+Authors: Daira-Emma Hopwood, Gregor Mitscha-Baude
 -/
 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.
+Instantiates the `CompElliptic.CurveOrder` fibre bound at the two Pasta curves, with no assumption:
+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).
+
+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 only *upper* bound needed is the elementary fibre
+bound `#E(F) ≤ 2·#F + 1`; whether it clears the order threshold is decided by a closed comparison
+of the two field sizes, and the Pasta cycle puts the two curves on opposite sides of it:
+
+* **Pallas** — order `q = PALLAS_SCALAR_CARD` over the base field of size `p`, and `p < q`, so
+  `2p + 1 < 2q` outright: `card_eq_of_prime_witness_of_card_lt_two_mul` closes it.
+* **Vesta** — order `p = PALLAS_BASE_CARD` over the base field of size `q`, and `p < q`, so only
+  `2q + 1 < 3p` is available. `#E = 2p` is ruled out separately: a 2-torsion point needs `y = 0`,
+  i.e. `x³ = -5`, which `Pasta.Vesta.no_onCurve_y_zero` forbids.
+
+Per the *Independently re-checkable trust* principle every obligation here is a closed numeric fact
+(`2p + 1 < 2q`, `2q + 1 < 3p`), discharged by kernel `decide`; the only trust is the prime-order
+witnesses (`q_nsmul_Gpt`, `p_nsmul_Gpt`), proved by `native_decide` and appearing in `#print axioms`
+for the two theorems below.
 -/
 
 namespace CompElliptic.Curves.Pasta
@@ -28,42 +39,46 @@ open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder CompEllipt
 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)⟩
+def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
 
-theorem Gpt_ne_zero : Gpt ≠ 0 := by native_decide
+theorem Gpt_ne_zero : Gpt ≠ 0 := by 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
+theorem q_nsmul_Gpt : PALLAS_SCALAR_CARD • Gpt = 0 := by native_decide
+
+/-- **The Pallas curve group has order `PALLAS_SCALAR_CARD`**, unconditionally.
 
-/-- **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
+The Pallas group order `q` exceeds its base-field size `p`, so the fibre bound `#E ≤ 2p + 1`
+already sits below `2q`, and the prime-order witness `G = (-1, 2)` pins the order outright. -/
+theorem card_eq : Nat.card (SWPoint curve) = PALLAS_SCALAR_CARD := by
+  refine card_eq_of_prime_witness_of_card_lt_two_mul curve PALLAS_SCALAR_is_prime Gpt_ne_zero
+    q_nsmul_Gpt ?_
+  rw [show Fintype.card Fp = 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)⟩
+def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
 
-theorem Gpt_ne_zero : Gpt ≠ 0 := by native_decide
+theorem Gpt_ne_zero : Gpt ≠ 0 := by 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
+theorem p_nsmul_Gpt : PALLAS_BASE_CARD • Gpt = 0 := by native_decide
+
+/-- **The Vesta curve group has order `PALLAS_BASE_CARD`**, unconditionally.
+
+Here the group order `p` is *below* the base-field size `q`, so the fibre bound only gives
+`#E ≤ 2q + 1 < 3p`, leaving `#E = 2p` open. That case needs a point of order 2, which would have
+`y = 0` — impossible by `no_onCurve_y_zero`. -/
+theorem card_eq : Nat.card (SWPoint curve) = PALLAS_BASE_CARD := by
+  refine card_eq_of_prime_witness_of_card_lt_three_mul curve PALLAS_BASE_is_prime Gpt_ne_zero
+    p_nsmul_Gpt ?_ ?_
+  · rw [show Fintype.card Fq = PALLAS_SCALAR_CARD from ZMod.card _]
+    decide
+  · exact fun _ => eq_zero_of_two_nsmul_eq_zero (by decide) no_onCurve_y_zero
 
 end Vesta
 

CompElliptic/Encodings/Pasta.lean

@@ -47,10 +47,8 @@ instance : Fact (PALLAS_SCALAR_CARD ≤ 2^255) := ⟨by decide⟩
 
 namespace Curves.Pasta.Pallas
 
-/-- The test point `G = (-1, 2)` as an on-curve `SWPoint`, for exercising `toBytes`.
-(`Valid` is `OnCurve ∨ · = (0, 0)`; only the `OnCurve` disjunct is `Decidable`, so we supply
-`Or.inl (by decide)` rather than deciding `Valid` directly.) -/
-def G_point : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
+/-- The test point `G = (-1, 2)` as an on-curve `SWPoint`, for exercising `toBytes`. -/
+def G_point : SWPoint curve := ⟨-1, 2, by decide⟩
 
 #eval (toBytes G_point).toList
 
@@ -59,8 +57,8 @@ end Curves.Pasta.Pallas
 namespace Curves.Pasta.Vesta
 
 /-- The test point `G = (-1, 2)` on the Vesta curve as an on-curve `SWPoint`, for exercising
-`toBytes` over the Vesta base field (`= PallasScalarField`). -/
-def G_point : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
+`toBytes` over the Vesta base field (`= Fq`). -/
+def G_point : SWPoint curve := ⟨-1, 2, by decide⟩
 
 #eval (toBytes G_point).toList
 

CompElliptic/Fields/Pasta.lean

@@ -22,7 +22,8 @@ namespace CompElliptic.Fields.Pasta
 -- Pallas base field p (= Vesta scalar field).
 @[reducible] def PALLAS_BASE_CARD : Nat := 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
 
-abbrev PallasBaseField := ZMod PALLAS_BASE_CARD
+/-- The Pallas base field `𝔽ₚ` — also the Vesta scalar field (the Pasta cycle). -/
+abbrev Fp := ZMod PALLAS_BASE_CARD
 
 theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by
   unfold PALLAS_BASE_CARD
@@ -88,12 +89,13 @@ theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by
       · exact .prime 772231 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
 
 instance : Fact (Nat.Prime PALLAS_BASE_CARD) := ⟨PALLAS_BASE_is_prime⟩
-instance : Field PallasBaseField := ZMod.instField PALLAS_BASE_CARD
+instance : Field Fp := ZMod.instField PALLAS_BASE_CARD
 
 -- Pallas scalar field q (= Vesta base field).
 @[reducible] def PALLAS_SCALAR_CARD : Nat := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
 
-abbrev PallasScalarField := ZMod PALLAS_SCALAR_CARD
+/-- The Pallas scalar field `𝔽_q` — also the Vesta base field (the Pasta cycle). -/
+abbrev Fq := ZMod PALLAS_SCALAR_CARD
 
 theorem PALLAS_SCALAR_is_prime : Nat.Prime PALLAS_SCALAR_CARD := by
   unfold PALLAS_SCALAR_CARD
@@ -159,16 +161,11 @@ theorem PALLAS_SCALAR_is_prime : Nat.Prime PALLAS_SCALAR_CARD := by
       · exact .prime 31649 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
 
 instance : Fact (Nat.Prime PALLAS_SCALAR_CARD) := ⟨PALLAS_SCALAR_is_prime⟩
-instance : Field PallasScalarField := ZMod.instField PALLAS_SCALAR_CARD
-
-/-- Vesta base field = Pallas scalar field. -/
-abbrev VestaBaseField := PallasScalarField
-/-- Vesta scalar field = Pallas base field. -/
-abbrev VestaScalarField := PallasBaseField
+instance : Field Fq := ZMod.instField PALLAS_SCALAR_CARD
 
 /-- Tonelli–Shanks data for the Pallas base field `𝔽ₚ`: `p-1 = 2^32 · T`, with `rootOfUnity = 5ᵀ`
 (`pallas.py`). -/
-def pallasBase : TonelliShanks PallasBaseField where
+def pallasBase : TonelliShanks Fp where
   twoAdicity := 32
   oddPart := 0x40000000000000000000000000000000224698fc094cf91b992d30ed
   rootOfUnity := 0x2bce74deac30ebda362120830561f81aea322bf2b7bb7584bdad6fabd87ea32f
@@ -177,11 +174,11 @@ def pallasBase : TonelliShanks PallasBaseField where
 example : (pallasBase.sqrt? 4).map (· ^ 2) = some 4 := by native_decide
 example : pallasBase.sqrt? 5 = none := by native_decide
 -- `√((-1)³ + 5) = √4`: the `y` of the test point `G = (-1, 2)`.
-example : (pallasBase.sqrt? ((-1 : PallasBaseField)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
+example : (pallasBase.sqrt? ((-1 : Fp)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
 
-/-- Tonelli–Shanks data for the Vesta base field `𝔽_q` (`= PallasScalarField`): `q-1 = 2^32 · T`,
+/-- Tonelli–Shanks data for the Vesta base field `𝔽_q` (`= Fq`): `q-1 = 2^32 · T`,
 with `rootOfUnity = 5ᵀ` (`vesta.py`). -/
-def vestaBase : TonelliShanks VestaBaseField where
+def vestaBase : TonelliShanks Fq where
   twoAdicity := 32
   oddPart := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb21
   rootOfUnity := 0x2de6a9b8746d3f589e5c4dfd492ae26e9bb97ea3c106f049a70e2c1102b6d05f
@@ -190,6 +187,6 @@ def vestaBase : TonelliShanks VestaBaseField where
 example : (vestaBase.sqrt? 4).map (· ^ 2) = some 4 := by native_decide
 example : vestaBase.sqrt? 5 = none := by native_decide
 -- `√((-1)³ + 5) = √4`: the `y` of the test point `G = (-1, 2)`.
-example : (vestaBase.sqrt? ((-1 : VestaBaseField)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
+example : (vestaBase.sqrt? ((-1 : Fq)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
 
 end CompElliptic.Fields.Pasta