feat(fields): add fast Goldilocks arithmetic

[varunthakore]

No description provided.

[github-actions]

🤖 PR Summary

Overview

This PR adds a complete, verified, high-performance implementation of the Goldilocks prime field ZMod (2^64 - 2^32 + 1) to the CompPoly project. The work is structured in layers, from a canonical mathematical model through to an optional natively-backed fast path, all accompanied by extensive correctness proofs and regression tests.

Mathematical Formalization

• CompPoly/Fields/Goldilocks/Basic.lean (new): defines the Goldilocks prime field in namespace Goldilocks.Basic. Provides fieldSize (a reducible definition for the modulus), the abbreviation Field for ZMod fieldSize, a theorem is_prime proved via pratt, and derived Fact and Field instances. Also supplies a NonBinaryField instance (characteristic ≠ 2).
• CompPoly/Fields/Goldilocks.lean (refactored): changed from a self-contained definition to a facade that re-exports Basic and Fast submodules.

Proof Completion (no sorries added)
All new theorems across the PR are fully proved. No sorry or admit appear in any added file.

Protocols / Soundness

• Fast arithmetic (verified): CompPoly/Fields/Goldilocks/Fast/ contains a UInt64-backed subtype carrier and its full suite of operations (add, neg, sub, mul, square, squareN, pow, inv, div, conversions, scalar multiplication, etc.). Each operation is defined using reduction primitives (wideMul, reduceUInt64Raw, etc.) whose correctness is proved in:
  • Reduction.lean – raw UInt64 kernels with lemmas showing results are below the modulus and their cast to Goldilocks.Basic.Field equals the field operation.
  • Internal.lean – low-level lemmas about UInt64 arithmetic (subtraction with borrow, overflow correction, limb splitting, 64×64 product decomposition), all proved by dec_trivial or explicit arithmetic.
  • Theorems.lean – high-level correctness: every Fast operation (add, mul, square, squareN, pow, inv, div, etc.) agrees with the ZMod operation via the toField embedding. Also proves toField is injective, a ring homomorphism, and a homomorphism for NSMul, ZSMul, NPow, ZPow, NNRatCast, RatCast, etc.
• Field instance transfer: CompPoly/Fields/Goldilocks/Fast/Field.lean provides ringEquiv : Field ≃+* Goldilocks.Basic.Field, then transfers the instField, instCommRing, and instNonBinaryField instances via the injective homomorphism. All proofs are provided.
• Fast extension (trusted native boundary): CompPoly/Fields/Goldilocks/FastExt.lean declares two @[extern] opaque primitives (mulHi, goldilocksMul) backed by C code in native/goldilocks_native.c. These provide an opt-in, faster path. The module defines mulWithMulHi, mulNative, squareWithMulHi, squareNative, squareNNative, invNative, and divNative using these primitives. Crucially, this native code is not verified – only the Lean-level types are checked. The default verified arithmetic is unchanged.

Infrastructure / CI

• lakefile.lean: adds a build step extern_lib for the native C library (goldilocks_native), links it into all existing lean_lib targets, and introduces a new lean_exe target CompPolyGoldilocksFastExtTests (rooted at CompPolyTests.Fields.Goldilocks.FastExt) to test the extern-backed operations (required because the interpreter cannot invoke C externs at elaboration time).
• native/goldilocks_native.c: provides the C implementations of lean_uint64_mul_hi and lean_goldilocks_mul. The latter uses a goldilocks_add_no_canonicalize helper. Performance-critical and trusted (not verified by Lean).

Documentation

• CompPoly/Fields/Goldilocks/Fast.lean serves as the public entry point for the fast field, documenting that importing it provides the Field, its operations, correctness theorems, and transferred instances.
• Module docstrings are present in the main files.

Refactoring

• CompPoly/Fields/Goldilocks.lean was significantly refactored: its previous definitions (fieldSize, Field, is_prime) were moved to Basic.lean, and it now simply re-exports Basic and Fast.
• CompPoly.lean adds seven new imports for the Goldilocks sublibrary, making the new modules accessible project-wide.

Tests

