test(fields): add Mersenne31 regression coverage by adrienlacombe · Pull Request #260 · Verified-zkEVM/CompPoly

adrienlacombe · 2026-06-26T17:35:43Z

Summary

Adds a small regression-test layer on top of #257's Mersenne31 implementation.

Changes

Adds CompPolyTests.Fields.Mersenne31.
Checks the canonical Mersenne31.Basic prime, field, and NonBinaryField instances.
Checks the Mersenne31.Fast field surface and representative/canonical conversion behavior for a few arithmetic paths.
Imports the test module from CompPolyTests.

Validation

lake build CompPolyTests.Fields.Mersenne31
lake build CompPolyTests
./scripts/lint-style.py tests/CompPolyTests/Fields/Mersenne31.lean
./scripts/lint-style.sh
./scripts/check-imports.sh
lake test

Stack note

This PR is intended as companion regression coverage for #257. The upstream repository does not currently have the fork PR's base branch pr257-mersenne31-base, and I do not have permission to push that branch to Verified-zkEVM/CompPoly, so this draft is temporarily opened against master. As a result, GitHub's raw diff includes the #257 implementation commits in addition to this PR's two test-file changes.

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

tests/CompPolyTests.lean
tests/CompPolyTests/Fields/Mersenne31.lean

Add guards for positive subtraction, negation, square, power edge cases, division, inverse products, int powers, and ringEquiv on multiplication. Use a flat Mersenne31.Fast namespace consistent with KoalaBear.Fast tests. Co-authored-by: Cursor <cursoragent@cursor.com>

github-actions · 2026-06-26T17:37:28Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: [codex] Add Mersenne31 regression tests for PR 257

Mathematical Formalization

Formalizes the Mersenne-31 prime field ($2^{31}-1$) using both a canonical ZMod representation and an optimized native word (UInt32/UInt64) implementation.
Proves primality for $2^{31}-1$ using Pratt certificates.
Introduces a NonBinaryField instance required for Circle STARK protocols.
Implements optimized arithmetic in the Fast module, featuring bit-shifted multiplication and a Fermat addition chain for inversion, with formal proofs of equivalence to the ZMod model.
All proofs are complete; no sorry or admit placeholders are present.

Quality Assurance & Regression Testing

Establishes tests/CompPolyTests/Fields/Mersenne31.lean to validate field arithmetic correctness.
Employs #guard statements and example instances to verify that optimized native operations mirror canonical ZMod behavior.
Integrates field tests into the global CompPolyTests suite for CI validation.

Refactoring & Architecture

Reorganizes the field directory by replacing Mersenne.lean with a specialized Mersenne31 module hierarchy.
Implements a facade in CompPoly/Fields/Mersenne31.lean to re-export internal implementations via a centralized API.
Updates the top-level CompPoly.lean to reflect the new module structure.

Note

The draft summary details a comprehensive field implementation and library refactoring, which contradicts the PR title and body characterizing this change strictly as a regression-test layer.

Statistics

Metric	Count
📝 Files Changed	7
✅ Lines Added	1119
❌ Lines Removed	27

Lean Declarations

✏️ **Removed:** 3 declaration(s)

abbrev Field in CompPoly/Fields/Mersenne.lean
def fieldSize : Nat in CompPoly/Fields/Mersenne.lean
theorem is_prime : Nat.Prime fieldSize in CompPoly/Fields/Mersenne.lean

✏️ **Added:** 114 declaration(s)

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

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

Style and Naming Guidelines

Copyright Year: Files CompPoly/Fields/Mersenne31/Fast.lean (line 2) and tests/CompPolyTests/Fields/Mersenne31.lean (line 2) use an incorrect future year 2026. This should be updated to 2024 (or the current year) to adhere to the standard file header format.
Empty Lines in Proofs: Several theorems in CompPoly/Fields/Mersenne31/Fast.lean contain empty lines within tactic blocks, violating the project guideline to avoid empty lines inside definitions or proofs. Key instances include:
- toField_inv_pow (lines 606, 610, 615, 620, 625, 630, 635, 640)
- toField_pow (line 673)

