feat(fields): add fast secp field arithmetic

[varunthakore]

Implemented on top of #262.

[github-actions]

🤖 PR Summary

This PR adds native-word-based fast arithmetic implementations for the Goldilocks and secp256k1 scalar fields, refactors the existing field definitions into facade modules, and provides the corresponding correctness proofs, test suites, and build infrastructure. The core new content is in the CompPoly/Fields/Goldilocks/Fast/ and CompPoly/Fields/Secp256k1/Scalar/Fast/ hierarchies; the remaining changes are mechanical or supportive.

---

Statistics

Metric	Count
📝 Files Changed	25
✅ Lines Added	6061
❌ Lines Removed	160

---

Lean Declarations

✏️ Removed: 10 declaration(s)

CompPoly/Fields/Goldilocks.lean (3)

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

CompPoly/Fields/Secp256k1.lean (7)

• abbrev BaseField
• abbrev ScalarField
• def BASE_FIELD_CARD : Nat
• def SCALAR_FIELD_CARD : Nat
• example :
• theorem BaseField_is_prime : Nat.Prime BASE_FIELD_CARD
• theorem ScalarField_is_prime : Nat.Prime SCALAR_FIELD_CARD

✏️ Added: 395 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

CompPoly/Fields/Secp256k1/Base/Basic.lean (6)

• abbrev Field
• def CARD : Nat
• instance card_prime_fact : Fact (Nat.Prime CARD)
• instance field : _root_.Field Field
• theorem card_eq_two_pow_256_sub : CARD = 2 ^ 256 - 2 ^ 32 - 977
• theorem card_is_prime : Nat.Prime CARD

CompPoly/Fields/Secp256k1/Scalar/Basic.lean (5)

• abbrev Field
• def CARD : Nat
• instance card_prime_fact : Fact (Nat.Prime CARD)
• instance field : _root_.Field Field
• theorem card_is_prime : Nat.Prime CARD

CompPoly/Fields/Secp256k1/Scalar/Fast/Arithmetic.lean (37)

• @[inline] def add (x y : Field) : Field

…and 245 more not listed.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

Coverage Notes

• AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• CompPoly/Fields/Secp256k1/Scalar/Fast/Reduction.lean (+2344/-0)

---

📋 **Additional Analysis**

The diff introduces a new native-code fast Goldilocks field implementation and refactors the existing canonical field and secp256k1 field definitions into a modular structure; no violations of the supplied instructions were found.

---

📄 **Per-File Summaries**