• tests/CompPolyTests/Fields/Goldilocks/Fast.lean (new): #guard-based regression checks for all verified fast operations, covering edge cases (field size wrapping, zero inverse, large exponents).
• tests/CompPolyTests/Fields/Goldilocks/FastExt.lean (new): executable tests comparing all FastExt operations against the verified Fast counterparts, run via the new lean_exe target.
• tests/CompPolyTests.lean updated to import the Fast tests.

The core mathematical and verification work is concentrated in the CompPoly/Fields/Goldilocks/Fast/ subdirectory (Arithmetic.lean, Reduction.lean, Internal.lean, Theorems.lean, Field.lean). The remaining files are infrastructure (lakefile, C code, test scaffolding, re-exports) that are mechanically driven by these core changes.

Note on PR body: The PR body was empty; this summary is based entirely on the per-file summaries.

---

Statistics

Metric	Count
📝 Files Changed	15
✅ Lines Added	1977
❌ Lines Removed	18

---

Lean Declarations

✏️ Removed: 3 declaration(s)

CompPoly/Fields/Goldilocks.lean (3)

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

✏️ Added: 151 declaration(s)

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

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

CompPoly/Fields/Goldilocks/Fast/Arithmetic.lean (41)

• abbrev Field : Type
• def add (x y : Field) : Field
• def div (x y : Field) : Field
• def inv (x : Field) : Field
• def invExponent : Nat
• def mul (x y : Field) : Field
• def neg (x : Field) : Field
• def ofCanonicalNat (n : Nat) (h : n < Goldilocks.Basic.fieldSize) : Field
• def ofField (x : Goldilocks.Basic.Field) : Field
• def ofInt (z : Int) : Field
• def ofNat (n : Nat) : Field
• def ofUInt64 (x : UInt64) : Field
• def one : Field
• def pow (x : Field) (n : Nat) : Field
• def raw (x : Field) : UInt64
• def reduceUInt64 (x : UInt64) : Field
• def square (x : Field) : Field
• def squareN (x : Field) : Nat → Field
• def sub (x y : Field) : Field
• def toField (x : Field) : Goldilocks.Basic.Field
• def toNat (x : Field) : Nat
• def zero : Field
• 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
• theorem reduceUInt64_cast (x : UInt64) :

CompPoly/Fields/Goldilocks/Fast/Field.lean (3)

• def ringEquiv : Field ≃+* Goldilocks.Basic.Field where
• theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x
• theorem ringEquiv_symm_apply (x : Goldilocks.Basic.Field) : ringEquiv.symm x = ofField x

CompPoly/Fields/Goldilocks/Fast/Internal.lean (25)

• def modulus : UInt64
• def neg_modulus : UInt64
• theorem addOverflowBounded_cast (a b : UInt64)
• theorem and_neg_modulus_toNat (x : UInt64) :
• theorem fieldSize_lt_uint64Size : Goldilocks.Basic.fieldSize < UInt64.size
• theorem fieldSize_pos : 0 < Goldilocks.Basic.fieldSize
• theorem hi_split_cast (hi : UInt64) :
• theorem modulus_toNat : modulus.toNat = Goldilocks.Basic.fieldSize
• theorem mul32_toNat (a b : UInt64) (ha : a.toNat < 2 ^ 32) (hb : b.toNat < 2 ^ 32) :
• theorem mul_neg_modulus_toNat_le (x : UInt64) (hx : x.toNat < 2 ^ 32) :
• theorem mul_neg_modulus_toNat_of_lt (x : UInt64) (hx : x.toNat < 2 ^ 32) :
• theorem neg_modulus_toNat : neg_modulus.toNat = 2 ^ 32 - 1
• theorem pow32_mul_neg_modulus_cast :
• theorem product_split32 (x y : UInt64) :
• theorem shiftRight32_toNat (x : UInt64) :
• theorem subBorrow_cast (a b : UInt64) (hb : b.toNat < 2 ^ 32) :
• theorem uint64_cast_eq_neg_modulus :
• theorem uint64_high32_lt (x : UInt64) :
• theorem uint64_low32_lt (x : UInt64) :
• theorem uint64_split32 (x : UInt64) :
• theorem uint64_toNat_lt_two_fieldSize (x : UInt64) :
• theorem wideMul_cast
• theorem wideMul_high_nat
• theorem wideMul_high_toNat
• theorem wideMul_low_toNat (lo : UInt64) (x y : UInt64) (hlo : lo = x * y) :

