test(fields): extend Mersenne31 regression coverage

[adrienlacombe]

Summary

Extends the Mersenne31 regression coverage added in #257. This branch has been refreshed onto #257 commit 5068d4c.

Changes

• Adds CompPolyTests.Fields.Mersenne31.Instances to check the canonical and fast Field and NonBinaryField instances, plus the canonical primality instance.
• Extends feat(fields): add fast Mersenne31 arithmetic #257's fast arithmetic tests with ringEquiv checks for addition and multiplication.
• Imports the new instance test module from CompPolyTests.

Validation

• lake build CompPolyTests.Fields.Mersenne31.Instances CompPolyTests.Fields.Mersenne31.Fast
• lake test
• ./scripts/lint-style.sh
• git diff --check

./scripts/check-imports.sh also runs, but currently reports an unchanged #257 baseline issue: CompPoly/Fields/Mersenne.lean exists while the generated CompPoly.lean does not export CompPoly.Fields.Mersenne.

Stack note

#257 is still open. GitHub requires this cross-repository PR to target a branch in Verified-zkEVM/CompPoly, and there is no upstream stack branch for #257, so this draft targets main. GitHub's raw diff therefore includes #257 as well as this companion commit.

The additive diff relative to adrienlacombe:pr257-mersenne31-base is now exactly:

• tests/CompPolyTests.lean
• tests/CompPolyTests/Fields/Mersenne31/Fast.lean
• tests/CompPolyTests/Fields/Mersenne31/Instances.lean

[github-actions]

🤖 PR Summary

Test / Regression Coverage

• A new test suite CompPolyTests.Fields.Mersenne31 checks the Basic.Field and Fast.Field Mersenne31 implementations. It verifies that both are fields and NonBinaryField (char ≠ 2), and then runs a comprehensive series of #guard statements exercising the fast arithmetic surface (add, sub, neg, mul, square, Nat/Int pow, inv, div) including edge cases at zero and the modulus boundary. The test module is imported from tests/CompPolyTests.lean.

Infrastructure / CI

• A lake build target CompPolyTests.Fields.Mersenne31 is added; the PR body also confirms lake test, lint-style, and check-imports pass.

Refactoring

• CompPoly.lean replaces its single import of CompPoly.Fields.Mersenne with three narrower imports: CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast, reflecting a reorganization or renaming of the Mersenne field modules.
• A facade file CompPoly/Fields/Mersenne31.lean is added, re-exporting CompPoly.Fields.Mersenne31.Basic and CompPoly.Fields.Mersenne31.Fast so that users can import a single module.

Remarks

• The PR body notes that the GitHub diff is inflated because it includes implementation commits from the upstream PR feat(fields): add fast Mersenne31 arithmetic #257. The additive test diff relative to that PR's base branch consists only of the two test files: tests/CompPolyTests.lean (import line) and tests/CompPolyTests/Fields/Mersenne31.lean. The four non-test files (CompPoly.lean, CompPoly/Fields/Mersenne31.lean, CompPoly/Fields/Mersenne31/Basic.lean, CompPoly/Fields/Mersenne31/Fast.lean) are part of the implementation and not new in this PR.
• No sorry or admit placeholders appear in any of the summarised files.

---

Statistics

Metric	Count
📝 Files Changed	7
✅ Lines Added	1119
❌ 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: 114 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

tests/CompPolyTests/Fields/Mersenne31.lean (6)

• example : (2 : Basic.Field) ≠ 0
• example : Fact (Nat.Prime Basic.fieldSize)
• example : NonBinaryField Basic.Field
• example : NonBinaryField Field
• example : _root_.Field Basic.Field
• example : _root_.Field Field

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff restructures the Mersenne field implementation, replacing the single-file Mersenne.lean with a Mersenne31/ directory containing Basic.lean, Fast.lean, and a facade. The changes largely follow the project's naming and file conventions, but multiple violations of the style guide are present, particularly regarding documentation and line length.

---

📄 **Per-File Summaries**

