Pasta: GLV endomorphism eigenvalue anchors

CompElliptic.lean

@@ -16,3 +16,4 @@ import CompElliptic.CurveForms.ShortWeierstrass
 import CompElliptic.CurveOrder
 import CompElliptic.Curves.Pasta
 import CompElliptic.Curves.PastaOrder
+import CompElliptic.Curves.PastaEndo

CompElliptic/Curves/Pasta.lean

@@ -27,18 +27,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 +54,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 +90,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,14 +117,14 @@ 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]⟩

CompElliptic/Curves/PastaEndo.lean

@@ -0,0 +1,67 @@
+import CompElliptic.Curves.Pasta
+import CompElliptic.Curves.PastaOrder
+
+/-!
+# The Pasta GLV endomorphism anchors
+
+Each Pasta curve `y² = x³ + 5` carries the GLV endomorphism `φ(x, y) = (β·x, y)` (`β` a
+primitive cube root of unity in the base field), which acts on the point group as
+multiplication by a scalar eigenvalue `λ`. This file provides the *computational anchor*
+of that fact, one certificate per curve: `λ • G = φ(G)` at the standard generator,
+checked by `native_decide` through the binary double-and-add `nsmul` — the same
+certificate style as the point counts in `PastaOrder.lean`.
+
+Downstream (the `pasta` package of l-adic/snarky) the anchor extends to every point:
+`φ` is a group homomorphism (field algebra over `β³ = 1`), the group is cyclic of prime
+order (Hasse), so `φ(kG) = k·φ(G) = k·λ·G = λ·(kG)`.
+-/
+
+namespace CompElliptic.Curves.Pasta
+
+open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.Fields.Pasta
+
+namespace Pallas
+
+/-- The Pallas base-field endomorphism coefficient `β` (a primitive cube root of unity). -/
+def endoBeta : Fp :=
+  20444556541222657078399132219657928148671392403212669005631716460534733845831
+
+/-- The scalar eigenvalue `λ` of the Pallas endomorphism, as a natural number. -/
+def endoLam : ℕ :=
+  26005156700822196841419187675678338661165322343552424574062261873906994770353
+
+/-- The image of the standard generator under `φ(x, y) = (β·x, y)`. -/
+def endoGpt : SWPoint curve :=
+  ⟨endoBeta * G.1, G.2, by
+    left
+    show G.2 ^ 2 = (endoBeta * G.1) ^ 3 + a * (endoBeta * G.1) + b
+    decide⟩
+
+/-- **The eigenvalue anchor**: `λ • G = φ(G)` at the standard generator. -/
+theorem endoLam_nsmul_Gpt : endoLam • Gpt = endoGpt := by native_decide
+
+end Pallas
+
+namespace Vesta
+
+/-- The Vesta base-field endomorphism coefficient `β` (a primitive cube root of unity). -/
+def endoBeta : Fq :=
+  2942865608506852014473558576493638302197734138389222805617480874486368177743
+
+/-- The scalar eigenvalue `λ` of the Vesta endomorphism, as a natural number. -/
+def endoLam : ℕ :=
+  8503465768106391777493614032514048814691664078728891710322960303815233784505
+
+/-- The image of the standard generator under `φ(x, y) = (β·x, y)`. -/
+def endoGpt : SWPoint curve :=
+  ⟨endoBeta * G.1, G.2, by
+    left
+    show G.2 ^ 2 = (endoBeta * G.1) ^ 3 + a * (endoBeta * G.1) + b
+    decide⟩
+
+/-- **The eigenvalue anchor**: `λ • G = φ(G)` at the standard generator. -/
+theorem endoLam_nsmul_Gpt : endoLam • Gpt = endoGpt := by native_decide
+
+end Vesta
+
+end CompElliptic.Curves.Pasta

CompElliptic/Curves/PastaOrder.lean

@@ -40,9 +40,9 @@ 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 _]
+  · rw [show Fintype.card Fp = 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
+  · rw [show Fintype.card Fp = PALLAS_BASE_CARD from ZMod.card _]; decide
 
 end Pallas
 
@@ -61,9 +61,9 @@ 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 _]
+  · rw [show Fintype.card Fq = 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
+  · rw [show Fintype.card Fq = PALLAS_SCALAR_CARD from ZMod.card _]; decide
 
 end Vesta
 

CompElliptic/Encodings/Pasta.lean

@@ -59,7 +59,7 @@ 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`). -/
+`toBytes` over the Vesta base field (`= Fq`). -/
 def G_point : SWPoint curve := ⟨-1, 2, Or.inl (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