CompPoly/Fields/Goldilocks/Fast/Reduction.lean (21)

• def negRaw (x : UInt64) : UInt64
• def reduceAddWithCarryRaw (lo : UInt64) (carry : Bool) : UInt64
• def reduceMulRaw (x y : UInt64) : UInt64
• def reduceUInt128Raw (lo hi : UInt64) : UInt64
• def reduceUInt64Raw (x : UInt64) : UInt64
• def subRaw (x y : UInt64) : UInt64
• def wideMul (x y : UInt64) : UInt64 × UInt64
• theorem addWithCarry_bound (x y : UInt64)
• theorem addWithCarry_value (x y : UInt64) :
• theorem negRaw_cast (x : UInt64) (hx : x.toNat < Goldilocks.Basic.fieldSize) :
• theorem negRaw_lt (x : UInt64) (hx : x.toNat < Goldilocks.Basic.fieldSize) :
• theorem reduceAddWithCarryRaw_cast (lo : UInt64) (carry : Bool)
• theorem reduceAddWithCarryRaw_lt (lo : UInt64) (carry : Bool)
• theorem reduceMulRaw_cast (x y : UInt64) :
• theorem reduceMulRaw_lt (x y : UInt64) :
• theorem reduceUInt128Raw_cast (lo hi : UInt64) :
• theorem reduceUInt128Raw_lt (lo hi : UInt64) :
• theorem reduceUInt64Raw_cast (x : UInt64) :
• theorem reduceUInt64Raw_lt (x : UInt64) :
• theorem subRaw_cast (x y : UInt64)
• theorem subRaw_lt (x y : UInt64)

CompPoly/Fields/Goldilocks/Fast/Theorems.lean (36)

• private lemma canonical_inv_eq_pow (a : Goldilocks.Basic.Field) (ha : a ≠ 0) :
• 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 toField_div_mul_inv (x y : Field) :
• private theorem toField_inv_chain (x : Field) :
• private theorem toField_inv_raw (x : Field) : toField (inv x) = (toField x)⁻¹
• private theorem toField_ofCanonicalNat (n : Nat) (h : n < Goldilocks.Basic.fieldSize) :
• private theorem toNat_ofCanonicalNat (n : Nat) (h : n < Goldilocks.Basic.fieldSize) :
• theorem ofField_toField (x : Field) : ofField (toField x) = x
• theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y
• theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y
• theorem toField_injective : Function.Injective toField
• theorem toField_intCast (n : Int) : toField (n : Field) = (n : Goldilocks.Basic.Field)
• theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹
• theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y
• theorem toField_mul_def (x y : Field) : toField (mul x y) = toField x * toField y
• theorem toField_natCast (n : Nat) : toField (n : Field) = (n : Goldilocks.Basic.Field)
• 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) : toField (q : Field) = (q : Goldilocks.Basic.Field)
• 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 : Goldilocks.Basic.Field) : toField (ofField x) = x
• theorem toField_ofInt (z : Int) :
• theorem toField_ofNat (n : Nat) :
• theorem toField_ofUInt64 (x : UInt64) :
• 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 : ℚ) : toField (q : Field) = (q : Goldilocks.Basic.Field)
• theorem toField_square (x : Field) : toField (square x) = toField x * toField x
• theorem toField_squareN (x : Field) (n : Nat) :
• 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

CompPoly/Fields/Goldilocks/FastExt.lean (9)

• def divNative (x y : Field) : Field
• def invNative (x : Field) : Field
• def mulNative (x y : Field) : Field
• def mulWithMulHi (x y : Field) : Field
• def squareNNative (x : Field) : Nat → Field
• def squareNative (x : Field) : Field
• def squareWithMulHi (x : Field) : Field
• opaque goldilocksMul (a b : UInt64) : UInt64
• opaque mulHi (a b : UInt64) : UInt64

lakefile.lean (4)

