feat(fields): fast BN254/BLS12-381/BLS12-377 scalar fields (8x32 Montgomery)

[graikos]

Fast scalar-field arithmetic for BN254, BLS12-381 and BLS12-377. Pure Lean, no externs, no native_decide.

• core 8x32 arithmetic is from @mitschabaude's draft Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta) #274, vendored unchanged - this PR supersedes that draft
• 32-bit limbs in UInt64 words, so macs never overflow
• inversion is Pornin's binary GCD: proof-free candidate, runtime-checked against the proven multiplier, proven Fermat fallback
• runtime defs are zero-import for precompileModules
• proven: the inversion certificate, divstep coefficient bounds, and mac-width safety of the candidate

The early commits are the original 4x64 implementation with C extern tiers; benchmarks for external C showed no significant speedup with only mulhi in C, and a fully external Montgomery/GCD implementation defeats the purpose. Hence, they were dropped in favor of the 8x32 implementation in pure Lean. secp256k1 is excluded (p > 2^255), it
gets a custom reduction separately.

[github-actions]

🤖 PR Summary

featu(fields): fast BN254/BLS12-381/BLS12-377 scalar fields (8x32 Montgomery)

---

Statistics

Metric	Count
📝 Files Changed	26
✅ Lines Added	3076
❌ Lines Removed	173

---

Lean Declarations

✏️ Removed: 9 declaration(s)

CompPoly/Fields/BLS12_377.lean (3)

• abbrev ScalarField
• def scalarFieldSize : Nat
• theorem ScalarField_is_prime : Nat.Prime scalarFieldSize

CompPoly/Fields/BLS12_381.lean (3)

• abbrev ScalarField
• def scalarFieldSize : Nat
• theorem ScalarField_is_prime : Nat.Prime scalarFieldSize

CompPoly/Fields/BN254.lean (3)

• abbrev ScalarField
• def scalarFieldSize : Nat
• theorem ScalarField_is_prime : Nat.Prime scalarFieldSize

✏️ Added: 236 declaration(s)

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

• abbrev ScalarField
• def scalarFieldSize : Nat
• theorem ScalarField_is_prime : Nat.Prime scalarFieldSize

CompPoly/Fields/BLS12_377/Fast.lean (5)

• abbrev ScalarField : Type
• def ofField (x : BLS12_377.ScalarField) : ScalarField
• def ringEquiv : ScalarField ≃+* BLS12_377.ScalarField
• instance instGcdData : GcdData BLS12_377.scalarFieldSize where
• instance instMont64x8Field : Mont64x8Field BLS12_377.scalarFieldSize where

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

• abbrev ScalarField
• def scalarFieldSize : Nat
• theorem ScalarField_is_prime : Nat.Prime scalarFieldSize

CompPoly/Fields/BLS12_381/Fast.lean (5)

• abbrev ScalarField : Type
• def ofField (x : BLS12_381.ScalarField) : ScalarField
• def ringEquiv : ScalarField ≃+* BLS12_381.ScalarField
• instance instGcdData : GcdData BLS12_381.scalarFieldSize where
• instance instMont64x8Field : Mont64x8Field BLS12_381.scalarFieldSize where

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

• abbrev ScalarField
• def scalarFieldSize : Nat
• theorem ScalarField_is_prime : Nat.Prime scalarFieldSize

CompPoly/Fields/BN254/Fast.lean (5)

• abbrev ScalarField : Type
• def ofField (x : BN254.ScalarField) : ScalarField
• def ringEquiv : ScalarField ≃+* BN254.ScalarField
• instance instGcdData : GcdData BN254.scalarFieldSize where
• instance instMont64x8Field : Mont64x8Field BN254.scalarFieldSize where

CompPoly/Fields/Montgomery/Native64x8.lean (44)