• CompPoly.lean: The import of CompPoly.Fields.Mersenne is replaced by three imports: CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast. This reflects a reorganization or renaming of the Mersenne field module, splitting it into a base module and submodules for basic and fast operations.
• CompPoly/Fields/Mersenne31.lean: This new file CompPoly/Fields/Mersenne31.lean serves as a facade module for the Mersenne31 field ($2^{31} - 1$). It imports and re-exports the canonical ZMod model from CompPoly.Fields.Mersenne31.Basic and the native-word implementation from CompPoly.Fields.Mersenne31.Fast, providing a single import point for users. No definitions or theorems are declared in this file; it only re-exports existing content.
• CompPoly/Fields/Mersenne31/Basic.lean: Added a new file CompPoly/Fields/Mersenne31/Basic.lean that defines the Mersenne31 prime field 2^{31}-1. It introduces fieldSize as 2^31 - 1, Field as ZMod fieldSize, and proves is_prime via the pratt tactic. It then registers a Fact (Nat.Prime fieldSize) instance, a Field instance for Field, and a NonBinaryField instance with char_neq_2 proved by decide. No sorry or admit are present.
• CompPoly/Fields/Mersenne31/Fast.lean: This 994-line file adds a new Fast submodule in CompPoly/Fields/Mersenne31/ that defines Fast.Field, a UInt32-backed subtype of canonical representatives below 2^31 - 1. It provides the core arithmetic operations (add, sub, neg, mul, square, pow, inv, div), supporting casts (ofNat, toNat, ofField, toField, ofUInt32, ofInt), and corresponding typeclass instances (Zero, One, Add, Sub, Neg, Mul, Inv, Div, NatCast, IntCast, Pow, SMul for ℕ, ℤ, ℚ≥0, ℚ), plus a ringEquiv to the canonical Mersenne31.Basic.Field. A Field instance is transferred via toField_injective.field, and a NonBinaryField instance is provided. Key correctness lemmas (toField_add, toField_mul, toField_inv) prove that each fast operation agrees with the corresponding operation in the canonical field, and the inversion chain computes x^(p-2) using a fixed addition chain. The file is complete; it contains no sorry or admit.
• tests/CompPolyTests.lean: Added an import of CompPolyTests.Fields.Mersenne31, making the Mersenne31 field module available in the test file. This ensures that any tests or definitions related to the Mersenne31 field are included and can be exercised as part of the test suite.
• tests/CompPolyTests/Fields/Mersenne31.lean: This new test file adds regression checks for the Mersenne31 field surfaces (Basic.Field and Fast.Field). It verifies that Basic.Field is a field and a NonBinaryField (by checking char_neq_2), and that Fast.Field is a field and a NonBinaryField. The file then provides a comprehensive suite of #guard statements for the fast surface, testing raw, toNat, toField, and ringEquiv operations, including addition, subtraction, negation, multiplication, squaring, exponentiation (both Nat and Int), inverse, and division, with explicit edge cases for zero and the modulus boundary.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): CompPoly/Fields/Mersenne.lean

---

Last updated: 2026-07-20 09:49 UTC.

[github-actions]

🤖 PR Summary

Summary

This PR adds regression test coverage for the Mersenne31 field implementation, which was originally introduced in upstream PR #257. The field itself (compressed into a subdirectory Mersenne31/) is already present in the repo; this PR's additive changes are confined to the test suite and a corresponding import update.

Test Coverage

• tests/CompPolyTests/Fields/Mersenne31/Fast.lean (new): Exercises the Fast native‑word representation. Checks that toNat and toField produce the expected results for zero, one, addition, subtraction (including underflow), negation, multiplication, exponentiation, and division (inverse and power with negative integer exponent). Also verifies that + and * in the Fast carrier agree with the canonical ZMod model via ringEquiv.
• tests/CompPolyTests/Fields/Mersenne31/Instances.lean (new): Regression checks that Mersenne31 and Mersenne31.Fast satisfy required typeclasses: Fact (Nat.Prime fieldSize), Field, and NonBinaryField. Includes an explicit proof (2 : Mersenne31.Field) ≠ 0 using NonBinaryField.char_neq_2. All proofs are closed by inferInstance or a single exact; no sorry or admit.
• tests/CompPolyTests.lean (modified): Adds two new public imports: CompPolyTests.Fields.Mersenne31.Fast and CompPolyTests.Fields.Mersenne31.Instances, pulling in the two test modules above.

Documentation

