Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta)

CompPoly.lean

@@ -162,6 +162,10 @@ public import CompPoly.Fields.Montgomery.Native64x8Field
 public import CompPoly.Fields.Montgomery.Native64x8Inv
 public import CompPoly.Fields.Montgomery.Native64x8InvDefs
 public import CompPoly.Fields.Montgomery.Native64x8Mul
+public import CompPoly.Fields.Montgomery.ScalarFft
+public import CompPoly.Fields.Pasta
+public import CompPoly.Fields.Pasta.Basic
+public import CompPoly.Fields.Pasta.Fast
 public import CompPoly.Fields.PrattCertificate
 public import CompPoly.Fields.Secp256k1
 public import CompPoly.LinearAlgebra.Dense

CompPoly/Fields/Montgomery/ScalarFft.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregor Mitscha-Baude
+-/
+module
+
+public import CompPoly.Fields.Montgomery.Native64x8Defs
+
+/-!
+# Radix-2 DIT FFT over eight-limb Montgomery elements (zero-import)
+
+An in-place radix-2 decimation-in-time FFT over `Limbs8` Montgomery residues: a bit-reversal
+permutation followed by `logN` rounds of butterflies against a precomputed Montgomery-form
+twiddle table.  Like the arithmetic in `CompPoly.Fields.Montgomery.Native64x8Defs`, the loop
+nest is generic over the modulus, taking `q` and `negInv` explicitly.
+
+As explained in `CompPoly.Fields.Montgomery.Native64x8Defs`, this module deliberately imports
+nothing beyond that (itself zero-import) module: downstream consumers put it into
+`precompileModules` native-compilation lanes, and `precompileModules` compiles the
+entire import closure — so the runtime definitions must not pull in mathlib.
+
+This module contains runtime definitions only; correctness specifications live downstream
+for now.
+-/
+
+@[expose] public section
+
+namespace Montgomery
+namespace ScalarFft
+
+open Native64x8 (Limbs8 add sub mul)
+
+/-- Bit-reversal permutation index. -/
+def bitreverse (n l : Nat) : Nat := Id.run do
+  let mut r := 0
+  let mut m := n
+  for _ in [0:l] do
+    r := (r <<< 1) ||| (m &&& 1)
+    m := m >>> 1
+  return r
+
+/-- In-place radix-2 DIT FFT over eight-limb Montgomery residues modulo `q`: bit-reversal
+permutation, then `logN` rounds of butterflies against the Montgomery-form twiddles `tw`. -/
+def fft (q : Limbs8) (negInv : UInt64) (a0 : Array Limbs8) (tw : Array Limbs8)
+    (logN : Nat) : Array Limbs8 := Id.run do
+  let n := a0.size
+  let mut a := a0
+  for k in [0:n] do
+    let rk := bitreverse k logN
+    if k < rk then
+      let ak := a[k]!
+      let ark := a[rk]!
+      a := (a.set! k ark).set! rk ak
+  let mut half := 1
+  for _ in [0:logN] do
+    let chunk := 2 * half
+    let twiddleChunk := n / chunk
+    for c in [0:n / chunk] do
+      let s := c * chunk
+      for j in [0:half] do
+        let twdl := tw[j * twiddleChunk]!
+        let aIdx := s + j
+        let bIdx := s + half + j
+        let aOld := a[aIdx]!
+        let t := mul q negInv twdl a[bIdx]!
+        a := a.set! aIdx (add q aOld t)
+        a := a.set! bIdx (sub q aOld t)
+    half := chunk
+  return a
+
+end ScalarFft
+end Montgomery

CompPoly/Fields/Pasta.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregor Mitscha-Baude
+-/
+module
+
+public import CompPoly.Fields.Pasta.Basic
+public import CompPoly.Fields.Pasta.Fast
+
+/-!
+# Pasta (Pallas / Vesta) fields
+
+Facade module for the Pasta base fields.  It re-exports the canonical `ZMod` models with
+their primality certificates from `CompPoly.Fields.Pasta.Basic` and the native-word
+eight-limb Montgomery implementations from `CompPoly.Fields.Pasta.Fast`.
+-/

CompPoly/Fields/Pasta/Basic.lean

