From 7187373bd70bd0ab50df093b35d0063bd39c8fbc Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 00:26:53 -0700 Subject: [PATCH 1/6] Fast/Projective/Core: field-generic RCB projective core Complete Renes-Costello-Batina projective addition, its completeness (threading hy0 and 2 != 0), the affine bridge toAffine/ofAffine, and the binary smulFast ladder proven equal to n . p -- all generic over [Field F] for any y^2 = x^3 + 5 curve. Vesta and Pallas instantiate this in Projective.lean. Claude-Session: https://claude.ai/code/session_01Y4Wf3zPJYCwXzHDgdBUytv --- .../Curves/Pasta/Fast/Projective/Core.lean | 576 ++++++++++++++++++ 1 file changed, 576 insertions(+) create mode 100644 CompElliptic/Curves/Pasta/Fast/Projective/Core.lean diff --git a/CompElliptic/Curves/Pasta/Fast/Projective/Core.lean b/CompElliptic/Curves/Pasta/Fast/Projective/Core.lean new file mode 100644 index 0000000..cbc6f7e --- /dev/null +++ b/CompElliptic/Curves/Pasta/Fast/Projective/Core.lean @@ -0,0 +1,576 @@ +/- +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: Gregor Mitscha-Baude +-/ +import CompElliptic.Curves.Pasta + +/-! +# Projective (Renes–Costello–Batina) point arithmetic, generic over the base field + +The affine group law pays a field inversion per addition. This module replaces it, for the hot +`n • point` loop, by the complete projective addition formulas of Renes, Costello and Batina +(EUROCRYPT 2016; the EFD `add-2015-rcb` sequence at `a = 0`): single branchless formulas in +`(X : Y : Z)` valid for *all* input pairs, with the inversion paid once in `toAffine`. + +This is the field-generic core shared by every short-Weierstrass curve of the shape `y² = x³ + 5` +(`a = 0`, `b = 5`, `b3 = 15`) — both Pasta curves. The `padd` closed forms and every polynomial +certificate are field-agnostic; the completeness arguments (`Z₃ ≠ 0` outside the genuine identity +cases) need only that the curve has no 2-torsion, threaded as the hypothesis +`hy0 : ∀ x, ¬ OnCurve 0 5 (x, 0)` — the fact that `−5` is not a cube — together with `2 ≠ 0` +(the doubling denominators). The bridge to the affine group `SWPoint E` is parametrized by a +curve `E` pinned to `E.A = 0`, `E.B = 5`. Each concrete curve instantiates this core in +`Projective.lean` by supplying its field and its `no_onCurve_y_zero` lemma. + +Specialized to `a = 0`, `b = 5`, `b3 = 15`, the closed forms are + +* `X₃ = X₁Y₁Y₂² − 15X₁Y₁Z₂² − 30X₁Z₁Y₂Z₂ + Y₁²X₂Y₂ − 15Z₁²X₂Y₂ − 30Y₁Z₁X₂Z₂` +* `Y₃ = Y₁²Y₂² + 45X₁²X₂Z₂ + 45X₁Z₁X₂² − 225Z₁²Z₂²` +* `Z₃ = Y₁²Y₂Z₂ + Y₁Z₁Y₂² + 3X₁²X₂Y₂ + 3X₁Y₁X₂² + 15Y₁Z₁Z₂² + 15Z₁²Y₂Z₂` + +The `Fast` interfaces are provisional: they are not guaranteed to remain public, and may be folded +into the existing API or otherwise changed incompatibly. +-/ + +open CompElliptic +open CompElliptic.CurveForms.ShortWeierstrass + +namespace CompElliptic.Curves.Pasta.Fast.Projective.Core + +variable {F : Type*} [Field F] + +/-- A projective point in `(X : Y : Z)` coordinates over the base field `F`. -/ +structure PPoint (F : Type*) where + /-- The projective `X`-coordinate. -/ + X : F + /-- The projective `Y`-coordinate. -/ + Y : F + /-- The projective `Z`-coordinate. -/ + Z : F +deriving DecidableEq + +namespace PPoint + +/-- Renes–Costello–Batina complete addition (`add-2015-rcb`, `a = 0`, `b3 = 15`). -/ +def padd (P Q : PPoint F) : PPoint F where + X := P.X*P.Y*Q.Y^2 - 15*P.X*P.Y*Q.Z^2 - 30*P.X*P.Z*Q.Y*Q.Z + + P.Y^2*Q.X*Q.Y - 15*P.Z^2*Q.X*Q.Y - 30*P.Y*P.Z*Q.X*Q.Z + Y := P.Y^2*Q.Y^2 + 45*P.X^2*Q.X*Q.Z + 45*P.X*P.Z*Q.X^2 - 225*P.Z^2*Q.Z^2 + Z := P.Y^2*Q.Y*Q.Z + P.Y*P.Z*Q.Y^2 + 3*P.X^2*Q.X*Q.Y + 3*P.X*P.Y*Q.X^2 + + 15*P.Y*P.Z*Q.Z^2 + 15*P.Z^2*Q.Y*Q.Z + +/-- Scalar (representative) rescaling `(X : Y : Z) ↦ (uX : uY : uZ)`. -/ +def smul (u : F) (P : PPoint F) : PPoint F := ⟨u*P.X, u*P.Y, u*P.Z⟩ + +/-- The projective identity `𝒪 = (0 : 1 : 0)`. -/ +def pid : PPoint F := ⟨0, 1, 0⟩ + +/-- The homogeneous projective curve equation `Y²Z = X³ + 5Z³` (`a = 0`, `b = 5`). -/ +def OnCurveP (P : PPoint F) : Prop := P.Y^2*P.Z = P.X^3 + 5*P.Z^3 + +/-- `OnCurveP` unfolds definitionally to a field equation, hence is decidable. This is what keeps +`toAffine` — and everything downstream of it — computable. -/ +instance [DecidableEq F] (P : PPoint F) : Decidable (OnCurveP P) := + inferInstanceAs (Decidable (P.Y^2*P.Z = P.X^3 + 5*P.Z^3)) + +/-- A representable projective point: on the projective curve and not the zero vector. -/ +def Valid (P : PPoint F) : Prop := OnCurveP P ∧ (P.X ≠ 0 ∨ P.Y ≠ 0 ∨ P.Z ≠ 0) + +/-- Affine interpretation as a raw coordinate pair: `Z ≠ 0 ↦ (X/Z, Y/Z)`, `Z = 0 ↦ 𝒪 = (0,0)`. -/ +def aff [DecidableEq F] (P : PPoint F) : F × F := if P.Z = 0 then (0, 0) else (P.X / P.Z, P.Y / P.Z) + +/-! ## `ring`/`linear_combination` certificates + +Each identity below is a polynomial identity over `F`, valid modulo the two curve equations +`e1 : y1² = x1³ + 5` and `e2 : y2² = x2³ + 5`. The cofactors were computed by an exact-rational +Gröbner/linear-algebra search over `ℚ[x1,y1,x2,y2]` (offline) and are checked here by `ring` +inside `linear_combination`; being identities over `ℤ`, they hold over any field. -/ + +variable {x1 y1 x2 y2 : F} + +/-- Reading off the coordinates of `padd` on `Z = 1` representatives. -/ +@[simp] theorem padd_z1_X (x1 y1 x2 y2 : F) : + (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).X + = y1^2*x2*y2 + x1*y1*y2^2 - 15*x2*y2 - 30*y1*x2 - 30*x1*y2 - 15*x1*y1 := by + simp only [padd]; ring + +@[simp] theorem padd_z1_Y (x1 y1 x2 y2 : F) : + (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Y + = y1^2*y2^2 + 45*x1*x2^2 + 45*x1^2*x2 - 225 := by + simp only [padd]; ring + +@[simp] theorem padd_z1_Z (x1 y1 x2 y2 : F) : + (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z + = 3*x1*y1*x2^2 + 3*x1^2*x2*y2 + y1*y2^2 + y1^2*y2 + 15*y2 + 15*y1 := by + simp only [padd]; ring + +/-- `X₃·(x₂−x₁)² = x3num·Z₃`, the numerator match for the affine `x`-coordinate (distinct `x`). -/ +theorem keyx_dist (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) : + (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).X * (x2 - x1)^2 + = ((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2) * (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z := by + simp only [padd_z1_X, padd_z1_Z] + linear_combination + ((2)*x2^3*y2 + (3)*x1*x2^2*y2 + (-3)*x1*y1*x2^2 + (-3)*x1^2*x2*y2 + y2^3 + y1*y2^2 - y1^2*y2 + (10)*y2 + (-15)*y1) * e1 + + ((-3)*x1*y1*x2^2 + (-3)*x1^2*x2*y2 + (3)*x1^2*y1*x2 + x1^3*y2 + (3)*x1^3*y1 - y1*y2^2 + (-10)*y2 + (15)*y1) * e2 + +/-- `Y₃·(x₂−x₁)³ = y3num·Z₃`, the numerator match for the affine `y`-coordinate (distinct `x`). -/ +theorem keyy_dist (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) : + (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Y * (x2 - x1)^3 + = ((y2 - y1)*(x1*(x2 - x1)^2 - ((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2)) - y1*(x2 - x1)^3) + * (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z := by + simp only [padd_z1_Y, padd_z1_Z] + linear_combination + ((6)*x1*x2^5 + (-9)*x1^2*x2^4 + (2)*x2^3*y2^2 + (2)*y1*x2^3*y2 + (-15)*x1*x2^2*y2^2 + (6)*x1*y1*x2^2*y2 + (-3)*x1*y1^2*x2^2 + (15)*x1^2*x2*y2^2 + (-3)*x1^2*y1*x2*y2 + (-2)*y2^4 + (2)*y1^2*y2^2 - y1^3*y2 + (30)*x2^3 + (-60)*x1*x2^2 + (10)*y2^2 + (25)*y1*y2 + (-15)*y1^2 + (-75)) * e1 + + ((-6)*x1^4*x2^2 + (9)*x1^5*x2 + (3)*x1*y1*x2^2*y2 + (3)*x1^2*x2*y2^2 + (-6)*x1^2*y1*x2*y2 + (-2)*x1^3*y2^2 + (-2)*x1^3*y1*y2 + y1*y2^3 + (-75)*x1*x2^2 + (135)*x1^2*x2 + (-30)*x1^3 + (5)*y2^2 + (-25)*y1*y2 + (75)) * e2 + +/-- Curve preservation on `Z = 1` representatives: `padd` lands on the projective curve. -/ +theorem oncurveP_padd_z1 (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) : + OnCurveP (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := by + simp only [OnCurveP, padd_z1_X, padd_z1_Y, padd_z1_Z] + linear_combination + (-x1^6*x2^3*y2^3 - x1^3*y1^2*x2^3*y2^3 + x1^6*y2^5 - y1^4*x2^3*y2^3 + (-135)*x1^3*y1*x2^6 + x1^3*y1^2*y2^5 + (-405)*x1^4*x2^5*y2 + (-135)*x1^5*x2^4*y2 + y1^3*y2^6 + y1^4*y2^5 + (135)*x1^2*y1*x2^4*y2^2 + (-135)*x1^2*y1^2*x2^4*y2 + (35)*x1^3*x2^3*y2^3 + (90)*x1^3*y1*x2^3*y2^2 + (405)*x1^4*x2^2*y2^3 + (135)*x1^5*x2*y2^3 + (-5)*x1^6*y2^3 + (40)*y1^2*x2^3*y2^3 + (90)*y1^3*x2^3*y2^2 + (135)*x1*y1*x2^2*y2^4 + (270)*x1*y1^2*x2^2*y2^3 + (270)*x1^2*y1*x2*y2^4 + (135)*x1^2*y1^2*x2*y2^3 + (100)*x1^3*y2^5 + (45)*x1^3*y1*y2^4 + (-5)*x1^3*y1^2*y2^3 + (5)*y1^2*y2^5 + (-5)*y1^4*y2^3 + (-675)*x1^2*x2^4*y2 + (-2025)*x1^2*y1*x2^4 + (-2700)*x1^3*x2^3*y2 + (-2025)*x1^4*x2^2*y2 + (-675)*x1^5*x2*y2 + (-475)*x2^3*y2^3 + (-2250)*y1*x2^3*y2^2 + (-2700)*y1^2*x2^3*y2 + (-4050)*x1*x2^2*y2^3 + (-12150)*x1*y1*x2^2*y2^2 + (-4050)*x1*y1^2*x2^2*y2 + (-11475)*x1^2*x2*y2^3 + (-5400)*x1^2*y1*x2*y2^2 + (-675)*x1^2*y1^2*x2*y2 + (-3875)*x1^3*y2^3 + (-900)*x1^3*y1*y2^2 + (-200)*y2^5 + (-1125)*y1*y2^4 + (-1150)*y1^2*y2^3 + (-225)*y1^3*y2^2 + (27000)*x2^3*y2 + (27000)*y1*x2^3 + (60750)*x1*x2^2*y2 + (30375)*x1*y1*x2^2 + (57375)*x1^2*x2*y2 + (20250)*x1^2*y1*x2 + (16875)*x1^3*y2 + (3375)*x1^3*y1 + (-22625)*y2^3 + (-18000)*y1*y2^2 + (-3375)*y1^2*y2 + (-16875)*y2 + (-16875)*y1) * e1 + + (x1^9*y2^3 + (135)*x1^6*y1*x2^3 + (405)*x1^7*x2^2*y2 + (135)*x1^8*x2*y2 + (270)*x1^5*y1*x2*y2^2 + (105)*x1^6*y2^3 + (45)*x1^6*y1*y2^2 + (-5400)*x1^3*y1*x2^3 + (-4050)*x1^4*x2^2*y2 + (-12150)*x1^4*y1*x2^2 + (-10800)*x1^5*x2*y2 + (-4050)*x1^5*y1*x2 + (-3375)*x1^6*y2 + (-675)*x1^6*y1 + (-2700)*x1^2*y1*x2*y2^2 + (300)*x1^3*y2^3 + (-3600)*x1^3*y1*y2^2 + (-27000)*x1^2*x2*y2 + (40500)*x1^2*y1*x2 + (-13500)*x1^3*y2 + (-1000)*y2^3 + (-9000)*y1*y2^2 + (-135000)*y2 + (-135000)*y1) * e2 + +/-- **Distinct-`x` completeness (2-torsion-free).** If `Z₃ = 0` for two on-curve `Z = 1` points +with distinct `x`, then `w = wnum/wden` (the `x`-coordinate of `P − Q`) is a cube root of `−5`, +i.e. `(w, 0)` is a 2-torsion point — impossible by `hy0`. Hence `Z₃ ≠ 0`. -/ +theorem Z_ne_zero_dist (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) (hne : x1 ≠ x2) : + (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z ≠ 0 := by + intro hZ + have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hne) + set wnum : F := (y1 + y2)^2 - (x1 + x2)*(x2 - x1)^2 with hwnumE + set wden : F := (x2 - x1)^2 with hwdenE + have hwdenne : wden ≠ 0 := by rw [hwdenE]; exact pow_ne_zero 2 hd + have hZpoly : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z + = 3*x1*y1*x2^2 + 3*x1^2*x2*y2 + y1*y2^2 + y1^2*y2 + 15*y2 + 15*y1 := padd_z1_Z x1 y1 x2 y2 + rw [hZpoly] at hZ + have hcube : wnum^3 = -5 * wden^3 := by + rw [hwnumE, hwdenE] + linear_combination + (-x2^3*y2 + (-2)*y1*x2^3 + (3)*x1*y1*x2^2 + (3)*x1^2*x2*y2 + (-2)*x1^3*y2 + (-4)*x1^3*y1 + y2^3 + (3)*y1*y2^2 + (3)*y1^2*y2 + (4)*y1^3 + (-15)*y1) * hZ + + ((8)*x2^6 + (-6)*x1*x2^5 + (-6)*x1^2*x2^4 + (8)*x1^3*x2^3 + (-3)*x1^5*x2 + x1^6 + (-12)*x2^3*y2^2 + (-6)*y1*x2^3*y2 + (-4)*y1^2*x2^3 + (12)*x1*x2^2*y2^2 + (-9)*x1*y1^2*x2^2 + (3)*x1^2*y1^2*x2 + (-3)*x1^3*y2^2 + (-6)*x1^3*y1*y2 + (-2)*x1^3*y1^2 + (3)*y2^4 + (10)*y1*y2^3 + (9)*y1^2*y2^2 + (2)*y1^3*y2 + y1^4 + (60)*x2^3 + (-75)*x1*x2^2 + (45)*x1^2*x2 + (-10)*x1^3 + (-15)*y2^2 + (-60)*y1*y2 + (-60)*y1^2 + (50)) * e1 + + (x2^6 + (-3)*x1*x2^5 + (-2)*x2^3*y2^2 + (-6)*y1*x2^3*y2 + (5)*y1^2*x2^3 + (3)*x1*x2^2*y2^2 + (9)*x1*y1*x2^2*y2 + (-6)*x1*y1^2*x2^2 + (6)*x1^2*y1^2*x2 + y2^4 + (5)*y1*y2^3 + (8)*y1^2*y2^2 + (4)*y1^3*y2 - y1^4 + (-50)*x2^3 + (75)*x1*x2^2 + (-45)*x1^2*x2 + (5)*y2^2 + (15)*y1*y2 + (25)*y1^2 + (-50)) * e2 + have hw : (wnum / wden)^3 = -5 := by + rw [div_pow, hcube, mul_div_assoc, div_self (pow_ne_zero 3 hwdenne), mul_one] + exact hy0 (wnum / wden) (by + show (0 : F)^2 = (wnum / wden)^3 + 0 * (wnum / wden) + 5 + rw [hw]; ring) + +/-- **Doubling `Z`-coordinate.** On `Z = 1` representatives with equal points, `Z₃ = 8y³`. -/ +theorem Z_doubling (e1 : y1^2 = x1^3 + 5) : + (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z = 8 * y1^3 := by + simp only [padd_z1_Z] + linear_combination ((-6)*y1) * e1 + +/-- `X₃·4y² = x3numd·Z₃`, doubling `x`-coordinate numerator match. -/ +theorem keyx_dbl (e1 : y1^2 = x1^3 + 5) : + (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).X * (4*y1^2) + = (9*x1^4 - 8*x1*y1^2) * (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z := by + simp only [padd_z1_X, padd_z1_Z] + linear_combination ((54)*x1^4*y1 + (24)*x1*y1^3) * e1 + +/-- `Y₃·8y³ = y3numd·Z₃`, doubling `y`-coordinate numerator match. -/ +theorem keyy_dbl (e1 : y1^2 = x1^3 + 5) : + (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Y * (8*y1^3) + = (3*x1^2*(12*x1*y1^2 - 9*x1^4) - 8*y1^4) * (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z := by + simp only [padd_z1_Y, padd_z1_Z] + linear_combination ((-162)*x1^6*y1 + (24)*y1^5 + (360)*y1^3) * e1 + +/-- **Inverse-case identity representative is nonzero (2-torsion-free).** +`padd P (−P) = (0 : Y₃ : 0)` with `Y₃ ≠ 0`: if `Y₃ = 0` then `w = wnum2/wden2` (the `x`-coordinate +of `2P`) is a cube root of `−5`, impossible by `hy0`. -/ +theorem Y_ne_zero_inv (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (e1 : y1^2 = x1^3 + 5) (hy : y1 ≠ 0) : + (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Y ≠ 0 := by + intro hY + have hYpoly : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Y = y1^4 + 90*x1^3 - 225 := by + simp only [padd]; ring + rw [hYpoly] at hY + set wnum2 : F := 9*x1^4 - 8*x1*y1^2 with hwnum2 + set wden2 : F := 4*y1^2 with hwden2E + have h4 : (4 : F) ≠ 0 := by rw [show (4:F) = 2*2 by norm_num]; exact mul_ne_zero htwo htwo + have hwden2ne : wden2 ≠ 0 := by rw [hwden2E]; exact mul_ne_zero h4 (pow_ne_zero 2 hy) + have hcube : wnum2^3 = -5 * wden2^3 := by + rw [hwnum2, hwden2E] + linear_combination + (x1^6 + (100)*x1^3 - 200) * hY + + ((-729)*x1^9 + (1215)*x1^6*y1^2 + (-512)*x1^3*y1^4 + (3735)*x1^6 + (-2340)*x1^3*y1^2 + (320)*y1^4 + (-9900)*x1^3 + (1800)*y1^2 + (9000)) * e1 + have hw : (wnum2 / wden2)^3 = -5 := by + rw [div_pow, hcube, mul_div_assoc, div_self (pow_ne_zero 3 hwden2ne), mul_one] + exact hy0 (wnum2 / wden2) (by + show (0 : F)^2 = (wnum2 / wden2)^3 + 0 * (wnum2 / wden2) + 5 + rw [hw]; ring) + +/-- Inverse `X`-coordinate vanishes: `padd P (−P) = (0 : Y₃ : 0)` (pure identity). -/ +theorem X_zero_inv (x1 y1 : F) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).X = 0 := by + simp only [padd]; ring + +/-- Inverse `Z`-coordinate vanishes (pure identity). -/ +theorem Z_zero_inv (x1 y1 : F) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Z = 0 := by + simp only [padd]; ring + +/-! ## Scaling (homogeneity) and affine interpretation -/ + +/-- `padd` is homogeneous of bidegree `(2,2)`: rescaling the inputs rescales the output. -/ +theorem smul_padd (u v : F) (P Q : PPoint F) : + padd (smul u P) (smul v Q) = smul (u^2*v^2) (padd P Q) := by + simp only [padd, smul, PPoint.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring + +/-- `aff` is invariant under nonzero rescaling. -/ +theorem aff_smul [DecidableEq F] (u : F) (hu : u ≠ 0) (P : PPoint F) : aff (smul u P) = aff P := by + rcases eq_or_ne P.Z 0 with h | h + · simp [aff, smul, h] + · have huz : u * P.Z ≠ 0 := mul_ne_zero hu h + simp only [aff, smul, if_neg h, if_neg huz] + rw [Prod.mk.injEq] + exact ⟨mul_div_mul_left _ _ hu, mul_div_mul_left _ _ hu⟩ + +/-- `OnCurveP` is preserved by rescaling. -/ +theorem oncurveP_smul (u : F) {P : PPoint F} (h : OnCurveP P) : OnCurveP (smul u P) := by + simp only [OnCurveP, smul] at h ⊢; linear_combination (u^3) * h + +/-- The nonzero-vector condition is preserved by nonzero rescaling. -/ +theorem nezVec_smul (u : F) (hu : u ≠ 0) {P : PPoint F} + (h : P.X ≠ 0 ∨ P.Y ≠ 0 ∨ P.Z ≠ 0) : + (smul u P).X ≠ 0 ∨ (smul u P).Y ≠ 0 ∨ (smul u P).Z ≠ 0 := by + simp only [smul] + rcases h with h | h | h + · exact Or.inl (mul_ne_zero hu h) + · exact Or.inr (Or.inl (mul_ne_zero hu h)) + · exact Or.inr (Or.inr (mul_ne_zero hu h)) + +@[simp] theorem aff_z1 [DecidableEq F] (x y : F) : aff (⟨x, y, 1⟩ : PPoint F) = (x, y) := by + simp [aff] + +/-- `P = P.Z • (X/Z : Y/Z : 1)` when `Z ≠ 0`: every finite point is a rescaled `Z = 1` rep. -/ +theorem eq_smul_normalize {P : PPoint F} (h : P.Z ≠ 0) : + P = smul P.Z ⟨P.X / P.Z, P.Y / P.Z, 1⟩ := by + obtain ⟨X, Y, Z⟩ := P + simp only [smul, PPoint.mk.injEq] + refine ⟨?_, ?_, ?_⟩ <;> field_simp + +/-! ## Unfolding the affine group law on `Z = 1` reps -/ + +/-- `(x₁,y₁)` and `(x₂,y₂)` on the curve are `≠ 𝒪 = (0,0)`. -/ +theorem onCurve_ne_zero (hfive : (5 : F) ≠ 0) {x y : F} (h : OnCurve 0 5 (x, y)) : + (x, y) ≠ ((0 : F), (0 : F)) := by + intro he + rw [Prod.mk.injEq] at he + obtain ⟨hx, hy⟩ := he; subst hx; subst hy + exact not_onCurve_zero hfive h + +/-- The affine sum in the distinct-`x` branch, with cleared denominators. -/ +theorem add_dist [DecidableEq F] (hfive : (5 : F) ≠ 0) {x1 y1 x2 y2 : F} + (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) (hne : x1 ≠ x2) : + add 0 (x1, y1) (x2, y2) + = (((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2) / (x2 - x1)^2, + ((y2 - y1)*(x1*(x2 - x1)^2 - ((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2)) - y1*(x2 - x1)^3) + / (x2 - x1)^3) := by + have hp0 := onCurve_ne_zero hfive h1 + have hq0 := onCurve_ne_zero hfive h2 + have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hne) + unfold add + dsimp only + rw [if_neg hp0, if_neg hq0, if_neg hne] + rw [Prod.mk.injEq] + constructor <;> field_simp <;> ring + +/-- The affine sum in the doubling branch (`a = 0`), with cleared denominators. -/ +theorem add_dbl [DecidableEq F] (htwo : (2 : F) ≠ 0) (hfive : (5 : F) ≠ 0) {x1 y1 : F} + (h1 : OnCurve 0 5 (x1, y1)) (hy : y1 ≠ 0) : + add 0 (x1, y1) (x1, y1) + = ((9*x1^4 - 8*x1*y1^2) / (4*y1^2), + (3*x1^2*(12*x1*y1^2 - 9*x1^4) - 8*y1^4) / (8*y1^3)) := by + have hp0 := onCurve_ne_zero hfive h1 + have h2y : y1 + y1 ≠ 0 := by rw [← two_mul]; exact mul_ne_zero htwo hy + have h4 : (4 : F) ≠ 0 := by rw [show (4:F) = 2*2 by norm_num]; exact mul_ne_zero htwo htwo + have h8 : (8 : F) ≠ 0 := by + rw [show (8:F) = 2*2*2 by norm_num]; exact mul_ne_zero (mul_ne_zero htwo htwo) htwo + unfold add + dsimp only + rw [if_neg hp0, if_neg hp0, if_pos rfl, if_neg h2y] + rw [Prod.mk.injEq] + constructor <;> field_simp <;> ring + +/-! ## The core equivalence -/ + +/-- **Core equivalence on `Z = 1` representatives.** For on-curve `(x₁,y₁),(x₂,y₂)`, the RCB +projective sum interprets affinely as the complete affine sum, and stays a valid projective point. -/ +theorem padd_spec_z1 [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + {x1 y1 x2 y2 : F} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) : + aff (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) = add 0 (x1, y1) (x2, y2) + ∧ Valid (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := by + have hfive : (5 : F) ≠ 0 := by + intro h5eq; exact hy0 0 (by show (0 : F)^2 = 0^3 + 0*0 + 5; rw [h5eq]; ring) + have e1 : y1^2 = x1^3 + 5 := by have h := h1; simp only [OnCurve] at h; linear_combination h + have e2 : y2^2 = x2^3 + 5 := by have h := h2; simp only [OnCurve] at h; linear_combination h + have hoc : OnCurveP (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := oncurveP_padd_z1 e1 e2 + have hy1 : y1 ≠ 0 := by + intro h; exact hy0 x1 (h ▸ h1) + by_cases hx : x1 = x2 + · subst hx + by_cases hy : y1 + y2 = 0 + · have hy2 : y2 = -y1 := by linear_combination hy + subst hy2 + refine ⟨?_, hoc, ?_⟩ + · have hz0 : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Z = 0 := Z_zero_inv x1 y1 + rw [aff, if_pos hz0] + have hnp : (x1, -y1) = CompElliptic.CurveForms.ShortWeierstrass.neg (x1, y1) := by + simp [CompElliptic.CurveForms.ShortWeierstrass.neg] + rw [hnp, CompElliptic.CurveForms.ShortWeierstrass.add_neg] + · exact Or.inr (Or.inl (Y_ne_zero_inv hy0 htwo e1 hy1)) + · have hyeq : y1 = y2 := by + have hz : (y1 - y2) * (y1 + y2) = 0 := by linear_combination e1 - e2 + rcases mul_eq_zero.mp hz with h | h + · exact sub_eq_zero.mp h + · exact absurd h hy + subst hyeq + have hZv : (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z = 8 * y1^3 := Z_doubling e1 + have h8 : (8 : F) ≠ 0 := by + rw [show (8:F) = 2*2*2 by norm_num]; exact mul_ne_zero (mul_ne_zero htwo htwo) htwo + have h4 : (4 : F) ≠ 0 := by rw [show (4:F) = 2*2 by norm_num]; exact mul_ne_zero htwo htwo + have hZne : (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z ≠ 0 := by + rw [hZv]; exact mul_ne_zero h8 (pow_ne_zero 3 hy1) + have hy2 : (4 : F) * y1^2 ≠ 0 := mul_ne_zero h4 (pow_ne_zero 2 hy1) + have hy3 : (8 : F) * y1^3 ≠ 0 := mul_ne_zero h8 (pow_ne_zero 3 hy1) + refine ⟨?_, hoc, ?_⟩ + · rw [aff, if_neg hZne, add_dbl htwo hfive h1 hy1, Prod.mk.injEq] + refine ⟨?_, ?_⟩ + · rw [div_eq_div_iff hZne hy2]; linear_combination keyx_dbl e1 + · rw [div_eq_div_iff hZne hy3]; linear_combination keyy_dbl e1 + · exact Or.inr (Or.inr hZne) + · have hZne : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z ≠ 0 := Z_ne_zero_dist hy0 e1 e2 hx + have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hx) + have hd2 : (x2 - x1)^2 ≠ 0 := pow_ne_zero 2 hd + have hd3 : (x2 - x1)^3 ≠ 0 := pow_ne_zero 3 hd + refine ⟨?_, hoc, ?_⟩ + · rw [aff, if_neg hZne, add_dist hfive h1 h2 hx, Prod.mk.injEq] + refine ⟨?_, ?_⟩ + · rw [div_eq_div_iff hZne hd2]; linear_combination keyx_dist e1 e2 + · rw [div_eq_div_iff hZne hd3]; linear_combination keyy_dist e1 e2 + · exact Or.inr (Or.inr hZne) + +/-! ## Structural facts about `Valid` points and the identity-input reductions -/ + +/-- A valid point with `Z = 0` has `X = 0` (only the identity is at infinity). -/ +theorem X_zero_of_Z_zero {P : PPoint F} (h : OnCurveP P) (hz : P.Z = 0) : P.X = 0 := by + have hX3 : P.X ^ 3 = 0 := by rw [OnCurveP, hz] at h; simpa using h.symm + exact pow_eq_zero_iff (by norm_num : (3 : ℕ) ≠ 0) |>.mp hX3 + +/-- A valid point always has nonzero `Y` (no 2-torsion; the identity is `(0 : 1 : 0)`). -/ +theorem Valid.Y_ne_zero (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + {P : PPoint F} (hP : Valid P) : P.Y ≠ 0 := by + rcases eq_or_ne P.Z 0 with hz | hz + · have hX := X_zero_of_Z_zero hP.1 hz + rcases hP.2 with h | h | h + · exact absurd hX h + · exact h + · exact absurd hz h + · intro hY + refine hy0 (P.X / P.Z) ?_ + have key : P.X^3 + 5 * P.Z^3 = 0 := by + have h := hP.1; rw [OnCurveP, hY] at h; linear_combination -h + show (0 : F)^2 = (P.X / P.Z)^3 + 0 * (P.X / P.Z) + 5 + field_simp; linear_combination -key + +/-- `padd` with the first argument an identity-type point `(0 : Y₁ : 0)` rescales the second. -/ +theorem padd_idL {P Q : PPoint F} (hX : P.X = 0) (hZ : P.Z = 0) : + padd P Q = smul (P.Y^2 * Q.Y) Q := by + simp only [padd, smul, hX, hZ, PPoint.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring + +/-- `padd` with the second argument an identity-type point `(0 : Y₂ : 0)` rescales the first. -/ +theorem padd_idR {P Q : PPoint F} (hX : Q.X = 0) (hZ : Q.Z = 0) : + padd P Q = smul (P.Y * Q.Y^2) P := by + simp only [padd, smul, hX, hZ, PPoint.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring + +/-- On-curve reading of the normalized affine coordinates of a finite valid point. -/ +theorem onCurve_norm {P : PPoint F} (h : OnCurveP P) (hz : P.Z ≠ 0) : + OnCurve 0 5 (P.X / P.Z, P.Y / P.Z) := by + have key : P.Y^2 * P.Z = P.X^3 + 5 * P.Z^3 := h + show (P.Y / P.Z)^2 = (P.X / P.Z)^3 + 0 * (P.X / P.Z) + 5 + field_simp; linear_combination key + +/-- **General equivalence.** For any two valid projective points, the RCB sum interprets +affinely as the complete affine sum, and stays valid. -/ +theorem padd_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + {P Q : PPoint F} (hP : Valid P) (hQ : Valid Q) : + aff (padd P Q) = add 0 (aff P) (aff Q) ∧ Valid (padd P Q) := by + have hPY := hP.Y_ne_zero hy0 + have hQY := hQ.Y_ne_zero hy0 + by_cases hPz : P.Z = 0 + · have hPX := X_zero_of_Z_zero hP.1 hPz + have hlam : P.Y^2 * Q.Y ≠ 0 := mul_ne_zero (pow_ne_zero 2 hPY) hQY + have haffP : aff P = (0, 0) := by rw [aff, if_pos hPz] + rw [padd_idL hPX hPz, haffP, CompElliptic.CurveForms.ShortWeierstrass.zero_add] + refine ⟨aff_smul _ hlam Q, oncurveP_smul _ hQ.1, nezVec_smul _ hlam hQ.2⟩ + · by_cases hQz : Q.Z = 0 + · have hQX := X_zero_of_Z_zero hQ.1 hQz + have hlam : P.Y * Q.Y^2 ≠ 0 := mul_ne_zero hPY (pow_ne_zero 2 hQY) + have haffQ : aff Q = (0, 0) := by rw [aff, if_pos hQz] + rw [padd_idR hQX hQz, haffQ, CompElliptic.CurveForms.ShortWeierstrass.add_zero] + refine ⟨aff_smul _ hlam P, oncurveP_smul _ hP.1, nezVec_smul _ hlam hP.2⟩ + · have hP1 := onCurve_norm hP.1 hPz + have hQ1 := onCurve_norm hQ.1 hQz + obtain ⟨haff, hvalid⟩ := padd_spec_z1 hy0 htwo hP1 hQ1 + have hu : P.Z^2 * Q.Z^2 ≠ 0 := mul_ne_zero (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz) + have hpadd : padd P Q = smul (P.Z^2 * Q.Z^2) (padd ⟨P.X/P.Z, P.Y/P.Z, 1⟩ ⟨Q.X/Q.Z, Q.Y/Q.Z, 1⟩) := by + conv_lhs => rw [eq_smul_normalize hPz, eq_smul_normalize hQz] + rw [smul_padd] + have haffP : aff P = (P.X / P.Z, P.Y / P.Z) := by rw [aff, if_neg hPz] + have haffQ : aff Q = (Q.X / Q.Z, Q.Y / Q.Z) := by rw [aff, if_neg hQz] + refine ⟨?_, ?_⟩ + · rw [hpadd, aff_smul _ hu, haff, haffP, haffQ] + · rw [hpadd] + exact ⟨oncurveP_smul _ hvalid.1, nezVec_smul _ hu hvalid.2⟩ + +/-- Validity is preserved by `padd` (closure). -/ +theorem valid_padd [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + {P Q : PPoint F} (hP : Valid P) (hQ : Valid Q) : Valid (padd P Q) := + (padd_spec hy0 htwo hP hQ).2 + +/-- `aff` is a homomorphism from `padd` to the affine group law on valid inputs. -/ +theorem aff_padd [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + {P Q : PPoint F} (hP : Valid P) (hQ : Valid Q) : + aff (padd P Q) = add 0 (aff P) (aff Q) := + (padd_spec hy0 htwo hP hQ).1 + +/-- The identity `(0 : 1 : 0)` is valid. -/ +theorem valid_pid : Valid (pid : PPoint F) := by + refine ⟨?_, Or.inr (Or.inl one_ne_zero)⟩ + simp [OnCurveP, pid] + +/-- `aff pid = 𝒪`. -/ +@[simp] theorem aff_pid [DecidableEq F] : aff (pid : PPoint F) = ((0 : F), (0 : F)) := by simp [aff, pid] + +/-! ## Bridge to the affine group `SWPoint E` for a curve `E` with `A = 0`, `B = 5` -/ + +section Bridge + +variable (E : SWCurve F) (hA : E.A = 0) (hB : E.B = 5) + +/-- Interpret a projective point as an element of the affine group `SWPoint E`: a finite on-curve +point maps to `(X/Z, Y/Z)`, everything else (points at infinity, off-curve junk) to `𝒪`. -/ +def toAffine [DecidableEq F] (P : PPoint F) : SWPoint E := + if h : OnCurveP P ∧ P.Z ≠ 0 then + ⟨P.X / P.Z, P.Y / P.Z, Or.inl (by rw [hA, hB]; exact onCurve_norm h.1 h.2)⟩ + else 0 + +/-- On valid points, `toAffine` agrees coordinatewise with `aff`. -/ +theorem toAffine_coords [DecidableEq F] {P : PPoint F} (hP : Valid P) : + ((toAffine E hA hB P).x, (toAffine E hA hB P).y) = aff P := by + rcases eq_or_ne P.Z 0 with hz | hz + · have h0 : toAffine E hA hB P = 0 := by rw [toAffine, dif_neg]; rintro ⟨_, h⟩; exact h hz + rw [h0, aff, if_pos hz]; rfl + · rw [toAffine, dif_pos ⟨hP.1, hz⟩, aff, if_neg hz] + +@[simp] theorem toAffine_pid [DecidableEq F] : toAffine E hA hB (pid : PPoint F) = 0 := by + rw [toAffine, dif_neg]; rintro ⟨_, h⟩; exact h rfl + +/-- **The homomorphism.** `toAffine` carries the projective RCB addition to the affine group law. -/ +theorem toAffine_padd [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + {P Q : PPoint F} (hP : Valid P) (hQ : Valid Q) : + toAffine E hA hB (padd P Q) = toAffine E hA hB P + toAffine E hA hB Q := by + apply SWPoint.ext_pair + have hL : ((toAffine E hA hB (padd P Q)).x, (toAffine E hA hB (padd P Q)).y) = aff (padd P Q) := + toAffine_coords E hA hB (valid_padd hy0 htwo hP hQ) + have hRc : ((toAffine E hA hB P + toAffine E hA hB Q).x, (toAffine E hA hB P + toAffine E hA hB Q).y) + = add E.A ((toAffine E hA hB P).x, (toAffine E hA hB P).y) + ((toAffine E hA hB Q).x, (toAffine E hA hB Q).y) := rfl + rw [hL, hRc, toAffine_coords E hA hB hP, toAffine_coords E hA hB hQ, hA, aff_padd hy0 htwo hP hQ] + +/-- Materialize an affine group element as a projective representative: `𝒪` as `(0 : 1 : 0)`, +a finite point as `(x : y : 1)`. -/ +def ofAffine [DecidableEq F] (p : SWPoint E) : PPoint F := + if p.x = 0 ∧ p.y = 0 then pid else ⟨p.x, p.y, 1⟩ + +include hA hB in +theorem valid_ofAffine [DecidableEq F] (p : SWPoint E) : Valid (ofAffine E p) := by + rw [ofAffine] + by_cases h : p.x = 0 ∧ p.y = 0 + · rw [if_pos h]; exact valid_pid + · rw [if_neg h] + have hoc : OnCurve 0 5 (p.x, p.y) := by + have hv := p.onCurve + rw [hA, hB] at hv + exact hv.resolve_right (by rw [Prod.mk.injEq]; exact h) + have e : p.y^2 = p.x^3 + 5 := by have := hoc; simp only [OnCurve] at this; linear_combination this + refine ⟨?_, Or.inr (Or.inr one_ne_zero)⟩ + simp only [OnCurveP]; linear_combination e + +theorem toAffine_ofAffine [DecidableEq F] (p : SWPoint E) : toAffine E hA hB (ofAffine E p) = p := by + rw [ofAffine] + by_cases h : p.x = 0 ∧ p.y = 0 + · rw [if_pos h, toAffine_pid] + apply SWPoint.ext_pair + obtain ⟨hx, hy⟩ := h + show ((0 : SWPoint E).x, (0 : SWPoint E).y) = (p.x, p.y) + rw [hx, hy]; rfl + · rw [if_neg h] + have hoc : OnCurve 0 5 (p.x, p.y) := by + have hv := p.onCurve; rw [hA, hB] at hv + exact hv.resolve_right (by rw [Prod.mk.injEq]; exact h) + have hZ : ((⟨p.x, p.y, 1⟩ : PPoint F)).Z ≠ 0 := one_ne_zero + have hocp : OnCurveP (⟨p.x, p.y, 1⟩ : PPoint F) := by + have e : p.y^2 = p.x^3 + 5 := by have := hoc; simp only [OnCurve] at this; linear_combination this + simp only [OnCurveP]; linear_combination e + apply SWPoint.ext_pair + rw [toAffine, dif_pos ⟨hocp, hZ⟩] + show (p.x / 1, p.y / 1) = (p.x, p.y) + rw [div_one, div_one] + +/-! ## Fast (binary) scalar multiplication -/ + +/-- Binary double-and-add scalar multiplication over `PPoint` using the RCB `padd`, matching the +`CompElliptic.binNsmul` recurrence used by the affine group's `nsmul`. -/ +def pnsmulFast (n : ℕ) (P : PPoint F) : PPoint F := binNsmul padd pid n P + +/-- **Fast scalar multiplication is the genuine group action.** By strong induction along the +`binNsmul` double-and-add recurrence: each intermediate stays valid (`valid_padd`) and `toAffine` +is a homomorphism (`toAffine_padd`), so the projective ladder computes `n • (toAffine P)`. -/ +theorem pnsmulFast_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + {P : PPoint F} (hP : Valid P) : ∀ n : ℕ, + Valid (pnsmulFast n P) ∧ toAffine E hA hB (pnsmulFast n P) = n • toAffine E hA hB P := by + intro n + induction n using Nat.strong_induction_on with + | _ n ih => + rw [pnsmulFast, binNsmul] + split + · rename_i h; subst h + exact ⟨valid_pid, by rw [toAffine_pid, zero_nsmul]⟩ + · rename_i hn + have hlt : n / 2 < n := Nat.div_lt_self (Nat.pos_of_ne_zero hn) (by decide) + obtain ⟨hvq, hq⟩ := ih (n / 2) hlt + rw [pnsmulFast] at hvq hq + set q := binNsmul padd pid (n / 2) P with hqdef + have hvd : Valid (padd q q) := valid_padd hy0 htwo hvq hvq + have hdaff : toAffine E hA hB (padd q q) + = (n / 2) • toAffine E hA hB P + (n / 2) • toAffine E hA hB P := by + rw [toAffine_padd E hA hB hy0 htwo hvq hvq, hq] + have key : n • toAffine E hA hB P + = (n / 2) • toAffine E hA hB P + (n / 2) • toAffine E hA hB P + + (n % 2) • toAffine E hA hB P := by + rw [← add_nsmul, ← add_nsmul]; congr 1; omega + split + · rename_i hodd + refine ⟨valid_padd hy0 htwo hvd hP, ?_⟩ + rw [toAffine_padd E hA hB hy0 htwo hvd hP, hdaff, key, hodd, one_nsmul] + · rename_i heven + refine ⟨hvd, ?_⟩ + rw [hdaff, key, show n % 2 = 0 from by omega, zero_nsmul, _root_.add_zero] + +/-- The packaged fast scalar multiplication on `SWPoint E`, going through projective coordinates. -/ +def smulFast [DecidableEq F] (n : ℕ) (p : SWPoint E) : SWPoint E := toAffine E hA hB (pnsmulFast n (ofAffine E p)) + +/-- **Correctness of `smulFast`:** it equals the affine scalar multiplication `n • p`, with the +field inversion paid once (in the final `toAffine`) instead of once per addition. -/ +theorem smulFast_eq [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (n : ℕ) (p : SWPoint E) : + smulFast E hA hB n p = n • p := by + rw [smulFast, (pnsmulFast_spec E hA hB hy0 htwo (valid_ofAffine E hA hB p) n).2, toAffine_ofAffine] + +end Bridge + +end PPoint +end CompElliptic.Curves.Pasta.Fast.Projective.Core From 2d22478bfea00a09d65cebcb0b912af3d6282c54 Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 00:37:25 -0700 Subject: [PATCH 2/6] Fast/Projective: Vesta as an instantiation of the generic core PVes := Core.PPoint Fq; padd/toAffine/ofAffine/smulFast and their lemmas delegate to the field-generic Core, fed Vesta's facts (curve A=0, B=5, 2!=0, 5!=0, no_onCurve_y_zero). The internal RCB certificates now live once in Core. paddFast/padd_eq_paddFast stay Vesta-local. MsmProj: drop three toAffine_pid simp args now redundant (toAffine is a reducible abbrev). Claude-Session: https://claude.ai/code/session_01Y4Wf3zPJYCwXzHDgdBUytv --- CompElliptic/Curves/Pasta/Fast/MsmProj.lean | 6 +- .../Curves/Pasta/Fast/Projective.lean | 579 +++--------------- .../Pasta/Fast/ProjectiveMontEquiv.lean | 4 +- 3 files changed, 89 insertions(+), 500 deletions(-) diff --git a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean index 0fd0481..fd4f830 100644 --- a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean +++ b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean @@ -49,7 +49,7 @@ theorem psum_cons (a : PVes) (xs : List PVes) : psum (a :: xs) = padd a (psum xs theorem psum_spec (L : List PVes) (h : ∀ P ∈ L, Valid P) : Valid (psum L) ∧ toAffine (psum L) = (L.map toAffine).sum := by induction L with - | nil => exact ⟨valid_pid, by simp [psum, toAffine_pid]⟩ + | nil => exact ⟨valid_pid, by simp [psum]⟩ | cons a xs ih => have ha : Valid a := h a (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) @@ -95,7 +95,7 @@ theorem foldr_paccStep_spec (L : List PVes) (h : ∀ P ∈ L, Valid P) : ∧ (toAffine (L.foldr paccStep (pid, pid)).1, toAffine (L.foldr paccStep (pid, pid)).2) = List.foldr Msm.accStep ((0 : Projective.G), (0 : Projective.G)) (L.map toAffine) := by induction L with - | nil => exact ⟨valid_pid, valid_pid, by simp [toAffine_pid]⟩ + | nil => exact ⟨valid_pid, valid_pid, by simp⟩ | cons a xs ih => have ha : Valid a := h a (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) @@ -166,7 +166,7 @@ theorem phornerList_spec (base : ℕ) (vals : List PVes) (h : ∀ P ∈ vals, Va Valid (phornerList base vals) ∧ toAffine (phornerList base vals) = Msm.hornerList base (vals.map toAffine) := by induction vals with - | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList, toAffine_pid]⟩ + | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList]⟩ | cons v xs ih => have hv : Valid v := h v (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) diff --git a/CompElliptic/Curves/Pasta/Fast/Projective.lean b/CompElliptic/Curves/Pasta/Fast/Projective.lean index 5d00624..fcf3ca4 100644 --- a/CompElliptic/Curves/Pasta/Fast/Projective.lean +++ b/CompElliptic/Curves/Pasta/Fast/Projective.lean @@ -5,22 +5,20 @@ as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Gregor Mitscha-Baude -/ import CompElliptic.Curves.Pasta +import CompElliptic.Curves.Pasta.Fast.Projective.Core /-! # Projective (Renes–Costello–Batina) point arithmetic for Vesta -The affine group law pays a field inversion per addition. This module replaces it, for the hot -`n • point` loop, by the complete projective addition formulas of Renes, Costello and Batina -(EUROCRYPT 2016; the EFD `add-2015-rcb` sequence at `a = 0`): single branchless formulas in -`(X : Y : Z)` valid for *all* input pairs, with the inversion paid once in `toAffine`. Their -completeness needs the curve to have no 2-torsion, which Vesta's odd prime order gives -(`Vesta.no_onCurve_y_zero`); that is what discharges `Z₃ ≠ 0` outside the genuine identity cases. +The Vesta instantiation of the field-generic projective core +(`CompElliptic.Curves.Pasta.Fast.Projective.Core`): `PVes` is `Core.PPoint 𝔽_q`, and every +operation and lemma below is the generic one specialized at the Vesta base field and curve. The +completeness hypotheses the core threads — no 2-torsion (`Vesta.no_onCurve_y_zero`), `2 ≠ 0`, +`5 ≠ 0` — and the curve coefficients `Vesta.curve.A = 0`, `Vesta.curve.B = 5` are discharged once, +here, and fed to the generic results. -Specialized to `a = 0`, `b = 5`, `b3 = 15`, the closed forms are - -* `X₃ = X₁Y₁Y₂² − 15X₁Y₁Z₂² − 30X₁Z₁Y₂Z₂ + Y₁²X₂Y₂ − 15Z₁²X₂Y₂ − 30Y₁Z₁X₂Z₂` -* `Y₃ = Y₁²Y₂² + 45X₁²X₂Z₂ + 45X₁Z₁X₂² − 225Z₁²Z₂²` -* `Z₃ = Y₁²Y₂Z₂ + Y₁Z₁Y₂² + 3X₁²X₂Y₂ + 3X₁Y₁X₂² + 15Y₁Z₁Z₂² + 15Z₁²Y₂Z₂` +The one genuinely Vesta-specific piece is `paddFast`: the raw-`ℕ` compiled spelling of `padd` at +the Vesta base-field modulus, with `padd_eq_paddFast` its proven equality. The `Fast` interfaces are provisional: they are not guaranteed to remain public, and may be folded into the existing API or otherwise changed incompatibly. @@ -38,512 +36,103 @@ abbrev Fq := CompElliptic.Fields.Pasta.VestaBaseField /-- The downstream affine group: on-curve points of Vesta with the complete affine group law. -/ abbrev G := SWPoint Vesta.curve -/-- A projective point in `(X : Y : Z)` coordinates over `𝔽_q`. -/ -structure PVes where - X : Fq - Y : Fq - Z : Fq -deriving DecidableEq +/-- A projective point in `(X : Y : Z)` coordinates over `𝔽_q`, from the generic core. -/ +abbrev PVes := Core.PPoint Fq namespace PVes -/-- Renes–Costello–Batina complete addition (`add-2015-rcb`, `a = 0`, `b3 = 15`). -/ -def padd (P Q : PVes) : PVes where - X := P.X*P.Y*Q.Y^2 - 15*P.X*P.Y*Q.Z^2 - 30*P.X*P.Z*Q.Y*Q.Z - + P.Y^2*Q.X*Q.Y - 15*P.Z^2*Q.X*Q.Y - 30*P.Y*P.Z*Q.X*Q.Z - Y := P.Y^2*Q.Y^2 + 45*P.X^2*Q.X*Q.Z + 45*P.X*P.Z*Q.X^2 - 225*P.Z^2*Q.Z^2 - Z := P.Y^2*Q.Y*Q.Z + P.Y*P.Z*Q.Y^2 + 3*P.X^2*Q.X*Q.Y + 3*P.X*P.Y*Q.X^2 - + 15*P.Y*P.Z*Q.Z^2 + 15*P.Z^2*Q.Y*Q.Z +/-! ## The Vesta curve facts feeding the generic core -/ -/-- Scalar (representative) rescaling `(X : Y : Z) ↦ (uX : uY : uZ)`. -/ -def smul (u : Fq) (P : PVes) : PVes := ⟨u*P.X, u*P.Y, u*P.Z⟩ +/-- Vesta's curve coefficient `A = 0`. -/ +theorem hA : Vesta.curve.A = 0 := rfl -/-- The projective identity `𝒪 = (0 : 1 : 0)`. -/ -def pid : PVes := ⟨0, 1, 0⟩ +/-- Vesta's curve coefficient `B = 5`. -/ +theorem hB : Vesta.curve.B = 5 := rfl + +/-- `2 ≠ 0` in the Vesta base field. -/ +theorem htwo : (2 : Fq) ≠ 0 := by decide + +/-- `5 ≠ 0` in the Vesta base field. -/ +theorem hfive : (5 : Fq) ≠ 0 := by decide -/-- The homogeneous projective curve equation `Y²Z = X³ + 5Z³` (Vesta, `a = 0`, `b = 5`). -/ -def OnCurveP (P : PVes) : Prop := P.Y^2*P.Z = P.X^3 + 5*P.Z^3 +/-- Vesta has no 2-torsion: no curve point with `y = 0` (`Vesta.no_onCurve_y_zero`). -/ +theorem hy0 : ∀ x : Fq, ¬ OnCurve 0 5 (x, 0) := Vesta.no_onCurve_y_zero -/-- `OnCurveP` unfolds definitionally to a field equation, hence is decidable. This is what keeps -`toAffine` — and everything downstream of it, `smulFast` in particular — computable. -/ -instance (P : PVes) : Decidable (OnCurveP P) := - inferInstanceAs (Decidable (P.Y^2*P.Z = P.X^3 + 5*P.Z^3)) +/-! ## Operations, specialized from the core -/ + +/-- Renes–Costello–Batina complete addition, at Vesta. -/ +abbrev padd : PVes → PVes → PVes := Core.PPoint.padd + +/-- Scalar (representative) rescaling, at Vesta. -/ +abbrev smul : Fq → PVes → PVes := Core.PPoint.smul + +/-- The projective identity `𝒪 = (0 : 1 : 0)`. -/ +abbrev pid : PVes := Core.PPoint.pid + +/-- The homogeneous projective curve equation, at Vesta. -/ +abbrev OnCurveP : PVes → Prop := Core.PPoint.OnCurveP /-- A representable projective point: on the projective curve and not the zero vector. -/ -def Valid (P : PVes) : Prop := OnCurveP P ∧ (P.X ≠ 0 ∨ P.Y ≠ 0 ∨ P.Z ≠ 0) - -/-- Affine interpretation as a raw coordinate pair: `Z ≠ 0 ↦ (X/Z, Y/Z)`, `Z = 0 ↦ 𝒪 = (0,0)`. -/ -def aff (P : PVes) : Fq × Fq := if P.Z = 0 then (0, 0) else (P.X / P.Z, P.Y / P.Z) - -/-! ## `ring`/`linear_combination` certificates - -Each identity below is a polynomial identity over `𝔽_q`, valid modulo the two curve equations -`e1 : y1² = x1³ + 5` and `e2 : y2² = x2³ + 5`. The cofactors were computed by an exact-rational -Gröbner/linear-algebra search over `ℚ[x1,y1,x2,y2]` (offline) and are checked here by `ring` -inside `linear_combination`. The `padd`-of-`Z=1`-points evaluation is spelled by `simp only [padd]` -which reduces the coordinate projections. -/ - -variable {x1 y1 x2 y2 : Fq} - -/-- Reading off the coordinates of `padd` on `Z = 1` representatives. -/ -@[simp] theorem padd_z1_X (x1 y1 x2 y2 : Fq) : - (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).X - = y1^2*x2*y2 + x1*y1*y2^2 - 15*x2*y2 - 30*y1*x2 - 30*x1*y2 - 15*x1*y1 := by - simp only [padd]; ring - -@[simp] theorem padd_z1_Y (x1 y1 x2 y2 : Fq) : - (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Y - = y1^2*y2^2 + 45*x1*x2^2 + 45*x1^2*x2 - 225 := by - simp only [padd]; ring - -@[simp] theorem padd_z1_Z (x1 y1 x2 y2 : Fq) : - (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z - = 3*x1*y1*x2^2 + 3*x1^2*x2*y2 + y1*y2^2 + y1^2*y2 + 15*y2 + 15*y1 := by - simp only [padd]; ring - -/-- `X₃·(x₂−x₁)² = x3num·Z₃`, the numerator match for the affine `x`-coordinate (distinct `x`). -/ -theorem keyx_dist (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) : - (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).X * (x2 - x1)^2 - = ((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2) * (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z := by - simp only [padd_z1_X, padd_z1_Z] - linear_combination - ((2)*x2^3*y2 + (3)*x1*x2^2*y2 + (-3)*x1*y1*x2^2 + (-3)*x1^2*x2*y2 + y2^3 + y1*y2^2 - y1^2*y2 + (10)*y2 + (-15)*y1) * e1 - + ((-3)*x1*y1*x2^2 + (-3)*x1^2*x2*y2 + (3)*x1^2*y1*x2 + x1^3*y2 + (3)*x1^3*y1 - y1*y2^2 + (-10)*y2 + (15)*y1) * e2 - -/-- `Y₃·(x₂−x₁)³ = y3num·Z₃`, the numerator match for the affine `y`-coordinate (distinct `x`). -/ -theorem keyy_dist (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) : - (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Y * (x2 - x1)^3 - = ((y2 - y1)*(x1*(x2 - x1)^2 - ((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2)) - y1*(x2 - x1)^3) - * (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z := by - simp only [padd_z1_Y, padd_z1_Z] - linear_combination - ((6)*x1*x2^5 + (-9)*x1^2*x2^4 + (2)*x2^3*y2^2 + (2)*y1*x2^3*y2 + (-15)*x1*x2^2*y2^2 + (6)*x1*y1*x2^2*y2 + (-3)*x1*y1^2*x2^2 + (15)*x1^2*x2*y2^2 + (-3)*x1^2*y1*x2*y2 + (-2)*y2^4 + (2)*y1^2*y2^2 - y1^3*y2 + (30)*x2^3 + (-60)*x1*x2^2 + (10)*y2^2 + (25)*y1*y2 + (-15)*y1^2 + (-75)) * e1 - + ((-6)*x1^4*x2^2 + (9)*x1^5*x2 + (3)*x1*y1*x2^2*y2 + (3)*x1^2*x2*y2^2 + (-6)*x1^2*y1*x2*y2 + (-2)*x1^3*y2^2 + (-2)*x1^3*y1*y2 + y1*y2^3 + (-75)*x1*x2^2 + (135)*x1^2*x2 + (-30)*x1^3 + (5)*y2^2 + (-25)*y1*y2 + (75)) * e2 - -/-- Curve preservation on `Z = 1` representatives: `padd` lands on the projective curve. -/ -theorem oncurveP_padd_z1 (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) : - OnCurveP (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := by - simp only [OnCurveP, padd_z1_X, padd_z1_Y, padd_z1_Z] - linear_combination - (-x1^6*x2^3*y2^3 - x1^3*y1^2*x2^3*y2^3 + x1^6*y2^5 - y1^4*x2^3*y2^3 + (-135)*x1^3*y1*x2^6 + x1^3*y1^2*y2^5 + (-405)*x1^4*x2^5*y2 + (-135)*x1^5*x2^4*y2 + y1^3*y2^6 + y1^4*y2^5 + (135)*x1^2*y1*x2^4*y2^2 + (-135)*x1^2*y1^2*x2^4*y2 + (35)*x1^3*x2^3*y2^3 + (90)*x1^3*y1*x2^3*y2^2 + (405)*x1^4*x2^2*y2^3 + (135)*x1^5*x2*y2^3 + (-5)*x1^6*y2^3 + (40)*y1^2*x2^3*y2^3 + (90)*y1^3*x2^3*y2^2 + (135)*x1*y1*x2^2*y2^4 + (270)*x1*y1^2*x2^2*y2^3 + (270)*x1^2*y1*x2*y2^4 + (135)*x1^2*y1^2*x2*y2^3 + (100)*x1^3*y2^5 + (45)*x1^3*y1*y2^4 + (-5)*x1^3*y1^2*y2^3 + (5)*y1^2*y2^5 + (-5)*y1^4*y2^3 + (-675)*x1^2*x2^4*y2 + (-2025)*x1^2*y1*x2^4 + (-2700)*x1^3*x2^3*y2 + (-2025)*x1^4*x2^2*y2 + (-675)*x1^5*x2*y2 + (-475)*x2^3*y2^3 + (-2250)*y1*x2^3*y2^2 + (-2700)*y1^2*x2^3*y2 + (-4050)*x1*x2^2*y2^3 + (-12150)*x1*y1*x2^2*y2^2 + (-4050)*x1*y1^2*x2^2*y2 + (-11475)*x1^2*x2*y2^3 + (-5400)*x1^2*y1*x2*y2^2 + (-675)*x1^2*y1^2*x2*y2 + (-3875)*x1^3*y2^3 + (-900)*x1^3*y1*y2^2 + (-200)*y2^5 + (-1125)*y1*y2^4 + (-1150)*y1^2*y2^3 + (-225)*y1^3*y2^2 + (27000)*x2^3*y2 + (27000)*y1*x2^3 + (60750)*x1*x2^2*y2 + (30375)*x1*y1*x2^2 + (57375)*x1^2*x2*y2 + (20250)*x1^2*y1*x2 + (16875)*x1^3*y2 + (3375)*x1^3*y1 + (-22625)*y2^3 + (-18000)*y1*y2^2 + (-3375)*y1^2*y2 + (-16875)*y2 + (-16875)*y1) * e1 - + (x1^9*y2^3 + (135)*x1^6*y1*x2^3 + (405)*x1^7*x2^2*y2 + (135)*x1^8*x2*y2 + (270)*x1^5*y1*x2*y2^2 + (105)*x1^6*y2^3 + (45)*x1^6*y1*y2^2 + (-5400)*x1^3*y1*x2^3 + (-4050)*x1^4*x2^2*y2 + (-12150)*x1^4*y1*x2^2 + (-10800)*x1^5*x2*y2 + (-4050)*x1^5*y1*x2 + (-3375)*x1^6*y2 + (-675)*x1^6*y1 + (-2700)*x1^2*y1*x2*y2^2 + (300)*x1^3*y2^3 + (-3600)*x1^3*y1*y2^2 + (-27000)*x1^2*x2*y2 + (40500)*x1^2*y1*x2 + (-13500)*x1^3*y2 + (-1000)*y2^3 + (-9000)*y1*y2^2 + (-135000)*y2 + (-135000)*y1) * e2 - -/-- **Distinct-`x` completeness (2-torsion-free).** If `Z₃ = 0` for two on-curve `Z = 1` points -with distinct `x`, then `w = wnum/wden` (the `x`-coordinate of `P − Q`) is a cube root of `−5`, -i.e. `(w, 0)` is a 2-torsion point — impossible on Vesta. Hence `Z₃ ≠ 0`. -/ -theorem Z_ne_zero_dist (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) (hne : x1 ≠ x2) : - (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z ≠ 0 := by - intro hZ - have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hne) - set wnum : Fq := (y1 + y2)^2 - (x1 + x2)*(x2 - x1)^2 with hwnumE - set wden : Fq := (x2 - x1)^2 with hwdenE - have hwdenne : wden ≠ 0 := by rw [hwdenE]; exact pow_ne_zero 2 hd - have hZpoly : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z - = 3*x1*y1*x2^2 + 3*x1^2*x2*y2 + y1*y2^2 + y1^2*y2 + 15*y2 + 15*y1 := padd_z1_Z x1 y1 x2 y2 - rw [hZpoly] at hZ - -- wnum^3 = -5 * wden^3 on the exceptional locus - have hcube : wnum^3 = -5 * wden^3 := by - rw [hwnumE, hwdenE] - linear_combination - (-x2^3*y2 + (-2)*y1*x2^3 + (3)*x1*y1*x2^2 + (3)*x1^2*x2*y2 + (-2)*x1^3*y2 + (-4)*x1^3*y1 + y2^3 + (3)*y1*y2^2 + (3)*y1^2*y2 + (4)*y1^3 + (-15)*y1) * hZ - + ((8)*x2^6 + (-6)*x1*x2^5 + (-6)*x1^2*x2^4 + (8)*x1^3*x2^3 + (-3)*x1^5*x2 + x1^6 + (-12)*x2^3*y2^2 + (-6)*y1*x2^3*y2 + (-4)*y1^2*x2^3 + (12)*x1*x2^2*y2^2 + (-9)*x1*y1^2*x2^2 + (3)*x1^2*y1^2*x2 + (-3)*x1^3*y2^2 + (-6)*x1^3*y1*y2 + (-2)*x1^3*y1^2 + (3)*y2^4 + (10)*y1*y2^3 + (9)*y1^2*y2^2 + (2)*y1^3*y2 + y1^4 + (60)*x2^3 + (-75)*x1*x2^2 + (45)*x1^2*x2 + (-10)*x1^3 + (-15)*y2^2 + (-60)*y1*y2 + (-60)*y1^2 + (50)) * e1 - + (x2^6 + (-3)*x1*x2^5 + (-2)*x2^3*y2^2 + (-6)*y1*x2^3*y2 + (5)*y1^2*x2^3 + (3)*x1*x2^2*y2^2 + (9)*x1*y1*x2^2*y2 + (-6)*x1*y1^2*x2^2 + (6)*x1^2*y1^2*x2 + y2^4 + (5)*y1*y2^3 + (8)*y1^2*y2^2 + (4)*y1^3*y2 - y1^4 + (-50)*x2^3 + (75)*x1*x2^2 + (-45)*x1^2*x2 + (5)*y2^2 + (15)*y1*y2 + (25)*y1^2 + (-50)) * e2 - -- so (wnum/wden) is a cube root of -5, contradicting no 2-torsion - have hw : (wnum / wden)^3 = -5 := by - rw [div_pow, hcube, mul_div_assoc, div_self (pow_ne_zero 3 hwdenne), mul_one] - exact Vesta.no_onCurve_y_zero (wnum / wden) (by - show (0 : Fq)^2 = (wnum / wden)^3 + Vesta.a * (wnum / wden) + Vesta.b - rw [hw]; simp [Vesta.a, Vesta.b]) - -/-- **Doubling `Z`-coordinate.** On `Z = 1` representatives with equal points, `Z₃ = 8y³`. -/ -theorem Z_doubling (e1 : y1^2 = x1^3 + 5) : - (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z = 8 * y1^3 := by - simp only [padd_z1_Z] - linear_combination ((-6)*y1) * e1 - -/-- `X₃·4y² = x3numd·Z₃`, doubling `x`-coordinate numerator match. -/ -theorem keyx_dbl (e1 : y1^2 = x1^3 + 5) : - (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).X * (4*y1^2) - = (9*x1^4 - 8*x1*y1^2) * (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z := by - simp only [padd_z1_X, padd_z1_Z] - linear_combination ((54)*x1^4*y1 + (24)*x1*y1^3) * e1 - -/-- `Y₃·8y³ = y3numd·Z₃`, doubling `y`-coordinate numerator match. -/ -theorem keyy_dbl (e1 : y1^2 = x1^3 + 5) : - (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Y * (8*y1^3) - = (3*x1^2*(12*x1*y1^2 - 9*x1^4) - 8*y1^4) * (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z := by - simp only [padd_z1_Y, padd_z1_Z] - linear_combination ((-162)*x1^6*y1 + (24)*y1^5 + (360)*y1^3) * e1 - -/-- **Inverse-case identity representative is nonzero (2-torsion-free).** `padd P (−P) = (0 : Y₃ : 0)` -with `Y₃ ≠ 0`: if `Y₃ = 0` then `w = wnum2/wden2` (the `x`-coordinate of `2P`) is a cube root of -`−5`, impossible on Vesta. -/ -theorem Y_ne_zero_inv (e1 : y1^2 = x1^3 + 5) (hy : y1 ≠ 0) : - (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Y ≠ 0 := by - intro hY - have hYpoly : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Y = y1^4 + 90*x1^3 - 225 := by - simp only [padd]; ring - rw [hYpoly] at hY - set wnum2 : Fq := 9*x1^4 - 8*x1*y1^2 with hwnum2 - set wden2 : Fq := 4*y1^2 with hwden2E - have hwden2ne : wden2 ≠ 0 := by rw [hwden2E]; exact mul_ne_zero (by decide) (pow_ne_zero 2 hy) - have hcube : wnum2^3 = -5 * wden2^3 := by - rw [hwnum2, hwden2E] - linear_combination - (x1^6 + (100)*x1^3 - 200) * hY - + ((-729)*x1^9 + (1215)*x1^6*y1^2 + (-512)*x1^3*y1^4 + (3735)*x1^6 + (-2340)*x1^3*y1^2 + (320)*y1^4 + (-9900)*x1^3 + (1800)*y1^2 + (9000)) * e1 - have hw : (wnum2 / wden2)^3 = -5 := by - rw [div_pow, hcube, mul_div_assoc, div_self (pow_ne_zero 3 hwden2ne), mul_one] - exact Vesta.no_onCurve_y_zero (wnum2 / wden2) (by - show (0 : Fq)^2 = (wnum2 / wden2)^3 + Vesta.a * (wnum2 / wden2) + Vesta.b - rw [hw]; simp [Vesta.a, Vesta.b]) - -/-- Inverse `X`-coordinate vanishes: `padd P (−P) = (0 : Y₃ : 0)` (pure identity). -/ -theorem X_zero_inv (x1 y1 : Fq) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).X = 0 := by - simp only [padd]; ring - -/-- Inverse `Z`-coordinate vanishes (pure identity). -/ -theorem Z_zero_inv (x1 y1 : Fq) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Z = 0 := by - simp only [padd]; ring - -/-! ## Scaling (homogeneity) and affine interpretation -/ - -/-- `padd` is homogeneous of bidegree `(2,2)`: rescaling the inputs rescales the output. -/ -theorem smul_padd (u v : Fq) (P Q : PVes) : - padd (smul u P) (smul v Q) = smul (u^2*v^2) (padd P Q) := by - simp only [padd, smul, PVes.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring - -/-- `aff` is invariant under nonzero rescaling. -/ -theorem aff_smul (u : Fq) (hu : u ≠ 0) (P : PVes) : aff (smul u P) = aff P := by - rcases eq_or_ne P.Z 0 with h | h - · simp [aff, smul, h] - · have huz : u * P.Z ≠ 0 := mul_ne_zero hu h - simp only [aff, smul, if_neg h, if_neg huz] - rw [Prod.mk.injEq] - exact ⟨mul_div_mul_left _ _ hu, mul_div_mul_left _ _ hu⟩ - -/-- `OnCurveP` is preserved by rescaling. -/ -theorem oncurveP_smul (u : Fq) {P : PVes} (h : OnCurveP P) : OnCurveP (smul u P) := by - simp only [OnCurveP, smul] at h ⊢; linear_combination (u^3) * h - -/-- The nonzero-vector condition is preserved by nonzero rescaling. -/ -theorem nezVec_smul (u : Fq) (hu : u ≠ 0) {P : PVes} - (h : P.X ≠ 0 ∨ P.Y ≠ 0 ∨ P.Z ≠ 0) : - (smul u P).X ≠ 0 ∨ (smul u P).Y ≠ 0 ∨ (smul u P).Z ≠ 0 := by - simp only [smul] - rcases h with h | h | h - · exact Or.inl (mul_ne_zero hu h) - · exact Or.inr (Or.inl (mul_ne_zero hu h)) - · exact Or.inr (Or.inr (mul_ne_zero hu h)) - -@[simp] theorem aff_z1 (x y : Fq) : aff ⟨x, y, 1⟩ = (x, y) := by - simp [aff] - -/-- `P = P.Z • (X/Z : Y/Z : 1)` when `Z ≠ 0`: every finite point is a rescaled `Z = 1` rep. -/ -theorem eq_smul_normalize {P : PVes} (h : P.Z ≠ 0) : - P = smul P.Z ⟨P.X / P.Z, P.Y / P.Z, 1⟩ := by - obtain ⟨X, Y, Z⟩ := P - simp only [smul, PVes.mk.injEq] - refine ⟨?_, ?_, ?_⟩ <;> field_simp - -/-! ## Unfolding the affine group law on `Z = 1` reps -/ - -/-- `(x₁,y₁)` and `(x₂,y₂)` on the curve are `≠ 𝒪 = (0,0)`. -/ -theorem onCurve_ne_zero {x y : Fq} (h : OnCurve 0 5 (x, y)) : (x, y) ≠ ((0 : Fq), (0 : Fq)) := by - intro he - rw [Prod.mk.injEq] at he - obtain ⟨hx, hy⟩ := he; subst hx; subst hy - exact not_onCurve_zero (show (5 : Fq) ≠ 0 by decide) h - -/-- The affine sum in the distinct-`x` branch, with cleared denominators. -/ -theorem add_dist {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) - (hne : x1 ≠ x2) : - add 0 (x1, y1) (x2, y2) - = (((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2) / (x2 - x1)^2, - ((y2 - y1)*(x1*(x2 - x1)^2 - ((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2)) - y1*(x2 - x1)^3) - / (x2 - x1)^3) := by - have hp0 := onCurve_ne_zero h1 - have hq0 := onCurve_ne_zero h2 - have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hne) - unfold add - dsimp only - rw [if_neg hp0, if_neg hq0, if_neg hne] - rw [Prod.mk.injEq] - constructor <;> field_simp <;> ring - -/-- The affine sum in the doubling branch (`a = 0`), with cleared denominators. -/ -theorem add_dbl {x1 y1 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (hy : y1 ≠ 0) : - add 0 (x1, y1) (x1, y1) - = ((9*x1^4 - 8*x1*y1^2) / (4*y1^2), - (3*x1^2*(12*x1*y1^2 - 9*x1^4) - 8*y1^4) / (8*y1^3)) := by - have hp0 := onCurve_ne_zero h1 - have h2y : y1 + y1 ≠ 0 := by rw [← two_mul]; exact mul_ne_zero (by decide) hy - have h2 : (2 : Fq) ≠ 0 := by decide - have h4 : (4 : Fq) ≠ 0 := by decide - have h8 : (8 : Fq) ≠ 0 := by decide - unfold add - dsimp only - rw [if_neg hp0, if_neg hp0, if_pos rfl, if_neg h2y] - rw [Prod.mk.injEq] - constructor <;> field_simp <;> ring - -/-! ## The core equivalence -/ - -/-- **Core equivalence on `Z = 1` representatives.** For on-curve `(x₁,y₁),(x₂,y₂)`, the RCB -projective sum interprets affinely as the complete affine sum, and stays a valid projective point. -/ -theorem padd_spec_z1 {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) : - aff (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) = add 0 (x1, y1) (x2, y2) - ∧ Valid (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := by - have e1 : y1^2 = x1^3 + 5 := by have h := h1; simp only [OnCurve] at h; linear_combination h - have e2 : y2^2 = x2^3 + 5 := by have h := h2; simp only [OnCurve] at h; linear_combination h - have hoc : OnCurveP (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := oncurveP_padd_z1 e1 e2 - have hy1 : y1 ≠ 0 := by - intro h; exact Vesta.no_onCurve_y_zero x1 (by rw [← h]; exact h1) - by_cases hx : x1 = x2 - · subst hx - by_cases hy : y1 + y2 = 0 - · -- inverse: y2 = -y1 - have hy2 : y2 = -y1 := by linear_combination hy - subst hy2 - refine ⟨?_, hoc, ?_⟩ - · have hz0 : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Z = 0 := Z_zero_inv x1 y1 - rw [aff, if_pos hz0] - have hnp : (x1, -y1) = CompElliptic.CurveForms.ShortWeierstrass.neg (x1, y1) := by - simp [CompElliptic.CurveForms.ShortWeierstrass.neg] - rw [hnp, CompElliptic.CurveForms.ShortWeierstrass.add_neg] - · exact Or.inr (Or.inl (Y_ne_zero_inv e1 hy1)) - · -- doubling: y1 = y2 - have hyeq : y1 = y2 := by - have hz : (y1 - y2) * (y1 + y2) = 0 := by linear_combination e1 - e2 - rcases mul_eq_zero.mp hz with h | h - · exact sub_eq_zero.mp h - · exact absurd h hy - subst hyeq - have hZv : (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z = 8 * y1^3 := Z_doubling e1 - have hZne : (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z ≠ 0 := by - rw [hZv]; exact mul_ne_zero (by decide) (pow_ne_zero 3 hy1) - have hy2 : (4 : Fq) * y1^2 ≠ 0 := mul_ne_zero (by decide) (pow_ne_zero 2 hy1) - have hy3 : (8 : Fq) * y1^3 ≠ 0 := mul_ne_zero (by decide) (pow_ne_zero 3 hy1) - refine ⟨?_, hoc, ?_⟩ - · rw [aff, if_neg hZne, add_dbl h1 hy1, Prod.mk.injEq] - refine ⟨?_, ?_⟩ - · rw [div_eq_div_iff hZne hy2]; linear_combination keyx_dbl e1 - · rw [div_eq_div_iff hZne hy3]; linear_combination keyy_dbl e1 - · exact Or.inr (Or.inr hZne) - · -- distinct x - have hZne : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z ≠ 0 := Z_ne_zero_dist e1 e2 hx - have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hx) - have hd2 : (x2 - x1)^2 ≠ 0 := pow_ne_zero 2 hd - have hd3 : (x2 - x1)^3 ≠ 0 := pow_ne_zero 3 hd - refine ⟨?_, hoc, ?_⟩ - · rw [aff, if_neg hZne, add_dist h1 h2 hx, Prod.mk.injEq] - refine ⟨?_, ?_⟩ - · rw [div_eq_div_iff hZne hd2]; linear_combination keyx_dist e1 e2 - · rw [div_eq_div_iff hZne hd3]; linear_combination keyy_dist e1 e2 - · exact Or.inr (Or.inr hZne) - -/-! ## Structural facts about `Valid` points and the identity-input reductions -/ - -/-- A valid point with `Z = 0` has `X = 0` (only the identity is at infinity). -/ -theorem X_zero_of_Z_zero {P : PVes} (h : OnCurveP P) (hz : P.Z = 0) : P.X = 0 := by - have hX3 : P.X ^ 3 = 0 := by rw [OnCurveP, hz] at h; simpa using h.symm - exact pow_eq_zero_iff (by norm_num : (3 : ℕ) ≠ 0) |>.mp hX3 - -/-- A valid point always has nonzero `Y` (no 2-torsion; the identity is `(0 : 1 : 0)`). -/ -theorem Valid.Y_ne_zero {P : PVes} (hP : Valid P) : P.Y ≠ 0 := by - rcases eq_or_ne P.Z 0 with hz | hz - · have hX := X_zero_of_Z_zero hP.1 hz - rcases hP.2 with h | h | h - · exact absurd hX h - · exact h - · exact absurd hz h - · intro hY - refine Vesta.no_onCurve_y_zero (P.X / P.Z) ?_ - have key : P.X^3 + 5 * P.Z^3 = 0 := by - have h := hP.1; rw [OnCurveP, hY] at h; linear_combination -h - show (0 : Fq)^2 = (P.X / P.Z)^3 + Vesta.a * (P.X / P.Z) + Vesta.b - rw [Vesta.a, Vesta.b]; field_simp; linear_combination -key - -/-- `padd` with the first argument an identity-type point `(0 : Y₁ : 0)` rescales the second. -/ -theorem padd_idL {P Q : PVes} (hX : P.X = 0) (hZ : P.Z = 0) : - padd P Q = smul (P.Y^2 * Q.Y) Q := by - simp only [padd, smul, hX, hZ, PVes.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring - -/-- `padd` with the second argument an identity-type point `(0 : Y₂ : 0)` rescales the first. -/ -theorem padd_idR {P Q : PVes} (hX : Q.X = 0) (hZ : Q.Z = 0) : - padd P Q = smul (P.Y * Q.Y^2) P := by - simp only [padd, smul, hX, hZ, PVes.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring - -/-- On-curve reading of the normalized affine coordinates of a finite valid point. -/ -theorem onCurve_norm {P : PVes} (h : OnCurveP P) (hz : P.Z ≠ 0) : - OnCurve 0 5 (P.X / P.Z, P.Y / P.Z) := by - have key : P.Y^2 * P.Z = P.X^3 + 5 * P.Z^3 := h - show (P.Y / P.Z)^2 = (P.X / P.Z)^3 + 0 * (P.X / P.Z) + 5 - field_simp; linear_combination key - -/-- **General equivalence.** For any two valid projective points, the RCB sum interprets -affinely as the complete affine sum, and stays valid. -/ -theorem padd_spec {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : - aff (padd P Q) = add 0 (aff P) (aff Q) ∧ Valid (padd P Q) := by - have hPY := hP.Y_ne_zero - have hQY := hQ.Y_ne_zero - by_cases hPz : P.Z = 0 - · -- P is an identity-type point - have hPX := X_zero_of_Z_zero hP.1 hPz - have hlam : P.Y^2 * Q.Y ≠ 0 := mul_ne_zero (pow_ne_zero 2 hPY) hQY - have haffP : aff P = (0, 0) := by rw [aff, if_pos hPz] - rw [padd_idL hPX hPz, haffP, CompElliptic.CurveForms.ShortWeierstrass.zero_add] - refine ⟨aff_smul _ hlam Q, oncurveP_smul _ hQ.1, nezVec_smul _ hlam hQ.2⟩ - · by_cases hQz : Q.Z = 0 - · -- Q is an identity-type point - have hQX := X_zero_of_Z_zero hQ.1 hQz - have hlam : P.Y * Q.Y^2 ≠ 0 := mul_ne_zero hPY (pow_ne_zero 2 hQY) - have haffQ : aff Q = (0, 0) := by rw [aff, if_pos hQz] - rw [padd_idR hQX hQz, haffQ, CompElliptic.CurveForms.ShortWeierstrass.add_zero] - refine ⟨aff_smul _ hlam P, oncurveP_smul _ hP.1, nezVec_smul _ hlam hP.2⟩ - · -- both finite: normalize to `Z = 1` and use the core lemma - have hP1 := onCurve_norm hP.1 hPz - have hQ1 := onCurve_norm hQ.1 hQz - obtain ⟨haff, hvalid⟩ := padd_spec_z1 hP1 hQ1 - have hu : P.Z^2 * Q.Z^2 ≠ 0 := mul_ne_zero (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz) - have hpadd : padd P Q = smul (P.Z^2 * Q.Z^2) (padd ⟨P.X/P.Z, P.Y/P.Z, 1⟩ ⟨Q.X/Q.Z, Q.Y/Q.Z, 1⟩) := by - conv_lhs => rw [eq_smul_normalize hPz, eq_smul_normalize hQz] - rw [smul_padd] - have haffP : aff P = (P.X / P.Z, P.Y / P.Z) := by rw [aff, if_neg hPz] - have haffQ : aff Q = (Q.X / Q.Z, Q.Y / Q.Z) := by rw [aff, if_neg hQz] - refine ⟨?_, ?_⟩ - · rw [hpadd, aff_smul _ hu, haff, haffP, haffQ] - · rw [hpadd] - exact ⟨oncurveP_smul _ hvalid.1, nezVec_smul _ hu hvalid.2⟩ +abbrev Valid : PVes → Prop := Core.PPoint.Valid + +/-- Affine interpretation as a raw coordinate pair. -/ +abbrev aff : PVes → Fq × Fq := Core.PPoint.aff + +/-- Interpret a projective point as an element of the affine group `G`. -/ +abbrev toAffine : PVes → G := Core.PPoint.toAffine Vesta.curve hA hB + +/-- Materialize an affine group element as a projective representative. -/ +abbrev ofAffine : G → PVes := Core.PPoint.ofAffine Vesta.curve + +/-- Binary double-and-add scalar multiplication over `PVes`. -/ +abbrev pnsmulFast : ℕ → PVes → PVes := Core.PPoint.pnsmulFast + +/-- The packaged fast scalar multiplication on `G`, through projective coordinates. -/ +abbrev smulFast : ℕ → G → G := Core.PPoint.smulFast Vesta.curve hA hB + +/-! ## Lemmas, specialized from the core -/ + +/-- The identity `(0 : 1 : 0)` is valid. -/ +theorem valid_pid : Valid pid := Core.PPoint.valid_pid /-- Validity is preserved by `padd` (closure). -/ theorem valid_padd {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : Valid (padd P Q) := - (padd_spec hP hQ).2 + Core.PPoint.valid_padd hy0 htwo hP hQ /-- `aff` is a homomorphism from `padd` to the affine group law on valid inputs. -/ theorem aff_padd {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : aff (padd P Q) = add 0 (aff P) (aff Q) := - (padd_spec hP hQ).1 - -/-- The identity `(0 : 1 : 0)` is valid. -/ -theorem valid_pid : Valid pid := by - refine ⟨?_, Or.inr (Or.inl one_ne_zero)⟩ - simp [OnCurveP, pid] + Core.PPoint.aff_padd hy0 htwo hP hQ -/-- `aff pid = 𝒪`. -/ -@[simp] theorem aff_pid : aff pid = ((0 : Fq), (0 : Fq)) := by simp [aff, pid] +/-- **General equivalence.** The RCB sum interprets affinely as the complete affine sum, and +stays valid. -/ +theorem padd_spec {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : + aff (padd P Q) = add 0 (aff P) (aff Q) ∧ Valid (padd P Q) := + Core.PPoint.padd_spec hy0 htwo hP hQ -/-! ## Bridge to the affine group `G = SWPoint Vesta.curve` -/ +@[simp] theorem toAffine_pid : toAffine pid = 0 := Core.PPoint.toAffine_pid Vesta.curve hA hB -/-- Interpret a projective point as an element of the affine group: a finite on-curve point maps to -`(X/Z, Y/Z)`, everything else (points at infinity, off-curve junk) to the identity `𝒪`. -/ -def toAffine (P : PVes) : G := - if h : OnCurveP P ∧ P.Z ≠ 0 then - ⟨P.X / P.Z, P.Y / P.Z, Or.inl (onCurve_norm h.1 h.2)⟩ - else 0 +/-- **The homomorphism.** `toAffine` carries the projective RCB addition to the affine group law. -/ +theorem toAffine_padd {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : + toAffine (padd P Q) = toAffine P + toAffine Q := + Core.PPoint.toAffine_padd Vesta.curve hA hB hy0 htwo hP hQ -/-- On valid points, `toAffine` agrees coordinatewise with `aff`. -/ -theorem toAffine_coords {P : PVes} (hP : Valid P) : - ((toAffine P).x, (toAffine P).y) = aff P := by - rcases eq_or_ne P.Z 0 with hz | hz - · have h0 : toAffine P = 0 := by rw [toAffine, dif_neg]; rintro ⟨_, h⟩; exact h hz - rw [h0, aff, if_pos hz]; rfl - · rw [toAffine, dif_pos ⟨hP.1, hz⟩, aff, if_neg hz] +/-- Every affine group element materializes to a valid projective representative. -/ +theorem valid_ofAffine (p : G) : Valid (ofAffine p) := + Core.PPoint.valid_ofAffine Vesta.curve hA hB p -@[simp] theorem toAffine_pid : toAffine pid = 0 := by - rw [toAffine, dif_neg]; rintro ⟨_, h⟩; exact h rfl +/-- `toAffine` is a left inverse of `ofAffine`. -/ +theorem toAffine_ofAffine (p : G) : toAffine (ofAffine p) = p := + Core.PPoint.toAffine_ofAffine Vesta.curve hA hB p -/-- **The homomorphism.** `toAffine` carries the projective RCB addition to the affine group law. -/ -theorem toAffine_padd {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : - toAffine (padd P Q) = toAffine P + toAffine Q := by - apply SWPoint.ext_pair - have hL : ((toAffine (padd P Q)).x, (toAffine (padd P Q)).y) = aff (padd P Q) := - toAffine_coords (valid_padd hP hQ) - have hRc : ((toAffine P + toAffine Q).x, (toAffine P + toAffine Q).y) - = add Vesta.curve.A ((toAffine P).x, (toAffine P).y) ((toAffine Q).x, (toAffine Q).y) := rfl - rw [hL, hRc, toAffine_coords hP, toAffine_coords hQ, aff_padd hP hQ] - rfl - -/-- Materialize an affine group element as a projective representative: the identity as `(0 : 1 : 0)`, -a finite point as `(x : y : 1)`. -/ -def ofAffine (p : G) : PVes := - if p.x = 0 ∧ p.y = 0 then pid else ⟨p.x, p.y, 1⟩ - -theorem valid_ofAffine (p : G) : Valid (ofAffine p) := by - rw [ofAffine] - by_cases h : p.x = 0 ∧ p.y = 0 - · rw [if_pos h]; exact valid_pid - · rw [if_neg h] - have hoc : OnCurve 0 5 (p.x, p.y) := by - have hv := p.onCurve - exact hv.resolve_right (by rw [Prod.mk.injEq]; exact h) - have e : p.y^2 = p.x^3 + 5 := by have := hoc; simp only [OnCurve] at this; linear_combination this - refine ⟨?_, Or.inr (Or.inr one_ne_zero)⟩ - simp only [OnCurveP]; linear_combination e - -theorem toAffine_ofAffine (p : G) : toAffine (ofAffine p) = p := by - rw [ofAffine] - by_cases h : p.x = 0 ∧ p.y = 0 - · rw [if_pos h, toAffine_pid] - apply SWPoint.ext_pair - obtain ⟨hx, hy⟩ := h - show ((0 : G).x, (0 : G).y) = (p.x, p.y) - rw [hx, hy]; rfl - · rw [if_neg h] - have hoc : OnCurve 0 5 (p.x, p.y) := p.onCurve.resolve_right (by rw [Prod.mk.injEq]; exact h) - have hZ : ((⟨p.x, p.y, 1⟩ : PVes)).Z ≠ 0 := one_ne_zero - have hocp : OnCurveP (⟨p.x, p.y, 1⟩ : PVes) := by - have e : p.y^2 = p.x^3 + 5 := by have := hoc; simp only [OnCurve] at this; linear_combination this - simp only [OnCurveP]; linear_combination e - apply SWPoint.ext_pair - rw [toAffine, dif_pos ⟨hocp, hZ⟩] - show (p.x / 1, p.y / 1) = (p.x, p.y) - rw [div_one, div_one] - -/-! ## Fast (binary) scalar multiplication -/ - -/-- Binary double-and-add scalar multiplication over `PVes` using the RCB `padd`, matching the -`CompElliptic.binNsmul` recurrence used by the affine group's `nsmul`. -/ -def pnsmulFast (n : ℕ) (P : PVes) : PVes := binNsmul padd pid n P - -/-- **Fast scalar multiplication is the genuine group action.** By strong induction along the -`binNsmul` double-and-add recurrence: each intermediate stays valid (`valid_padd`) and `toAffine` -is a homomorphism (`toAffine_padd`), so the projective ladder computes `n • (toAffine P)`. -/ +/-- **Fast scalar multiplication is the genuine group action**, projectively. -/ theorem pnsmulFast_spec {P : PVes} (hP : Valid P) : ∀ n : ℕ, - Valid (pnsmulFast n P) ∧ toAffine (pnsmulFast n P) = n • toAffine P := by - intro n - induction n using Nat.strong_induction_on with - | _ n ih => - rw [pnsmulFast, binNsmul] - split - · rename_i h; subst h - exact ⟨valid_pid, by rw [toAffine_pid, zero_nsmul]⟩ - · rename_i hn - have hlt : n / 2 < n := Nat.div_lt_self (Nat.pos_of_ne_zero hn) (by decide) - obtain ⟨hvq, hq⟩ := ih (n / 2) hlt - rw [pnsmulFast] at hvq hq - set q := binNsmul padd pid (n / 2) P with hqdef - have hvd : Valid (padd q q) := valid_padd hvq hvq - have hdaff : toAffine (padd q q) = (n / 2) • toAffine P + (n / 2) • toAffine P := by - rw [toAffine_padd hvq hvq, hq] - have key : n • toAffine P - = (n / 2) • toAffine P + (n / 2) • toAffine P + (n % 2) • toAffine P := by - rw [← add_nsmul, ← add_nsmul]; congr 1; omega - split - · rename_i hodd - refine ⟨valid_padd hvd hP, ?_⟩ - rw [toAffine_padd hvd hP, hdaff, key, hodd, one_nsmul] - · rename_i heven - refine ⟨hvd, ?_⟩ - rw [hdaff, key, show n % 2 = 0 from by omega, zero_nsmul, _root_.add_zero] - -/-- The packaged fast scalar multiplication on `G`, going through projective coordinates. -/ -def smulFast (n : ℕ) (p : G) : G := toAffine (pnsmulFast n (ofAffine p)) - -/-- **Correctness of `smulFast`:** it equals the affine scalar multiplication `n • p`, with the -field inversion paid once (in the final `toAffine`) instead of once per addition. -/ -theorem smulFast_eq (n : ℕ) (p : G) : smulFast n p = n • p := by - rw [smulFast, (pnsmulFast_spec (valid_ofAffine p) n).2, toAffine_ofAffine] + Valid (pnsmulFast n P) ∧ toAffine (pnsmulFast n P) = n • toAffine P := + Core.PPoint.pnsmulFast_spec Vesta.curve hA hB hy0 htwo hP + +/-- **Correctness of `smulFast`:** it equals the affine scalar multiplication `n • p`. -/ +theorem smulFast_eq (n : ℕ) (p : G) : smulFast n p = n • p := + Core.PPoint.smulFast_eq Vesta.curve hA hB hy0 htwo n p /-! ## Fast compiled spelling of `padd` (compiled-tier only) @@ -625,7 +214,7 @@ this `@[csimp]` (or the Montgomery successor) makes every compiled call site (in `native_decide` auxiliaries) run the fused raw-`ℕ` form. -/ theorem padd_eq_paddFast : @padd = @paddFast := by funext P Q - simp only [padd, paddFast, PVes.mk.injEq] + simp only [padd, Core.PPoint.padd, paddFast, Core.PPoint.mk.injEq] refine ⟨?_, ?_, ?_⟩ <;> simp only [cast_fadd, cast_fmul, cast_fsub, cast_val, Nat.cast_ofNat] <;> ring diff --git a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean index 6586478..c15f4ac 100644 --- a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean +++ b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean @@ -198,7 +198,7 @@ theorem toPVesM_padd {p r : PM} (hp : WFP p) (hr : WFP r) : toPVesM (PM.padd p r) = PVes.padd (toPVesM p) (toPVesM r) := by obtain ⟨hpx, hpy, hpz⟩ := hp obtain ⟨hrx, hry, hrz⟩ := hr - simp only [toPVesM, PM.padd, PVes.padd, PVes.mk.injEq] + simp only [toPVesM, PM.padd, PVes.padd, Core.PPoint.padd, Core.PPoint.mk.injEq] refine ⟨?_, ?_, ?_⟩ <;> simp (maxDischargeDepth := 16) only [montVal_add, montVal_sub, montVal_mul, montVal_square, montVal_c3, montVal_c15, montVal_c30, montVal_c45, montVal_c225, @@ -207,7 +207,7 @@ theorem toPVesM_padd {p r : PM} (hp : WFP p) (hr : WFP r) : ring @[simp] theorem toPVesM_pid : toPVesM PM.pid = PVes.pid := by - simp only [toPVesM, PM.pid, PVes.pid, PVes.mk.injEq] + simp only [toPVesM, PM.pid, PVes.pid, Core.PPoint.pid, Core.PPoint.mk.injEq] exact ⟨montVal_zero, montVal_one, montVal_zero⟩ /-- **The kernel's negation is coordinate negation of `Y`**, the short-Weierstrass inverse. -/ From 137dd1b52f65deb6ae351865bcd17d44a48d46c8 Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 00:41:36 -0700 Subject: [PATCH 3/6] Fast/Projective: Pallas instances beside Vesta namespace Pallas mirrors the flat Vesta decls: PPal := Core.PPoint Fp, G := SWPoint Pallas.curve, and padd/toAffine/ofAffine/smulFast with their lemmas delegating to the generic Core fed Pallas's facts (curve A=0, B=5, 2!=0, 5!=0, Pallas.no_onCurve_y_zero). smulFast_eq gives the projective fast ladder = n . p over Pallas. Claude-Session: https://claude.ai/code/session_01Y4Wf3zPJYCwXzHDgdBUytv --- .../Curves/Pasta/Fast/Projective.lean | 114 ++++++++++++++++++ 1 file changed, 114 insertions(+) diff --git a/CompElliptic/Curves/Pasta/Fast/Projective.lean b/CompElliptic/Curves/Pasta/Fast/Projective.lean index fcf3ca4..3e229e0 100644 --- a/CompElliptic/Curves/Pasta/Fast/Projective.lean +++ b/CompElliptic/Curves/Pasta/Fast/Projective.lean @@ -219,4 +219,118 @@ theorem padd_eq_paddFast : @padd = @paddFast := by simp only [cast_fadd, cast_fmul, cast_fsub, cast_val, Nat.cast_ofNat] <;> ring end PVes + +/-! # The Pallas instantiation + +The Pallas analogue of the Vesta block above: `PPal` is `Core.PPoint 𝔽_p`, and every operation and +lemma is the generic core specialized at the Pallas base field and curve. The completeness +hypotheses are discharged once here — no 2-torsion (`Pallas.no_onCurve_y_zero`), `2 ≠ 0`, `5 ≠ 0`, +and the coefficients `Pallas.curve.A = 0`, `Pallas.curve.B = 5`. No `paddFast` here: the raw-`ℕ` +compiled spelling is Vesta-only. -/ + +namespace Pallas + +/-- The Pallas base field `𝔽_p`, over which the Pallas curve is defined. -/ +abbrev Fp := CompElliptic.Fields.Pasta.PallasBaseField + +/-- The downstream affine group: on-curve points of Pallas with the complete affine group law. -/ +abbrev G := SWPoint Pallas.curve + +/-- A projective point in `(X : Y : Z)` coordinates over `𝔽_p`, from the generic core. -/ +abbrev PPal := Core.PPoint Fp + +/-! ## The Pallas curve facts feeding the generic core -/ + +/-- Pallas's curve coefficient `A = 0`. -/ +theorem hA : Pallas.curve.A = 0 := rfl + +/-- Pallas's curve coefficient `B = 5`. -/ +theorem hB : Pallas.curve.B = 5 := rfl + +/-- `2 ≠ 0` in the Pallas base field. -/ +theorem htwo : (2 : Fp) ≠ 0 := by decide + +/-- `5 ≠ 0` in the Pallas base field. -/ +theorem hfive : (5 : Fp) ≠ 0 := by decide + +/-- Pallas has no 2-torsion: no curve point with `y = 0` (`Pallas.no_onCurve_y_zero`). -/ +theorem hy0 : ∀ x : Fp, ¬ OnCurve 0 5 (x, 0) := Pallas.no_onCurve_y_zero + +/-! ## Operations, specialized from the core -/ + +/-- Renes–Costello–Batina complete addition, at Pallas. -/ +abbrev padd : PPal → PPal → PPal := Core.PPoint.padd + +/-- Scalar (representative) rescaling, at Pallas. -/ +abbrev smul : Fp → PPal → PPal := Core.PPoint.smul + +/-- The projective identity `𝒪 = (0 : 1 : 0)`. -/ +abbrev pid : PPal := Core.PPoint.pid + +/-- The homogeneous projective curve equation, at Pallas. -/ +abbrev OnCurveP : PPal → Prop := Core.PPoint.OnCurveP + +/-- A representable projective point: on the projective curve and not the zero vector. -/ +abbrev Valid : PPal → Prop := Core.PPoint.Valid + +/-- Affine interpretation as a raw coordinate pair. -/ +abbrev aff : PPal → Fp × Fp := Core.PPoint.aff + +/-- Interpret a projective point as an element of the affine group `G`. -/ +abbrev toAffine : PPal → G := Core.PPoint.toAffine Pallas.curve hA hB + +/-- Materialize an affine group element as a projective representative. -/ +abbrev ofAffine : G → PPal := Core.PPoint.ofAffine Pallas.curve + +/-- Binary double-and-add scalar multiplication over `PPal`. -/ +abbrev pnsmulFast : ℕ → PPal → PPal := Core.PPoint.pnsmulFast + +/-- The packaged fast scalar multiplication on `G`, through projective coordinates. -/ +abbrev smulFast : ℕ → G → G := Core.PPoint.smulFast Pallas.curve hA hB + +/-! ## Lemmas, specialized from the core -/ + +/-- The identity `(0 : 1 : 0)` is valid. -/ +theorem valid_pid : Valid pid := Core.PPoint.valid_pid + +/-- Validity is preserved by `padd` (closure). -/ +theorem valid_padd {P Q : PPal} (hP : Valid P) (hQ : Valid Q) : Valid (padd P Q) := + Core.PPoint.valid_padd hy0 htwo hP hQ + +/-- `aff` is a homomorphism from `padd` to the affine group law on valid inputs. -/ +theorem aff_padd {P Q : PPal} (hP : Valid P) (hQ : Valid Q) : + aff (padd P Q) = add 0 (aff P) (aff Q) := + Core.PPoint.aff_padd hy0 htwo hP hQ + +/-- **General equivalence.** The RCB sum interprets affinely as the complete affine sum, and +stays valid. -/ +theorem padd_spec {P Q : PPal} (hP : Valid P) (hQ : Valid Q) : + aff (padd P Q) = add 0 (aff P) (aff Q) ∧ Valid (padd P Q) := + Core.PPoint.padd_spec hy0 htwo hP hQ + +@[simp] theorem toAffine_pid : toAffine pid = 0 := Core.PPoint.toAffine_pid Pallas.curve hA hB + +/-- **The homomorphism.** `toAffine` carries the projective RCB addition to the affine group law. -/ +theorem toAffine_padd {P Q : PPal} (hP : Valid P) (hQ : Valid Q) : + toAffine (padd P Q) = toAffine P + toAffine Q := + Core.PPoint.toAffine_padd Pallas.curve hA hB hy0 htwo hP hQ + +/-- Every affine group element materializes to a valid projective representative. -/ +theorem valid_ofAffine (p : G) : Valid (ofAffine p) := + Core.PPoint.valid_ofAffine Pallas.curve hA hB p + +/-- `toAffine` is a left inverse of `ofAffine`. -/ +theorem toAffine_ofAffine (p : G) : toAffine (ofAffine p) = p := + Core.PPoint.toAffine_ofAffine Pallas.curve hA hB p + +/-- **Fast scalar multiplication is the genuine group action**, projectively. -/ +theorem pnsmulFast_spec {P : PPal} (hP : Valid P) : ∀ n : ℕ, + Valid (pnsmulFast n P) ∧ toAffine (pnsmulFast n P) = n • toAffine P := + Core.PPoint.pnsmulFast_spec Pallas.curve hA hB hy0 htwo hP + +/-- **Correctness of `smulFast`:** it equals the affine scalar multiplication `n • p`. -/ +theorem smulFast_eq (n : ℕ) (p : G) : smulFast n p = n • p := + Core.PPoint.smulFast_eq Pallas.curve hA hB hy0 htwo n p + +end Pallas end CompElliptic.Curves.Pasta.Fast.Projective From c62d3aa01e7aa2b9df1fbd25525d041b6f0ebbd0 Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 06:41:32 -0700 Subject: [PATCH 4/6] Fast/MsmProj/Core: field-generic projective Pippenger MSM The windowed Pippenger MSM run entirely in projective coordinates (basic, single-pass-scatter, and windows-parallel paths), generic over the Core.PPoint projective core for any y^2 = x^3 + 5 curve, proving pippengerProj_eq_msm = the naive MSM for c >= 1. Vesta and Pallas instantiate it. Claude-Session: https://claude.ai/code/session_01Y4Wf3zPJYCwXzHDgdBUytv --- .../Curves/Pasta/Fast/MsmProj/Core.lean | 461 ++++++++++++++++++ 1 file changed, 461 insertions(+) create mode 100644 CompElliptic/Curves/Pasta/Fast/MsmProj/Core.lean diff --git a/CompElliptic/Curves/Pasta/Fast/MsmProj/Core.lean b/CompElliptic/Curves/Pasta/Fast/MsmProj/Core.lean new file mode 100644 index 0000000..0916a0e --- /dev/null +++ b/CompElliptic/Curves/Pasta/Fast/MsmProj/Core.lean @@ -0,0 +1,461 @@ +/- +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: Gregor Mitscha-Baude +-/ +import CompElliptic.Curves.Pasta.Fast.Msm +import CompElliptic.Curves.Pasta.Fast.Projective.Core + +/-! +# The windowed Pippenger MSM run in projective coordinates, generic over the base field + +The affine Pippenger accelerator (`Fast.Msm`) is already generic over any `[AddCommGroup G]`, but at +a curve's affine group every group addition pays a field inversion. This module runs the whole +Pippenger interior over the field-generic `Projective.Core.PPoint` with `padd`/`pnsmulFast` — one +inversion per MSM instead of one per add — and proves the result equal to the affine accelerator +(`pippengerProj_eq`) and to the naive MSM (`pippengerProj_eq_msm`). + +`PPoint` is not a lawful monoid on the nose (associativity only holds after `toAffine`), so the +Pippenger equality is not re-run here: each fold of `Fast.Msm` is mirrored by a `padd`/`pid` version +and shown to commute with `toAffine`, carrying `Valid` through every intermediate (`psum_spec`, +`pbucketOf_spec`, `foldr_paccStep_spec`, `pwindowValue_spec`, `phornerList_spec`). + +This is the field-generic core; each Pasta curve instantiates it (Vesta in `Fast/MsmProj.lean`, +Pallas in `Fast/MsmProjPallas.lean`) by supplying its curve `E` (with `E.A = 0`, `E.B = 5`) and the +no-2-torsion facts `hy0`/`htwo`. Only the basic path is generic here; the Array-scatter and +parallel variants remain in the Vesta module. + +The `Fast` interfaces are provisional: they are not guaranteed to remain public, and may be folded +into the existing API or otherwise changed incompatibly. +-/ + +open CompElliptic +open CompElliptic.CurveForms.ShortWeierstrass +open CompElliptic.Curves.Pasta.Fast +open CompElliptic.Curves.Pasta.Fast.Projective.Core +open CompElliptic.Curves.Pasta.Fast.Projective.Core.PPoint + +namespace CompElliptic.Curves.Pasta.Fast.MsmProj.Core + +variable {F : Type*} [Field F] [DecidableEq F] +variable (E : SWCurve F) (hA : E.A = 0) (hB : E.B = 5) + +/-- The affine group `SWPoint E` carries a default point, needed to instantiate the `Fast.Msm` +wrapper (`Msm.pippenger`) whose section fixes `[Inhabited G]`. -/ +local instance : Inhabited (SWPoint E) := ⟨0⟩ + +/-! ## Projective bucket sum (`foldr padd pid`), mirroring `Fast.Msm.bucketOf` -/ + +/-- The `padd`-fold sum of a list of projective points, from the projective identity `pid`. -/ +def psum (L : List (PPoint F)) : PPoint F := L.foldr padd pid + +omit [DecidableEq F] in +theorem psum_cons (a : PPoint F) (xs : List (PPoint F)) : + psum (a :: xs) = padd a (psum xs) := rfl + +/-- A projective `padd`-sum of valid points is valid, and `toAffine` carries it to the affine sum. -/ +theorem psum_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (L : List (PPoint F)) (h : ∀ P ∈ L, Valid P) : + Valid (psum L) ∧ toAffine E hA hB (psum L) = (L.map (toAffine E hA hB)).sum := by + induction L with + | nil => exact ⟨valid_pid, by simp [psum]⟩ + | cons a xs ih => + have ha : Valid a := h a (by simp) + have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) + obtain ⟨hvxs, hxseq⟩ := ih hxs + rw [psum_cons] + exact ⟨valid_padd hy0 htwo ha hvxs, by + rw [toAffine_padd E hA hB hy0 htwo ha hvxs, hxseq, List.map_cons, List.sum_cons]⟩ + +/-- The projective bucket-`b` sum: `padd`-fold the points whose digit tag is `b`. -/ +def pbucketOf (dp : List (ℕ × PPoint F)) (b : ℕ) : PPoint F := + psum (dp.filterMap fun p => if p.1 = b then some p.2 else none) + +/-- The projective bucket sum is valid and matches `Fast.Msm.bucketOf` of the `toAffine`-mapped +digit-tagged list. -/ +theorem pbucketOf_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (dp : List (ℕ × PPoint F)) (b : ℕ) (h : ∀ p ∈ dp, Valid p.2) : + Valid (pbucketOf dp b) + ∧ toAffine E hA hB (pbucketOf dp b) + = Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) b := by + have hval : ∀ P ∈ dp.filterMap (fun p => if p.1 = b then some p.2 else none), Valid P := by + intro P hP + rw [List.mem_filterMap] at hP + obtain ⟨q, hq, hqeq⟩ := hP + by_cases hc : q.1 = b + · rw [if_pos hc, Option.some.injEq] at hqeq; rw [← hqeq]; exact h q hq + · rw [if_neg hc] at hqeq; exact absurd hqeq (by simp) + obtain ⟨hv, heq⟩ := psum_spec E hA hB hy0 htwo _ hval + refine ⟨hv, ?_⟩ + rw [pbucketOf, heq, Msm.bucketOf, List.filterMap_map, List.map_filterMap] + refine congrArg List.sum (congrArg (dp.filterMap ·) ?_) + funext p + by_cases hc : p.1 = b <;> simp [hc, Function.comp] + +/-! ## Projective suffix-sum accumulator, mirroring `Fast.Msm.accStep` -/ + +/-- One step of the projective suffix-sum accumulator: carry `(running, total)`, `padd` the next +bucket into `running`, then `padd` `running` into `total`. -/ +def paccStep (a : PPoint F) (p : PPoint F × PPoint F) : PPoint F × PPoint F := + (padd p.1 a, padd p.2 (padd p.1 a)) + +/-- Folding `paccStep` over valid points keeps both accumulator components valid, and `toAffine` +carries the whole fold (componentwise) to the affine `Fast.Msm.accStep` fold. -/ +theorem foldr_paccStep_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (L : List (PPoint F)) (h : ∀ P ∈ L, Valid P) : + Valid (L.foldr paccStep (pid, pid)).1 ∧ Valid (L.foldr paccStep (pid, pid)).2 + ∧ (toAffine E hA hB (L.foldr paccStep (pid, pid)).1, + toAffine E hA hB (L.foldr paccStep (pid, pid)).2) + = List.foldr Msm.accStep ((0 : SWPoint E), (0 : SWPoint E)) (L.map (toAffine E hA hB)) := by + induction L with + | nil => exact ⟨valid_pid, valid_pid, by simp⟩ + | cons a xs ih => + have ha : Valid a := h a (by simp) + have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) + obtain ⟨hv1, hv2, heq⟩ := ih hxs + have hstep : (a :: xs).foldr paccStep (pid, pid) + = paccStep a (xs.foldr paccStep (pid, pid)) := rfl + rw [hstep] + have hv1' : Valid (padd (xs.foldr paccStep (pid, pid)).1 a) := valid_padd hy0 htwo hv1 ha + refine ⟨hv1', valid_padd hy0 htwo hv2 hv1', ?_⟩ + rw [List.map_cons, List.foldr_cons, ← heq, Msm.accStep] + simp only [paccStep, toAffine_padd E hA hB hy0 htwo hv1 ha, + toAffine_padd E hA hB hy0 htwo hv2 hv1'] + +/-! ## Projective window value, mirroring `Fast.Msm.windowValue` -/ + +/-- The digit-tagged projective term list for window `i`. -/ +def pdpOf (base i : ℕ) (pterms : List (ℕ × PPoint F)) : List (ℕ × PPoint F) := + pterms.map fun t => (Msm.digit base i t.1, t.2) + +/-- The projective window value: build the `base − 1` projective buckets, then run the projective +suffix-sum accumulation. -/ +def pwindowValue (base i : ℕ) (pterms : List (ℕ × PPoint F)) : PPoint F := + (List.foldr paccStep (pid, pid) + ((List.range (base - 1)).map fun k => pbucketOf (pdpOf base i pterms) (k + 1))).2 + +/-- The projective window value is valid and matches `Fast.Msm.windowValue` of the `toAffine`-mapped +terms. -/ +theorem pwindowValue_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (base i : ℕ) (pterms : List (ℕ × PPoint F)) (h : ∀ p ∈ pterms, Valid p.2) : + Valid (pwindowValue base i pterms) + ∧ toAffine E hA hB (pwindowValue base i pterms) + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine E hA hB t.2)) := by + have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by + intro p hp + rw [pdpOf, List.mem_map] at hp + obtain ⟨t, ht, rfl⟩ := hp + exact h t ht + simp only [pwindowValue] + set buckets := (List.range (base - 1)).map fun k => pbucketOf (pdpOf base i pterms) (k + 1) + with hbuck + have hbval : ∀ P ∈ buckets, Valid P := by + intro P hP + rw [hbuck, List.mem_map] at hP + obtain ⟨k, _, rfl⟩ := hP + exact (pbucketOf_spec E hA hB hy0 htwo _ _ hdp).1 + obtain ⟨_, hv2, heq⟩ := foldr_paccStep_spec E hA hB hy0 htwo buckets hbval + refine ⟨hv2, ?_⟩ + have hmap : buckets.map (toAffine E hA hB) + = (List.range (base - 1)).map fun k => + Msm.bucketOf (Msm.dpOf base i (pterms.map fun t => (t.1, toAffine E hA hB t.2))) (k + 1) := by + rw [hbuck, List.map_map] + apply List.map_congr_left + intro k _ + rw [Function.comp_apply, (pbucketOf_spec E hA hB hy0 htwo _ _ hdp).2] + congr 1 + simp only [pdpOf, Msm.dpOf, List.map_map, Function.comp_def] + rw [Msm.windowValue, ← hmap, ← heq] + +/-! ## Projective Horner fold, mirroring `Fast.Msm.hornerList` -/ + +/-- Horner across windows in projective coordinates: each `base •` doubling is the fast binary +scalar multiplication `pnsmulFast base`, and the window value is folded in with `padd`. -/ +def phornerList (base : ℕ) (vals : List (PPoint F)) : PPoint F := + List.foldr (fun v acc => padd (pnsmulFast base acc) v) pid vals + +/-- The projective Horner fold is valid and matches `Fast.Msm.hornerList` of the `toAffine`-mapped +window values; each `base`-fold doubling transports via `pnsmulFast_spec`. -/ +theorem phornerList_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (base : ℕ) (vals : List (PPoint F)) (h : ∀ P ∈ vals, Valid P) : + Valid (phornerList base vals) + ∧ toAffine E hA hB (phornerList base vals) + = Msm.hornerList base (vals.map (toAffine E hA hB)) := by + induction vals with + | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList]⟩ + | cons v xs ih => + have hv : Valid v := h v (by simp) + have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) + obtain ⟨hvacc, heq⟩ := ih hxs + have hstep : phornerList base (v :: xs) + = padd (pnsmulFast base (phornerList base xs)) v := rfl + rw [hstep] + refine ⟨valid_padd hy0 htwo (pnsmulFast_spec E hA hB hy0 htwo hvacc base).1 hv, ?_⟩ + rw [toAffine_padd E hA hB hy0 htwo (pnsmulFast_spec E hA hB hy0 htwo hvacc base).1 hv, + (pnsmulFast_spec E hA hB hy0 htwo hvacc base).2, heq, List.map_cons] + simp only [Msm.hornerList, List.foldr_cons] + +/-! ## The projective Pippenger MSM and its equality to the affine accelerator -/ + +/-- **Windowed Pippenger MSM run in projective coordinates.** Each affine point is lifted via +`ofAffine`; the windowed algorithm (digits, buckets, suffix-sum, Horner doublings) runs over +`PPoint` with `padd`/`pnsmulFast`; a single `toAffine` (one field inversion) is taken at the end. -/ +def pippengerProj (c : ℕ) (terms : List (ℕ × SWPoint E)) : SWPoint E := + toAffine E hA hB (phornerList (2 ^ c) + ((List.range (Msm.numWindows c terms)).map fun i => + pwindowValue (2 ^ c) i (terms.map fun t => (t.1, ofAffine E t.2)))) + +/-- **The projective Pippenger equals the affine Pippenger.** Lifting by `ofAffine` and reading back +by `toAffine` is the identity on terms (`toAffine_ofAffine`); each window and the Horner fold commute +with `toAffine`, so the whole projective interior collapses to the affine `Fast.Msm.pippenger`. -/ +theorem pippengerProj_eq (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (c : ℕ) (terms : List (ℕ × SWPoint E)) : + pippengerProj E hA hB c terms = Msm.pippenger c terms := by + rw [pippengerProj] + set pterms := terms.map (fun t => (t.1, ofAffine E t.2)) with hpterms + set windows := (List.range (Msm.numWindows c terms)).map fun i => pwindowValue (2 ^ c) i pterms + with hwin + have hval : ∀ p ∈ pterms, Valid p.2 := by + intro p hp + rw [hpterms, List.mem_map] at hp + obtain ⟨t, _, rfl⟩ := hp + exact valid_ofAffine E hA hB t.2 + have hf : pterms.map (fun t => (t.1, toAffine E hA hB t.2)) = terms := by + rw [hpterms, List.map_map] + conv_rhs => rw [← List.map_id terms] + apply List.map_congr_left + intro t _ + simp only [Function.comp_apply, toAffine_ofAffine E hA hB, id_eq] + have hwval : ∀ P ∈ windows, Valid P := by + intro P hP + rw [hwin, List.mem_map] at hP + obtain ⟨i, _, rfl⟩ := hP + exact (pwindowValue_spec E hA hB hy0 htwo (2 ^ c) i pterms hval).1 + rw [(phornerList_spec E hA hB hy0 htwo (2 ^ c) windows hwval).2, Msm.pippenger] + congr 1 + rw [hwin, List.map_map] + apply List.map_congr_left + intro i _ + rw [Function.comp_apply, (pwindowValue_spec E hA hB hy0 htwo (2 ^ c) i pterms hval).2, hf] + +/-- **The projective Pippenger equals the naive MSM.** End-to-end correctness for `c ≥ 1`. -/ +theorem pippengerProj_eq_msm (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (c : ℕ) (hc : 0 < c) (terms : List (ℕ × SWPoint E)) : + pippengerProj E hA hB c terms = (terms.map fun t => t.1 • t.2).sum := by + rw [pippengerProj_eq E hA hB hy0 htwo, Msm.pippenger_eq_msm c hc] + +/-! ## Single-pass Array bucketing for the projective interior + +`pwindowValue`'s per-bucket `filterMap` dominates the group work at `base = 2 ^ 8`; `pbucketScatter` +builds all buckets in one pass. Its invariant cannot reuse `Msm.bucketScatter_toList` (that uses +`add_assoc`, and `padd` is not associative on the nose), so it too is transported through +`toAffine` (`foldl_pscatterStep_spec`). -/ + +/-- One projective scatter step: drop digit-`0` terms, otherwise `padd` the point into bucket +slot `d − 1` (slot `k` holds bucket `k + 1`). -/ +def pscatterStep (a : Array (PPoint F)) (p : ℕ × PPoint F) : Array (PPoint F) := + if p.1 = 0 then a else a.modify (p.1 - 1) (fun v => padd v p.2) + +/-- Scatter a digit-tagged projective point list into its `base − 1` buckets in one pass. -/ +def pbucketScatter (base : ℕ) (dp : List (ℕ × PPoint F)) : Array (PPoint F) := + dp.foldl pscatterStep (Array.replicate (base - 1) pid) + +omit [DecidableEq F] in +@[simp] theorem size_pscatterStep (a : Array (PPoint F)) (p : ℕ × PPoint F) : + (pscatterStep a p).size = a.size := by + unfold pscatterStep; split <;> simp + +omit [DecidableEq F] in +@[simp] theorem size_foldl_pscatterStep (dp : List (ℕ × PPoint F)) (a : Array (PPoint F)) : + (dp.foldl pscatterStep a).size = a.size := by + induction dp generalizing a with + | nil => rfl + | cons p dp ih => rw [List.foldl_cons, ih, size_pscatterStep] + +omit [DecidableEq F] in +/-- A single projective scatter step through `getElem?`: slot `k` gains a right-`padd` of `x` +exactly when the digit is `k + 1`. -/ +theorem getElem?_pscatterStep (a : Array (PPoint F)) (d : ℕ) (x : PPoint F) (k : ℕ) : + (pscatterStep a (d, x))[k]? + = if d = k + 1 then a[k]?.map (fun v => padd v x) else a[k]? := by + unfold pscatterStep + by_cases h0 : d = 0 + · subst h0 + rw [if_pos rfl, if_neg (by omega)] + · rw [if_neg h0, Array.getElem?_modify] + by_cases hdk : d = k + 1 + · rw [if_pos (by omega), if_pos hdk] + · rw [if_neg (by omega), if_neg hdk] + +/-- **The scatter fold invariant, transported through `toAffine`.** Starting from a valid slot +value `v`, slot `k` ends valid and reads — in `SWPoint E` — as `toAffine v` plus the affine bucket +sum of the processed digit-tagged list. -/ +private theorem foldl_pscatterStep_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (dp : List (ℕ × PPoint F)) (hdp : ∀ p ∈ dp, Valid p.2) : + ∀ (a : Array (PPoint F)) (k : ℕ) (v : PPoint F), a[k]? = some v → Valid v → + ∃ w, (dp.foldl pscatterStep a)[k]? = some w ∧ Valid w ∧ + toAffine E hA hB w = toAffine E hA hB v + + Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) (k + 1) := by + induction dp with + | nil => + intro a k v hv hval + exact ⟨v, hv, hval, by simp⟩ + | cons p dp ih => + intro a k v hv hval + obtain ⟨d, x⟩ := p + have hx : Valid x := hdp (d, x) (by simp) + have hdp' : ∀ q ∈ dp, Valid q.2 := fun q hq => hdp q (by simp [hq]) + rw [List.foldl_cons] + by_cases hdk : d = k + 1 + · have hv' : (pscatterStep a (d, x))[k]? = some (padd v x) := by + rw [getElem?_pscatterStep, if_pos hdk, hv, Option.map_some] + obtain ⟨w, hw, hwval, hweq⟩ := + ih hdp' (pscatterStep a (d, x)) k (padd v x) hv' (valid_padd hy0 htwo hval hx) + refine ⟨w, hw, hwval, ?_⟩ + rw [hweq, toAffine_padd E hA hB hy0 htwo hval hx, List.map_cons, Msm.bucketOf_cons, + if_pos hdk, _root_.add_assoc] + · have hv' : (pscatterStep a (d, x))[k]? = some v := by + rw [getElem?_pscatterStep, if_neg hdk, hv] + obtain ⟨w, hw, hwval, hweq⟩ := ih hdp' (pscatterStep a (d, x)) k v hv' hval + refine ⟨w, hw, hwval, ?_⟩ + rw [hweq, List.map_cons, Msm.bucketOf_cons, if_neg hdk, _root_.zero_add] + +/-- **The scattered buckets are the affine bucket list, slotwise.** Every slot is valid, and +`toAffine` maps the slot list to exactly the bucket list `Msm.windowValue` folds over. -/ +theorem pbucketScatter_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (base : ℕ) (dp : List (ℕ × PPoint F)) (hdp : ∀ p ∈ dp, Valid p.2) : + (∀ P ∈ (pbucketScatter base dp).toList, Valid P) + ∧ (pbucketScatter base dp).toList.map (toAffine E hA hB) + = (List.range (base - 1)).map fun k => + Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) (k + 1) := by + have hsize : (pbucketScatter base dp).size = base - 1 := by + rw [pbucketScatter, size_foldl_pscatterStep, Array.size_replicate] + have hslot : ∀ k, k < base - 1 → + ∃ w, (pbucketScatter base dp)[k]? = some w ∧ Valid w ∧ + toAffine E hA hB w = Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) (k + 1) := by + intro k hk + have hinit : (Array.replicate (base - 1) (pid : PPoint F))[k]? = some pid := by + rw [Array.getElem?_replicate, if_pos hk] + obtain ⟨w, hw, hwval, hweq⟩ := + foldl_pscatterStep_spec E hA hB hy0 htwo dp hdp (Array.replicate (base - 1) pid) k pid + hinit valid_pid + exact ⟨w, hw, hwval, by rw [hweq, toAffine_pid E hA hB, _root_.zero_add]⟩ + constructor + · intro P hP + obtain ⟨k, hk, hPk⟩ := List.mem_iff_getElem.mp hP + have hk' : k < base - 1 := by + rw [Array.length_toList, hsize] at hk + exact hk + obtain ⟨w, hw, hwval, -⟩ := hslot k hk' + have hPk? : (pbucketScatter base dp)[k]? = some P := by + rw [← Array.getElem?_toList, List.getElem?_eq_getElem hk, hPk] + rw [hPk?] at hw + obtain rfl : P = w := Option.some.inj hw + exact hwval + · apply List.ext_getElem? + intro k + rw [List.getElem?_map, List.getElem?_map, Array.getElem?_toList] + by_cases hk : k < base - 1 + · obtain ⟨w, hw, -, hweq⟩ := hslot k hk + rw [hw, List.getElem?_range hk, Option.map_some, Option.map_some, hweq] + · rw [Array.getElem?_eq_none (by rw [hsize]; omega), + List.getElem?_eq_none (by rw [List.length_range]; omega)] + rfl + +/-- The projective window value via the single-pass scatter (mirror of `Msm.windowValueFast`). -/ +def pwindowValueFast (base i : ℕ) (pterms : List (ℕ × PPoint F)) : PPoint F := + (List.foldr paccStep (pid, pid) (pbucketScatter base (pdpOf base i pterms)).toList).2 + +/-- The scatter-bucketed projective window value is valid and matches `Msm.windowValue` of the +`toAffine`-mapped terms — the scatter twin of `pwindowValue_spec`. -/ +theorem pwindowValueFast_spec (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (base i : ℕ) (pterms : List (ℕ × PPoint F)) (h : ∀ p ∈ pterms, Valid p.2) : + Valid (pwindowValueFast base i pterms) + ∧ toAffine E hA hB (pwindowValueFast base i pterms) + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine E hA hB t.2)) := by + have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by + intro p hp + rw [pdpOf, List.mem_map] at hp + obtain ⟨t, ht, rfl⟩ := hp + exact h t ht + obtain ⟨hbval, hbmap⟩ := pbucketScatter_spec E hA hB hy0 htwo base (pdpOf base i pterms) hdp + have hdpof : (pdpOf base i pterms).map (fun t => (t.1, toAffine E hA hB t.2)) + = Msm.dpOf base i (pterms.map fun t => (t.1, toAffine E hA hB t.2)) := by + simp only [pdpOf, Msm.dpOf, List.map_map, Function.comp_def] + rw [hdpof] at hbmap + obtain ⟨-, hv2, heq⟩ := foldr_paccStep_spec E hA hB hy0 htwo _ hbval + simp only [pwindowValueFast] + refine ⟨hv2, ?_⟩ + rw [Msm.windowValue, ← hbmap, ← heq] + +/-! ## The scatter-bucketed projective Pippenger MSM -/ + +/-- **Windowed Pippenger MSM in projective coordinates with single-pass Array bucketing** — the +fast serial form of `pippengerProj`. Proven equal to the affine `Msm.pippenger`. -/ +def pippengerProjScatter (c : ℕ) (terms : List (ℕ × SWPoint E)) : SWPoint E := + toAffine E hA hB (phornerList (2 ^ c) + ((List.range (Msm.numWindows c terms)).map fun i => + pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine E t.2)))) + +/-- **The scatter-bucketed projective Pippenger equals the affine Pippenger** — same transport as +`pippengerProj_eq`, window values via `pwindowValueFast_spec`. -/ +theorem pippengerProjScatter_eq (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (c : ℕ) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatter E hA hB c terms = Msm.pippenger c terms := by + rw [pippengerProjScatter] + set pterms := terms.map (fun t => (t.1, ofAffine E t.2)) with hpterms + set windows := (List.range (Msm.numWindows c terms)).map fun i => + pwindowValueFast (2 ^ c) i pterms + with hwin + have hval : ∀ p ∈ pterms, Valid p.2 := by + intro p hp + rw [hpterms, List.mem_map] at hp + obtain ⟨t, _, rfl⟩ := hp + exact valid_ofAffine E hA hB t.2 + have hf : pterms.map (fun t => (t.1, toAffine E hA hB t.2)) = terms := by + rw [hpterms, List.map_map] + conv_rhs => rw [← List.map_id terms] + apply List.map_congr_left + intro t _ + simp only [Function.comp_apply, toAffine_ofAffine E hA hB, id_eq] + have hwval : ∀ P ∈ windows, Valid P := by + intro P hP + rw [hwin, List.mem_map] at hP + obtain ⟨i, _, rfl⟩ := hP + exact (pwindowValueFast_spec E hA hB hy0 htwo (2 ^ c) i pterms hval).1 + rw [(phornerList_spec E hA hB hy0 htwo (2 ^ c) windows hwval).2, Msm.pippenger] + congr 1 + rw [hwin, List.map_map] + apply List.map_congr_left + intro i _ + rw [Function.comp_apply, (pwindowValueFast_spec E hA hB hy0 htwo (2 ^ c) i pterms hval).2, hf] + +/-- The scatter-bucketed projective Pippenger equals the naive MSM. -/ +theorem pippengerProjScatter_eq_msm (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (c : ℕ) (hc : 0 < c) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatter E hA hB c terms = (terms.map fun t => t.1 • t.2).sum := by + rw [pippengerProjScatter_eq E hA hB hy0 htwo, Msm.pippenger_eq_msm c hc] + +/-! ## Windows-parallel projective Pippenger -/ + +/-- **Windows-parallel scatter-bucketed projective Pippenger**: `pippengerProjScatter` with the +window values evaluated as parallel tasks (`Msm.parMap`). -/ +def pippengerProjScatterPar (c : ℕ) (terms : List (ℕ × SWPoint E)) : SWPoint E := + toAffine E hA hB (phornerList (2 ^ c) + (Msm.parMap (fun i => + pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine E t.2))) + (List.range (Msm.numWindows c terms)))) + +/-- The windows-parallel projective Pippenger is the sequential one: `parMap` is `map`. -/ +theorem pippengerProjScatterPar_eq (c : ℕ) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatterPar E hA hB c terms = pippengerProjScatter E hA hB c terms := by + rw [pippengerProjScatterPar, Msm.parMap_eq_map, pippengerProjScatter] + +/-- The windows-parallel projective Pippenger equals the naive MSM. -/ +theorem pippengerProjScatterPar_eq_msm (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (htwo : (2 : F) ≠ 0) + (c : ℕ) (hc : 0 < c) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatterPar E hA hB c terms = (terms.map fun t => t.1 • t.2).sum := by + rw [pippengerProjScatterPar_eq E hA hB c terms, pippengerProjScatter_eq_msm E hA hB hy0 htwo c hc] + +end CompElliptic.Curves.Pasta.Fast.MsmProj.Core From b1154827d6c37738dbad97230f7525fea19695ab Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 06:41:41 -0700 Subject: [PATCH 5/6] Fast/MsmProj: Vesta as an instantiation of the generic core MsmProj's projective-Pippenger decls delegate to MsmProj.Core at Vesta (commit_lagrange wrappers stay Vesta-local: coeffs in VestaScalarField). ProjectiveMontEquiv tracks the refactor: PVes.mk.injEq -> Core.PPoint.mk.injEq (from the Projective PVes abbrev) and Core.* names added to the scatter simp-normal-forms. Claude-Session: https://claude.ai/code/session_01Y4Wf3zPJYCwXzHDgdBUytv --- CompElliptic/Curves/Pasta/Fast/MsmProj.lean | 490 ++++-------------- .../Pasta/Fast/ProjectiveMontEquiv.lean | 6 +- 2 files changed, 106 insertions(+), 390 deletions(-) diff --git a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean index fd4f830..b3b9890 100644 --- a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean +++ b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean @@ -6,22 +6,23 @@ Authors: Gregor Mitscha-Baude -/ import CompElliptic.Curves.Pasta.Fast.Msm import CompElliptic.Curves.Pasta.Fast.Projective +import CompElliptic.Curves.Pasta.Fast.MsmProj.Core /-! -# The windowed Pippenger MSM run entirely in projective coordinates +# The windowed Pippenger MSM run entirely in projective coordinates (Vesta) -Instantiated at the Vesta affine group, every group addition of `Msm.lean` pays a field inversion. -This module runs the whole Pippenger interior over `Projective.PVes` with `padd`/`pnsmulFast` — -one inversion per MSM instead of one per add — and proves the result equal to the affine -accelerator (`pippengerProj_eq`, `pippengerProjScatter_eq`, and `..._eq_msm` to the naive MSM). +The Vesta instantiation of the field-generic `MsmProj.Core`: `PVes`/`Projective.G` at +`Vesta.curve`, with the basic, single-pass-scatter, and windows-parallel projective Pippenger +paths delegating to the core (fed Vesta's `no_onCurve_y_zero`/`2 ≠ 0` facts). Every group addition +of `Msm.lean` at the affine group pays a field inversion; this runs the whole interior over `PVes` +with `padd`/`pnsmulFast`, one inversion per MSM. -`PVes` is not a lawful monoid on the nose (associativity only holds after `toAffine`), so the -Pippenger equality is not re-run here: each fold of `Msm.lean` is mirrored by a `padd`/`pid` -version and shown to commute with `toAffine`, carrying `Valid` through every intermediate -(`psum_spec`, `pbucketOf_spec`, `foldr_paccStep_spec`, `pwindowValue_spec`, `phornerList_spec`). +The `commit_lagrange` wrappers stay here: their coefficients live in `Msm.Fp = VestaScalarField`, +so they are Vesta-specific; they delegate to the (now core-backed) `pippengerProj` / +`pippengerProjScatter`. -The `Fast` interfaces are provisional: they are not guaranteed to remain public, and -may be folded into the existing API or otherwise changed incompatibly. +The `Fast` interfaces are provisional: they are not guaranteed to remain public, and may be folded +into the existing API or otherwise changed incompatibly. -/ open CompElliptic.Curves.Pasta.Fast @@ -34,416 +35,134 @@ open CompElliptic.Curves.Pasta namespace CompElliptic.Curves.Pasta.Fast.MsmProj -/-- The Vesta affine group carries a default point, needed to instantiate the `Fast.Msm` wrapper -(`commitLagrangeSpec`, `commitLagrangeFastWith_eq`) whose section fixes `[Inhabited G]`. -/ +/-- The Vesta affine group carries a default point (the `Fast.Msm` wrapper section fixes +`[Inhabited G]`). -/ local instance : Inhabited Projective.G := ⟨0⟩ -/-! ## Projective bucket sum (`foldr padd pid`), mirroring `Fast.Msm.bucketOf` -/ +/-! ## Basic path — the Vesta instantiation of `MsmProj.Core` -/ -/-- The `padd`-fold sum of a list of projective points, from the projective identity `pid`. -/ -def psum (L : List PVes) : PVes := L.foldr padd pid +/-- The `padd`-fold sum of a list of projective points (Vesta instance of `Core.psum`). -/ +abbrev psum : List PVes → PVes := Core.psum (F := Fq) -theorem psum_cons (a : PVes) (xs : List PVes) : psum (a :: xs) = padd a (psum xs) := rfl +theorem psum_cons (a : PVes) (xs : List PVes) : psum (a :: xs) = padd a (psum xs) := + Core.psum_cons (F := Fq) a xs -/-- A projective `padd`-sum of valid points is valid, and `toAffine` carries it to the affine sum. -/ theorem psum_spec (L : List PVes) (h : ∀ P ∈ L, Valid P) : - Valid (psum L) ∧ toAffine (psum L) = (L.map toAffine).sum := by - induction L with - | nil => exact ⟨valid_pid, by simp [psum]⟩ - | cons a xs ih => - have ha : Valid a := h a (by simp) - have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) - obtain ⟨hvxs, hxseq⟩ := ih hxs - rw [psum_cons] - exact ⟨valid_padd ha hvxs, by rw [toAffine_padd ha hvxs, hxseq, List.map_cons, List.sum_cons]⟩ - -/-- The projective bucket-`b` sum: `padd`-fold the points whose digit tag is `b`. -/ -def pbucketOf (dp : List (ℕ × PVes)) (b : ℕ) : PVes := - psum (dp.filterMap fun p => if p.1 = b then some p.2 else none) - -/-- The projective bucket sum is valid and matches `Fast.Msm.bucketOf` of the `toAffine`-mapped -digit-tagged list. -/ + Valid (psum L) ∧ toAffine (psum L) = (L.map toAffine).sum := + Core.psum_spec Vesta.curve hA hB hy0 htwo L h + +/-- The projective bucket-`b` sum (Vesta instance of `Core.pbucketOf`). -/ +abbrev pbucketOf : List (ℕ × PVes) → ℕ → PVes := Core.pbucketOf (F := Fq) + theorem pbucketOf_spec (dp : List (ℕ × PVes)) (b : ℕ) (h : ∀ p ∈ dp, Valid p.2) : Valid (pbucketOf dp b) - ∧ toAffine (pbucketOf dp b) - = Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) b := by - have hval : ∀ P ∈ dp.filterMap (fun p => if p.1 = b then some p.2 else none), Valid P := by - intro P hP - rw [List.mem_filterMap] at hP - obtain ⟨q, hq, hqeq⟩ := hP - by_cases hc : q.1 = b - · rw [if_pos hc, Option.some.injEq] at hqeq; rw [← hqeq]; exact h q hq - · rw [if_neg hc] at hqeq; exact absurd hqeq (by simp) - obtain ⟨hv, heq⟩ := psum_spec _ hval - refine ⟨hv, ?_⟩ - rw [pbucketOf, heq, Msm.bucketOf, List.filterMap_map, List.map_filterMap] - refine congrArg List.sum (congrArg (dp.filterMap ·) ?_) - funext p - by_cases hc : p.1 = b <;> simp [hc, Function.comp] - -/-! ## Projective suffix-sum accumulator, mirroring `Fast.Msm.accStep` -/ - -/-- One step of the projective suffix-sum accumulator: carry `(running, total)`, `padd` the next -bucket into `running`, then `padd` `running` into `total`. -/ -def paccStep (a : PVes) (p : PVes × PVes) : PVes × PVes := - (padd p.1 a, padd p.2 (padd p.1 a)) - -/-- Folding `paccStep` over valid points keeps both accumulator components valid, and `toAffine` -carries the whole fold (componentwise) to the affine `Fast.Msm.accStep` fold. -/ + ∧ toAffine (pbucketOf dp b) = Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) b := + Core.pbucketOf_spec Vesta.curve hA hB hy0 htwo dp b h + +/-- One step of the projective suffix-sum accumulator (Vesta instance of `Core.paccStep`). -/ +abbrev paccStep : PVes → PVes × PVes → PVes × PVes := Core.paccStep (F := Fq) + theorem foldr_paccStep_spec (L : List PVes) (h : ∀ P ∈ L, Valid P) : Valid (L.foldr paccStep (pid, pid)).1 ∧ Valid (L.foldr paccStep (pid, pid)).2 ∧ (toAffine (L.foldr paccStep (pid, pid)).1, toAffine (L.foldr paccStep (pid, pid)).2) - = List.foldr Msm.accStep ((0 : Projective.G), (0 : Projective.G)) (L.map toAffine) := by - induction L with - | nil => exact ⟨valid_pid, valid_pid, by simp⟩ - | cons a xs ih => - have ha : Valid a := h a (by simp) - have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) - obtain ⟨hv1, hv2, heq⟩ := ih hxs - have hstep : (a :: xs).foldr paccStep (pid, pid) = paccStep a (xs.foldr paccStep (pid, pid)) := - rfl - rw [hstep] - have hv1' : Valid (padd (xs.foldr paccStep (pid, pid)).1 a) := valid_padd hv1 ha - refine ⟨hv1', valid_padd hv2 hv1', ?_⟩ - rw [List.map_cons, List.foldr_cons, ← heq, Msm.accStep] - simp only [paccStep, toAffine_padd hv1 ha, toAffine_padd hv2 hv1'] - -/-! ## Projective window value, mirroring `Fast.Msm.windowValue` -/ - -/-- The digit-tagged projective term list for window `i`. -/ -def pdpOf (base i : ℕ) (pterms : List (ℕ × PVes)) : List (ℕ × PVes) := - pterms.map fun t => (Msm.digit base i t.1, t.2) - -/-- The projective window value: build the `base − 1` projective buckets, then run the projective -suffix-sum accumulation. -/ -def pwindowValue (base i : ℕ) (pterms : List (ℕ × PVes)) : PVes := - (List.foldr paccStep (pid, pid) - ((List.range (base - 1)).map fun k => pbucketOf (pdpOf base i pterms) (k + 1))).2 - -/-- The projective window value is valid and matches `Fast.Msm.windowValue` of the `toAffine`-mapped -terms. -/ -theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes)) - (h : ∀ p ∈ pterms, Valid p.2) : + = List.foldr Msm.accStep ((0 : Projective.G), (0 : Projective.G)) (L.map toAffine) := + Core.foldr_paccStep_spec Vesta.curve hA hB hy0 htwo L h + +/-- The digit-tagged projective term list for window `i` (Vesta instance of `Core.pdpOf`). -/ +abbrev pdpOf : ℕ → ℕ → List (ℕ × PVes) → List (ℕ × PVes) := Core.pdpOf (F := Fq) + +/-- The projective window value (Vesta instance of `Core.pwindowValue`). -/ +abbrev pwindowValue : ℕ → ℕ → List (ℕ × PVes) → PVes := Core.pwindowValue (F := Fq) + +theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes)) (h : ∀ p ∈ pterms, Valid p.2) : Valid (pwindowValue base i pterms) ∧ toAffine (pwindowValue base i pterms) - = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine t.2)) := by - have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by - intro p hp - rw [pdpOf, List.mem_map] at hp - obtain ⟨t, ht, rfl⟩ := hp - exact h t ht - simp only [pwindowValue] - set buckets := (List.range (base - 1)).map fun k => pbucketOf (pdpOf base i pterms) (k + 1) - with hbuck - have hbval : ∀ P ∈ buckets, Valid P := by - intro P hP - rw [hbuck, List.mem_map] at hP - obtain ⟨k, _, rfl⟩ := hP - exact (pbucketOf_spec _ _ hdp).1 - obtain ⟨_, hv2, heq⟩ := foldr_paccStep_spec buckets hbval - refine ⟨hv2, ?_⟩ - have hmap : buckets.map toAffine - = (List.range (base - 1)).map fun k => - Msm.bucketOf (Msm.dpOf base i (pterms.map fun t => (t.1, toAffine t.2))) (k + 1) := by - rw [hbuck, List.map_map] - apply List.map_congr_left - intro k _ - rw [Function.comp_apply, (pbucketOf_spec _ _ hdp).2] - congr 1 - simp only [pdpOf, Msm.dpOf, List.map_map, Function.comp_def] - rw [Msm.windowValue, ← hmap, ← heq] - -/-! ## Projective Horner fold, mirroring `Fast.Msm.hornerList` -/ - -/-- Horner across windows in projective coordinates: each `base •` doubling is the fast binary -scalar multiplication `pnsmulFast base`, and the window value is folded in with `padd`. -/ -def phornerList (base : ℕ) (vals : List PVes) : PVes := - List.foldr (fun v acc => padd (pnsmulFast base acc) v) pid vals - -/-- The projective Horner fold is valid and matches `Fast.Msm.hornerList` of the `toAffine`-mapped -window values; each `2^c`-fold doubling transports via `pnsmulFast_spec`. -/ + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine t.2)) := + Core.pwindowValue_spec Vesta.curve hA hB hy0 htwo base i pterms h + +/-- Horner across windows in projective coordinates (Vesta instance of `Core.phornerList`). -/ +abbrev phornerList : ℕ → List PVes → PVes := Core.phornerList (F := Fq) + theorem phornerList_spec (base : ℕ) (vals : List PVes) (h : ∀ P ∈ vals, Valid P) : Valid (phornerList base vals) - ∧ toAffine (phornerList base vals) = Msm.hornerList base (vals.map toAffine) := by - induction vals with - | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList]⟩ - | cons v xs ih => - have hv : Valid v := h v (by simp) - have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) - obtain ⟨hvacc, heq⟩ := ih hxs - have hstep : phornerList base (v :: xs) - = padd (pnsmulFast base (phornerList base xs)) v := rfl - rw [hstep] - refine ⟨valid_padd (pnsmulFast_spec hvacc base).1 hv, ?_⟩ - rw [toAffine_padd (pnsmulFast_spec hvacc base).1 hv, (pnsmulFast_spec hvacc base).2, heq, - List.map_cons] - simp only [Msm.hornerList, List.foldr_cons] - -/-! ## The projective Pippenger MSM and its equality to the affine accelerator -/ - -/-- **Windowed Pippenger MSM run in projective coordinates.** Each affine point is lifted via -`ofAffine`; the same windowed algorithm (digits, buckets, suffix-sum, Horner doublings) runs over -`PVes` with `padd`/`pnsmulFast`; a single `toAffine` (one field inversion) is taken at the end. -Proven equal to the affine `Fast.Msm.pippenger` (`pippengerProj_eq`). -/ -def pippengerProj (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine (phornerList (2 ^ c) - ((List.range (Msm.numWindows c terms)).map fun i => - pwindowValue (2 ^ c) i (terms.map fun t => (t.1, ofAffine t.2)))) - -/-- **The projective Pippenger equals the affine Pippenger.** Lifting by `ofAffine` and reading back -by `toAffine` is the identity on terms (`toAffine_ofAffine`); each window and the Horner fold commute -with `toAffine` (`pwindowValue_spec`, `phornerList_spec`), so the whole projective interior collapses -to the affine `Fast.Msm.pippenger`. -/ + ∧ toAffine (phornerList base vals) = Msm.hornerList base (vals.map toAffine) := + Core.phornerList_spec Vesta.curve hA hB hy0 htwo base vals h + +/-! ## The projective Pippenger MSM -/ + +/-- **Windowed Pippenger MSM run in projective coordinates** (Vesta instance of +`Core.pippengerProj`): one field inversion per MSM instead of one per add. -/ +abbrev pippengerProj : ℕ → List (ℕ × Projective.G) → Projective.G := + Core.pippengerProj Vesta.curve hA hB + theorem pippengerProj_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : - pippengerProj c terms = Msm.pippenger c terms := by - rw [pippengerProj] - set pterms := terms.map (fun t => (t.1, ofAffine t.2)) with hpterms - set windows := (List.range (Msm.numWindows c terms)).map fun i => pwindowValue (2 ^ c) i pterms - with hwin - have hval : ∀ p ∈ pterms, Valid p.2 := by - intro p hp - rw [hpterms, List.mem_map] at hp - obtain ⟨t, _, rfl⟩ := hp - exact valid_ofAffine t.2 - have hf : pterms.map (fun t => (t.1, toAffine t.2)) = terms := by - rw [hpterms, List.map_map] - conv_rhs => rw [← List.map_id terms] - apply List.map_congr_left - intro t _ - simp only [Function.comp_apply, toAffine_ofAffine, id_eq] - have hwval : ∀ P ∈ windows, Valid P := by - intro P hP - rw [hwin, List.mem_map] at hP - obtain ⟨i, _, rfl⟩ := hP - exact (pwindowValue_spec (2 ^ c) i pterms hval).1 - rw [(phornerList_spec (2 ^ c) windows hwval).2, Msm.pippenger] - congr 1 - rw [hwin, List.map_map] - apply List.map_congr_left - intro i _ - rw [Function.comp_apply, (pwindowValue_spec (2 ^ c) i pterms hval).2, hf] - -/-- **The projective Pippenger equals the naive MSM.** End-to-end correctness for `c ≥ 1`. -/ + pippengerProj c terms = Msm.pippenger c terms := + Core.pippengerProj_eq Vesta.curve hA hB hy0 htwo c terms + +/-- **The projective Pippenger equals the naive MSM.** -/ theorem pippengerProj_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × Projective.G)) : - pippengerProj c terms = (terms.map fun t => t.1 • t.2).sum := by - rw [pippengerProj_eq, Msm.pippenger_eq_msm c hc] - -/-! ## Single-pass Array bucketing for the projective interior - -`pwindowValue`'s per-bucket `filterMap` dominates the group work at `base = 2 ^ 8` (~5× slower -than the scatter below). `pbucketScatter` builds all buckets in one pass; its invariant cannot -reuse `Msm.bucketScatter_toList` (that one uses `add_assoc`, and `padd` is not associative on the -nose), so it too is transported through `toAffine` (`foldl_pscatterStep_spec`). -/ - -/-- One projective scatter step: drop digit-`0` terms, otherwise `padd` the point into bucket -slot `d − 1` (slot `k` holds bucket `k + 1`). -/ -def pscatterStep (a : Array PVes) (p : ℕ × PVes) : Array PVes := - if p.1 = 0 then a else a.modify (p.1 - 1) (fun v => padd v p.2) - -/-- Scatter a digit-tagged projective point list into its `base − 1` buckets in one pass. -/ -def pbucketScatter (base : ℕ) (dp : List (ℕ × PVes)) : Array PVes := - dp.foldl pscatterStep (Array.replicate (base - 1) pid) - -@[simp] theorem size_pscatterStep (a : Array PVes) (p : ℕ × PVes) : - (pscatterStep a p).size = a.size := by - unfold pscatterStep; split <;> simp - -@[simp] theorem size_foldl_pscatterStep (dp : List (ℕ × PVes)) (a : Array PVes) : - (dp.foldl pscatterStep a).size = a.size := by - induction dp generalizing a with - | nil => rfl - | cons p dp ih => rw [List.foldl_cons, ih, size_pscatterStep] - -/-- A single projective scatter step through `getElem?`: slot `k` gains a right-`padd` of `x` -exactly when the digit is `k + 1`. -/ -theorem getElem?_pscatterStep (a : Array PVes) (d : ℕ) (x : PVes) (k : ℕ) : - (pscatterStep a (d, x))[k]? - = if d = k + 1 then a[k]?.map (fun v => padd v x) else a[k]? := by - unfold pscatterStep - by_cases h0 : d = 0 - · subst h0 - rw [if_pos rfl, if_neg (by omega)] - · rw [if_neg h0, Array.getElem?_modify] - by_cases hdk : d = k + 1 - · rw [if_pos (by omega), if_pos hdk] - · rw [if_neg (by omega), if_neg hdk] - -/-- **The scatter fold invariant, transported through `toAffine`.** Starting from a valid slot -value `v`, slot `k` ends valid and reads — in `G` — as `toAffine v` plus the affine bucket sum -of the processed digit-tagged list. -/ -private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes)) (hdp : ∀ p ∈ dp, Valid p.2) : - ∀ (a : Array PVes) (k : ℕ) (v : PVes), a[k]? = some v → Valid v → - ∃ w, (dp.foldl pscatterStep a)[k]? = some w ∧ Valid w ∧ - toAffine w = toAffine v - + Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := by - induction dp with - | nil => - intro a k v hv hval - exact ⟨v, hv, hval, by simp⟩ - | cons p dp ih => - intro a k v hv hval - obtain ⟨d, x⟩ := p - have hx : Valid x := hdp (d, x) (by simp) - have hdp' : ∀ q ∈ dp, Valid q.2 := fun q hq => hdp q (by simp [hq]) - rw [List.foldl_cons] - by_cases hdk : d = k + 1 - · have hv' : (pscatterStep a (d, x))[k]? = some (padd v x) := by - rw [getElem?_pscatterStep, if_pos hdk, hv, Option.map_some] - obtain ⟨w, hw, hwval, hweq⟩ := - ih hdp' (pscatterStep a (d, x)) k (padd v x) hv' (valid_padd hval hx) - refine ⟨w, hw, hwval, ?_⟩ - rw [hweq, toAffine_padd hval hx, List.map_cons, Msm.bucketOf_cons, if_pos hdk, _root_.add_assoc] - · have hv' : (pscatterStep a (d, x))[k]? = some v := by - rw [getElem?_pscatterStep, if_neg hdk, hv] - obtain ⟨w, hw, hwval, hweq⟩ := ih hdp' (pscatterStep a (d, x)) k v hv' hval - refine ⟨w, hw, hwval, ?_⟩ - rw [hweq, List.map_cons, Msm.bucketOf_cons, if_neg hdk, _root_.zero_add] - -/-- **The scattered buckets are the affine bucket list, slotwise.** Every slot is valid, and -`toAffine` maps the slot list to exactly the bucket list `Msm.windowValue` folds over. -/ + pippengerProj c terms = (terms.map fun t => t.1 • t.2).sum := + Core.pippengerProj_eq_msm Vesta.curve hA hB hy0 htwo c hc terms + +/-! ## Single-pass Array bucketing -/ + +/-- One projective scatter step (Vesta instance of `Core.pscatterStep`). -/ +abbrev pscatterStep : Array PVes → ℕ × PVes → Array PVes := Core.pscatterStep (F := Fq) + +/-- Scatter into `base − 1` buckets in one pass (Vesta instance of `Core.pbucketScatter`). -/ +abbrev pbucketScatter : ℕ → List (ℕ × PVes) → Array PVes := Core.pbucketScatter (F := Fq) + theorem pbucketScatter_spec (base : ℕ) (dp : List (ℕ × PVes)) (hdp : ∀ p ∈ dp, Valid p.2) : (∀ P ∈ (pbucketScatter base dp).toList, Valid P) ∧ (pbucketScatter base dp).toList.map toAffine = (List.range (base - 1)).map fun k => - Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := by - have hsize : (pbucketScatter base dp).size = base - 1 := by - rw [pbucketScatter, size_foldl_pscatterStep, Array.size_replicate] - have hslot : ∀ k, k < base - 1 → - ∃ w, (pbucketScatter base dp)[k]? = some w ∧ Valid w ∧ - toAffine w = Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := by - intro k hk - have hinit : (Array.replicate (base - 1) pid)[k]? = some pid := by - rw [Array.getElem?_replicate, if_pos hk] - obtain ⟨w, hw, hwval, hweq⟩ := - foldl_pscatterStep_spec dp hdp (Array.replicate (base - 1) pid) k pid hinit valid_pid - exact ⟨w, hw, hwval, by rw [hweq, toAffine_pid, _root_.zero_add]⟩ - constructor - · intro P hP - obtain ⟨k, hk, hPk⟩ := List.mem_iff_getElem.mp hP - have hk' : k < base - 1 := by - rw [Array.length_toList, hsize] at hk - exact hk - obtain ⟨w, hw, hwval, -⟩ := hslot k hk' - have hPk? : (pbucketScatter base dp)[k]? = some P := by - rw [← Array.getElem?_toList, List.getElem?_eq_getElem hk, hPk] - rw [hPk?] at hw - obtain rfl : P = w := Option.some.inj hw - exact hwval - · apply List.ext_getElem? - intro k - rw [List.getElem?_map, List.getElem?_map, Array.getElem?_toList] - by_cases hk : k < base - 1 - · obtain ⟨w, hw, -, hweq⟩ := hslot k hk - rw [hw, List.getElem?_range hk, Option.map_some, Option.map_some, hweq] - · rw [Array.getElem?_eq_none (by rw [hsize]; omega), - List.getElem?_eq_none (by rw [List.length_range]; omega)] - rfl - -/-- The projective window value via the single-pass scatter (mirror of -`Msm.windowValueFast`). -/ -def pwindowValueFast (base i : ℕ) (pterms : List (ℕ × PVes)) : PVes := - (List.foldr paccStep (pid, pid) (pbucketScatter base (pdpOf base i pterms)).toList).2 - -/-- The scatter-bucketed projective window value is valid and matches `Msm.windowValue` of the -`toAffine`-mapped terms — the scatter twin of `pwindowValue_spec`. -/ + Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := + Core.pbucketScatter_spec Vesta.curve hA hB hy0 htwo base dp hdp + +/-- The scatter-bucketed projective window value (Vesta instance of `Core.pwindowValueFast`). -/ +abbrev pwindowValueFast : ℕ → ℕ → List (ℕ × PVes) → PVes := Core.pwindowValueFast (F := Fq) + theorem pwindowValueFast_spec (base i : ℕ) (pterms : List (ℕ × PVes)) (h : ∀ p ∈ pterms, Valid p.2) : Valid (pwindowValueFast base i pterms) ∧ toAffine (pwindowValueFast base i pterms) - = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine t.2)) := by - have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by - intro p hp - rw [pdpOf, List.mem_map] at hp - obtain ⟨t, ht, rfl⟩ := hp - exact h t ht - obtain ⟨hbval, hbmap⟩ := pbucketScatter_spec base (pdpOf base i pterms) hdp - have hdpof : (pdpOf base i pterms).map (fun t => (t.1, toAffine t.2)) - = Msm.dpOf base i (pterms.map fun t => (t.1, toAffine t.2)) := by - simp only [pdpOf, Msm.dpOf, List.map_map, Function.comp_def] - rw [hdpof] at hbmap - obtain ⟨-, hv2, heq⟩ := foldr_paccStep_spec _ hbval - simp only [pwindowValueFast] - refine ⟨hv2, ?_⟩ - rw [Msm.windowValue, ← hbmap, ← heq] + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine t.2)) := + Core.pwindowValueFast_spec Vesta.curve hA hB hy0 htwo base i pterms h /-! ## The scatter-bucketed projective Pippenger MSM -/ -/-- **Windowed Pippenger MSM in projective coordinates with single-pass Array bucketing** — -the fast serial form of `pippengerProj`. Proven equal to the affine `Msm.pippenger` -(`pippengerProjScatter_eq`). -/ -def pippengerProjScatter (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine (phornerList (2 ^ c) - ((List.range (Msm.numWindows c terms)).map fun i => - pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine t.2)))) +/-- **Scatter-bucketed projective Pippenger** (Vesta instance of `Core.pippengerProjScatter`). -/ +abbrev pippengerProjScatter : ℕ → List (ℕ × Projective.G) → Projective.G := + Core.pippengerProjScatter Vesta.curve hA hB -/-- **The scatter-bucketed projective Pippenger equals the affine Pippenger** — same transport -as `pippengerProj_eq`, window values via `pwindowValueFast_spec`. -/ theorem pippengerProjScatter_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : - pippengerProjScatter c terms = Msm.pippenger c terms := by - rw [pippengerProjScatter] - set pterms := terms.map (fun t => (t.1, ofAffine t.2)) with hpterms - set windows := (List.range (Msm.numWindows c terms)).map fun i => - pwindowValueFast (2 ^ c) i pterms - with hwin - have hval : ∀ p ∈ pterms, Valid p.2 := by - intro p hp - rw [hpterms, List.mem_map] at hp - obtain ⟨t, _, rfl⟩ := hp - exact valid_ofAffine t.2 - have hf : pterms.map (fun t => (t.1, toAffine t.2)) = terms := by - rw [hpterms, List.map_map] - conv_rhs => rw [← List.map_id terms] - apply List.map_congr_left - intro t _ - simp only [Function.comp_apply, toAffine_ofAffine, id_eq] - have hwval : ∀ P ∈ windows, Valid P := by - intro P hP - rw [hwin, List.mem_map] at hP - obtain ⟨i, _, rfl⟩ := hP - exact (pwindowValueFast_spec (2 ^ c) i pterms hval).1 - rw [(phornerList_spec (2 ^ c) windows hwval).2, Msm.pippenger] - congr 1 - rw [hwin, List.map_map] - apply List.map_congr_left - intro i _ - rw [Function.comp_apply, (pwindowValueFast_spec (2 ^ c) i pterms hval).2, hf] - -/-- The scatter-bucketed projective Pippenger equals the naive MSM. -/ -theorem pippengerProjScatter_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × Projective.G)) : - pippengerProjScatter c terms = (terms.map fun t => t.1 • t.2).sum := by - rw [pippengerProjScatter_eq, Msm.pippenger_eq_msm c hc] + pippengerProjScatter c terms = Msm.pippenger c terms := + Core.pippengerProjScatter_eq Vesta.curve hA hB hy0 htwo c terms -/-! ## Windows-parallel projective Pippenger +theorem pippengerProjScatter_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × Projective.G)) : + pippengerProjScatter c terms = (terms.map fun t => t.1 • t.2).sum := + Core.pippengerProjScatter_eq_msm Vesta.curve hA hB hy0 htwo c hc terms -The window values are mutually independent; evaluating them through the proven `Msm.parMap` -changes only the evaluation strategy, so the equality is purely `Msm.parMap_eq_map`. Measured -(interpreted, `n = 2048`, `c = 8`, 12 cores): `4.3 s → 0.8 s` per MSM on top of the scatter -port. -/ +/-! ## Windows-parallel projective Pippenger -/ -/-- **Windows-parallel scatter-bucketed projective Pippenger**: `pippengerProjScatter` with the -window values evaluated as parallel tasks. -/ -def pippengerProjScatterPar (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine (phornerList (2 ^ c) - (Msm.parMap (fun i => - pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine t.2))) - (List.range (Msm.numWindows c terms)))) +/-- **Windows-parallel scatter-bucketed projective Pippenger** (Vesta instance of +`Core.pippengerProjScatterPar`). -/ +abbrev pippengerProjScatterPar : ℕ → List (ℕ × Projective.G) → Projective.G := + Core.pippengerProjScatterPar Vesta.curve hA hB -/-- The windows-parallel projective Pippenger is the sequential one: `parMap` is `map`. -/ theorem pippengerProjScatterPar_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : - pippengerProjScatterPar c terms = pippengerProjScatter c terms := by - rw [pippengerProjScatterPar, Msm.parMap_eq_map, pippengerProjScatter] + pippengerProjScatterPar c terms = pippengerProjScatter c terms := + Core.pippengerProjScatterPar_eq Vesta.curve hA hB c terms -/-- The windows-parallel projective Pippenger equals the naive MSM. -/ theorem pippengerProjScatterPar_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × Projective.G)) : - pippengerProjScatterPar c terms = (terms.map fun t => t.1 • t.2).sum := by - rw [pippengerProjScatterPar_eq, pippengerProjScatter_eq_msm c hc] + pippengerProjScatterPar c terms = (terms.map fun t => t.1 • t.2).sum := + Core.pippengerProjScatterPar_eq_msm Vesta.curve hA hB hy0 htwo c hc terms -/-! ## The `commit_lagrange` wrapper -/ +/-! ## The `commit_lagrange` wrapper (Vesta-specific: coeffs in `Msm.Fp = VestaScalarField`) -/ -/-- The fast `commit_lagrange` run in projective coordinates: projective windowed Pippenger over the -`(coeffᵢ.val, basisᵢ)` terms (single final inversion), plus the blind. The terms are zipped -identically to `Fast.Msm.commitLagrangeFastWith` so the wrapper equality reuses `zip_terms_eq`. -/ +/-- The fast `commit_lagrange` in projective coordinates: projective windowed Pippenger over the +`(coeffᵢ.val, basisᵢ)` terms (single final inversion), plus the blind. -/ def commitLagrangeProjWith (c : ℕ) (blind : Projective.G) (basis : List Projective.G) (coeffs : List Fp) : Projective.G := pippengerProj c @@ -451,7 +170,7 @@ def commitLagrangeProjWith (c : ℕ) (blind : Projective.G) (basis : List Projec fun t => (t.1.val, t.2)) + blind /-- **The projective commitment equals the naive `commit_lagrange` spec** -(`Fast.Msm.commitLagrangeSpec`, verbatim from `Keygen.commitLagrangeWith`). -/ +(`Fast.Msm.commitLagrangeSpec`). -/ theorem commitLagrangeProjWith_eq (c : ℕ) (hc : 0 < c) (blind : Projective.G) (basis : List Projective.G) (coeffs : List Fp) : commitLagrangeProjWith c blind basis coeffs = Msm.commitLagrangeSpec blind basis coeffs := by @@ -459,17 +178,14 @@ theorem commitLagrangeProjWith_eq (c : ℕ) (hc : 0 < c) rw [pippengerProj_eq, Msm.zip_terms_eq, Msm.pippenger_eq_msm c hc, List.map_map] rfl -/-- The fast `commit_lagrange` with scatter-bucketed projective Pippenger — the drop-in -committer for the certificate's per-column pass (serial per column; the 44-column outer -`parMap` already saturates the cores). -/ +/-- The fast `commit_lagrange` with scatter-bucketed projective Pippenger. -/ def commitLagrangeProjScatterWith (c : ℕ) (blind : Projective.G) (basis : List Projective.G) (coeffs : List Fp) : Projective.G := pippengerProjScatter c ((coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map fun t => (t.1.val, t.2)) + blind -/-- **The scatter-bucketed projective commitment equals the naive `commit_lagrange` spec** -(`Fast.Msm.commitLagrangeSpec`). -/ +/-- **The scatter-bucketed projective commitment equals the naive `commit_lagrange` spec**. -/ theorem commitLagrangeProjScatterWith_eq (c : ℕ) (hc : 0 < c) (blind : Projective.G) (basis : List Projective.G) (coeffs : List Fp) : commitLagrangeProjScatterWith c blind basis coeffs diff --git a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean index c15f4ac..f2028bc 100644 --- a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean +++ b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean @@ -472,7 +472,7 @@ instead of `pnsmulFast (2 ^ c)`), so it goes through `toGM` directly, and private theorem RA_scatterStep {a : Array PM} {b : Array PVes} (h : RA a b) {t : ℕ × PM} (ht : WFP t.2) : RA (PM.scatterStep a t) (MsmProj.pscatterStep b (t.1, toPVesM t.2)) := by - simp only [PM.scatterStep, MsmProj.pscatterStep] + simp only [PM.scatterStep, MsmProj.pscatterStep, MsmProj.Core.pscatterStep] by_cases h0 : t.1 = 0 · rw [if_pos h0, if_pos h0] exact h @@ -482,7 +482,7 @@ private theorem RA_scatterStep {a : Array PM} {b : Array PVes} (h : RA a b) {t : private theorem RA_bucketScatter (base : ℕ) (dp : List (ℕ × PM)) (h : ∀ t ∈ dp, WFP t.2) : RA (PM.bucketScatter base dp) (MsmProj.pbucketScatter base (dp.map fun t => (t.1, toPVesM t.2))) := by - simp only [PM.bucketScatter, MsmProj.pbucketScatter, List.foldl_map] + simp only [PM.bucketScatter, MsmProj.pbucketScatter, MsmProj.Core.pbucketScatter, List.foldl_map] refine foldl_rel₂ RA (fun t : ℕ × PM => WFP t.2) dp _ _ (fun s s' x hx hs => RA_scatterStep (t := x) hs hx) h _ _ ?_ simp only [RA, Array.toList_replicate] @@ -512,7 +512,7 @@ private theorem RM_windowValue (base i : ℕ) (terms : List (ℕ × PM)) have halign : (terms.map fun t : ℕ × PM => (t.1 / base ^ i % base, t.2)).map (fun t : ℕ × PM => (t.1, toPVesM t.2)) = MsmProj.pdpOf base i (terms.map fun t : ℕ × PM => (t.1, toPVesM t.2)) := by - simp only [MsmProj.pdpOf, Msm.digit, List.map_map, Function.comp_def] + simp only [MsmProj.pdpOf, MsmProj.Core.pdpOf, Msm.digit, List.map_map, Function.comp_def] rw [halign] at hb exact (RM2_foldr_accStep hb).2 From 4ca6b7149f7fa0b94efd350703f4e58915c27423 Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 06:41:50 -0700 Subject: [PATCH 6/6] Fast/MsmProjPallas: Pallas projective Pippenger MSM The Pallas instantiation of MsmProj.Core: basic, scatter, and parallel pippengerProj variants, each proven equal to the naive MSM. This is the fast Pallas MSM the snarky verifier's 2^15-point sg-check needs. Claude-Session: https://claude.ai/code/session_01Y4Wf3zPJYCwXzHDgdBUytv --- .../Curves/Pasta/Fast/MsmProjPallas.lean | 109 ++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 CompElliptic/Curves/Pasta/Fast/MsmProjPallas.lean diff --git a/CompElliptic/Curves/Pasta/Fast/MsmProjPallas.lean b/CompElliptic/Curves/Pasta/Fast/MsmProjPallas.lean new file mode 100644 index 0000000..0be5b2a --- /dev/null +++ b/CompElliptic/Curves/Pasta/Fast/MsmProjPallas.lean @@ -0,0 +1,109 @@ +/- +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: Gregor Mitscha-Baude +-/ +import CompElliptic.Curves.Pasta.Fast.MsmProj.Core +import CompElliptic.Curves.Pasta.Fast.Projective + +/-! +# The projective Pippenger MSM at the Pallas curve + +The Pallas instantiation of the field-generic projective Pippenger core +(`Fast.MsmProj.Core`): the windowed multi-scalar multiplication run in projective coordinates +over the Pallas affine group `SWPoint Pallas.curve`, proven equal to the naive MSM. The curve +facts (`A = 0`, `B = 5`, no 2-torsion, `2 ≠ 0`) are supplied by `Fast.Projective.Pallas`. The +basic path, the single-pass-scatter path, and the windows-parallel path all delegate to the +core. + +This is the fast MSM a recursion verifier's `2^k`-point IPA opening check uses on the Pallas +side — one field inversion for the whole sum instead of one per addition. The `commit_lagrange` +wrappers are Vesta-only (their coefficients live in `VestaScalarField`), so they are not mirrored +here. + +The `Fast` interfaces are provisional: they are not guaranteed to remain public, and may be +folded into the existing API or otherwise changed incompatibly. +-/ + +open CompElliptic +open CompElliptic.CurveForms.ShortWeierstrass +open CompElliptic.Curves.Pasta +open CompElliptic.Curves.Pasta.Fast +open CompElliptic.Curves.Pasta.Fast.Projective.Pallas + +namespace CompElliptic.Curves.Pasta.Fast.MsmProjPallas + +/-! ## The projective Pippenger MSM -/ + +/-- Pallas' windowed Pippenger MSM run in projective coordinates: the generic core +(`MsmProj.Core.pippengerProj`) at the Pallas curve. -/ +abbrev pippengerProj : ℕ → List (ℕ × G) → G := MsmProj.Core.pippengerProj Pallas.curve hA hB + +theorem pippengerProj_eq (c : ℕ) (terms : List (ℕ × G)) : + pippengerProj c terms = Msm.pippenger c terms := + MsmProj.Core.pippengerProj_eq Pallas.curve hA hB hy0 htwo c terms + +/-- **Pallas' projective Pippenger equals the naive MSM** (`c ≥ 1`): the whole multi-scalar +multiplication runs in projective coordinates, one inversion at the end, and computes +`∑ᵢ aᵢ • gᵢ`. -/ +theorem pippengerProj_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × G)) : + pippengerProj c terms = (terms.map fun t => t.1 • t.2).sum := + MsmProj.Core.pippengerProj_eq_msm Pallas.curve hA hB hy0 htwo c hc terms + +/-! ## Single-pass Array bucketing -/ + +/-- One projective scatter step (Pallas instance of `Core.pscatterStep`). -/ +abbrev pscatterStep : Array PPal → ℕ × PPal → Array PPal := MsmProj.Core.pscatterStep (F := Fp) + +/-- Scatter into `base − 1` buckets in one pass (Pallas instance of `Core.pbucketScatter`). -/ +abbrev pbucketScatter : ℕ → List (ℕ × PPal) → Array PPal := MsmProj.Core.pbucketScatter (F := Fp) + +theorem pbucketScatter_spec (base : ℕ) (dp : List (ℕ × PPal)) (hdp : ∀ p ∈ dp, Valid p.2) : + (∀ P ∈ (pbucketScatter base dp).toList, Valid P) + ∧ (pbucketScatter base dp).toList.map toAffine + = (List.range (base - 1)).map fun k => + Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := + MsmProj.Core.pbucketScatter_spec Pallas.curve hA hB hy0 htwo base dp hdp + +/-- The scatter-bucketed projective window value (Pallas instance of `Core.pwindowValueFast`). -/ +abbrev pwindowValueFast : ℕ → ℕ → List (ℕ × PPal) → PPal := + MsmProj.Core.pwindowValueFast (F := Fp) + +theorem pwindowValueFast_spec (base i : ℕ) (pterms : List (ℕ × PPal)) + (h : ∀ p ∈ pterms, Valid p.2) : + Valid (pwindowValueFast base i pterms) + ∧ toAffine (pwindowValueFast base i pterms) + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine t.2)) := + MsmProj.Core.pwindowValueFast_spec Pallas.curve hA hB hy0 htwo base i pterms h + +/-! ## The scatter-bucketed projective Pippenger MSM -/ + +/-- **Scatter-bucketed projective Pippenger** (Pallas instance of `Core.pippengerProjScatter`). -/ +abbrev pippengerProjScatter : ℕ → List (ℕ × G) → G := + MsmProj.Core.pippengerProjScatter Pallas.curve hA hB + +theorem pippengerProjScatter_eq (c : ℕ) (terms : List (ℕ × G)) : + pippengerProjScatter c terms = Msm.pippenger c terms := + MsmProj.Core.pippengerProjScatter_eq Pallas.curve hA hB hy0 htwo c terms + +theorem pippengerProjScatter_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × G)) : + pippengerProjScatter c terms = (terms.map fun t => t.1 • t.2).sum := + MsmProj.Core.pippengerProjScatter_eq_msm Pallas.curve hA hB hy0 htwo c hc terms + +/-! ## Windows-parallel projective Pippenger -/ + +/-- **Windows-parallel scatter-bucketed projective Pippenger** (Pallas instance of +`Core.pippengerProjScatterPar`). -/ +abbrev pippengerProjScatterPar : ℕ → List (ℕ × G) → G := + MsmProj.Core.pippengerProjScatterPar Pallas.curve hA hB + +theorem pippengerProjScatterPar_eq (c : ℕ) (terms : List (ℕ × G)) : + pippengerProjScatterPar c terms = pippengerProjScatter c terms := + MsmProj.Core.pippengerProjScatterPar_eq Pallas.curve hA hB c terms + +theorem pippengerProjScatterPar_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × G)) : + pippengerProjScatterPar c terms = (terms.map fun t => t.1 • t.2).sum := + MsmProj.Core.pippengerProjScatterPar_eq_msm Pallas.curve hA hB hy0 htwo c hc terms + +end CompElliptic.Curves.Pasta.Fast.MsmProjPallas