• private theorem carry_top_zero {S A B Q c : ℕ} (h : S + 2 ^ 256 * c = A + B)
• private theorem cond_eq_mod {T Q : ℕ} (h : T < 2 * Q) :
• private theorem cond_of_borrow_one {M Q T : ℕ} (h : M + Q = T + 2 ^ 256) (hM : M < 2 ^ 256) :
• private theorem cond_of_borrow_zero {M Q T : ℕ} (h : M + Q = T) (hM : M < 2 ^ 256) :
• private theorem land_mask32 (x : ℕ) : x &&& 4294967295 = x % 4294967296
• private theorem sub_of_borrow_one {A B Q D E c : ℕ} (hD : D + B = A + 2 ^ 256 * 1)
• private theorem sub_of_borrow_zero {A B Q D : ℕ} (h : D + B = A + 2 ^ 256 * 0)
• private theorem toNat_zero : (0 : UInt64).toNat = 0
• theorem Limbs8.ext_of_toNat {x y : Limbs8} (hx : x.Bounded) (hy : y.Bounded)
• theorem Limbs8.toNat_lt {x : Limbs8} (hx : x.Bounded) : x.toNat < 2 ^ 256
• theorem adcLo_lt (x y c : UInt64) : (adcLo x y c).toNat < 2 ^ 32
• theorem adc_spec (x y c : UInt64) (hx : x.toNat < 2 ^ 32) (hy : y.toNat < 2 ^ 32)
• theorem adc_spec_wide (x y c : UInt64) (hx : x.toNat < 2 ^ 33) (hy : y.toNat < 2 ^ 32)
• theorem addLimbs_bounded (a b : Limbs8) : (addLimbs a b).Bounded
• theorem addLimbs_toNat (a b : Limbs8) (ha : a.Bounded) (hb : b.Bounded) :
• theorem add_bounded (q a b : Limbs8) : (add q a b).Bounded
• theorem add_lt (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
• theorem add_toNat (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
• theorem borrow_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 : ℕ}
• theorem carry_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 : ℕ}
• theorem condSub_bounded (q t : Limbs8) (ht : t.Bounded) : (condSub q t).Bounded
• theorem condSub_lt (q t : Limbs8) (hq : q.Bounded) (ht : t.Bounded)
• theorem condSub_toNat (q t : Limbs8) (hq : q.Bounded) (ht : t.Bounded) :
• theorem macLo_lt (t x y c : UInt64) : (macLo t x y c).toNat < 2 ^ 32
• theorem mac_spec (t x y c : UInt64) (ht : t.toNat < 2 ^ 32) (hx : x.toNat < 2 ^ 32)
• theorem montM_lt (s negInv : UInt64) : (montM s negInv).toNat < 2 ^ 32
• theorem montM_toNat (s negInv : UInt64) (hs : s.toNat < 2 ^ 32) (hn : negInv.toNat < 2 ^ 32) :
• theorem neg_bounded (q a : Limbs8) : (neg q a).Bounded
• theorem neg_lt (q a : Limbs8) (hq : q.Bounded) (ha : a.Bounded)
• theorem neg_toNat (q a : Limbs8) (hq : q.Bounded) (ha : a.Bounded)
• theorem ofNat_bounded (n : ℕ) : (ofNat n).Bounded
• theorem ofNat_toNat (n : ℕ) : (ofNat n).toNat = n % 2 ^ 256
• theorem one_bounded : one.Bounded
• theorem one_toNat : one.toNat = 1
• theorem sbbLo_lt (x y b : UInt64) : (sbbLo x y b).toNat < 2 ^ 32
• theorem sbb_spec (x y b : UInt64) (hx : x.toNat < 2 ^ 32) (hy : y.toNat < 2 ^ 32)
• theorem subLimbs_bounded (a b : Limbs8) : (subLimbs a b).Bounded
• theorem subLimbs_spec (a b : Limbs8) (ha : a.Bounded) (hb : b.Bounded) :
• theorem sub_bounded (q a b : Limbs8) : (sub q a b).Bounded
• theorem sub_lt (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
• theorem sub_toNat (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
• theorem sum8_lt {a0 a1 a2 a3 a4 a5 a6 a7 : ℕ} (h0 : a0 < 2 ^ 32) (h1 : a1 < 2 ^ 32)
• theorem zero_bounded : zero.Bounded
• theorem zero_toNat : zero.toNat = 0

CompPoly/Fields/Montgomery/Native64x8Defs.lean (26)

• @[inline] def adcCo (x y c : UInt64) : UInt64
• @[inline] def adcLo (x y c : UInt64) : UInt64
• @[inline] def add (q a b : Limbs8) : Limbs8
• @[inline] def addLimbs (a b : Limbs8) : Limbs8
• @[inline] def condSub (q t : Limbs8) : Limbs8
• @[inline] def macHi (t x y c : UInt64) : UInt64
• @[inline] def macLo (t x y c : UInt64) : UInt64
• @[inline] def mask : UInt64
• @[inline] def montM (s negInv : UInt64) : UInt64
• @[inline] def mul (q : Limbs8) (negInv : UInt64) (a b : Limbs8) : Limbs8
• @[inline] def mulAccum (a : Limbs8) (bi : UInt64) (t : State9) : State9
• @[inline] def mulReduce (q : Limbs8) (negInv : UInt64) (s : State9) : State9
• @[inline] def mulRound (q : Limbs8) (negInv : UInt64) (a : Limbs8) (bi : UInt64)
• @[inline] def neg (q a : Limbs8) : Limbs8
• @[inline] def ofNat (n : Nat) : Limbs8
• @[inline] def sbbBo (x y b : UInt64) : UInt64
• @[inline] def sbbLo (x y b : UInt64) : UInt64
• @[inline] def square (q : Limbs8) (negInv : UInt64) (a : Limbs8) : Limbs8
• @[inline] def sub (q a b : Limbs8) : Limbs8
• @[inline] def subBorrow (a b : Limbs8) : UInt64
• @[inline] def subLimbs (a b : Limbs8) : Limbs8
• @[inline] def toLimbs8 (t : State9) : Limbs8
• @[inline] def zero : State9
• def Bounded (t : State9) : Prop
• def one : Limbs8
• def toNat (t : State9) : Nat

CompPoly/Fields/Montgomery/Native64x8Field.lean (74)

• @[inline] def add (x y : FastField modulus) : FastField modulus
• @[inline] def div (x y : FastField modulus) : FastField modulus
• @[inline] def inv (x : FastField modulus) : FastField modulus
• @[inline] def mul (x y : FastField modulus) : FastField modulus
• @[inline] def neg (x : FastField modulus) : FastField modulus
• @[inline] def ofCanonicalNat (n : ℕ) (h : n < modulus) : FastField modulus
• @[inline] def ofField (x : ZMod modulus) : FastField modulus
• @[inline] def ofInt (modulus : ℕ) [P : Mont64x8Field modulus] (n : Int) :
• @[inline] def ofNat (modulus : ℕ) [P : Mont64x8Field modulus] (n : ℕ) : FastField modulus
• @[inline] def square (x : FastField modulus) : FastField modulus
• @[inline] def sub (x y : FastField modulus) : FastField modulus
• @[inline] def toField (x : FastField modulus) : ZMod modulus
• @[inline] def toLimbs8 (x : FastField modulus) : Limbs8
• @[inline] def toNat (x : FastField modulus) : ℕ
• @[specialize] def pow (x : FastField modulus) (n : ℕ) : FastField modulus
• def FastField (modulus : ℕ) [Mont64x8Field modulus] : Type
• def one (modulus : ℕ) [P : Mont64x8Field modulus] : FastField modulus
• def ringEquiv (modulus : ℕ) [P : Mont64x8Field modulus] :
• def zero (modulus : ℕ) [P : Mont64x8Field modulus] : FastField modulus
• instance instField : _root_.Field (FastField modulus)
• instance instNonBinaryField : NonBinaryField (FastField modulus) where
• private theorem inv_eq_pow {a : ZMod modulus} (ha : a ≠ 0) : a⁻¹ = a ^ (modulus - 2)
• private theorem mul_assoc' (x y z : FastField modulus) : x * y * z = x * (y * z)
• private theorem mul_cast (x y : Limbs8) (hx : x.Bounded) (hy : y.Bounded)
• private theorem ofCanonicalNat_val_cast {n : ℕ} (h : n < modulus) :
• private theorem pow_succ_field (x : FastField modulus) (n : ℕ) : pow x (n + 1) = pow x n * x
• private theorem toField_eq (x : FastField modulus) :
• private theorem val_cast (x : FastField modulus) :
• theorem add_def (x y : FastField modulus) : x + y = FastField.add x y
• theorem div_def (x y : FastField modulus) : x / y = x * y⁻¹
• theorem inv_def (x : FastField modulus) : x⁻¹ = FastField.inv x
• theorem modulus_lt : modulus < 2 ^ 256
• theorem modulus_pos : 0 < modulus
• theorem mul_def (x y : FastField modulus) : x * y = FastField.mul x y
• theorem negInv_mul_q : P.montgomeryNegInv.toNat * P.modulusLimbs.toNat % 2 ^ 32 = 2 ^ 32 - 1
• theorem neg_def (x : FastField modulus) : -x = FastField.neg x
• theorem ofField_toField (x : FastField modulus) : ofField (toField x) = x
• theorem one_def : (1 : FastField modulus) = FastField.one modulus
• theorem q_toNat : P.modulusLimbs.toNat = modulus
• theorem r_ne_zero : ((2 ^ 256 : ℕ) : ZMod modulus) ≠ 0
• theorem ringEquiv_apply {x : FastField modulus} : ringEquiv modulus x = toField x
• theorem ringEquiv_symm_apply {x : ZMod modulus} : (ringEquiv modulus).symm x = ofField x
• theorem square_def (x : FastField modulus) : FastField.square x = x * x
• theorem sub_def (x y : FastField modulus) : x - y = FastField.sub x y
• theorem toField_add (x y : FastField modulus) : toField (x + y) = toField x + toField y
• theorem toField_div (x y : FastField modulus) : toField (x / y) = toField x / toField y
• theorem toField_injective : Function.Injective (toField (modulus
• theorem toField_intCast (n : Int) : toField (n : FastField modulus) = (n : ZMod modulus)
• theorem toField_inv (x : FastField modulus) : toField x⁻¹ = (toField x)⁻¹
• theorem toField_mul (x y : FastField modulus) : toField (x * y) = toField x * toField y
• theorem toField_natCast (n : ℕ) : toField (n : FastField modulus) = (n : ZMod modulus)
• theorem toField_neg (x : FastField modulus) : toField (-x) = -toField x
• theorem toField_nnqsmul (q : ℚ≥0) (x : FastField modulus) : toField (q • x) = q • toField x
• theorem toField_nnratCast (q : ℚ≥0) : toField (q : FastField modulus) = (q : ZMod modulus)
• theorem toField_npow (x : FastField modulus) (n : ℕ) : toField (x ^ n) = toField x ^ n
• theorem toField_nsmul (n : ℕ) (x : FastField modulus) : toField (n • x) = n • toField x

…and 86 more not listed.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff is part of a large contribution that splits the BLS12-377, BLS12-381, and BN254 scalar field modules into Basic and Fast facades, and adds an extensive eight-limb Montgomery implementation (Native64x8 family), plus benchmarks, tests, and CI wiring. I reviewed it against the supplied CompPoly contributing guidelines, focusing on style, naming, module layout, documentation, and process requirements. No critical issues relative to the formal correctness are raised (I am not verifying proofs); the findings below are adherence points and minor style concerns.

Findings from the Review

Adherence to Style and Naming Guidelines

• The core style conventions are followed. New files have proper .lean extensions, headers with copyright/license/authors, module docstrings, 2-space indentation, fun ↦ for binders, and by at line ends. Imports are grouped at file tops. New theorem names use snake_case (e.g., addLimbs_toNat, mulReduce_spec, gcdInner_succ), and new definitions use lowerCamelCase or UpperCamelCase as appropriate.
• Line-length violations. Several .lean source lines exceed the 100-character limit. Notable examples (all in new files within the diff):
  • CompPoly/Fields/Montgomery/Native64x8Inv.lean: line gcdLinearCombMontyRed_lt (f := if signA < 0 then -f0 else f0) exceeds 100 chars.
  • CompPoly/Fields/Montgomery/Native64x8Inv.lean: line have hU' := gcdLinearCombMontyRed_lt (f := if signA < 0 then -f0 else f0) exceeds 100 chars. Other long lines with gcdLinearCombMontyRed_lt and gcdMainLoop_bounded also exceed the limit.
  • CompPoly/Fields/Montgomery/Native64x8Field.lean: lines in ofCanonicalNat arguments, such as the mul_spec invocation containing (Mont64x8Field.negInv_mul_q ...) and the first long mul definition in FastField.mul, are over 100 chars. Recommended to run scripts/lint-style.sh to catch all such lines.
• Operator spacing and line breaks are correct. Operators (:=, +, *, ∧, ↔) have surrounding spaces; operators are placed at end-of-line breaks rather than beginning-of-line (no violations observed).
• Structure and instance syntax. The new Structure-like definitions use where for class/instance fields (e.g., GcdData, Mont64x8Field), matching the preferred style.
• by placement is correct. Tactics are placed after by on the preceding line, with blocks indented.

File and Module Layout

• Compliant with the module layout guidance. Implementation is split into logical modules: zero-import *Defs files (Native64x8Defs, Native64x8InvDefs) for precompileModules, correctness modules (Native64x8, Native64x8Mul, Native64x8Inv, Native64x8Field), and facade files (BLS12_377.lean, BN254.lean, etc.). This follows the existing Montgomery/ pattern.
• CompPoly/Fields/README.md updated. The module documentation table was updated to include the new Basic/Fast files and Native64x8 entries, satisfying the requirement to update docs/wiki/ or module README.md when repo structure changes. Note: the guidelines specifically mention docs/wiki/, though updating the module-level README is acceptable in this project for a modular refactor.
• Minor drift in the README text. The guidelines specify docs/wiki/README.md as the guide for contribution/repo structure; this PR changed CompPoly/Fields/README.md and bench/README.md but did not touch docs/wiki/. If docs/wiki/ documents the fast-field architecture, a corresponding update is recommended for consistency.

Documentation Standards

• Good docstrings are present. Each new declaration and major theorem has a documentation comment (e.g., mulAccum, mulReduce, gcdInner, gcdInvCandidate, invGcdRaw, FastField, ringEquiv). This exceeds the minimum standard.
• Inline comments (--) are used for clarifying multi-step logic, which is acceptable, though they are used more heavily in test files than in the main proof files; the latter rely on docstrings and have blocks.
• Citation usage has minor gaps. The Fast.lean files cite GcdData schedules but do not reference the underlying algorithm (Pornin's binary GCD). The Native64x8InvDefs.lean docstring does not include a citation key or a ## References section for the algorithm paper (eprint 2020/972) it is based on.
• Recommendation: Add a ## References section to CompPoly/Fields/Montgomery/Native64x8InvDefs.lean (or the parent Native64x8Inv.lean) following the citation standard (e.g., [Por20]) and add the corresponding BibTeX entry to blueprint/src/references.bib. Ensure the inline README.md link (which currently uses [eprint 2020/972](https://eprint.iacr.org/2020/972)) is migrated to the citation key format.

PR Title and Description (Process)

• Not in the diff, so not assessed. The diff contains only code changes, not the PR description/title. It is assumed that the required feat, doc, etc. prefix and imperative subject are present in the PR itself. This cannot be verified from the diff alone.

Deprecation Policy and Compatibility

• The refactor is backward-compatible. The old BLS12_377.lean, BLS12_381.lean, and BN254.lean re-export the same definitions from the new Basic modules, so downstream code will continue to see the same namespace and declarations (e.g., BLS12_377.ScalarField, BLS12_377.scalarFieldSize, BLS12_377.ScalarField_is_prime). No deprecated aliases are required.
• The refactor is behaviour-preserving in terms of the canonical field definitions; only the scalarFieldSize literal was changed from decimal to hexadecimal representation (e.g., in BLS12_377/Basic.lean). The previous decimal value and new hex value are identical (e.g., 0x12ab655e... equals the old 844446...), so this is purely cosmetic and does not need a changelog flag.

Test Coverage

• Good use of #guard tests covering the added fast-field operations, round trips, inversions, and agreement with the canonical ZMod model. This aligns with the test type conventions.
• Minor style point: The test files contain numerous -- comments explaining each #guard. These are helpful but slightly verbose; they are not a violation.

No Blocking Issues

No violations of the hard-and-fast rules (e.g., banned syntax, incorrect file naming, missing module headers, incorrect import grouping) were found. The only concrete actionable items are the line-length violations and the missing citation entry for the inversion algorithm.

---

📄 **Per-File Summaries**

• .github/workflows/lean_action_ci.yml: In .github/workflows/lean_action_ci.yml, the list of test benchmarks in the env block was extended by appending three new entries — univariate-dense-bls12-381 and univariate-dense-bls12-377 to the univariate-dense-* group, and fields-mont64x8-bn254-inv, fields-mont64x8-bls12-381-inv, and fields-mont64x8-bls12-377-inv to the fields-* group — so CI will now cover these dense univariate evaluation and Montgomery field inversion test cases in its standard run.
• CompPoly.lean: Added public imports for new field modules: BLS12_377.Basic, BLS12_377.Fast, BLS12_381.Basic, BLS12_381.Fast, BN254.Basic, BN254.Fast, and several Montgomery 64×8 arithmetic modules (Native64x8, Native64x8Defs, Native64x8Field, Native64x8Inv, Native64x8InvDefs, Native64x8Mul). These imports expose the basic and optimized field implementations for BLS12-377, BLS12-381, and BN254 curves, as well as new Montgomery multiplication/inversion support for 64-bit × 8-limb representations. No other changes or sorrys present.
• CompPoly/Fields/BLS12_377.lean: The file was refactored from a self-contained definition of the BLS12-377 scalar field (including scalarFieldSize, the ScalarField abbreviation, the ScalarField_is_prime primality proof using a Pratt certificate, and the Fact and Field instances) into a facade module that re-exports CompPoly.Fields.BLS12_377.Basic and CompPoly.Fields.BLS12_377.Fast. The original inline code is removed, and the module documentation now describes the new role. This change modularizes the field implementation by separating the canonical ZMod model from a native-word Montgomery implementation.
• CompPoly/Fields/BLS12_377/Basic.lean: This new file CompPoly/Fields/BLS12_377/Basic.lean introduces the CompPoly module BLS12_377, defining the scalar prime field for the BLS12-377 curve. It provides scalarFieldSize (a concrete 253-bit natural number), the abbreviation ScalarField as ZMod scalarFieldSize, and a proof ScalarField_is_prime that scalarFieldSize is prime using a Pratt certificate and the auxiliary PrattCertificate' API. A Fact instance for primality and a Field instance for ScalarField are also derived.
• CompPoly/Fields/BLS12_377/Fast.lean: This file introduces a new module CompPoly.Fields.BLS12_377.Fast providing a native eight-limb Montgomery implementation of the BLS12-377 scalar field. It defines instGcdData with the binary-GCD inverse schedule (final rounds = 39, initU as a 32-bit-limb vector), instMont64x8Field with the field prime, modulus limbs, rModModulus, r2ModModulus, and montgomeryNegInv constants, an abbrev ScalarField for the fast carrier type, a conversion function ofField from the canonical field, and a ringEquiv ring equivalence between the fast and canonical representations.
• CompPoly/Fields/BLS12_381.lean: The file CompPoly/Fields/BLS12_381.lean was refactored from a monolithic module that defined the scalar field size, proved its primality using a Pratt certificate, and declared the ScalarField type and field instance, to a facade module that re-exports the canonical ZMod model from CompPoly.Fields.BLS12_381.Basic and the native-word Montgomery implementation from CompPoly.Fields.BLS12_381.Fast. The previous definitions (including scalarFieldSize, ScalarField, ScalarField_is_prime, and the Fact and Field instances) are no longer present in this file, having been moved to the new submodules. The module now also lists Georgios Raikos as an additional author.
• CompPoly/Fields/BLS12_381/Basic.lean: Adds a new file Basic.lean defining the BLS12-381 scalar prime field. It introduces the definable constant scalarFieldSize (the 255-bit prime 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001), an abbreviation ScalarField as ZMod scalarFieldSize, and a theorem ScalarField_is_prime that proves Nat.Prime scalarFieldSize using a Pratt primality certificate and factorization into thirteen prime-power factors (including 2^32, 906349^2, and 254760293^2). Two instances are provided: a Fact giving Nat.Prime scalarFieldSize and an instField for ScalarField.
• CompPoly/Fields/BLS12_381/Fast.lean: This new file (CompPoly/Fields/BLS12_381/Fast.lean) introduces a native eight-limb Montgomery implementation of the BLS12-381 scalar field. It provides the instGcdData instance with a binary-GCD inverse schedule (finalRounds and initU), the instMont64x8Field instance supplying the field constants (prime, modulusLimbs, rModModulus, r2ModModulus, montgomeryNegInv), an abbrev ScalarField for the fast field carrier type, and two conversion functions — ofField (from the canonical BLS12_381.ScalarField into Montgomery form) and ringEquiv (a ring equivalence between the fast and canonical representations). No sorry or admit appear in the added code.
• CompPoly/Fields/BN254.lean: This change refactors CompPoly/Fields/BN254.lean from a self-contained definition of the BN254 scalar field (including scalarFieldSize, ScalarField, and a Pratt-certificate proof ScalarField_is_prime together with the corresponding Fact and Field instances) into a facade module that publicly re-exports CompPoly.Fields.BN254.Basic (the canonical ZMod model) and CompPoly.Fields.BN254.Fast (a native-word Montgomery implementation). The original definitions are removed from this file, and the module docstring now describes it as a re-export facade. No sorry or admit is introduced in the diff.
• CompPoly/Fields/BN254/Basic.lean: This new file, CompPoly/Fields/BN254/Basic.lean, introduces the BN254 scalar prime field from the alt_bn128 curve (per EIP-196). It defines scalarFieldSize as the 254-bit prime 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001, introduces ScalarField as ZMod scalarFieldSize, and proves ScalarField_is_prime via a Pratt certificate (using PrattCertificate'.out and .prime/.split with reduce_mod_char tactics). It then registers a Fact (Nat.Prime scalarFieldSize) instance and a Field ScalarField instance. The proof is fully completed with no sorry or admit; notable details include the factorization of the prime into 2^28 * 3^2 * 13 * 29 * 983 * 11003 * 237073 * 405928799 * 1670836401704629 * 13818364434197438864469338081, with nested Pratt certificates for the two large composite cofactors.
• CompPoly/Fields/BN254/Fast.lean: This new file CompPoly/Fields/BN254/Fast.lean introduces a fast, eight-limb (32-bit-limb) Montgomery representation of the BN254 scalar field. It instantiates GcdData and Mont64x8Field for BN254.scalarFieldSize, providing the concrete constants (divstep schedule, modulus limbs, r, r², and Montgomery negative inverse) needed for Montgomery arithmetic. It defines ScalarField as the abbreviation FastField BN254.scalarFieldSize, and provides ofField to convert from the canonical BN254.ScalarField into this fast form, plus a ring equivalence ringEquiv : ScalarField ≃+* BN254.ScalarField. The file contains no sorry or admit.
• CompPoly/Fields/Montgomery/Native64x8.lean: This new file CompPoly/Fields/Montgomery/Native64x8.lean proves the correctness of modular arithmetic operations on Limbs8 (eight 32-bit limbs in UInt64 words) for a modulus below 2^255. It adds the theorems condSub_toNat, add_toNat, sub_toNat, and neg_toNat, each with an accompanying <op>_lt bound lemma and _bounded property, establishing that conditional subtraction, addition, subtraction, and negation produce the correct reduced result modulo q. The proofs rely on the ad-hoc helper specifications adc_spec, adc_spec_wide, sbb_spec, mac_spec, and montM_toNat (each giving existential toNat decompositions), the eight-limb Limbs8 lemmas zero_bounded/zero_toNat/one_bounded/one_toNat/ofNat_bounded/ofNat_toNat, the telescoping chain lemmas carry_chain_sum and borrow_chain_sum, and private auxiliary lemmas cond_of_borrow_zero, cond_of_borrow_one, cond_eq_mod, carry_top_zero, sub_of_borrow_zero, sub_of_borrow_one, land_mask32, and toNat_zero. No sorries or admits appear.
• CompPoly/Fields/Montgomery/Native64x8Defs.lean: This new file adds the runtime definitions for eight-limb Montgomery arithmetic, split out from CompPoly.Fields.Montgomery.Native64x8 with zero imports for precompileModules compatibility. It defines the Limbs8 structure (eight 32-bit limbs), the State9 accumulator structure (nine limbs), and low-level word helpers (mask, adcLo, adcCo, sbbLo, sbbBo, macLo, macHi, montM). It provides limbwise addition/subtraction with carry/borrow (addLimbs, subLimbs, subBorrow), conditional subtraction with modular addition/subtraction/negation (condSub, add, sub, neg), and the CIOS multiplication pipeline (mulAccum, mulReduce, mulRound, mul, square). The Bounded predicates and zero/one/ofNat/toNat conversions are also included; all correctness proofs are in the sibling module that imports this file.
• CompPoly/Fields/Montgomery/Native64x8Field.lean: Added the new file CompPoly/Fields/Montgomery/Native64x8Field.lean, which implements fast eight-limb Montgomery field arithmetic for prime moduli below 2^255. It defines the Mont64x8Field typeclass (holding per-field constants like modulusLimbs, rModModulus, r2ModModulus, montgomeryNegInv), the FastField carrier subtype of Limbs8 with boundedness and value constraints, and all field operations (add, sub, neg, mul, square, pow, inv, div) along with conversions (toField, toNat, ofCanonicalNat, ofField, ofNat, ofInt). The correctness is established via toField — a ring isomorphism FastField modulus ≃+* ZMod modulus — and the @[simp] theorems toField_add, toField_mul, toField_inv, etc. Finally, instField and instNonBinaryField are provided, transferring the field structure from ZMod.
• CompPoly/Fields/Montgomery/Native64x8Inv.lean: This new file CompPoly/Fields/Montgomery/Native64x8Inv.lean proves the correctness of the GCD-based field inversion for eight-limb Montgomery fields. It establishes the bound gcdInner_natAbs_le_31 for divstep coefficients, uses it to prove gcdLinearCombMontyRed_lt that the Montgomery linear combination stays canonical, and then proves gcdMainLoop_bounded and gcdFinalChunks_lt to maintain bounds throughout the main loop. The file also proves montPow_eq_mul_pow and montPow_eq_inv for the Fermat fallback, and then invGcdRaw_eq_inv to show that the raw candidate (or the fallback) computes the field inverse. Finally, it provides the proof-carrying wrapper FastField.invGcd and shows invGcd_eq_inv.
• CompPoly/Fields/Montgomery/Native64x8InvDefs.lean: This new file (CompPoly/Fields/Montgomery/Native64x8InvDefs.lean) adds a Mathlib-free runtime implementation of the Pornin binary-GCD inverse candidate for eight-limb (Limbs8) Montgomery arithmetic. It defines the GcdData typeclass (carrying per-field schedule finalRounds and initU with decide-based proofs) and the core computational functions: gcdBitLen, gcdInner, gcdLimb, gcdNumBits, gcdApprox, gcdAdd9/gcdSub9, gcdLinearCombDiv/gcdLinearCombMontyRed, gcdMainLoop, gcdFinalChunks, gcdInvCandidate, montPow, and invGcdRaw. The invGcdRaw function attempts the GCD candidate and falls back to Fermat exponentiation (montPow) if the candidate does not verify. No sorry or admit appear.
• CompPoly/Fields/Montgomery/Native64x8Mul.lean: This new file adds the full correctness proof of eight-limb CIOS Montgomery multiplication (mul) in the Montgomery.Native64x8 namespace. It introduces three main specification theorems (mulAccum_spec, mulReduce_spec, mulRound_spec) that describe the accumulation and reduction steps and the round invariant, together with the top-level mul_spec stating that mul returns a bounded result less than q and satisfies the Montgomery congruence 2^256 * ⟦mul q negInv a b⟧ ≡ ⟦a⟧·⟦b⟧ [MOD q.toNat]. Several private helper lemmas (sum8_mul, mul_sum8, Limbs8.toNat_mod, montM_low_zero, round_bound, accum_assemble, reduce_assemble, fold8, mul_finish) support the reasoning. The file is complete with no sorry or admit.
• CompPoly/Fields/README.md: The file expands the table of contents to document a new set of modules implementing eight-limb 64-bit Montgomery arithmetic and inversion for large prime fields. Specifically, it adds entries for BLS12_377, BLS12_381, and BN254 each split into a Basic.lean, a Fast.lean (which provides Mont64x8Field and GcdData constants, ScalarField, and ringEquiv), and a facade .lean file re-exporting those. It also adds six new Montgomery modules (Native64x8Defs.lean, Native64x8.lean, Native64x8Mul.lean, Native64x8Field.lean, Native64x8InvDefs.lean, Native64x8Inv.lean) covering runtime definitions, word-level correctness proofs for addition/subtraction/negation and CIOS multiplication, the Mont64x8Field class and its canonical-field bridge for moduli below 2^255, and correctness of a binary-GCD inversion routine (citing eprint 2020/972). This matters because it documents the addition of verified fast field arithmetic targeting larger 253–255 bit prime fields previously listed only as monolithic single-module placeholders, and makes the supported field family explicit.
• bench/CompPolyBench/Fields/Montgomery.lean: This new file adds scalar-field inversion benchmarks for the eight-limb Montgomery fields of BN254, BLS12-381, and BLS12-377. It defines scalarInvShape ("256 random elements"), montgomeryInvGroupInfos (group metadata for the three curves), a runScalarInv helper parameterized by modulus and budgets that times three implementations on shared inputs—ZMod's inv (xgcd), invGcd (binary GCD), and inv (Fermat) on FastField—with cross-checked checksums, plus individual runners runBn254ScalarInv, runBls12_381ScalarInv, and runBls12_377ScalarInv using per-curve budgets via BenchPreset.selectNat. Finally, montgomeryInvTasks registers these runners as BenchTask entries. The diff contains no sorry or admit.
• bench/CompPolyBench/Setup.lean: The diff adds a public import CompPolyBench.Fields.Montgomery line to expose the Montgomery field benchmarks, and appends montgomeryInvTasks to the list of tasks in allTasks, thereby registering Montgomery inversion as a new benchmark group alongside the existing groups.
• bench/CompPolyBench/Univariate/Basic.lean: This change extends the univariate benchmarking suite to cover two additional elliptic-curve fields: BLS12‑381 and BLS12‑377. It adds public imports for CompPoly.Fields.BLS12_381 and CompPoly.Fields.BLS12_377, defines new private conversion and checksum helpers (bls12_381FastArray, checksumBls12_381Fast, bls12_377FastArray, checksumBls12_377Fast), and introduces private benchmark runners (runBls12_381UnivariateDense, runBls12_377UnivariateDense) that call runDenseUnivariateWithFast with the new field’s parameters. The existing univariateBasicGroupInfos, univariateBasicTasks, and the reworked runBn254UnivariateDense are also updated to register these new benchmark groups/tasks and to use the WithFast helper infrastructure (which includes zmodArray and size‑selection lambdas) instead of the old direct runDenseUnivariateZMod call.
• bench/README.md: The bench/README.md documentation was updated to reflect that scalar-field inversion is now a measured category (citing fields-mont64x8-*-inv with three algorithmic variants: extended Euclid, checked binary GCD, and Fermat) and to expand the list of prime-field groups that run against both ZMod and Montgomery representations, adding univariate-dense-bn254, univariate-dense-bls12-381, and univariate-dense-bls12-377 alongside the existing KoalaBear and BabyBear entries. The phrasing of the paragraph describing which groups use the dual representation was also reworded from "Small-prime groups run each implementation" to "Some groups run each implementation" to align with the broader coverage.
• tests/CompPolyTests.lean: In tests/CompPolyTests.lean, the import list is reordered and extended: the Bivariate.Kronecker and Bivariate.Factor imports are swapped in order, and three new Fast field-arithmetic modules for BLS12_377, BLS12_381, and BN254 are added. This broadens the compiled test surface to include the recently added fast field implementations, ensuring they are type-checked as part of the test suite. No theorems or definitions are modified in this file, and no sorry or admit is introduced.
• tests/CompPolyTests/Fields/BLS12_377/Fast.lean: This new test file (tests/CompPolyTests/Fields/BLS12_377/Fast.lean) adds #guard regression checks for the executable eight-limb Montgomery representation of the BLS12-377 scalar field provided by CompPoly.Fields.BLS12_377.Fast. The checks verify: stored Montgomery residues for zero and one; numeric literal round trips with modulus reduction; addition, subtraction, negation, multiplication, squaring, and exponentiation (including agreement with the canonical BLS12_377.ScalarField model via .toField); Fermat inversion and division (with 0⁻¹ = 0); and the checked binary-GCD inversion (invGcd) — ensuring it matches the Fermat inverse and that its raw candidate equals gcdInvCandidate. A direct montPow call exercises the Fermat fallback path. The file imports CompPoly.Fields.BLS12_377.Fast and opens BLS12_377 and Montgomery.Native64x8; it uses set_option maxRecDepth 4000. No sorry or admit are present.
• tests/CompPolyTests/Fields/BLS12_381/Fast.lean: Added a new test file tests/CompPolyTests/Fields/BLS12_381/Fast.lean containing regression checks for the executable eight-limb Montgomery representation of the BLS12-381 scalar field (CompPoly.Fields.BLS12_381.Fast). The file exercises stored residues for 0 and 1, literal round trips via toNat, addition (with wraparound), subtraction (with borrow), negation, multiplication, squaring, exponentiation (including agreement with the canonical BLS12_381.ScalarField via toField), Fermat inversion, division, and the checked binary-GCD inversion (invGcd) compared to the Fermat inverse and to a raw candidate computed by gcdInvCandidate; it also exercises the montPow fallback. All checks are concrete #guard statements; no sorry or admit are present.
• tests/CompPolyTests/Fields/BN254/Fast.lean: This new file adds regression tests for the fast eight-limb Montgomery representation of the BN254 scalar field (CompPoly.Fields.BN254.Fast). It checks that stored Montgomery residues, numeric literal round trips, addition (with and without wraparound), subtraction, negation, multiplication, squaring, exponentiation, Fermat inversion, division, and the checked binary-GCD inversion (invGcd) all produce correct values, and that exponentiation and inversion agree with the canonical BN254.ScalarField via toField. A direct test of the Fermat fallback (montPow) is also included. No proofs or sorrys appear; all checks are compile-time #guard assertions.

---

Last updated: 2026-08-05 11:05 UTC.

[mitschabaude]

should there be benchmarks as well?

[mitschabaude]

is there no performance overhead from this well-founded recursion?

[graikos]

No, the WF overhead is specialized away by the compiler in this case, I verified in the emitted IR/C. The args are unpacked and since it's a tail call, it's compiled as a loop. Either way this is only the fallback path for inv of x=0 or if the candidate inverse from Pornin's GCD is wrong (which shouldn't be), so not the hot path.

[graikos]

There are no benchmarks in the PR right now, but maybe it's a good idea to add them, yes

[mitschabaude]

great!

[dhsorens]

this looks great, thank you @graikos and @mitschabaude !