• CompPoly/Fields/README.md (modified): Updated to reflect the change from a single Mersenne.lean entry to the multi‑file Mersenne31/ directory structure, listing the new Mersenne31.lean facade, Basic.lean, Fast.lean, and the deprecated Mersenne.lean compatibility shim.

Refactoring / Deprecation

• CompPoly/Fields/Mersenne.lean (modified): Replaced the original definitions with a deprecated compatibility shim (deprecated_module as of 2026‑08‑25). The file now public imports CompPoly.Fields.Mersenne31 and adds a co‑author credit. The original fieldSize, Field, and pratt‑based proof are no longer defined here; they live in the new Basic submodule.
• CompPoly/Fields/Mersenne31.lean (new): Facade module that publicly re‑exports both CompPoly.Fields.Mersenne31.Basic (canonical ZMod model) and CompPoly.Fields.Mersenne31.Fast (native‑word implementation), with an @[expose] section to streamline imports.
• CompPoly.lean (modified): The import CompPoly.Fields.Mersenne was replaced by CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast, updating the project's top‑level import to the new split structure.

Mathematical Formalization (underlying, not additive in this PR)

No changes were made to the formalization itself in this PR; the following files are present as a consequence of the upstream #257 merge but are not new in this PR:

• CompPoly/Fields/Mersenne31/Basic.lean: Defines fieldSize := 2^31 - 1, Field := ZMod fieldSize, and proves primality via a Pratt certificate. Provides NonBinaryField instance.
• CompPoly/Fields/Mersenne31/Fast.lean: Native‑word implementation on UInt32 with verified equivalence to the ZMod model via a ringEquiv. Implements efficient add, sub, neg, mul, square, pow, inv, div using the Mersenne identity. No sorry or admit in this file.

CI / Validation (mentioned in PR body)

The PR body lists lint style, import checking, and lake build / lake test commands, but these are not directly visible in the diffs provided. No CI configuration changes are included in the per‑file summaries.

Note: The PR body acknowledges that because the branch pr257-mersenne31-base is unavailable, GitHub's diff includes the upstream #257 implementation commits as noise. The additive test diff is reported to be confined to the two new test files and the import update in tests/CompPolyTests.lean.

---

Statistics

Metric	Count
📝 Files Changed	9
✅ Lines Added	1145
❌ Lines Removed	20

---

Lean Declarations

✏️ Removed: 3 declaration(s)

CompPoly/Fields/Mersenne.lean (3)

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

✏️ Added: 113 declaration(s)

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

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

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