• CompPoly.lean: The file CompPoly.lean now imports several Goldilocks field modules: CompPoly.Fields.Goldilocks.Basic, CompPoly.Fields.Goldilocks.Fast (with its submodules Arithmetic, Field, Internal, Reduction, and Theorems), and CompPoly.Fields.Goldilocks.FastExt. These additions bring the Goldilocks field and its fast arithmetic into the scope of the CompPoly library, enabling its use in formal verification of Goldilocks-based computations.
• CompPoly/Fields/Goldilocks.lean: This diff transforms CompPoly/Fields/Goldilocks.lean from a self-contained definition of the Goldilocks prime field into a facade module. Previously, the file defined fieldSize as 2^64 - 2^32 + 1, introduced Field as ZMod fieldSize, and proved is_prime via the pratt tactic. Now it merely re-exports two submodules: CompPoly.Fields.Goldilocks.Basic, which presumably provides the canonical ZMod model, and CompPoly.Fields.Goldilocks.Fast, which provides a native-word implementation. The definitions fieldSize, Field, and is_prime have been removed (and moved into Basic), the PrattCertificate import has been replaced with these two submodule imports, and the authors include Varun Thakore alongside Quang Dao.
• CompPoly/Fields/Goldilocks/Basic.lean: This new file CompPoly/Fields/Goldilocks/Basic.lean introduces the Goldilocks prime field with modulus 2⁶⁴ - 2³² + 1. It defines the modulus as fieldSize and the field as Field := ZMod fieldSize. It provides theorem is_prime using the pratt tactic to prove primality via a Pratt certificate, and registers a Fact instance for Nat.Prime fieldSize. It also defines a Group instance for Field via ZMod.instField and a NonBinaryField instance with a proof that the characteristic is not two.
• CompPoly/Fields/Goldilocks/Fast.lean: Added a new public entry point module CompPoly/Fields/Goldilocks/Fast.lean that 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 new file CompPoly/Fields/Goldilocks/Fast/Arithmetic.lean introduces the fast UInt64-based Goldilocks field carrier Field (an abbreviation for the subtype of UInt64 with values less than Goldilocks.Basic.fieldSize) and its foundational conversions (reduceUInt64, ofNat, ofUInt64, ofField, ofInt, toNat, toField) with proven correctness lemmas like reduceUInt64_cast. It defines all arithmetic operations (add, neg, sub, mul, square, squareN, pow, inv, div), where mul reduces a 128-bit intermediate via the Goldilocks identity using Reduction.reduceMulRaw, add manages carry with Reduction.reduceAddWithCarryRaw, and inv implements an addition-chain exponentiation for p - 2. The file then provides the full suite of notation instances (Zero, One, Add, Neg, Sub, Mul, Inv, Div, NatCast, IntCast, Pow for Nat and Int, SMul for Nat, Int, ℚ≥0, and ℚ, plus NNRatCast and RatCast) so that the fast representation supports standard mathematical notation and coercion.
• CompPoly/Fields/Goldilocks/Fast/Field.lean: This file, newly created in the pull request, builds on the fast Goldilocks arithmetic layer by constructing a ring equivalence ringEquiv : Field ≃+* Goldilocks.Basic.Field, which links the fast UInt64 representation (Field) to the canonical Goldilocks field. Using the toField map and the helper lemmas (toField_zero, toField_one, etc.) from CompPoly.Fields.Goldilocks.Fast.Theorems, it transfers the field structure via toField_injective.field as a Field instance (instField), and provides the CommRing instance (instCommRing) by inference. It also adds a NonBinaryField instance (instNonBinaryField) that proves characteristic not equal to 2 by checking (2 : UInt64) ≠ 0. No definitions are left with sorry or admit.
• CompPoly/Fields/Goldilocks/Fast/Internal.lean: This new file adds internal lemmas for fast Goldilocks field arithmetic using UInt64. It defines the modulus 0xffffffff00000001 and its two's complement 0xffffffff as UInt64 constants, and proves their correspondence to the mathematical Goldilocks modulus (modulus_toNat, neg_modulus_toNat). It provides supporting theorems for bitwise operations (shiftRight32_toNat, and_neg_modulus_toNat), modular arithmetic with borrow/overflow corrections (subBorrow_cast, addOverflowBounded_cast), and a full suite of lemmas for decomposing a 64‑bit word into 32‑bit limbs and for verifying the correctness of a 64‑by‑64 product computed via limb‑wise multiplication (uint64_split32, product_split32, wideMul_low_toNat, wideMul_high_toNat, wideMul_cast). No sorry or admit appear.
• CompPoly/Fields/Goldilocks/Fast/Reduction.lean: This new file CompPoly/Fields/Goldilocks/Fast/Reduction.lean introduces raw UInt64 arithmetic kernels and their correctness lemmas for fast Goldilocks field operations. It defines reduceUInt64Raw (single-word reduction), reduceUInt128Raw (128-bit reduction), reduceMulRaw (product reduction via wideMul), reduceAddWithCarryRaw (addition with carry), negRaw (negation), and subRaw (subtraction), each accompanied by a theorem proving the result is below the prime modulus (_lt) and a theorem proving the result's canonical field element matches the intended arithmetic (_cast). Additionally, it provides addWithCarry_bound and addWithCarry_value to support the correctness of addition with carry. All theorems are stated in terms of Goldilocks.Basic.fieldSize and UInt64 operations, and no sorry or admit appear in the file.
• CompPoly/Fields/Goldilocks/Fast/Theorems.lean: This new file CompPoly/Fields/Goldilocks/Fast/Theorems.lean proves the correctness of the fast UInt64-based Goldilocks field arithmetic by showing that the mapping toField from the Fast field into Goldilocks.Basic.Field (as a ZMod) is a ring homomorphism. It adds simp theorems toField_zero, toField_one, toField_add, toField_neg, toField_sub, toField_mul, toField_mul_def, toField_square, toField_squareN, toField_pow, toField_inv, toField_div, toField_natCast, toField_intCast, toField_nsmul, toField_zsmul, toField_npow, toField_zpow, toField_nnratCast, toField_ratCast, toField_nnqsmul, and toField_qsmul establishing that toField commutes with these operations, and toField_injective that it is injective. It also provides private lemmas canonical_inv_eq_pow, mul_assoc_field, pow_succ, toField_inv_chain, and toField_inv_raw used in the proofs. No sorry or admit appear in the diff.
• CompPoly/Fields/Goldilocks/FastExt.lean: This new file introduces an extern-backed performance layer for the Goldilocks fast field, defining opaque extern primitives mulHi (high 64 bits of unsigned 64x64 multiply) and goldilocksMul (full Goldilocks multiplication with canonical output), alongside Lean wrapper functions mulWithMulHi, mulNative, squareWithMulHi, squareNative, squareNNative for repeated squaring, invNative (inversion via the Goldilocks p-2 addition chain) and divNative. The correctness of mulHi and goldilocksMul is explicitly marked as trusted from the linked C implementations; all arithmetic functions remain typed over the existing Field structure, using reduceUInt64 to embed results safely. No sorry or admit appear in the file.
• CompPoly/Fields/Secp256k1.lean: This commit replaces the entire content of CompPoly/Fields/Secp256k1.lean, which previously directly defined the secp256k1 base and scalar prime fields (BASE_FIELD_CARD, BaseField, SCALAR_FIELD_CARD, ScalarField), proved their primality via Pratt certificates (BaseField_is_prime, ScalarField_is_prime), and provided Field instances, with a new facade module. The new version deletes all those definitions, proofs, and instances, and instead simply re-exports the relevant submodules CompPoly.Fields.Secp256k1.Base.Basic, CompPoly.Fields.Secp256k1.Scalar.Basic, and CompPoly.Fields.Secp256k1.Scalar.Fast. Additionally, the author list was updated to include Varun Thakore, and the module-level docstring was simplified to describe the file as a facade module.
• CompPoly/Fields/Secp256k1/Base/Basic.lean: Introduces the secp256k1 base field. Defines CARD as the prime 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f and proves card_eq_two_pow_256_sub showing it equals 2^256 - 2^32 - 977. Creates the Field abbreviation ZMod CARD, proves primality via card_is_prime using a nested PrattCertificate', and registers the Fact instance card_prime_fact along with the field instance via ZMod.instField.
• CompPoly/Fields/Secp256k1/Scalar/Basic.lean: This new file introduces the secp256k1 scalar field for the project. It defines CARD as the prime order 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141, the Field as ZMod CARD, and provides a card_is_prime theorem proving Nat.Prime CARD via a nested Pratt certificate. It registers Fact (Nat.Prime CARD) as card_prime_fact and provides a field instance via ZMod.instField CARD. The Pratt certificate uses helper commands reduce_mod_char and pratt (and norm_num) to verify the necessary prime factorizations and orders; no sorry or admit are present.
• CompPoly/Fields/Secp256k1/Scalar/Fast.lean: Added a new file CompPoly/Fields/Secp256k1/Scalar/Fast.lean that serves as the public entry point for the 4×UInt64 secp256k1 scalar implementation. Importing this module makes available the Secp256k1.Scalar.Fast.Field structure along with conversion functions, verified arithmetic operations, correctness theorems relating the fast field to the canonical Secp256k1.Scalar.Basic.Field, and the ring equivalence.
• CompPoly/Fields/Secp256k1/Scalar/Fast/Arithmetic.lean: This new file defines the fast secp256k1 scalar field type Field (a subtype of Repr with a canonical bound) and its arithmetic API. It provides zero, one, conversions (ofNat, ofField, ofInt, toNat, toField), and operations (add, neg, sub, mul, square, pow, invFermat, inv, div), all implemented using the reduction primitives from CompPoly.Fields.Secp256k1.Scalar.Fast.Reduction. It then registers the corresponding instances (Zero, One, Add, Neg, Sub, Mul, Inv, Div, NatCast, IntCast, SMul for Nat and Int, Pow for Nat and Int, NNRatCast, RatCast, and SMul for ℚ≥0 and ℚ) to enable the standard algebraic notation for fast scalar arithmetic. No sorry or admit appear in the file.
• CompPoly/Fields/Secp256k1/Scalar/Fast/Field.lean: This new file CompPoly/Fields/Secp256k1/Scalar/Fast/Field.lean defines the transfer of the secp256k1 scalar field structure to a fast four-limb UInt64 representation. It introduces a ringEquiv ring equivalence (Field ≃+* Secp256k1.Scalar.Basic.Field) with its toFun, invFun, and proofs (ofField_toField, toField_ofField, toField_add, toField_mul), along with simp lemmas ringEquiv_apply and ringEquiv_symm_apply. It provides an instField instance (priority low) for _root_.Field Field via toField_injective.field, supplied with all the required homomorphism proofs (toField_zero, toField_one, toField_add, toField_mul, toField_neg, toField_sub, toField_inv, toField_div, toField_nsmul, toField_zsmul, toField_nnqsmul, toField_qsmul, toField_npow, toField_zpow, toField_natCast, toField_intCast, toField_nnratCast, toField_ratCast). It also adds an instNonBinaryField instance (priority low) proving NonBinaryField Field by using by decide to show char_neq_2.
• CompPoly/Fields/Secp256k1/Scalar/Fast/Internal.lean: This file adds a new module Secp256k1.Scalar.Fast.Internal defining low-level constants (the secp256k1 scalar order limbs and complement), a 4-limb representation Repr with conversion to Nat and proofs of injectivity and canonical representation, and raw limb arithmetic helpers (addCarry, subBorrow, mul64Lo/mul64Hi, addRaw, subRaw) along with value theorems. It also translates libsecp256k1's C macros (mulAdd, mulAddFast, sumAdd, sumAddFast, extract, extractFast) into Lean functions with corresponding correctness theorems.
• CompPoly/Fields/Secp256k1/Scalar/Fast/Reduction.lean: This new file (CompPoly/Fields/Secp256k1/Scalar/Fast/Reduction.lean) adds the modular reduction and arithmetic routines for the secp256k1 scalar field, mirroring the C implementation's fast reduction path. It defines reduceRaw and canonicalizeRaw for conditional reduction by the scalar order, addModRaw, subModRaw, negRaw for modular operations, and mul512Raw for full 512-bit multiplication. The reduction pipeline (stages reduce512To385Raw, reduce385To258Raw, reduce258Raw) is implemented and proven correct with theorems reduce512To385Raw_value, reduce385To258Raw_value, reduce258Raw_value, and mul512Raw_value. The proofs establish that the fast arithmetic matches the natural-number representation and respects the field's modulus.
• CompPoly/Fields/Secp256k1/Scalar/Fast/Theorems.lean: This pull request adds a new file CompPoly/Fields/Secp256k1/Scalar/Fast/Theorems.lean containing correctness proofs that the conversion toField from the fast secp256k1 scalar field representation to the canonical scalar field Secp256k1.Scalar.Basic.Field preserves all constructors, arithmetic operations, powers, casts, and scalar actions. It introduces the theorem toField_injective establishing that toField is injective, and a private lemma pow_card_sub_two_eq_inv proving Fermat inversion for the canonical field. It then proves toField respects ofNat, ofField, zero, one, addition, negation, subtraction, multiplication, squaring, exponentiation (toField_pow), inversion via Fermat (toField_invFermat and toField_inv), division (toField_div), and casts from Nat, Int, ℚ≥0, and ℚ, as well as the corresponding scalar multiplications (toField_nsmul, toField_zsmul, toField_nnqsmul, toField_qsmul) and powers (toField_npow, toField_zpow). The file contains no sorry or admit.
• lakefile.lean: The lakefile.lean adds a nativeLib function that compiles a C source file into a static library via compileO and ar, and declares an extern_lib liblean_goldilocks_native using it. The existing lean_lib targets CompPoly and CompPolyTests now include moreLinkArgs linking that native library, and a new lean_exe CompPolyGoldilocksFastExtTests is added (root: CompPolyTests.Fields.Goldilocks.FastExt) with the same link arguments. This enables the project to use native C code for the Goldilocks field fast extension arithmetic.
• native/goldilocks_native.c: This new file native/goldilocks_native.c provides native C implementations of Goldilocks field arithmetic primitives that are called from Lean via @[extern] declarations in CompPoly/Fields/Goldilocks/FastExt.lean. It exports lean_uint64_mul_hi (extracting the high 64 bits of a 64×64 unsigned multiplication), lean_goldilocks_mul (modular multiplication modulo the Goldilocks prime p = 2^64 − 2^32 + 1), and a static helper goldilocks_add_no_canonicalize for conditional addition of the negated modulus. This native code forms part of the trusted boundary for the opt-in FastExt module, supplementing the verified Lean default implementation.
• tests/CompPolyTests.lean: The file tests/CompPolyTests.lean now imports CompPolyTests.Fields.Goldilocks.Fast and CompPolyTests.Fields.Secp256k1.Scalar.Fast, adding test coverage for the Goldilocks field and the Secp256k1 scalar field, respectively. No other changes appear.
• tests/CompPolyTests/Fields/Goldilocks/Fast.lean: This commit adds a new test file tests/CompPolyTests/Fields/Goldilocks/Fast.lean that provides regression checks for the Goldilocks.Fast field representation (based on UInt64). The file defines a local constant p as Goldilocks.Basic.fieldSize and uses #guard statements to verify that the raw constant, toNat, toField, toUInt64 (via ofUInt64), square, and arithmetic operations (+, -, *, ^, ⁻¹, /) on the Field type are consistent with the reference Goldilocks.Basic.Field implementation. Specific checks cover modulo reduction, addition under overflow, subtraction yielding negative results, negation, squaring, exponentiation (including with negative integer exponent), and inverse/division. The tests ensure that the fast representation behaves correctly both against expected Nat values and against the canonical Goldilocks.Basic field.
• tests/CompPolyTests/Fields/Goldilocks/FastExt.lean: Adds tests/CompPolyTests/Fields/Goldilocks/FastExt.lean, a new executable test file that compares each extern-backed operation in Goldilocks.Fast.Ext (mulWithMulHi, mulNative, squareWithMulHi, squareNative, squareNNative, invNative, divNative) against the corresponding verified Goldilocks.Fast implementation. The tests use named private values (including nearTop = modulus − 1 and maxUInt64) and exercise both basic calls and edge cases (e.g., multiplication near the modulus and with the maximum UInt64 input). The file defines a runChecks function that prints failures to stderr, and a main entry point returning exit code 0 on success or 1 on failure; this executable structure is used because Lean's module interpreter cannot invoke project-local C externs during elaboration.
• tests/CompPolyTests/Fields/Secp256k1/Scalar/Fast.lean: This new file tests/CompPolyTests/Fields/Secp256k1/Scalar/Fast.lean adds regression checks for the pure‑Lean 4×64 secp256k1 scalar field implementation. It verifies that the Field type satisfies the CommRing, Field, and NonBinaryField typeclasses via #synth commands. The #guard statements test a range of operations—mul64Hi, toNat, toField, square, addition, subtraction, negation, multiplication, exponentiation, inverse (invFermat and ⁻¹), and division—on concrete values, comparing results against the Secp256k1.Scalar.Basic.Field implementation. No sorry or admit are present.

---

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