Pull Request Guidelines

Repository Structure: This PR introduces a new directory structure CompPoly/Fields/Mersenne31/ and reorganizes existing field modules. According to the guidelines, changes to the repository structure should be accompanied by an update to the corresponding page in docs/wiki/. No such updates were found in this diff.
Blueprints: As this contribution introduces a substantial new implementation (native-word optimized field arithmetic), contributors are encouraged to develop or reference a blueprint/strategy discussion in an issue prior to merging.

Progress and Framework

Consolidation: The PR successfully transitions the Mersenne31 definition from a standalone file to a modular hierarchy consisting of a canonical ZMod model (Basic.lean) and an optimized UInt32 implementation (Fast.lean).
Verification: The new Fast implementation is well-documented with docstrings for all major definitions and is accompanied by a suite of regression tests in tests/CompPolyTests/Fields/Mersenne31.lean that verify its correctness against the canonical model.

📄 **Per-File Summaries**

CompPoly.lean: This change updates the imports in CompPoly.lean to replace the generic Mersenne field module with specialized Mersenne31 implementations, including basic and optimized versions. The modification refines the library's field dependencies without introducing new theorems or sorry placeholders in this file.
CompPoly/Fields/Mersenne.lean: This change deletes the CompPoly/Fields/Mersenne.lean file, which contained the definitions for the Mersenne prime field $2^{31}-1$ and a primality proof for its field size.
CompPoly/Fields/Mersenne31.lean: This new file acts as a facade module for the Mersenne-31 prime field, re-exporting both the canonical ZMod representation and the optimized native-word implementation. It provides module-level documentation and a central entry point for the field's definitions without introducing new theorems, proofs, or any 'sorry' placeholders.
CompPoly/Fields/Mersenne31/Basic.lean: This new file defines the Mersenne 31 prime field ($2^{31} - 1$) and establishes its fundamental algebraic properties, including a Pratt-certificate-based primality proof and instances for its field structure. It also introduces a NonBinaryField instance to verify that the field characteristic is not two, supporting its application in Circle STARKs.
CompPoly/Fields/Mersenne31/Fast.lean: This file introduces a performance-optimized implementation of the Mersenne-31 field using UInt32 and UInt64 native word arithmetic. It defines core field operations—including multiplication via bit-shifting and inversion via an optimized Fermat addition chain—alongside a complete Field instance and proofs of equivalence to the canonical ZMod model. No sorry or admit placeholders are used in the implementation.
tests/CompPolyTests.lean: This change expands the test suite by adding an import for the Mersenne31 field module, likely to include tests related to this specific field implementation.
tests/CompPolyTests/Fields/Mersenne31.lean: This file introduces regression tests for the Mersenne31 field implementations, verifying core field properties and arithmetic operations for both canonical and optimized versions. It utilizes example instances and #guard statements to ensure correctness and equivalence between implementations, with no sorry placeholders.

Last updated: 2026-06-26 17:37 UTC.

varunthakore and others added 6 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

Add Mersenne31 field regression tests

456531b

adrienlacombe changed the title ~~[codex] Add Mersenne31 regression tests for PR 257~~ test(fields): add Mersenne31 regression coverage Jun 26, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

test(fields): add Mersenne31 regression coverage#260

test(fields): add Mersenne31 regression coverage#260
adrienlacombe wants to merge 6 commits into
Verified-zkEVM:masterfrom
adrienlacombe:feat/pr257-mersenne31-tests

adrienlacombe commented Jun 26, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 26, 2026

Style and Naming Guidelines

Pull Request Guidelines

Progress and Framework

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

adrienlacombe commented Jun 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Changes

Validation

Stack note

Uh oh!

github-actions Bot commented Jun 26, 2026

🤖 PR Summary

Mathematical Formalization

Quality Assurance & Regression Testing

Refactoring & Architecture

Style and Naming Guidelines

Pull Request Guidelines

Progress and Framework

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

adrienlacombe commented Jun 26, 2026 •

edited

Loading