@@ -0,0 +1,216 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daira-Emma Hopwood, Gregor Mitscha-Baude
+-/
+module
+
+public import CompPoly.Fields.PrattCertificate
+
+/-!
+# The Pasta (Pallas / Vesta) base prime fields
+
+The Pallas and Vesta curves form a 2-cycle: the base field of one is the scalar field of the
+other.  This module defines the two underlying 255-bit primes together with their Lucas/Pratt
+primality certificates, following the pattern of `CompPoly.Fields.Secp256k1`.
+
+* `Pallas.baseFieldSize` is the Pallas base field size, equal to the Vesta scalar field size;
+* `Vesta.baseFieldSize` is the Vesta base field size, equal to the Pallas scalar field size.
+
+Both primes are `1 mod 2 ^ 32` and have 2-adicity 32.  The certificates were generated from
+the factorizations of `p - 1` and `q - 1`; see <https://github.com/zcash/pasta>.
+-/
+
+@[expose] public section
+
+namespace Pallas
+
+/-- The base field size of the Pallas curve, which is the scalar field size of Vesta. -/
+@[reducible]
+def baseFieldSize : Nat :=
+  0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
+
+/-- The Pallas base field as a `ZMod`. -/
+abbrev BaseField := ZMod baseFieldSize
+
+/-- The Pallas base field size is prime. -/
+theorem baseFieldSize_is_prime : Nat.Prime baseFieldSize := by
+  unfold baseFieldSize
+  refine PrattCertificate'.out
+    (p := 28948022309329048855892746252171976963363056481941560715954676764349967630337)
+    ⟨5, (by reduce_mod_char), ?_⟩
+  refine .split [2 ^ 32, 3, 463, 539204044132271846773,
+    8999194758858563409123804352480028797519453] (fun r hr => ?_) (by norm_num)
+  simp at hr
+  rcases hr with hr | hr | hr | hr | hr
+  all_goals rw [hr]
+  · exact .prime 2 32 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 3 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 463 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · refine .prime 539204044132271846773 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+    refine PrattCertificate'.out (p := 539204044132271846773) ⟨5, (by reduce_mod_char), ?_⟩
+    refine .split [2 ^ 2, 3 ^ 5, 89, 14923, 417677162933] (fun r hr => ?_) (by norm_num)
+    simp at hr
+    rcases hr with hr | hr | hr | hr | hr
+    all_goals rw [hr]
+    · exact .prime 2 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 3 5 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 89 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 14923 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · refine .prime 417677162933 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+      refine PrattCertificate'.out (p := 417677162933) ⟨2, (by reduce_mod_char), ?_⟩
+      refine .split [2 ^ 2, 59, 1973, 897019] (fun r hr => ?_) (by norm_num)
+      simp at hr
+      rcases hr with hr | hr | hr | hr
+      all_goals rw [hr]
+      · exact .prime 2 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 59 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 1973 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 897019 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · refine .prime 8999194758858563409123804352480028797519453 1 _ ?_ (by reduce_mod_char; decide)
+      (by norm_num)
+    refine PrattCertificate'.out (p := 8999194758858563409123804352480028797519453)
+      ⟨2, (by reduce_mod_char), ?_⟩
+    refine .split [2 ^ 2, 3 ^ 4, 11, 2531, 115603, 1197907, 22160661629, 325086459374267]
+      (fun r hr => ?_) (by norm_num)
+    simp at hr
+    rcases hr with hr | hr | hr | hr | hr | hr | hr | hr
+    all_goals rw [hr]
+    · exact .prime 2 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 3 4 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 11 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 2531 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 115603 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 1197907 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · refine .prime 22160661629 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+      refine PrattCertificate'.out (p := 22160661629) ⟨3, (by reduce_mod_char), ?_⟩
+      refine .split [2 ^ 2, 7, 19, 41655379] (fun r hr => ?_) (by norm_num)
+      simp at hr
+      rcases hr with hr | hr | hr | hr
+      all_goals rw [hr]
+      · exact .prime 2 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 7 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 19 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 41655379 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · refine .prime 325086459374267 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+      refine PrattCertificate'.out (p := 325086459374267) ⟨2, (by reduce_mod_char), ?_⟩
+      refine .split [2, 509, 413527, 772231] (fun r hr => ?_) (by norm_num)
+      simp at hr
+      rcases hr with hr | hr | hr | hr
+      all_goals rw [hr]
+      · exact .prime 2 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 509 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 413527 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 772231 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+
+instance : Fact (Nat.Prime baseFieldSize) := ⟨baseFieldSize_is_prime⟩
+
+instance : Field BaseField := ZMod.instField baseFieldSize
+
+end Pallas
+
+namespace Vesta
+
+/-- The base field size of the Vesta curve, which is the scalar field size of Pallas. -/
+@[reducible]
+def baseFieldSize : Nat :=
+  0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
+
+/-- The Vesta base field as a `ZMod`. -/
+abbrev BaseField := ZMod baseFieldSize
+
+/-- The Vesta base field size is prime. -/
+theorem baseFieldSize_is_prime : Nat.Prime baseFieldSize := by
+  unfold baseFieldSize
+  refine PrattCertificate'.out
+    (p := 28948022309329048855892746252171976963363056481941647379679742748393362948097)
+    ⟨5, (by reduce_mod_char), ?_⟩
+  refine .split [2 ^ 32, 3 ^ 2, 1709, 24859, 1690502597179744445941507,
+    10427374428728808478656897599072717] (fun r hr => ?_) (by norm_num)
+  simp at hr
+  rcases hr with hr | hr | hr | hr | hr | hr
+  all_goals rw [hr]
+  · exact .prime 2 32 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 3 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 1709 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 24859 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · refine .prime 1690502597179744445941507 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+    refine PrattCertificate'.out (p := 1690502597179744445941507) ⟨2, (by reduce_mod_char), ?_⟩
+    refine .split [2, 3, 13, 4129989133, 5247740253619] (fun r hr => ?_) (by norm_num)
+    simp at hr
+    rcases hr with hr | hr | hr | hr | hr
+    all_goals rw [hr]
+    · exact .prime 2 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 3 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 13 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · refine .prime 4129989133 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+      refine PrattCertificate'.out (p := 4129989133) ⟨5, (by reduce_mod_char), ?_⟩
+      refine .split [2 ^ 2, 3, 359, 958679] (fun r hr => ?_) (by norm_num)
+      simp at hr
+      rcases hr with hr | hr | hr | hr
+      all_goals rw [hr]
+      · exact .prime 2 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 3 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 359 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 958679 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · refine .prime 5247740253619 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+      refine PrattCertificate'.out (p := 5247740253619) ⟨2, (by reduce_mod_char), ?_⟩
+      refine .split [2, 3 ^ 3, 17, 71, 80513981] (fun r hr => ?_) (by norm_num)
+      simp at hr
+      rcases hr with hr | hr | hr | hr | hr
+      all_goals rw [hr]
+      · exact .prime 2 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 3 3 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 17 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 71 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 80513981 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · refine .prime 10427374428728808478656897599072717 1 _ ?_ (by reduce_mod_char; decide)
+      (by norm_num)
+    refine PrattCertificate'.out (p := 10427374428728808478656897599072717)
+      ⟨2, (by reduce_mod_char), ?_⟩
+    refine .split [2 ^ 2, 294793, 4229279, 399082391, 5239247429827] (fun r hr => ?_)
+      (by norm_num)
+    simp at hr
+    rcases hr with hr | hr | hr | hr | hr
+    all_goals rw [hr]
+    · exact .prime 2 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 294793 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 4229279 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · exact .prime 399082391 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+    · refine .prime 5239247429827 1 _ ?_ (by reduce_mod_char; decide) (by norm_num)
+      refine PrattCertificate'.out (p := 5239247429827) ⟨2, (by reduce_mod_char), ?_⟩
+      refine .split [2, 3 ^ 2, 757, 12149, 31649] (fun r hr => ?_) (by norm_num)
+      simp at hr
+      rcases hr with hr | hr | hr | hr | hr
+      all_goals rw [hr]
+      · exact .prime 2 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 3 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 757 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 12149 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+      · exact .prime 31649 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+
+instance : Fact (Nat.Prime baseFieldSize) := ⟨baseFieldSize_is_prime⟩
+
+instance : Field BaseField := ZMod.instField baseFieldSize
+
+end Vesta
+
+namespace Pallas
+
+/-- The scalar field size of Pallas is the base field size of Vesta. -/
+abbrev scalarFieldSize : Nat := Vesta.baseFieldSize
+
+/-- The Pallas scalar field is the Vesta base field. -/
+abbrev ScalarField := Vesta.BaseField
+
+end Pallas
+
+namespace Vesta
+
+/-- The scalar field size of Vesta is the base field size of Pallas. -/
+abbrev scalarFieldSize : Nat := Pallas.baseFieldSize
+
+/-- The Vesta scalar field is the Pallas base field. -/
+abbrev ScalarField := Pallas.BaseField
+
+end Vesta