feat(fields): add fast Mersenne31 arithmetic by varunthakore · Pull Request #257 · Verified-zkEVM/CompPoly

varunthakore · 2026-06-23T06:46:04Z

No description provided.

github-actions · 2026-06-23T06:47:46Z

🤖 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:

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

dhsorens

Summary

Solid Fast track: Mersenne reduction (not Montgomery) is the right call for 2^31-1, and the toField_* / ringEquiv / inv addition-chain proofs are in good shape.

Blockers before merge: green CI, rebase onto current main, and a #guard test file matching BabyBear/KoalaBear Fast.

Inline notes are the actionable items.

dhsorens · 2026-07-31T11:12:57Z

+  if hxy : x.val ≥ y.val then
+    ⟨x.val - y.val, by
+      have hy_le_x : y.val.toNat ≤ x.val.toNat := by
+        simpa [UInt32.le_iff_toNat_le] using hxy


Build break. CI fails here: simpa leaves hxy : y.val ≤ x.val where the goal wants y.val.toNat ≤ x.val.toNat.

Please rewrite with an explicit UInt32.le_iff_toNat_le (or avoid simpa). This also leaves toField_sub with a sorry warning.

dhsorens · 2026-07-31T11:12:57Z

+-/
+
+namespace Mersenne31
+namespace Basic


Namespace. Prefer namespace Mersenne31 only (like BabyBear/KoalaBear), so the public type is Mersenne31.Field / Mersenne31.fieldSize, not Mersenne31.Basic.Field.

Old Mersenne.lean used Mersenne31.Field — keep that name.

dhsorens · 2026-07-31T11:12:57Z

+
+/-- The Mersenne31 prime `2^31 - 1` as a native `UInt32`. -/
+@[inline]
+def modulus : UInt32 := 2147483647


Nit: use hex for native constants, matching siblings (0x7FFFFFFF / 0x7FFFFFFF for modulus64). Decimal 2147483647 is harder to scan as a Mersenne modulus.

dhsorens · 2026-07-31T11:12:57Z

+  ⟨reduceUInt64Raw x, reduceUInt64Raw_lt x h⟩
+
+/-- Bounded `UInt64` reduction preserves the represented canonical field element. -/
+private theorem reduceUInt64_cast (x : UInt64)


Dup: the bound/have blocks here are copy-pasted from reduceUInt64Raw_lt above. Extract a private lemma for the split-sum bounds and reuse it in both places.

dhsorens · 2026-07-31T11:12:57Z

+/-!
+  # Mersenne31 prime field `2^{31} - 1`
+
+  Facade module for the Mersenne31 field. It re-exports the canonical `ZMod` model


Follow-ups (not in this file, but needed for the PR):

Add tests/CompPolyTests/Fields/Mersenne31/Fast.lean mirroring Koala/Baby #guard coverage (zero/one, wrap, ±, mul, pow, inv, int powers).

Update CompPoly/Fields/README.md (Mersenne.lean → Mersenne31/).

Rebase onto current main (post-feat(fields): add fast KoalaBear/BabyBear arithmetic #258 Montgomery + Lean 4.32).

Optional: thin deprecated CompPoly/Fields/Mersenne.lean re-export so old imports keep working.

varunthakore added 3 commits June 16, 2026 15:27

feat(fields): add Mersenne31 field scaffold

2b0f575

feat(fields): implement fast Mersenne31 arithmetic

251290c

chore(fields): add comments

4d8a983

Merge branch 'master' into mersenne31

5742dfa

This was referenced Jun 26, 2026

[codex] Add Mersenne31 regression tests for PR 257 adrienlacombe/CompPoly#2

Draft

[codex] Add Mersenne31 circle domain skeleton adrienlacombe/CompPoly#3

Draft

test(fields): add Mersenne31 regression coverage #260

Draft

MavenRain approved these changes Jun 28, 2026

View reviewed changes

Merge branch 'master' into mersenne31

8b16d84

dhsorens requested changes Jul 31, 2026

View reviewed changes

Navigation Menu

Uh oh!

feat(fields): add fast Mersenne31 arithmetic - #257

feat(fields): add fast Mersenne31 arithmetic#257
varunthakore wants to merge 5 commits into
Verified-zkEVM:mainfrom
varunthakore:mersenne31

varunthakore commented Jun 23, 2026

Uh oh!

github-actions Bot commented Jun 23, 2026 •

edited

Loading

Uh oh!

MavenRain left a comment

Uh oh!

dhsorens left a comment

Uh oh!

dhsorens Jul 31, 2026

Uh oh!

dhsorens Jul 31, 2026

Uh oh!

dhsorens Jul 31, 2026

Uh oh!

dhsorens Jul 31, 2026

Uh oh!

dhsorens Jul 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

varunthakore commented Jun 23, 2026

Uh oh!

github-actions Bot commented Jun 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Overview

Restructuring

Mathematical Formalization

Fast Arithmetic Implementation

Uh oh!

MavenRain left a comment

Choose a reason for hiding this comment

Uh oh!

dhsorens left a comment

Choose a reason for hiding this comment

Summary

Uh oh!

dhsorens Jul 31, 2026

Choose a reason for hiding this comment

Uh oh!

dhsorens Jul 31, 2026

Choose a reason for hiding this comment

Uh oh!

dhsorens Jul 31, 2026

Choose a reason for hiding this comment

Uh oh!

dhsorens Jul 31, 2026

Choose a reason for hiding this comment

Uh oh!

dhsorens Jul 31, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented Jun 23, 2026 •

edited

Loading