• def nativeBuildDir : FilePath
• def nativeDir : FilePath
• def nativeLib (name src : String) (extraCcArgs : Array String
• def nativeLinkArgs (name : String) : Array String

tests/CompPolyTests/Fields/Goldilocks/Fast.lean (1)

• private def p : Nat

tests/CompPolyTests/Fields/Goldilocks/FastExt.lean (8)

• def main : IO UInt32
• private def a : Goldilocks.Fast.Field
• private def b : Goldilocks.Fast.Field
• private def c : Goldilocks.Fast.Field
• private def check (name : String) (ok : Bool) : IO Bool
• private def maxUInt64 : Goldilocks.Fast.Field
• private def nearTop : Goldilocks.Fast.Field

…and 1 more not listed.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The PR introduces a fast native-word implementation of the Goldilocks field, including verified reduction arithmetic, a transferred field structure, extern-backed performance primitives, and tests. The contribution is substantial and well-structured, but several violations of the project's style guide and pull request guidelines are present. The most significant issue is the absence of updates to docs/wiki/ to reflect the new build system and repository structure, which is required by the PR guidelines. Additional violations include line length exceeding 100 characters in several .lean files, empty lines inside proofs, and a naming convention issue (neg_modulus should be negModulus).

---

📄 **Per-File Summaries**

• CompPoly.lean: The file CompPoly.lean adds seven imports for the CompPoly.Fields.Goldilocks sublibrary: Basic, Fast, Fast.Arithmetic, Fast.Field, Fast.Internal, Fast.Reduction, Fast.Theorems, and FastExt. This makes the definitions, theorems, and structures from these modules available in any file that imports CompPoly.lean, expanding the project's coverage of Goldilocks field arithmetic and fast operations.
• CompPoly/Fields/Goldilocks.lean: The file was refactored from a self-contained definition of the Goldilocks prime field (with fieldSize, Field abbreviation, and is_prime theorem using pratt) into a facade module that imports and re-exports CompPoly.Fields.Goldilocks.Basic and CompPoly.Fields.Goldilocks.Fast. The previous definitions have been removed from this file, presumably moved to the Basic submodule, and the authorship was updated to include Varun Thakore. No sorry or admit were added.
• CompPoly/Fields/Goldilocks/Basic.lean: Added the file CompPoly/Fields/Goldilocks/Basic.lean to define the Goldilocks prime field ZMod (2^64 - 2^32 + 1) in the namespace Goldilocks.Basic. The file provides the reducible definition fieldSize for the modulus, the abbreviation Field for the ZMod model, and a theorem is_prime (proved via pratt) that fieldSize is prime, together with a Fact instance to make the primality available to Mathlib. It also furnishes a Field instance for Field via ZMod.instField and a NonBinaryField instance proving that the characteristic is not 2, by computing that 2 ≠ 0 in the ring.
• CompPoly/Fields/Goldilocks/Fast.lean: This diff adds a new file CompPoly/Fields/Goldilocks/Fast.lean which serves as the public entry point for the native-word Goldilocks field implementation. It imports CompPoly.Fields.Goldilocks.Fast.Field and documents that importing this module provides the fast UInt64-backed Goldilocks.Fast.Field, its arithmetic operations, correctness theorems relating it to Goldilocks.Basic.Field, and the transferred field instances.
• CompPoly/Fields/Goldilocks/Fast/Arithmetic.lean: This file introduces the Goldilocks.Fast.Field carrier type — a subtype of UInt64 containing values below the Goldilocks prime — along with its arithmetic operations and notation instances. It defines the reduction primitives reduceUInt64, add, neg, sub, mul, square, squareN, pow, and inv, each backed by the raw word‑level functions proved correct in CompPoly.Fields.Goldilocks.Fast.Reduction; correctness theorems such as reduceUInt64_cast are provided. The file also supplies conversion functions (ofNat, ofUInt64, ofField, ofInt, toNat, toField) and the full set of Lean algebraic instances (Zero, One, Add, Neg, Sub, Mul, Inv, Div, NatCast, IntCast, Nat/Int/ℚ≥0/ℚ scalar multiplication, Pow for Nat and Int, and NNRatCast/RatCast), wiring fast arithmetic into overloaded notation. No sorry or admit appear anywhere in the file.
• CompPoly/Fields/Goldilocks/Fast/Field.lean: This file introduces the ringEquiv ring equivalence (Field ≃+* Goldilocks.Basic.Field) via toField/ofField, with simp lemmas ringEquiv_apply and ringEquiv_symm_apply showing how each direction acts. It then provides the transferred instField : _root_.Field Field using toField_injective.field with all needed homomorphism proofs (toField_zero, toField_one, toField_add, etc.), along with an instCommRing : CommRing Field derived by inference. Finally, it adds instNonBinaryField : NonBinaryField Field with a proof that char_neq_2 (using a by decide check that (2 : UInt64) ≠ 0). No sorry or admit appear.
• CompPoly/Fields/Goldilocks/Fast/Internal.lean: This new file defines modulus and neg_modulus as UInt64 constants matching the Goldilocks prime field, then proves a collection of low-level lemmas relating UInt64 arithmetic to the field. The theorems cover subtraction with borrow correction (subBorrow_cast), bounded addition with overflow correction (addOverflowBounded_cast), splitting a UInt64 into 32‑bit limbs (product_split32, hi_split_cast, uint64_split32), bounds on the limb values (uint64_low32_lt, uint64_high32_lt), and a full 64‑by‑64 product decomposed into low and high words (wideMul_low_toNat, wideMul_high_nat, wideMul_high_toNat, wideMul_cast). No sorry or admit appear; all proofs are completed by dec_trivial or explicit arithmetic reasoning.
• CompPoly/Fields/Goldilocks/Fast/Reduction.lean: This new file CompPoly/Fields/Goldilocks/Fast/Reduction.lean introduces raw UInt64 arithmetic kernels for fast Goldilocks field arithmetic, along with their correctness lemmas. It defines wideMul (full 64-by-64 product as (lo, hi) words), reduceUInt64Raw (canonical reduction of a single UInt64), reduceUInt128Raw (reduction of a 128-bit integer represented as low and high words), reduceMulRaw (reduction of a 64-by-64 product), reduceAddWithCarryRaw (reduction of a 65-bit addition via low word and carry boolean), negRaw (canonical modular negation), and subRaw (canonical modular subtraction). For each kernel, theorems are provided that the result is below the Goldilocks modulus (..._lt) and that the result's cast to the field Goldilocks.Basic.Field equals the expected field operation (..._cast, with the addition kernel also using a helper bound addWithCarry_bound and an exact-sum lemma addWithCarry_value). No sorry or admit statements are present.
• CompPoly/Fields/Goldilocks/Fast/Theorems.lean: This new file proves correctness theorems for the fast UInt64-based Goldilocks field arithmetic, showing that all fast operations (add, mul, square, squareN, pow, inv, div, neg, sub, ofNat, ofInt, ofUInt64, ofField, and scalar multiplications) agree with the corresponding canonical ZMod operations via the toField embedding. Key lemmas establish that toField is injective, that the fast inversion chain computes the Fermat exponent, and that toField is a ring homomorphism and a homomorphism for NSMul, ZSMul, NPow, ZPow, NNRatCast, RatCast, NNQSMul, and QSMul. All theorems are fully proved (no sorryoradmit`).
• CompPoly/Fields/Goldilocks/FastExt.lean: The file adds a new module Goldilocks.Fast.Ext with seven functions that provide opt-in, extern-backed arithmetic for the 'fast Goldilocks' field. Two @[extern] opaque primitives mulHi (high 64 bits of 64-bit multiplication) and goldilocksMul (Goldilocks multiplication) are declared as a trusted native boundary. Using these, four multiplication variants are defined: mulWithMulHi (combines native mulHi with Lean reduction), mulNative (wraps goldilocksMul), squareWithMulHi, squareNative, and squareNNative (repeated squaring). Two higher-level routines are provided: invNative, implementing p - 2 inversion via an addition chain of these operations, and divNative, which combines invNative and mulNative. No sorry or admit present.
• lakefile.lean: The lakefile.lean adds a build step for a native C library (goldilocks_native) via extern_lib, with helper functions nativeDir, nativeBuildDir, nativeLib, and nativeLinkArgs to configure its compilation and linking. The existing lean_lib targets (CompPoly, CompPolyTests, CompPolyBenchLib) now have moreLinkArgs := nativeLinkArgs "goldilocks_native" to link against this native library. A new lean_exe target CompPolyGoldilocksFastExtTests is introduced, rooted at CompPolyTests.Fields.Goldilocks.FastExt, also linking the native library.
• native/goldilocks_native.c: This new file native/goldilocks_native.c provides native performance primitives for the Goldilocks field arithmetic used by the FastExt module. It defines lean_uint64_mul_hi to compute the high 64 bits of a 64×64 unsigned multiplication, and lean_goldilocks_mul which implements Goldilocks multiplication modulo p = 2^{64} - 2^{32} + 1 using a helper goldilocks_add_no_canonicalize. These functions are called from Lean via @[extern] declarations and are part of the trusted native boundary, meaning the arithmetic performed here is not verified by Lean—only the types are checked. The default verified Lean implementation remains unchanged; this native code is used only by the opt-in FastExt module, so this change adds a performance-critical but trusted component.
• tests/CompPolyTests.lean: Adding an import of CompPolyTests.Fields.Goldilocks.Fast to the test file.
• tests/CompPolyTests/Fields/Goldilocks/Fast.lean: Added a new test file tests/CompPolyTests/Fields/Goldilocks/Fast.lean with regression checks for the verified UInt64 fast representation of the Goldilocks field. The tests use #guard to verify that raw, toNat, ofNat, ofUInt64, addition, subtraction, negation, multiplication, square, exponentiation (including zero and negative integer exponents), inverse, and division all produce results consistent with the Goldilocks.Basic.Field representation, covering edge cases such as field size wrapping, zero inverse, and large exponents.
• tests/CompPolyTests/Fields/Goldilocks/FastExt.lean: Added a new test file tests/CompPolyTests/Fields/Goldilocks/FastExt.lean containing runtime regression checks for the Goldilocks.Fast.Ext extern-backed field operations. The file defines a check helper, several test values (including edge cases near the modulus and max UInt64), and a runChecks function that compares Goldilocks.Fast.Ext.mulWithMulHi, mulNative, squareWithMulHi, squareNative, squareNNative, invNative, and divNative against the corresponding verified Goldilocks.Fast operations (*, square, squareN, ⁻¹, /). A main function runs the checks and returns 0 on success or 1 on failure. These tests are implemented as an executable because Lean’s module interpreter cannot invoke project-local C externs during elaboration.

---

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

[dhsorens]

Summary

Verified Goldilocks.Fast looks solid: modular split (Internal/Reduction/Arithmetic/Theorems), Goldilocks reduction (not Montgomery), toField_* bridge, and #guard tests match the Baby/Koala Fast bar. C/FastExt is fine as experimental perf scaffolding.

Blockers: green CI (namespace), keep FastExt out of the default TCB (import + link), rebase onto current main.

Inline notes are the actionable items.

[dhsorens]

Build break. Nested namespace Basic renames the public API to Goldilocks.Basic.fieldSize / .Field. CI fails in benches that still use Goldilocks.fieldSize / Goldilocks.is_prime.

Prefer namespace Goldilocks only (like BabyBear/KoalaBear) so callers keep Goldilocks.Field.

[dhsorens]

TCB / packaging. Drop this umbrella import.

FastExt should stay experimental/test-only (and later optional benches). Default import CompPoly must not pull @[extern] opaques into the main library surface. Only the FastExt test (and future opt-in consumers) should import it.

[dhsorens]

TCB / packaging. Don't link goldilocks_native into the main CompPoly (or CompPolyTests) libs.

Keep moreLinkArgs only on CompPolyGoldilocksFastExtTests (and later any exe that deliberately uses Ext). Verified Fast needs no C; everyday builds shouldn't expand the trust/link surface.

[dhsorens]

Docs nit. Please state explicitly that this module is not for production CompPoly proofs / default field use: experimental performance path + regression against verified Goldilocks.Fast only. C is outside the Lean TCB.

(Also fine to note: nothing in-tree uses Ext for benches yet — tests only for now.)

[dhsorens]

Follow-ups:

1. Rebase onto current main (Lean/Mathlib 4.32).
2. Update Fields/README.md for the Basic/Fast split.
3. Optional later: a small bench comparing Lean Fast mul vs mulNative so the perf-spec story is real — not required to merge once packaging is test-only.