From d9e02df2dbf43a1a13f7a9a95c55e19402aaa080 Mon Sep 17 00:00:00 2001 From: Gregor's Bot Date: Sat, 25 Jul 2026 02:40:45 +0200 Subject: [PATCH 1/2] feat(fields): Pasta base fields on the eight-limb Montgomery implementation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add `Fields/Pasta`, the per-field facade for the Pallas and Vesta base fields, following the KoalaBear layering: * `Pasta/Basic.lean` — the two 255-bit primes with Pratt primality certificates (ported from the certificates by Daira-Emma Hopwood, using CompPoly's own `PrattCertificate` infrastructure), their `Fact` and `Field` instances, and the 2-cycle abbreviations relating each curve's scalar field to the other's base field; * `Pasta/Fast.lean` — the `Mont64x8Field` constants for both fields and the namespaced `Pallas.Fast` / `Vesta.Fast` API over the shared eight-limb implementation, with the canonical-field bridge; * `Pasta.lean` — the facade re-exporting both. `Mont64x8Field` moves from the raw layer to `Montgomery/Native64x8Field` alongside the carrier it parameterizes, mirroring `Mont32Field` in `Montgomery/Native32Field`, and now carries `prime` like its single-word counterpart, so the bridge no longer takes a separate `Fact` argument. Tests cross-check both fast fields against canonical `ZMod` arithmetic for powers and inverses. Co-Authored-By: Claude Fable 5 --- CompPoly.lean | 5 + CompPoly/Fields/Pasta.lean | 17 ++ CompPoly/Fields/Pasta/Basic.lean | 216 +++++++++++++++++++++ CompPoly/Fields/Pasta/Fast.lean | 93 +++++++++ CompPoly/Fields/README.md | 3 + tests/CompPolyTests.lean | 1 + tests/CompPolyTests/Fields/Pasta/Fast.lean | 113 +++++++++++ 7 files changed, 448 insertions(+) create mode 100644 CompPoly/Fields/Pasta.lean create mode 100644 CompPoly/Fields/Pasta/Basic.lean create mode 100644 CompPoly/Fields/Pasta/Fast.lean create mode 100644 tests/CompPolyTests/Fields/Pasta/Fast.lean diff --git a/CompPoly.lean b/CompPoly.lean index d495f3a9..4eb814b8 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -157,11 +157,16 @@ public import CompPoly.Fields.Montgomery.Basic public import CompPoly.Fields.Montgomery.Native32 public import CompPoly.Fields.Montgomery.Native32Field public import CompPoly.Fields.Montgomery.Native64x8 +public import CompPoly.Fields.Montgomery.Native64x8 +public import CompPoly.Fields.Montgomery.Native64x8 public import CompPoly.Fields.Montgomery.Native64x8Defs 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.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 diff --git a/CompPoly/Fields/Pasta.lean b/CompPoly/Fields/Pasta.lean new file mode 100644 index 00000000..bca45de2 --- /dev/null +++ b/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`. +-/ diff --git a/CompPoly/Fields/Pasta/Basic.lean b/CompPoly/Fields/Pasta/Basic.lean new file mode 100644 index 00000000..16d17a20 --- /dev/null +++ b/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 . +-/ + +@[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 diff --git a/CompPoly/Fields/Pasta/Fast.lean b/CompPoly/Fields/Pasta/Fast.lean new file mode 100644 index 00000000..72585d2a --- /dev/null +++ b/CompPoly/Fields/Pasta/Fast.lean @@ -0,0 +1,93 @@ +/- +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.Montgomery.Native64x8Field + +/-! +# Fast Pasta base fields + +Native-word Montgomery implementations of the Pallas and Vesta base field arithmetic. The +shared algorithms and proofs live in `CompPoly.Fields.Montgomery.Native64x8Field`; this module +supplies the two sets of constants and the concrete API. + +Both Pasta primes are `1 mod 2 ^ 32`, so both have `montgomeryNegInv = 2 ^ 32 - 1`. +-/ + +@[expose] public section + +namespace Pallas.Fast + +open Montgomery.Native64x8 (Mont64x8Field FastField) + +/-! ## Parameters and carrier -/ + +/-- The per-field data realizing the Pallas base field as a fast eight-limb Montgomery +field. -/ +instance instMont64x8Field : Mont64x8Field Pallas.baseFieldSize where + prime := Pallas.baseFieldSize_is_prime + modulusLimbs := ⟨0x1, 0x992d30ed, 0x94cf91b, 0x224698fc, 0x0, 0x0, 0x0, 0x40000000⟩ + rModModulus := + ⟨0xfffffffd, 0x34786d38, 0xe41914ad, 0x992c350b, 0xffffffff, 0xffffffff, 0xffffffff, + 0x3fffffff⟩ + r2ModModulus := + ⟨0xf, 0x8c78ecb3, 0x8b0de0e7, 0xd7d30dbd, 0xc3c95d18, 0x7797a99b, 0x7b9cb714, 0x96d41af⟩ + montgomeryNegInv := 0xffffffff + +/-- The fast native-word Pallas base field carrier, stored as a Montgomery residue. -/ +abbrev Field : Type := FastField Pallas.baseFieldSize + +/-! ## Conversions -/ + +/-- Convert from the canonical `ZMod` Pallas base field into fast Montgomery form. -/ +@[inline] +def ofField (x : Pallas.BaseField) : Field := + Montgomery.Native64x8.FastField.ofField x + +/-! ## Canonical bridge -/ + +/-- Ring equivalence between the fast Montgomery representation and `Pallas.BaseField`. -/ +def ringEquiv : Field ≃+* Pallas.BaseField := + Montgomery.Native64x8.FastField.ringEquiv Pallas.baseFieldSize + +end Pallas.Fast + +namespace Vesta.Fast + +open Montgomery.Native64x8 (Mont64x8Field FastField) + +/-! ## Parameters and carrier -/ + +/-- The per-field data realizing the Vesta base field as a fast eight-limb Montgomery +field. -/ +instance instMont64x8Field : Mont64x8Field Vesta.baseFieldSize where + prime := Vesta.baseFieldSize_is_prime + modulusLimbs := ⟨0x1, 0x8c46eb21, 0x994a8dd, 0x224698fc, 0x0, 0x0, 0x0, 0x40000000⟩ + rModModulus := + ⟨0xfffffffd, 0x5b2b3e9c, 0xe3420567, 0x992c350b, 0xffffffff, 0xffffffff, 0xffffffff, + 0x3fffffff⟩ + r2ModModulus := + ⟨0xf, 0xfc9678ff, 0x891a16e3, 0x67bb433d, 0x4ccf590, 0x7fae2310, 0x7ccfdaa9, 0x96d41af⟩ + montgomeryNegInv := 0xffffffff + +/-- The fast native-word Vesta base field carrier, stored as a Montgomery residue. -/ +abbrev Field : Type := FastField Vesta.baseFieldSize + +/-! ## Conversions -/ + +/-- Convert from the canonical `ZMod` Vesta base field into fast Montgomery form. -/ +@[inline] +def ofField (x : Vesta.BaseField) : Field := + Montgomery.Native64x8.FastField.ofField x + +/-! ## Canonical bridge -/ + +/-- Ring equivalence between the fast Montgomery representation and `Vesta.BaseField`. -/ +def ringEquiv : Field ≃+* Vesta.BaseField := + Montgomery.Native64x8.FastField.ringEquiv Vesta.baseFieldSize + +end Vesta.Fast diff --git a/CompPoly/Fields/README.md b/CompPoly/Fields/README.md index aa8d7ddd..7a83aa10 100644 --- a/CompPoly/Fields/README.md +++ b/CompPoly/Fields/README.md @@ -56,6 +56,9 @@ This directory contains formally verified field infrastructure used in zero-know | **Montgomery/Native64x8Field.lean** | The `Mont64x8Field` class, `FastField` carrier, arithmetic, instances, and canonical-field bridge for moduli below `2^255`. | | **Montgomery/Native64x8InvDefs.lean** | Mathlib-free binary-GCD inversion runtime ([eprint 2020/972](https://eprint.iacr.org/2020/972)): the `GcdData` schedule, the candidate, and the checked `invGcdRaw`. | | **Montgomery/Native64x8Inv.lean** | Correctness of the checked inversion (`invGcdRaw`, wrapper `FastField.invGcd`), the divstep coefficient bounds, and the candidate's mac-width safety. | +| **Pasta.lean** | Facade for the Pasta modules, re-exporting the canonical Pallas/Vesta base fields and their fast native-word implementations. | +| **Pasta/Basic.lean** | The two 255-bit Pasta base primes (Pallas base = Vesta scalar and vice versa), with Pratt primality certificates. | +| **Pasta/Fast.lean** | Pallas- and Vesta-namespaced API over the shared eight-limb fast-field implementation, with per-field constants and canonical-field bridges. | | **Secp256k1.lean** | Base and scalar fields for the Secp256k1 curve (used in Bitcoin/Ethereum). | ## Binary-field modules diff --git a/tests/CompPolyTests.lean b/tests/CompPolyTests.lean index 3a698dba..ed95eab6 100644 --- a/tests/CompPolyTests.lean +++ b/tests/CompPolyTests.lean @@ -37,6 +37,7 @@ public import CompPolyTests.Fields.Goldilocks.Fast public import CompPolyTests.Fields.KoalaBear.Fast public import CompPolyTests.Fields.Mersenne31.Fast public import CompPolyTests.Fields.Mersenne31.Instances +public import CompPolyTests.Fields.Pasta.Fast public import CompPolyTests.Fields.PrattCertificate public import CompPolyTests.LinearAlgebra.Dense public import CompPolyTests.LinearAlgebra.PolynomialMatrix.Approximant diff --git a/tests/CompPolyTests/Fields/Pasta/Fast.lean b/tests/CompPolyTests/Fields/Pasta/Fast.lean new file mode 100644 index 00000000..5ea4a2b7 --- /dev/null +++ b/tests/CompPolyTests/Fields/Pasta/Fast.lean @@ -0,0 +1,113 @@ +/- +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 meta import CompPoly.Fields.Pasta + +/-! +# Fast Pasta Field Tests + +Regression checks for the raw eight-limb operations and the Pallas/Vesta fast-field +instantiations against externally computed values. +-/ + +public meta section + +namespace CompPolyTests.Fields.Pasta + +open _root_.Montgomery.Native64x8 + +private def q : Limbs8 := Vesta.Fast.instMont64x8Field.modulusLimbs + +private def negInv : UInt64 := Vesta.Fast.instMont64x8Field.montgomeryNegInv + +private def rMod : Limbs8 := Vesta.Fast.instMont64x8Field.rModModulus + +private def modulus : ℕ := Vesta.baseFieldSize + +private def a : Limbs8 := + ⟨0x90abcdef, 0x12345678, 0x90abcdef, 0x12345678, 0x90abcdef, 0x12345678, 0x90abcdef, + 0x12345678⟩ + +private def b : Limbs8 := + ⟨0x98765432, 0x1fedcba0, 0x98765432, 0x1fedcba0, 0x98765432, 0x1fedcba0, 0x98765432, + 0xfedcba0⟩ + +private def montA : Limbs8 := + ⟨0x4657fff9, 0xb89185c2, 0x7fa63616, 0xac5206fd, 0xca71bcaa, 0x4a1382e8, 0xd2416c1e, + 0x3ec0c11b⟩ + +private def montB : Limbs8 := + ⟨0x96717045, 0xa13e865, 0xeda4684, 0x5fa53078, 0xadca6010, 0x8c0bc7ff, 0x6af4be5b, + 0x2bde1e93⟩ + +private def montAB : Limbs8 := + ⟨0x5bfbc390, 0xa6073176, 0x8f8933a9, 0xbed1aec1, 0x630437f1, 0xba615782, 0x92dc822b, + 0x77a4b3f⟩ + +#guard q.toNat = modulus +#guard condSub q q = Limbs8.zero +#guard condSub q Limbs8.zero = Limbs8.zero +#guard (add q a b).toNat = (a.toNat + b.toNat) % modulus +#guard add q a (neg q a) = Limbs8.zero +#guard (sub q a b).toNat = (a.toNat + (modulus - b.toNat)) % modulus +#guard (sub q b a).toNat = (b.toNat + (modulus - a.toNat)) % modulus +#guard (neg q a).toNat = (modulus - a.toNat) % modulus +#guard neg q Limbs8.zero = Limbs8.zero +#guard mul q negInv montA montB = montAB +#guard mul q negInv rMod rMod = rMod +#guard mul q negInv rMod Limbs8.zero = Limbs8.zero +#guard square q negInv rMod = rMod + +private abbrev F := Vesta.Fast.Field + +#guard (0 : F).toNat = 0 +#guard (1 : F).toNat = 1 +#guard (37 : F).toNat = 37 +#guard ((Vesta.baseFieldSize : F)).toNat = 0 +#guard ((12345 : F) * 12345).toNat = 12345 * 12345 +#guard ((0 : F) - 1).toNat = Vesta.baseFieldSize - 1 +#guard (-(1 : F)).toNat = Vesta.baseFieldSize - 1 +#guard (((Vesta.baseFieldSize - 1 : ℕ) : F) * ((Vesta.baseFieldSize - 1 : ℕ) : F)).toNat = 1 +#guard ((123456789 : F) ^ 17).toNat = 123456789 ^ 17 % Vesta.baseFieldSize +#guard ((37 : F)⁻¹ * 37).toNat = 1 +#guard ((37 : F) / 37).toNat = 1 +#guard ((0 : F)⁻¹).toNat = 0 + +private def pq : Limbs8 := Pallas.Fast.instMont64x8Field.modulusLimbs + +private def pNegInv : UInt64 := Pallas.Fast.instMont64x8Field.montgomeryNegInv + +private def pMontA : Limbs8 := + ⟨0x73c65f1d, 0x4e0a938e, 0xd71d5fef, 0x6a1193b, 0xe42540dc, 0xcb40dac3, 0xc6cffd09, + 0x335fa2c8⟩ + +private def pMontB : Limbs8 := + ⟨0x5153d947, 0x26211be3, 0x38e82d52, 0xcb949678, 0xb6f80c7e, 0xf369686f, 0x7c2907b8, + 0xd91e296⟩ + +private def pMontAB : Limbs8 := + ⟨0x8d6b3f08, 0xe5c0528e, 0x22646fad, 0xaec941cc, 0xfec4a4c0, 0x4f5e09aa, 0x69b735b5, + 0x179b8aa1⟩ + +#guard pq.toNat = Pallas.baseFieldSize +#guard mul pq pNegInv pMontA pMontB = pMontAB +#guard (add pq a b).toNat = (a.toNat + b.toNat) % Pallas.baseFieldSize +#guard condSub pq pq = Limbs8.zero + +private abbrev G := Pallas.Fast.Field + +#guard (37 : G).toNat = 37 +#guard ((12345 : G) * 12345).toNat = 12345 * 12345 +#guard ((37 : G)⁻¹ * 37).toNat = 1 + +#guard ((123456789 : F) ^ 17).toField = ((123456789 : Vesta.BaseField) ^ 17) +#guard ((37 : F)⁻¹).toField = ((37 : Vesta.BaseField)⁻¹) +#guard Vesta.Fast.ofField ((37 : Vesta.BaseField)⁻¹) = (37 : F)⁻¹ +#guard ((123456789 : G) ^ 17).toField = ((123456789 : Pallas.BaseField) ^ 17) +#guard ((37 : G)⁻¹).toField = ((37 : Pallas.BaseField)⁻¹) + +end CompPolyTests.Fields.Pasta From 37685bc67c41a19e4f96820ecd19705347e0a4c5 Mon Sep 17 00:00:00 2001 From: Gregor's Bot Date: Sun, 26 Jul 2026 08:58:39 +0200 Subject: [PATCH 2/2] feat(fields): scalar radix-2 FFT over eight-limb Montgomery elements Co-Authored-By: Claude Fable 5 --- CompPoly.lean | 3 +- CompPoly/Fields/Montgomery/ScalarFft.lean | 73 +++++++++++++++++++++++ CompPoly/Fields/README.md | 1 + 3 files changed, 75 insertions(+), 2 deletions(-) create mode 100644 CompPoly/Fields/Montgomery/ScalarFft.lean diff --git a/CompPoly.lean b/CompPoly.lean index 4eb814b8..c39e7598 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -157,13 +157,12 @@ public import CompPoly.Fields.Montgomery.Basic public import CompPoly.Fields.Montgomery.Native32 public import CompPoly.Fields.Montgomery.Native32Field public import CompPoly.Fields.Montgomery.Native64x8 -public import CompPoly.Fields.Montgomery.Native64x8 -public import CompPoly.Fields.Montgomery.Native64x8 public import CompPoly.Fields.Montgomery.Native64x8Defs 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 diff --git a/CompPoly/Fields/Montgomery/ScalarFft.lean b/CompPoly/Fields/Montgomery/ScalarFft.lean new file mode 100644 index 00000000..38ab2f98 --- /dev/null +++ b/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 diff --git a/CompPoly/Fields/README.md b/CompPoly/Fields/README.md index 7a83aa10..67e4503f 100644 --- a/CompPoly/Fields/README.md +++ b/CompPoly/Fields/README.md @@ -56,6 +56,7 @@ This directory contains formally verified field infrastructure used in zero-know | **Montgomery/Native64x8Field.lean** | The `Mont64x8Field` class, `FastField` carrier, arithmetic, instances, and canonical-field bridge for moduli below `2^255`. | | **Montgomery/Native64x8InvDefs.lean** | Mathlib-free binary-GCD inversion runtime ([eprint 2020/972](https://eprint.iacr.org/2020/972)): the `GcdData` schedule, the candidate, and the checked `invGcdRaw`. | | **Montgomery/Native64x8Inv.lean** | Correctness of the checked inversion (`invGcdRaw`, wrapper `FastField.invGcd`), the divstep coefficient bounds, and the candidate's mac-width safety. | +| **Montgomery/ScalarFft.lean** | Zero-import in-place radix-2 DIT FFT over eight-limb Montgomery residues and precomputed twiddles. | | **Pasta.lean** | Facade for the Pasta modules, re-exporting the canonical Pallas/Vesta base fields and their fast native-word implementations. | | **Pasta/Basic.lean** | The two 255-bit Pasta base primes (Pallas base = Vesta scalar and vice versa), with Pratt primality certificates. | | **Pasta/Fast.lean** | Pallas- and Vesta-namespaced API over the shared eight-limb fast-field implementation, with per-field constants and canonical-field bridges. |