feat(fields): fast BN254/BLS12-381/BLS12-377 scalar fields (8x32 Montgomery)

.github/workflows/lean_action_ci.yml

@@ -20,6 +20,7 @@ env:
     univariate-sparse-koalabear,
     univariate-monic-remainder-small-koalabear,
     univariate-dense-goldilocks,univariate-dense-bn254,
+    univariate-dense-bls12-381,univariate-dense-bls12-377,
     univariate-batch-small-koalabear,
     univariate-many-one-point-koalabear,
     univariate-mul-koalabear,univariate-mul-babybear,
@@ -35,7 +36,9 @@ env:
     guruswami-sudan-filtered-core-small-koalabear,
     additive-ntt-btf3-l2-r2,additive-ntt-btf3-l4-r2,additive-ntt-btf4-l7-r2,
     fields-extension-koalabear-ext4-mul,fields-extension-koalabear-ext4-inv,
-    fields-extension-babybear-ext4-mul,fields-extension-babybear-ext4-inv
+    fields-extension-babybear-ext4-mul,fields-extension-babybear-ext4-inv,
+    fields-mont64x8-bn254-inv,fields-mont64x8-bls12-381-inv,
+    fields-mont64x8-bls12-377-inv
 
 jobs:
   build:

CompPoly.lean

@@ -67,8 +67,14 @@ public import CompPoly.Data.RingTheory.AlgebraTower
 public import CompPoly.Data.RingTheory.CanonicalEuclideanDomain
 public import CompPoly.Data.Vector.Basic
 public import CompPoly.Fields.BLS12_377
+public import CompPoly.Fields.BLS12_377.Basic
+public import CompPoly.Fields.BLS12_377.Fast
 public import CompPoly.Fields.BLS12_381
+public import CompPoly.Fields.BLS12_381.Basic
+public import CompPoly.Fields.BLS12_381.Fast
 public import CompPoly.Fields.BN254
+public import CompPoly.Fields.BN254.Basic
+public import CompPoly.Fields.BN254.Fast
 public import CompPoly.Fields.BabyBear
 public import CompPoly.Fields.BabyBear.Basic
 public import CompPoly.Fields.BabyBear.Ext4
@@ -124,6 +130,12 @@ public import CompPoly.Fields.Mersenne
 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.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.PrattCertificate
 public import CompPoly.Fields.Secp256k1
 public import CompPoly.LinearAlgebra.Dense

CompPoly/Fields/BLS12_377.lean

@@ -1,56 +1,17 @@
 /-
 Copyright (c) 2024 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Quang Dao
+Authors: Quang Dao, Georgios Raikos
 -/
 module
 
-public import CompPoly.Fields.PrattCertificate
-/-!
-  # The BLS12-377 scalar prime field
-
-  The 253-bit prime number that divides the order of the BLS12-377 curve.
-
-  This prime has 2-adicity 47.
-
-  This is called `r` in [BCGMMW18].
+public import CompPoly.Fields.BLS12_377.Basic
+public import CompPoly.Fields.BLS12_377.Fast
 
