test(fields): add Mersenne31 regression coverage

CompPoly.lean

@@ -102,7 +102,9 @@ import CompPoly.Fields.Goldilocks
 import CompPoly.Fields.KoalaBear
 import CompPoly.Fields.KoalaBear.Basic
 import CompPoly.Fields.KoalaBear.Fast
-import CompPoly.Fields.Mersenne
+import CompPoly.Fields.Mersenne31
+import CompPoly.Fields.Mersenne31.Basic
+import CompPoly.Fields.Mersenne31.Fast
 import CompPoly.Fields.PrattCertificate
 import CompPoly.Fields.Secp256k1
 import CompPoly.LinearAlgebra.Dense

CompPoly/Fields/Mersenne31.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2024 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao, Varun Thakore
+-/
+
+import CompPoly.Fields.Mersenne31.Basic
+import CompPoly.Fields.Mersenne31.Fast
+
+/-!
+  # Mersenne31 prime field `2^{31} - 1`
+
+  Facade module for the Mersenne31 field. It re-exports the canonical `ZMod` model
+  from `CompPoly.Fields.Mersenne31.Basic` and the native-word implementation from
+  `CompPoly.Fields.Mersenne31.Fast`.
+-/

CompPoly/Fields/Mersenne31/Basic.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2024 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao, Varun Thakore
+-/
+
+import CompPoly.Fields.Basic
+import CompPoly.Fields.PrattCertificate
+
+/-!
+  # Mersenne prime field `2^{31} - 1`
+
+  This is the field used in Circle STARKs.
+-/
+
+namespace Mersenne31
+namespace Basic
+
+/-- The Mersenne31 prime modulus `2^31 - 1`. -/
+@[reducible]
+def fieldSize : Nat := 2 ^ 31 - 1
+
+/-- The canonical mathematical Mersenne31 field, implemented as integers modulo
+`fieldSize`. -/
+abbrev Field := ZMod fieldSize
+
+/-- The Mersenne31 modulus is prime, verified by a Pratt certificate. -/
+theorem is_prime : Nat.Prime fieldSize := by
+  unfold fieldSize
+  pratt
+
+/-- Register primality of `fieldSize` for Mathlib instances such as `ZMod.instField`. -/
+instance : Fact (Nat.Prime fieldSize) := ⟨is_prime⟩
+
+/-- The canonical Mersenne31 carrier is a field because its modulus is prime. -/
+instance : _root_.Field Field := ZMod.instField fieldSize
+
+/-- Mersenne31 has characteristic different from two. -/
+instance : NonBinaryField Field where
+  char_neq_2 := by
+    -- `decide` can discharge this concrete ZMod equality.
+    simpa [Field, fieldSize] using
+      (by decide : (2 : ZMod (2 ^ 31 - 1)) ≠ 0)
+
+end Basic
+end Mersenne31