• 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.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.Field where
• def square (x : Field) : Field
• def sub (x y : Field) : Field
• def toField (x : Field) : Mersenne31.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.fieldSize) : 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 theorem fieldSize_add_fieldSize_lt_uint32Size :
• private theorem fieldSize_lt_uint32Size : Mersenne31.fieldSize < UInt32.size
• private theorem fieldSize_mul_fieldSize_lt_two64 :
• private theorem fieldSize_pos : 0 < Mersenne31.fieldSize
• private theorem modulus64_toNat : modulus64.toNat = Mersenne31.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 reduceUInt64_split_sum_bounds (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.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.fieldSize) :
• theorem modulus_toNat : modulus.toNat = Mersenne31.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.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.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.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.fieldSize) :
• theorem toNat_ofField (x : Mersenne31.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

tests/CompPolyTests/Fields/Mersenne31/Instances.lean (6)

• example : (2 : Field) ≠ 0
• example : Fact (Nat.Prime fieldSize)
• example : NonBinaryField Field
• example : NonBinaryField Field
• example : _root_.Field Field
• example : _root_.Field Field

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• CompPoly.lean: The import CompPoly.Fields.Mersenne was replaced by three imports: CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast. This refactors the Mersenne field module, splitting it into a top-level Mersenne31 namespace with separate Basic and Fast submodules, likely for better organization or to support optimized implementations.
• CompPoly/Fields/Mersenne.lean: This diff replaces the entire contents of CompPoly/Fields/Mersenne.lean with a deprecated compatibility shim: the original local definitions of Mersenne31.fieldSize, Mersenne31.Field, and the is_prime proof using pratt are removed, and the module now public imports CompPoly.Fields.Mersenne31 (the new canonical home) and adds a deprecated_module attribute with a since date of 2026-08-25, instructing users to use the new import path. The changes add co-author credit (Varun Thakore) and a documentation note explaining the module is now a compatibility re-export.
• CompPoly/Fields/Mersenne31.lean: This new facade module CompPoly/Fields/Mersenne31.lean publicly re-exports two submodules: CompPoly.Fields.Mersenne31.Basic (the canonical ZMod (2^31 - 1) model) and CompPoly.Fields.Mersenne31.Fast (a native-word implementation). It also introduces an @[expose] public section that will make the contents of those submodules available without prefix, streamlining downstream use of the Mersenne31 field.
• CompPoly/Fields/Mersenne31/Basic.lean: This new file defines the Mersenne31 prime field $2^{31} - 1$, used in Circle STARKs. It introduces fieldSize as $2^{31} - 1$, Field as an abbreviation for ZMod fieldSize, and proves is_prime via a Pratt certificate. A Fact (Nat.Prime fieldSize) instance enables Mathlib's ZMod.instField for the field structure, and a NonBinaryField instance asserts the field has characteristic different from two (proved by decide).
• CompPoly/Fields/Mersenne31/Fast.lean: This new file (CompPoly/Fields/Mersenne31/Fast.lean) introduces a native‑word implementation of Mersenne‑31 field arithmetic, defining the carrier Fast.Field as a subtype of UInt32 with values below the modulus. It provides efficient operations (add, sub, neg, mul, square, pow, inv, div) that reduce intermediate results using the Mersenne identity 2^31 ≡ 1 (mod p); mul reduces a bounded UInt64 product via a bit‑split adder, and inv implements a fixed Fermat addition chain for x^(p‑2). The file proves that all fast operations agree with the canonical Mersenne31.Field (ZMod model) and establishes a ringEquiv : Fast.Field ≃+* Mersenne31.Field and a full Field instance transferred through toField. No sorry or admit appear in the diff.
• CompPoly/Fields/README.md: The README was updated to document the replacement of the monolithic Mersenne.lean entry with a new multi-file Mersenne31 module structure. Specifically, the old single-line entry for Mersenne.lean (describing it as containing the 2^31 - 1 Circle STARK field) was replaced with four new entries: a Mersenne31.lean facade (re-exporting the canonical ZMod model and the fast native implementation), a Mersenne31/Basic.lean (canonical field model and primality proof), a Mersenne31/Fast.lean (verified UInt32 arithmetic implementation), and a now-deprecated Mersenne.lean (kept as a compatibility re-export for existing imports). This change matters because it brings the documentation into alignment with the actual on-disk file organization after the Mersenne31 field was split into its own subdirectory, ensuring that developers and reviewers can correctly identify which file provides which component of the field implementation.
• tests/CompPolyTests.lean: This change adds two new public imports to the test file: CompPolyTests.Fields.Mersenne31.Fast and CompPolyTests.Fields.Mersenne31.Instances. These imports bring in the fast arithmetic routines and instance definitions for the Mersenne31 field, extending the test coverage to that field alongside the previously imported KoalaBear, binary, and extension field modules.
• tests/CompPolyTests/Fields/Mersenne31/Fast.lean: Added a new file tests/CompPolyTests/Fields/Mersenne31/Fast.lean containing regression tests for the CompPoly.Fields.Mersenne31.Fast module's executable native-word field representation. The test suite checks that toNat and toField computations match expected values for zero, one, addition, subtraction (including underflow), negation, multiplication, exponentiation, and division (including inverse and power with negative integer exponent); it also uses ringEquiv to verify that + and * in the Fast representation match the original Mersenne31.Field. No sorry or admit appear anywhere in the file.
• tests/CompPolyTests/Fields/Mersenne31/Instances.lean: This new file tests/CompPolyTests/Fields/Mersenne31/Instances.lean adds regression-check examples that verify the Mersenne31 and Mersenne31.Fast field types satisfy key typeclass instances: Fact (Nat.Prime fieldSize), Field, and NonBinaryField. It also includes an explicit proof that (2 : Mersenne31.Field) ≠ 0 using NonBinaryField.char_neq_2. No sorry, admit, or unimplemented proofs are present; all examples are closed by inferInstance or a single application of exact. The file ensures these instances remain available and correctly inferred as the project evolves.

---

Last updated: 2026-08-26 08:10 UTC.