feat(fields): add fast Mersenne31 arithmetic

[varunthakore]

No description provided.

[github-actions]

🤖 PR Summary

Overview

This PR restructures the Mersenne31 field implementation and adds a fast, UInt32-backed arithmetic core. The module is split from a single file into a subdirectory with three components: a facade, a canonical ZMod-based definition, and a native-word implementation.

Restructuring

• The old CompPoly/Fields/Mersenne.lean has been deleted. It previously held the Mersenne31 namespace, a reducible fieldSize definition, Field as ZMod fieldSize, and a primality proof via the pratt tactic. These definitions have been removed from the project.
• A new facade CompPoly/Fields/Mersenne31.lean provides a single entry point that re-exports both the ZMod model and the fast implementation.
• The file CompPoly.lean was updated to import the new module structure.

Mathematical Formalization

• CompPoly/Fields/Mersenne31/Basic.lean defines the Mersenne31 prime field 2^31 - 1 as used in Circle STARKs. It provides:
  • fieldSize : ℕ := 2^31 - 1
  • Field : Type as ZMod fieldSize
  • is_prime : Nat.Prime fieldSize, proved via a Pratt certificate
  • Fact (Nat.Prime fieldSize) and Field instance
  • NonBinaryField instance (characteristic ≠ 2)

Fast Arithmetic Implementation

• CompPoly/Fields/Mersenne31/Fast.lean (994 lines) introduces a UInt32-backed carrier Fast.Field as a subtype of UInt32 with toNat < fieldSize. It implements add, sub, neg, mul, inv, div, and pow, reducing intermediate UInt32 or UInt64 results via the Mersenne identity 2^31 ≡ 1 mod p.
• Correctness is established via a ring isomorphism ringEquiv : Fast.Field ≃+* Basic.Field (the canonical ZMod model), using toField_injective.field. The toField_* morphism theorems verify the arithmetic.
• A Field instance and instNonBinaryField (showing 2 ≠ 0) are provided.

No sorry or admit placeholders are present in any of the new or modified files.

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	1059
❌ Lines Removed	27

---

Lean Declarations

✏️ Removed: 3 declaration(s)

CompPoly/Fields/Mersenne.lean (3)

• abbrev Field
• def fieldSize : Nat
• theorem is_prime : Nat.Prime fieldSize

✏️ Added: 108 declaration(s)

CompPoly/Fields/Mersenne31/Basic.lean (3)

• abbrev Field
• def fieldSize : Nat
• theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/Mersenne31/Fast.lean (105)

• abbrev Field : Type
• def add (x y : Field) : Field
• def div (x y : Field) : Field
• def inv (x : Field) : Field
• def modulus : UInt32
• def mul (x y : Field) : Field
• def neg (x : Field) : Field
• def ofField (x : Mersenne31.Basic.Field) : Field
• def ofInt (z : Int) : Field
• def ofNat (n : Nat) : Field
• def ofUInt32 (x : UInt32) : Field
• def pow (x : Field) (n : Nat) : Field
• def raw (x : Field) : UInt32
• def ringEquiv : Field ≃+* Mersenne31.Basic.Field where
• def square (x : Field) : Field
• def sub (x y : Field) : Field
• def toField (x : Field) : Mersenne31.Basic.Field
• def toNat (x : Field) : Nat
• instance instAddField : Add Field where
• instance instDivField : Div Field where
• instance instIntCastField : IntCast Field where
• instance instIntSMulField : SMul Int Field where
• instance instInvField : Inv Field where
• instance instMulField : Mul Field where
• instance instNNRatCastField : NNRatCast Field where
• instance instNNRatSMulField : SMul ℚ≥0 Field where
• instance instNatCastField : NatCast Field where
• instance instNatSMulField : SMul Nat Field where
• instance instNegField : Neg Field where
• instance instOneField : One Field where
• instance instPowFieldInt : Pow Field Int where
• instance instPowFieldNat : Pow Field Nat where
• instance instRatCastField : RatCast Field where
• instance instRatSMulField : SMul ℚ Field where
• instance instSubField : Sub Field where
• instance instZeroField : Zero Field where
• private def invExponent : Nat
• private def modulus64 : UInt64
• private def ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) : Field
• private def one : Field
• private def reduceUInt32Lt2Modulus (x : UInt32)
• private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32
• private def reduceUInt64 (x : UInt64)
• private def reduceUInt64Raw (x : UInt64) : UInt32
• private def shift4Mul (acc digit : Field) : Field
• private def zero : Field
• private theorem fieldSize_add_fieldSize_lt_uint32Size :
• private theorem fieldSize_lt_uint32Size : Mersenne31.Basic.fieldSize < UInt32.size
• private theorem fieldSize_mul_fieldSize_lt_two64 :
• private theorem fieldSize_pos : 0 < Mersenne31.Basic.fieldSize
• private theorem modulus64_toNat : modulus64.toNat = Mersenne31.Basic.fieldSize
• private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z)
• private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x
• private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32)
• private theorem reduceUInt32Lt2Modulus_cast (x : UInt32)
• private theorem reduceUInt64Raw_lt (x : UInt64)
• private theorem reduceUInt64Raw_split_toNat (x : UInt64)
• private theorem reduceUInt64_cast (x : UInt64)
• private theorem toField_injective : Function.Injective toField
• private theorem toField_inv_pow (x : Field) :
• private theorem toField_mul_pow (base x y : Field) (m n : Nat)
• private theorem toField_ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) :
• private theorem toField_reduceUInt64 (x : UInt64)
• private theorem toField_shift4Mul (acc digit : Field) :
• private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat)
• private theorem toNat_ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) :
• theorem modulus_toNat : modulus.toNat = Mersenne31.Basic.fieldSize
• theorem ofField_toField (x : Field) :
• theorem raw_eq_val (x : Field) : raw x = x.val
• theorem raw_mk (x : UInt32) (h : x.toNat < Mersenne31.Basic.fieldSize) :
• theorem raw_one : raw (1 : Field) = 1
• theorem raw_zero : raw (0 : Field) = 0
• theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x
• theorem ringEquiv_symm_apply (x : Mersenne31.Basic.Field) : ringEquiv.symm x = ofField x
• theorem toField_add (x y : Field) :
• theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y
• theorem toField_intCast (n : Int) :
• theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹
• theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y
• theorem toField_natCast (n : Nat) :
• theorem toField_neg (x : Field) : toField (-x) = -toField x
• theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x
• theorem toField_nnratCast (q : ℚ≥0) :
• theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n
• theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x
• theorem toField_ofField (x : Mersenne31.Basic.Field) :
• theorem toField_ofInt (z : Int) :
• theorem toField_ofNat (n : Nat) :
• theorem toField_ofUInt32 (x : UInt32) :
• theorem toField_one : toField (1 : Field) = 1
• theorem toField_pow (x : Field) (n : Nat) : toField (pow x n) = toField x ^ n
• theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x
• theorem toField_ratCast (q : ℚ) :
• theorem toField_square (x : Field) : toField (square x) = toField x * toField x
• theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y
• theorem toField_zero : toField (0 : Field) = 0
• theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n
• theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x
• theorem toNat_eq_val_toNat (x : Field) : toNat x = x.val.toNat
• theorem toNat_mk (x : UInt32) (h : x.toNat < Mersenne31.Basic.fieldSize) :
• theorem toNat_ofField (x : Mersenne31.Basic.Field) : toNat (ofField x) = x.val
• theorem toNat_ofNat (n : Nat) :
• theorem toNat_ofUInt32 (x : UInt32) :
• theorem toNat_one : toNat (1 : Field) = 1
• theorem toNat_zero : toNat (0 : Field) = 0

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff implements a significant refactoring/improvement (replacing the single Mersenne.lean file with a structured Mersenne31/ subdirectory containing Basic.lean and Fast.lean). The analysis covers the diff's adherence to the provided guidelines, identifying compliance with most major points (title format, licensing, file/copyright, naming conventions, module layout, proof placement, deprecation handling, imports, documentation structure) but noting specific issues: variable naming inconsistency for hsum_lt_uint32 (should be hsum_lt_uint32Size), missing citation entry in blueprint/src/references.bib for any paper describing the fast reduction algorithm, and a minor style-preference issue regarding leaving non-terminal simp calls unsqueezed. Two time commands discovered two compliance fixes: the simp after toField_div can stay unsqueezed (it's terminal), and there is a correct deprecation alias was added (dominated by the removal).