-  ## References
-
-  * [Bowe, S., Chiesa, A., Green, M., Miers, I., Mishra, P., and Wu, H.,
-      *Zexe: Enabling Decentralized Private Computation*][BCGMMW18]
-  * See also [snarkos-curves](https://github.com/ProvableHQ/snarkOS/tree/c9e5f823b8493f8c3a6c43e6f4dfd16173b99957/curves), from which this is adapted.
+/-!
+# BLS12-377 Scalar Field
 
+Facade module for the BLS12-377 scalar field. It re-exports the canonical `ZMod` model
+from `CompPoly.Fields.BLS12_377.Basic` and the native-word Montgomery implementation from
+`CompPoly.Fields.BLS12_377.Fast`.
 -/
-
-@[expose] public section
-
-namespace BLS12_377
-
-@[reducible]
-def scalarFieldSize : Nat :=
-  8444461749428370424248824938781546531375899335154063827935233455917409239041
-
-abbrev ScalarField := ZMod scalarFieldSize
-
-theorem ScalarField_is_prime : Nat.Prime scalarFieldSize := by
-  unfold scalarFieldSize
-  refine PrattCertificate'.out (p := scalarFieldSize) ⟨22, (by reduce_mod_char), ?_⟩
-  refine .split [2 ^ 47, 3, 5, 7, 13, 499, 958612291309063373, 9586122913090633729 ^ 2]
-    (fun r hr => ?_) (by norm_num)
-  simp at hr
-  rcases hr with hr | hr | hr | hr | hr | hr | hr | hr <;> rw [hr]
-  · exact .prime 2 47 _ (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 5 1 _ (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 13 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 499 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 958612291309063373 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 9586122913090633729 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-
-instance : Fact (Nat.Prime scalarFieldSize) := ⟨ScalarField_is_prime⟩
-
-instance : Field ScalarField := ZMod.instField scalarFieldSize
-
-end BLS12_377

CompPoly/Fields/BLS12_377/Basic.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2024 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+public import CompPoly.Fields.PrattCertificate
+/-!
+  # The BLS12-377 scalar prime field
+
+  `r` of the BLS12-377 curve, 253-bit, 2-adicity 47
+  ([Zexe, BCGMMW18](https://eprint.iacr.org/2018/962)).
+-/
+
+@[expose] public section
+
+namespace BLS12_377
+
+@[reducible]
+def scalarFieldSize : Nat :=
+  0x12ab655e9a2ca55660b44d1e5c37b00159aa76fed00000010a11800000000001
+
+abbrev ScalarField := ZMod scalarFieldSize
+
+theorem ScalarField_is_prime : Nat.Prime scalarFieldSize := by
+  unfold scalarFieldSize
+  refine PrattCertificate'.out (p := scalarFieldSize) ⟨22, (by reduce_mod_char), ?_⟩
+  refine .split [2 ^ 47, 3, 5, 7, 13, 499, 958612291309063373, 9586122913090633729 ^ 2]
+    (fun r hr => ?_) (by norm_num)
+  simp at hr
+  rcases hr with hr | hr | hr | hr | hr | hr | hr | hr <;> rw [hr]
+  · exact .prime 2 47 _ (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 5 1 _ (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 13 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 499 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 958612291309063373 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 9586122913090633729 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+
+instance : Fact (Nat.Prime scalarFieldSize) := ⟨ScalarField_is_prime⟩
+
+instance : Field ScalarField := ZMod.instField scalarFieldSize
+
+end BLS12_377

CompPoly/Fields/BLS12_377/Fast.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Georgios Raikos
+-/
+module
+
+public import CompPoly.Fields.BLS12_377.Basic
+public import CompPoly.Fields.Montgomery.Native64x8Inv
+
+/-!
+# Fast BLS12-377 Scalar Field
+
+A native eight-limb Montgomery implementation of BLS12-377 scalar arithmetic
+(`CompPoly.Fields.Montgomery.Native64x8Field`). This module supplies the BLS12-377
+constants.
+-/
+
+@[expose] public section
+
+namespace BLS12_377.Fast
+
+open Montgomery.Native64x8 (Mont64x8Field FastField GcdData)
+
+set_option exponentiation.threshold 1100
+
+/-! ## Parameters and carrier -/
+
+/-- Divstep schedule of the binary-GCD inverse candidate. -/
+instance instGcdData : GcdData BLS12_377.scalarFieldSize where
+  finalRounds := 39
+  initU :=
+    ⟨0x94e01332, 0xa5707af0, 0x6f1abbfb, 0xf9af464a, 0x7f75c179, 0x65dbc6f7, 0xc9364c65,
+      0x10e76cd3⟩
+
+/-- The per-field data realizing BLS12-377's scalar field as a fast eight-limb
+(32-bit-limb) Montgomery field. -/
+instance instMont64x8Field : Mont64x8Field BLS12_377.scalarFieldSize where
+  prime := BLS12_377.ScalarField_is_prime
+  modulusLimbs :=
+    ⟨0x1, 0xa118000, 0xd0000001, 0x59aa76fe, 0x5c37b001, 0x60b44d1e, 0x9a2ca556,
+      0x12ab655e⟩
+  rModModulus :=
+    ⟨0xfffffff3, 0x7d1c7fff, 0x6ffffff2, 0x7257f50f, 0x512c0fee, 0x16d81575, 0x2bbb9a9d,
+      0xd4bda32⟩
+  r2ModModulus :=
+    ⟨0xb861857b, 0x25d577ba, 0x8860591f, 0xcc2c27b5, 0xe5dc8593, 0xa7cc008f, 0xeff1c939,
+      0x11fdae7⟩
+  montgomeryNegInv := 0xffffffff
+
+/-- The eight-limb BLS12-377 scalar field carrier, stored as a Montgomery residue. -/
+abbrev ScalarField : Type := FastField BLS12_377.scalarFieldSize
+
+/-- Convert from the canonical `BLS12_377.ScalarField` field into fast Montgomery form. -/
+@[inline]
+def ofField (x : BLS12_377.ScalarField) : ScalarField :=
+  FastField.ofField x
+
+/-- Ring equivalence between the eight-limb representation and the canonical
+`BLS12_377.ScalarField`. -/
+def ringEquiv : ScalarField ≃+* BLS12_377.ScalarField :=
+  FastField.ringEquiv BLS12_377.scalarFieldSize
+
+end BLS12_377.Fast

CompPoly/Fields/BLS12_381.lean

@@ -1,58 +1,17 @@
 /-
 Copyright (c) 2024 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Quang Dao
+Authors: Quang Dao, Georgios Raikos
 -/
 module
 
-public import CompPoly.Fields.PrattCertificate
-/-!
-  # The BLS12-381 scalar prime field
-
-  The 253-bit prime number that divides the order of the BLS12-381 curve.
-
-  This prime has 2-adicity 47.
-
-  ## References
+public import CompPoly.Fields.BLS12_381.Basic
+public import CompPoly.Fields.BLS12_381.Fast
 
-  This is `r` in [BCGMMW18].
-
-  See also (https://github.com/ProvableHQ/snarkOS/tree/c9e5f823b8493f8c3a6c43e6f4dfd16173b99957/curves).
+/-!
+# BLS12-381 Scalar Field
 
+Facade module for the BLS12-381 scalar field. It re-exports the canonical `ZMod` model
+from `CompPoly.Fields.BLS12_381.Basic` and the native-word Montgomery implementation from
+`CompPoly.Fields.BLS12_381.Fast`.
 -/
-
-@[expose] public section
-
-namespace BLS12_381
-
-@[reducible]
-def scalarFieldSize : Nat :=
-  52435875175126190479447740508185965837690552500527637822603658699938581184513
-
-abbrev ScalarField := ZMod scalarFieldSize
-
-theorem ScalarField_is_prime : Nat.Prime scalarFieldSize := by
-  unfold scalarFieldSize
-  refine PrattCertificate'.out (p := scalarFieldSize) ⟨7, (by reduce_mod_char), ?_⟩
-  refine .split [2 ^ 32, 3, 11, 19, 10177, 125527, 859267, 906349 ^ 2, 2508409, 2529403, 52437899,
-    254760293 ^ 2] (fun r hr => ?_) (by norm_num)
-  simp at hr
-  rcases hr with hr | hr | hr | hr | hr | hr | hr | hr | hr | hr | hr | hr <;> 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 11 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 10177 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 125527 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 859267 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 906349 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 2508409 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 2529403 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 52437899 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-  · exact .prime 254760293 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
-
-instance : Fact (Nat.Prime scalarFieldSize) := ⟨ScalarField_is_prime⟩
-
-instance : Field ScalarField := ZMod.instField scalarFieldSize
-
-end BLS12_381

CompPoly/Fields/BLS12_381/Basic.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+public import CompPoly.Fields.PrattCertificate
+/-!
+  # The BLS12-381 scalar prime field
+
+  `r` of the BLS12-381 curve, 255-bit, 2-adicity 32
+  ([IETF pairing-friendly-curves draft](https://datatracker.ietf.org/doc/draft-irtf-cfrg-pairing-friendly-curves/)).
+-/
+
+@[expose] public section
+
+namespace BLS12_381
+
+@[reducible]
+def scalarFieldSize : Nat :=
+  0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001
+
+abbrev ScalarField := ZMod scalarFieldSize
+
+theorem ScalarField_is_prime : Nat.Prime scalarFieldSize := by
+  unfold scalarFieldSize
+  refine PrattCertificate'.out (p := scalarFieldSize) ⟨7, (by reduce_mod_char), ?_⟩
+  refine .split [2 ^ 32, 3, 11, 19, 10177, 125527, 859267, 906349 ^ 2, 2508409, 2529403, 52437899,
+    254760293 ^ 2] (fun r hr => ?_) (by norm_num)
+  simp at hr
+  rcases hr with hr | hr | hr | hr | hr | hr | hr | hr | hr | hr | hr | hr <;> 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 11 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 10177 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 125527 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 859267 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 906349 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 2508409 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 2529403 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 52437899 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+  · exact .prime 254760293 2 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
+
+instance : Fact (Nat.Prime scalarFieldSize) := ⟨ScalarField_is_prime⟩
+
+instance : Field ScalarField := ZMod.instField scalarFieldSize
+
+end BLS12_381