---

📄 **Per-File Summaries**

• CompPoly.lean: Replaced the single import of CompPoly.Fields.Mersenne with three imports: CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast. This restructures the Mersenne field module from a single file into a subdirectory containing a basic definition file and a fast operations file, improving modularity.
• CompPoly/Fields/Mersenne.lean: The file CompPoly/Fields/Mersenne.lean was deleted, removing the Mersenne31 namespace along with the reducible definition fieldSize : Nat := 2 ^ 31 - 1, the abbreviation Field := ZMod fieldSize, and the theorem is_prime : Nat.Prime fieldSize (proved via the pratt tactic). This eliminates the Mersenne‑31 prime field construction used in Circle STARKs from the project.
• CompPoly/Fields/Mersenne31.lean: Added a new facade module CompPoly/Fields/Mersenne31.lean that imports and re-exports the canonical ZMod model of the Mersenne31 prime field (2^{31} - 1) from CompPoly.Fields.Mersenne31.Basic and the native-word implementation from CompPoly.Fields.Mersenne31.Fast. This module provides a single entry point for users of the Mersenne31 field.
• CompPoly/Fields/Mersenne31/Basic.lean: Added CompPoly/Fields/Mersenne31/Basic.lean, which defines the Mersenne31 prime field 2³¹-1 used in Circle STARKs. It introduces fieldSize as 2^31 - 1, Field as ZMod fieldSize, proves is_prime via a Pratt certificate, and registers Fact (Nat.Prime fieldSize) and a Field instance. It also provides a NonBinaryField instance showing the field has characteristic different from 2.
• CompPoly/Fields/Mersenne31/Fast.lean: This new file (994 lines) introduces Mersenne31.Fast, a UInt32-backed implementation of the Mersenne31 prime field (2^31 - 1). It defines the carrier abbrev Field as the subtype of UInt32 with toNat < fieldSize and provides arithmetic operations (add, sub, neg, mul, inv, div, pow) that reduce intermediate UInt32 or UInt64 results using the Mersenne identity 2^31 ≡ 1 mod p. The file establishes a Field instance via a ring equivalence ringEquiv : Field ≃+* Mersenne31.Basic.Field (the canonical ZMod model) using toField_injective.field, and demonstrates correctness through toField_* morphism theorems. It also provides instNonBinaryField showing 2 ≠ 0. No sorry or admit are present.

---

Last updated: 2026-07-20 08:30 UTC.

[MavenRain]

A couple of things:

1. Consider adding tests for Mersenne31.Fast
2. Mersenne.lean is still referenced in the docs. Consider updating.
3. Consider extracting the four have blocks duplicated between reduceUInt64_cast and reduceUInt64Raw_lt into a private lemma.