feat(fields): add fast KoalaBear/BabyBear arithmetic by graikos · Pull Request #258 · Verified-zkEVM/CompPoly

graikos · 2026-06-24T13:36:37Z

No description provided.

github-actions · 2026-06-24T13:38:23Z

🤖 PR Summary

This pull request implements native 32-bit Montgomery arithmetic for the KoalaBear and BabyBear prime fields, replacing self-contained implementations with a shared, verified Montgomery reduction pipeline. The changes span new modules for radix-generic and 32-bit-word-level reduction, field typeclasses and fast field carriers, facade refactors for both fields, simplification of the Domain structure in NTT, and corresponding updates to benchmarks, tests, and documentation.

Statistics

Metric	Count
📝 Files Changed	21
✅ Lines Added	1438
❌ Lines Removed	1690

Lean Declarations

✏️ Removed: 150 declaration(s)

CompPoly/Fields/BabyBear.lean (21)

@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1
@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) :
@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) :
abbrev Field
def fieldSize : Nat
def pBits : Nat
def twoAdicGenerators : List Field
def twoAdicity : Nat
lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15
lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) :
lemma twoAdicGenerator_unit_mem_rootsOfUnity
lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt
lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1)
private def sqChain (g : Field) : Nat → Field
private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) :
private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28)
private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) :
private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) :
theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/KoalaBear/Fast.lean (121)

@[simp] theorem modulus64_toNat : modulus64.toNat = KoalaBear.fieldSize
@[simp] theorem modulus_toNat : modulus.toNat = KoalaBear.fieldSize
def add (x y : Field) : Field
def div (x y : Field) : Field
def inv (x : Field) : Field
def invExponent : Nat
def modulus : UInt32
def modulus64 : UInt64
def montgomeryNegInv : UInt32
def montgomeryReduce (x : UInt64) : Field
def mul (x y : Field) : Field
def neg (x : Field) : Field
def ofCanonicalNat (n : Nat) (_h : n < KoalaBear.fieldSize) : Field
def ofInt (n : Int) : Field
def ofNat (n : Nat) : Field
def one : Field
def pow (x : Field) (n : Nat) : Field
def r2ModModulus : UInt32
def rModModulus : UInt32
def raw (x : Field) : UInt32
def reduceUInt64 (x : UInt64) : Field
def square (x : Field) : Field
def sub (x y : Field) : Field
def toCanonicalUInt32 (x : Field) : UInt32
def toField (x : Field) : KoalaBear.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
private def montgomeryReduceBounded (x : UInt64)
private def montgomeryReduceBoundedRaw (x : UInt64) : UInt32
private def montgomeryReduceNat (x : Nat) : Nat
private def reduceUInt32 (x : UInt32) : Field
private def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * KoalaBear.fieldSize) :
private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32
private def shift4Mul (acc digit : Field) : Field
private theorem fieldSize_add_fieldSize_lt_two64 :
private theorem fieldSize_add_fieldSize_lt_uint32Size :
private theorem fieldSize_lt_uint32Size : KoalaBear.fieldSize < UInt32.size
private theorem fieldSize_mul_fieldSize_lt_two64 :
private theorem fieldSize_mul_uint32Size_lt_two64 :
private theorem fieldSize_pos : 0 < KoalaBear.fieldSize
private theorem montgomeryQuotient_cast (x : Nat) :
private theorem montgomeryReduceBoundedRaw_lt (x : UInt64)
private theorem montgomeryReduceBounded_cast (x : UInt64)
private theorem montgomeryReduceNat_cast (x : Nat) :
private theorem montgomeryReduceNat_lt (x : Nat)
private theorem montgomery_sum_dvd (x : Nat) :
private theorem montgomery_u_eq_nat (x : UInt64)
private theorem montgomery_u_lt_two_fieldSize (x : UInt64)
private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z)
private theorem nat_eq_of_field_eq {a b : Nat} (ha : a < KoalaBear.fieldSize)
private theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < KoalaBear.fieldSize) :
private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x
private theorem r2ModModulus_cast :
private theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < KoalaBear.fieldSize
private theorem rModModulus_cast :
private theorem rModModulus_lt_fieldSize : rModModulus.toNat < KoalaBear.fieldSize
private theorem raw_cast_eq_toField_mul (x : Field) :
private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32)
private theorem reduceUInt32Lt2Modulus_cast (x : UInt32)
private theorem reduceUInt32Lt2Modulus_val_eq_nat (x : UInt32)
private theorem reduceUInt64_raw_cast (x : UInt64) :
private theorem toField_div_mul_inv (x y : Field) :
private theorem toField_eq_raw_mul_inv (x : Field) :
private theorem toField_inv_pow (x : Field) :
private theorem toField_inv_raw (x : Field) : toField (inv x) = (toField x)⁻¹
private theorem toField_mul_pow (base x y : Field) (m n : Nat)
private theorem toField_mul_raw (x y : Field) : toField (mul x y) = toField x * toField y
private theorem toField_ofCanonicalNat_aux (n : Nat) (h : n < KoalaBear.fieldSize) :
private theorem toField_shift4Mul (acc digit : Field) :
private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat)
private theorem toNat_lt_fieldSize (x : Field) : toNat x < KoalaBear.fieldSize
private theorem two_fieldSize_mul_uint32Size_lt_two64 :
private theorem uint32Size_lt_three_fieldSize :
private theorem uint32Size_ne_zero_in_field :
theorem ofField_toField (x : Field) : ofField (toField x) = x
theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x
theorem ringEquiv_symm_apply (x : KoalaBear.Field) : ringEquiv.symm x = ofField 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 : KoalaBear.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_natCast (n : Nat) : toField (n : Field) = (n : KoalaBear.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 : KoalaBear.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_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) :
theorem toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x
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 : KoalaBear.Field)
theorem toField_reduceUInt64 (x : UInt64) :
theorem toField_square (x : Field) : toField (square x) = toField x * toField x
theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y
theorem toField_zero : toField (0 : Field) = 0
theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n
theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x
theorem toNat_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) :
theorem toNat_reduceUInt64 (x : UInt64) :

CompPoly/Univariate/NTT/BabyBear.lean (1)

theorem twoPowNatCast_ne_zero

CompPoly/Univariate/NTT/KoalaBear.lean (3)

theorem fast_isPrimitiveRoot_twoAdicGenerator
theorem fast_twoPowNatCast_ne_zero
theorem twoPowNatCast_ne_zero

bench/CompPolyBench/Univariate/Common.lean (4)

def koalaBearFastDomainOfLogN (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) :
noncomputable def koalaBearFastRingEquiv : KoalaBear.Fast.Field ≃+* KoalaBear.Field where
theorem koalaBearFast_isPrimitiveRoot_twoAdicGenerator
theorem koalaBearFast_twoPowNatCast_ne_zero

✏️ Added: 129 declaration(s)

CompPoly/Fields/BabyBear/Basic.lean (22)

@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1
@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) :
@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) :
abbrev Field
def fieldSize : Nat
def pBits : Nat
def twoAdicGenerators : List Field
def twoAdicity : Nat
lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15
lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2)
lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) :
lemma twoAdicGenerator_unit_mem_rootsOfUnity
lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt
lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1)
private def sqChain (g : Field) : Nat → Field
private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) :
private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28)
private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) :
private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) :
theorem is_prime : Nat.Prime fieldSize

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

abbrev Field : Type
def ofField (x : BabyBear.Field) : Field
def ofUInt32 (x : UInt32) : Field
def ringEquiv : Field ≃+* BabyBear.Field
instance instMont32Field : Mont32Field BabyBear.fieldSize where

CompPoly/Fields/KoalaBear/Fast.lean (3)

def twoAdicGenerators : List Field
instance instMont32Field : Mont32Field KoalaBear.fieldSize where
theorem twoAdicGenerators_eq_map :

CompPoly/Fields/Montgomery/Basic.lean (8)

def reduceNat (R p negInv x : ℕ) : ℕ
def reduceNatQuotient (R p negInv x : ℕ) : ℕ
theorem dvd_add (R p negInv : ℕ) (hR : 0 < R)
theorem natCast_inj_of_lt {p a b : ℕ} (h : (a : ZMod p) = (b : ZMod p))
theorem reduceNatQuotient_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R)
theorem reduceNatQuotient_lt_two_mul (R p negInv x : ℕ)
theorem reduceNat_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R)
theorem reduceNat_lt (R p negInv x : ℕ)

CompPoly/Fields/Montgomery/Native32.lean (11)

def conditionalSubtract (p32 : UInt32) (u : UInt32) : UInt32
def reduceQuotient (negInv : UInt32) (p x : UInt64) : UInt32
def reduceRaw (p32 : UInt32) (p64 : UInt64) (negInv : UInt32) (x : UInt64) : UInt32
theorem conditionalSubtract_cast :
theorem conditionalSubtract_lt (h : u.toNat < 2 * p32.toNat) :
theorem conditionalSubtract_toNat :
theorem reduceQuotient_toNat (hp_pos : 0 < p64.toNat) (hbound : p64.toNat < 2 ^ 31)
theorem reduceRaw_cast [Fact (Nat.Prime modulus)]
theorem reduceRaw_eq_conditionalSubtract :
theorem reduceRaw_lt (hp : p32.toNat = p64.toNat) (hp_pos : 0 < p64.toNat)
theorem reduceRaw_toNat (hp32 : p32.toNat = modulus) (hp64 : p64.toNat = modulus)

CompPoly/Fields/Montgomery/Native32Field.lean (79)

@[simp] theorem modulus32_lt_two_pow_31 : P.modulus32.toNat < 2 ^ 31
@[simp] theorem modulus32_pos : 0 < P.modulus32.toNat
@[simp] theorem modulus64_lt_two_pow_31 : P.modulus64.toNat < 2 ^ 31
@[simp] theorem modulus64_pos : 0 < P.modulus64.toNat
@[simp] theorem modulus_lt_two_pow_32 : modulus < 2 ^ 32
def FastField (modulus : ℕ) [Mont32Field modulus] : Type
def add (x y : FastField modulus) : FastField modulus
def div (x y : FastField modulus) : FastField modulus
def inv (x : FastField modulus) : FastField modulus
def mul (x y : FastField modulus) : FastField modulus
def neg (x : FastField modulus) : FastField modulus
def ofCanonicalNat (n : ℕ) (h : n < modulus) : FastField modulus
def ofField (x : ZMod modulus) : FastField modulus
def ofNat (modulus : ℕ) [P : Mont32Field modulus] (n : ℕ) : FastField modulus
def ofUInt32 (modulus : ℕ) [P : Mont32Field modulus] (x : UInt32) : FastField modulus
def one (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus
def pow (x : FastField modulus) (n : ℕ) : FastField modulus
def reduce (x : UInt64) (h : x.toNat < modulus * 2 ^ 32) : FastField modulus
def ringEquiv (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus ≃+* ZMod modulus where
def square (x : FastField modulus) : FastField modulus
def sub (x y : FastField modulus) : FastField modulus
def toField (x : FastField modulus) : ZMod modulus
def toNat (x : FastField modulus) : ℕ
def toUInt32 (x : FastField modulus) : UInt32
def zero (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus
instance instField : _root_.Field (FastField modulus)
instance instNonBinaryField : NonBinaryField (FastField modulus) where
private def ofInt (modulus : ℕ) [P : Mont32Field modulus] (n : Int) : FastField modulus
private theorem inv_eq_pow {a : ZMod modulus} (ha : a ≠ 0) :
private theorem mul_assoc (x y z : FastField modulus) : (x * y) * z = x * (y * z)
private theorem mul_val_toNat_cast (x y : FastField modulus) :
private theorem ofCanonicalNat_val_toNat_cast {n : ℕ} (h : n < modulus) :
private theorem pow_succ_field (x : FastField modulus) (n : ℕ) : pow x (n + 1) = pow x n * x
private theorem reduce_val_toNat_cast {x : UInt64}
private theorem toField_eq_val_toNat_cast_mul_inv {x : FastField modulus} :
private theorem val_toNat_cast_eq_toField_mul {x : FastField modulus} :
theorem FastField.val_toNat_lt (x : FastField modulus) : x.val.toNat < modulus
theorem add_def (x y : FastField modulus) : x + y = add x y
theorem div_def (x y : FastField modulus) : x / y = x * y⁻¹
theorem inv_def (x : FastField modulus) : x⁻¹ = inv x
theorem modulus_pos : 0 < modulus
theorem modulus_sq_lt_two_pow_64 : modulus ^ 2 < 2 ^ 64
theorem mul_def (x y : FastField modulus) : x * y = mul x y
theorem neg_def (x : FastField modulus) : -x = neg x
theorem ofField_toField (x : FastField modulus) : ofField (toField x) = x
theorem one_def : (1 : FastField modulus) = one modulus
theorem r2ModModulus_lt_modulus : (2 ^ 32) ^ 2 % modulus < modulus
theorem ringEquiv_apply {x : FastField modulus} : ringEquiv modulus x = toField x
theorem ringEquiv_symm_apply {x : ZMod modulus} :
theorem square_def (x : FastField modulus) : square x = x * x
theorem sub_def (x y : FastField modulus) : x - y = 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
theorem toField_ofCanonicalNat {n : ℕ} (h : n < modulus) :
theorem toField_ofField (x : ZMod modulus) : toField (ofField x) = x
theorem toField_one : toField (1 : FastField modulus) = 1
theorem toField_pow (x : FastField modulus) (n : ℕ) : toField (pow x n) = toField x ^ n
theorem toField_qsmul (q : ℚ) (x : FastField modulus) : toField (q • x) = q • toField x
theorem toField_ratCast (q : ℚ) : toField (q : FastField modulus) = (q : ZMod modulus)
theorem toField_square (x : FastField modulus) : toField (square x) = toField x * toField x
theorem toField_sub (x y : FastField modulus) : toField (x - y) = toField x - toField y
theorem toField_zero : toField (0 : FastField modulus) = 0
theorem toField_zpow (x : FastField modulus) (n : Int) : toField (x ^ n) = toField x ^ n
theorem toField_zsmul (n : Int) (x : FastField modulus) : toField (n • x) = n • toField x
theorem toNat_lt_modulus {x : FastField modulus} : toNat x < modulus
theorem toNat_ofCanonicalNat {n : ℕ} (h : n < modulus) :
theorem two_ne_zero : (2 : ZMod modulus) ≠ 0
theorem two_pow_32_ne_zero : ((2 ^ 32 : ℕ) : ZMod modulus) ≠ 0
theorem zero_def : (0 : FastField modulus) = zero modulus

CompPoly/Univariate/NTT/Domain.lean (1)

theorem natCast_ne_zero (D : Domain R) : ((D.n : Nat) : R) ≠ 0

✏️ Affected: 2 declaration(s) (line number changed)

abbrev Field : Type in CompPoly/Fields/KoalaBear/Fast.lean moved from L42 to L35
def ringEquiv : Field ≃+* KoalaBear.Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L1003 to L52

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff introduces a refactoring of the fast field implementations for BabyBear and KoalaBear into a shared Montgomery framework. Overall, the changes are consistent with the project's style and guidelines. The most notable deviation is a systematic violation of the 100-character line limit in several .lean files.

Line length violations (.lean files)

CompPoly/Fields/Montgomery/Basic.lean – many theorem statements and proof lines exceed 100 characters.
CompPoly/Fields/Montgomery/Native32.lean – lines in reduceRaw_toNat, reduceQuotient_toNat, and reduceRaw_cast exceed the limit.
CompPoly/Fields/Montgomery/Native32Field.lean – lines in toField_add, mul_val_toNat_cast, ofCanonicalNat_val_toNat_cast and others exceed 100 characters.

(Note: Markdown files and CI configuration are exempt from this rule per the guidelines.)

Naming conventions – All new names follow the required UpperCamelCase for types, lowerCamelCase for functions and terms, and snake_case for theorems/lemmas. No violations found.

Module layout – The refactoring correctly places shared Montgomery infrastructure in a separate Montgomery/ directory and keeps field-specific wrappers in BabyBear/ and KoalaBear/. Transport and equivalence lemmas are kept near the bridge layer, as advised.

Documentation – Every top-level definition and theorem in the new files has a docstring. The docs/wiki/ and Fields/README.md are updated to reflect the new structure.

Other guidelines – The diff uses where syntax for instances, places by at line ends, and follows the 2-space indent rule. No other violations of the contributed style guide were observed.

📄 **Per-File Summaries**

CompPoly.lean: Added import statements for CompPoly.Fields.BabyBear.Basic, CompPoly.Fields.BabyBear.Fast, CompPoly.Fields.Montgomery.Basic, CompPoly.Fields.Montgomery.Native32, and CompPoly.Fields.Montgomery.Native32Field, making these modules available for use elsewhere in the project.
CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean: The file simplifies two proofs after a refactor of the KoalaBear.Fast representation. In fastKoalaBearFiniteFieldContext, the frobenius_fixed proof is rewritten: it replaces KoalaBear.Fast.toField_injective, KoalaBear.Fast.toField_npow, and ZMod.pow_card calls with Montgomery.Native32.toField_injective, Montgomery.Native32.toField_npow, and a direct simp on KoalaBear.fieldSize. In fastKoalaBearPrimitiveRoot_order, the simpa call is simplified by using KoalaBear.Fast.ringEquiv and KoalaBear.Fast.ofField instead of KoalaBear.Fast.ringEquiv_apply and KoalaBear.Fast.toField_ofField. No definitions or signatures change; only the proof tactics are updated to match the new internal structure.
CompPoly/Fields/BabyBear.lean: Rewrote CompPoly/Fields/BabyBear.lean from a self-contained definition of the BabyBear field (including fieldSize, Field, is_prime, twoAdicity, the full table of two-adic generators, and all supporting lemmas and instances) into a facade that simply re‑exports the canonical ZMod model from CompPoly.Fields.BabyBear.Basic and the native‑word implementation from CompPoly.Fields.BabyBear.Fast. The imports were changed accordingly (removing CompPoly.Fields.Basic, CompPoly.Fields.PrattCertificate, and others). No sorry or admit are introduced by this diff.
CompPoly/Fields/BabyBear/Basic.lean: This file introduces the BabyBear prime field ZMod (2^31 - 2^27 + 1) along with its primality proof (is_prime), a NonBinaryField instance, and an inv_eq_pow lemma providing a Fermat-style inversion formula. It defines key constants pBits (31) and twoAdicity (27), with a factorization fieldSize - 1 = 2^27 * 15. A precomputed list twoAdicGenerators of 28 elements is provided, with theorems proving properties: the list has twoAdicity + 1 entries, consecutive generators square to the previous ones (twoAdicGenerators_succ_square_eq), the maximal two-adicity condition (twoAdicity_maximal), and each generator is a primitive 2^bits-th root of unity (isPrimitiveRoot_twoAdicGenerator) of order 2^bits (twoAdicGenerators_order). No sorry or admit statements are present.
CompPoly/Fields/BabyBear/Fast.lean: Created CompPoly/Fields/BabyBear/Fast.lean, a new module providing a native 32-bit Montgomery arithmetic implementation of the BabyBear field. It defines instMont32Field to instantiate Mont32Field with BabyBear's prime and precomputed Montgomery constants (modulus32, modulus64, rModModulus, r2ModModulus, montgomeryNegInv), declares the carrier Field as an abbreviation for FastField BabyBear.fieldSize, and supplies conversion functions ofUInt32 and ofField. A ringEquiv from Montgomery.Native32.ringEquiv establishes the ring isomorphism between the fast Montgomery representation and the canonical BabyBear.Field. The module imports CompPoly.Fields.BabyBear.Basic and CompPoly.Fields.Montgomery.Native32Field. No sorry or admit are present.
CompPoly/Fields/KoalaBear/Basic.lean: This diff adjusts the KoalaBear/Basic.lean file, making two key changes. First, it removes the set_option maxRecDepth 4096 directive that previously preceded the inv_eq_pow lemma, leaving the lemma's statement and use of ZMod.card unchanged. Second, it simplifies the proof of the primitiveRoot_pow_127_eq_twoAdicGenerator lemma: the previous statement used a Fin subtype (⟨twoAdicity, by omega⟩) to index into twoAdicGenerators, which has been replaced with a plain twoAdicity index, and the proof tactic has been changed from unfold ...; decide to norm_num [primitiveRoot, twoAdicity, twoAdicGenerators]; rfl. The set_option maxRecDepth 100000 directive that preceded this lemma is also removed. No other definitions, lemmas, or sorry/admit are introduced or removed.
CompPoly/Fields/KoalaBear/Fast.lean: The file was rewritten to delegate almost all implementation to the shared library CompPoly.Fields.Montgomery.Native32Field. The previous self-contained definitions (modulus, montgomeryReduce, add, mul, inv, etc.) and all their proofs have been removed. Instead, a single instMont32Field instance provides the KoalaBear-specific constants (prime, modulus32, modulus64, rModModulus, r2ModModulus, montgomeryNegInv) for the generic Mont32Field structure. The Field carrier is now an abbreviation FastField KoalaBear.fieldSize. The conversion functions ofUInt32 and ofField delegate to Montgomery.Native32.FastField.ofUInt32 and Montgomery.Native32.FastField.ofField. The ringEquiv is obtained from Montgomery.Native32.ringEquiv. A new definition twoAdicGenerators : List Field and a theorem twoAdicGenerators_eq_map proving that this list equals KoalaBear.twoAdicGenerators.map ofField were added; these were not present before.
CompPoly/Fields/Montgomery/Basic.lean: Adds CompPoly/Fields/Montgomery/Basic.lean, a new module providing a radix-generic specification of single-word Montgomery reduction in ℕ. The file defines reduceNat (the reduction algorithm) and reduceNatQuotient (the pre‑subtraction quotient). It then proves reduceNatQuotient_lt_two_mul (the quotient is below 2*p), reduceNat_lt (the result is below p), dvd_add (the key divisibility identity under the assumption negInv * p % R = R - 1), reduceNatQuotient_cast and reduceNat_cast (the quotient and the reduction result equal x * R⁻¹ in ZMod p), and natCast_inj_of_lt (two naturals below p are equal if their ZMod p casts agree). No sorry or admit appear.
CompPoly/Fields/Montgomery/Native32.lean: This file introduces Native32, a new namespace in Montgomery that provides raw 32-bit word-level implementations and verified specifications for Montgomery reduction with radix 2^32. It defines four UInt32/UInt64-based operations—reduceRaw, reduceQuotient, and conditionalSubtract—alongside theorems that relate them to the existing Nat-level specifications reduceNatQuotient, reduceNat, and reduceNat_lt. Key theorems include reduceQuotient_toNat (agreement with reduceNatQuotient under positivity, bound, and domain constraints), reduceRaw_toNat (full equivalence to reduceNat), conditionalSubtract_lt (output less than the modulus), conditionalSubtract_cast (equality in ZMod), reduceRaw_lt (bound on the output), and reduceRaw_cast (correctness in ZMod under primality, modulus, and non‑zero radix hypotheses). The file contains no sorry or admit terms.
CompPoly/Fields/Montgomery/Native32Field.lean: This new file defines and implements fast 32-bit Montgomery field arithmetic for a prime modulus. It introduces the typeclass Mont32Field (with fields modulus32, modulus64, rModModulus, r2ModModulus, montgomeryNegInv and by decide proofs of the required arithmetic identities) and the carrier type FastField modulus (a subtype of UInt32 whose value is below the modulus).

The file provides:

conversion functions (ofCanonicalNat, ofNat, ofUInt32, ofField, ofInt, toUInt32, toNat, toField) and the corresponding NatCast, IntCast, RatCast, NNRatCast instances;
the arithmetic operations zero, one, add, neg, sub, mul, square, pow, inv, div, all implemented using the underlying Native32 reduction primitives, together with the corresponding Zero, One, Add, Neg, Sub, Mul, Inv, Div, Pow, and SMul instances;
correctness theorems (toField_*, toField_ofCanonicalNat, toField_ofField, ofField_toField, toField_injective) that prove each fast operation is a homomorphism to the canonical ZMod modulus field;
a ringEquiv from FastField modulus to ZMod modulus;
a Field instance transferred from ZMod modulus via toField;
a NonBinaryField instance showing the field is not of characteristic 2.

No sorry or admit appear in the diff.

CompPoly/Fields/README.md: The README table was reorganized to reflect a modular restructuring of the BabyBear field: the entry for BabyBear.lean was updated from a bare prime notation to a facade description, and two new entries (BabyBear/Basic.lean and BabyBear/Fast.lean) were added for the submodules, with BabyBear/Fast.lean described as a thin wrapper over the shared Montgomery/Native32Field.lean implementation. The description of KoalaBear/Fast.lean was revised to match this new pattern. Additionally, three new Montgomery modules were added: Montgomery/Basic.lean (radix-generic reduction), Montgomery/Native32.lean (raw UInt32/UInt64 reduction with bounds and correctness), and Montgomery/Native32Field.lean (per-field parameters, FastField carrier, and canonical-field bridge).
CompPoly/Univariate/NTT/BabyBear.lean: Removed the theorem twoPowNatCast_ne_zero (which proved that 2^logN is nonzero in the BabyBear field) and its use as the natCast_ne_zero field in the domainOfLogN definition. This eliminates a previously required condition of the Domain structure.
CompPoly/Univariate/NTT/Domain.lean: This diff removes the natCast_ne_zero field from the Domain structure and replaces it with a standalone theorem of the same name, proved using Domain.n_ne_zero and IsPrimitiveRoot.neZero'. The inverse function is updated to no longer provide a natCast_ne_zero argument. This change means that the nonzeroness of the domain size in the coefficient ring is now derived from the primitive root condition via a lemma, rather than being stored as a field; the Domain structure itself becomes slimmer by one field.
CompPoly/Univariate/NTT/KoalaBear.lean: Removed the theorems twoPowNatCast_ne_zero, fast_isPrimitiveRoot_twoAdicGenerator, and fast_twoPowNatCast_ne_zero, and removed the natCast_ne_zero fields from both domainOfLogN and fastDomainOfLogN, likely because the Domain structure no longer requires that field or the property is now derivable. The omega field of fastDomainOfLogN now directly uses KoalaBear.Fast.twoAdicGenerators[bitsOfLogN logN hlogN] instead of KoalaBear.Fast.ofField KoalaBear.twoAdicGenerators[bitsOfLogN logN hlogN], and its primitive proof is simplified using KoalaBear.Fast.twoAdicGenerators_eq_map and map_of_injective of the original primitive root, eliminating the need for the separate fast_isPrimitiveRoot_twoAdicGenerator lemma.
bench/CompPolyBench/Common.lean: Modified checksumKoalaBearFast to use x.toNat instead of KoalaBear.Fast.toNat x. This replaces an explicit call to the standalone toNat function with the dot-notation method on KoalaBear.Fast.Field, likely for consistency with the type’s API.
bench/CompPolyBench/Univariate/Common.lean: The diff removes three locally-defined items — koalaBearFastRingEquiv, koalaBearFast_isPrimitiveRoot_twoAdicGenerator, koalaBearFast_twoPowNatCast_ne_zero, and koalaBearFastDomainOfLogN — and replaces their usage in koalaBearFastMulNttDomain and koalaBearFastBestDomainForLength? with corresponding declarations from the upstream module CPolynomial.NTT.KoalaBear. Specifically, koalaBearFastMulNttDomain now calls CPolynomial.NTT.KoalaBear.fastDomainOfLogN instead of the local koalaBearFastDomainOfLogN, and koalaBearFastBestDomainForLength? now delegates entirely to CPolynomial.NTT.KoalaBear.fastBestDomainForLength? instead of computing the domain inline.
bench/CompPolyBench/Univariate/NTT/FastMul.lean: The diff refactors the KoalaBear benchmark in FastMul.lean by introducing a private BenchField structure (with id and checksum fields) to encapsulate field metadata. It renames locally scoped variables such as koalaBearMulNttFastPlan to canonicalPlan and koalaBearFastMulNttFastPlan to fastPlan, and similarly renames all benchmark records (e.g., koalaBearMulNaive to canonicalNaive, koalaBearFastMulNttFastPlanRecord to fastNttFastPlan). The runTimed calls are updated to use BenchField values (canonicalField and fastField) and precomputed checksum thunks (canonicalChecksum, fastChecksum) instead of inline checksumKoalaBear / checksumKoalaBearFast and string literals. No new theorems, definitions, or sorry/admit are introduced; the change is purely a refactor to improve maintainability and consistency in the benchmark harness.
docs/wiki/binary-fields-and-ntt.md: The documentation file docs/wiki/binary-fields-and-ntt.md was updated to reflect the addition of new subdirectories and files in the project's directory tree listing. Specifically, the diff adds entries for BabyBear/Fast/ and KoalaBear/Fast/, each containing files Prelude.lean, Montgomery.lean, and Convert.lean, as well as a new top-level Montgomery/ directory with files Basic.lean, Native32.lean, and Native32Field.lean. These changes ensure the documentation accurately describes the current project structure, which is important for developers navigating the codebase to find the newly added Montgomery arithmetic and field implementations.
tests/CompPolyTests.lean: Added an import of CompPolyTests.Fields.BabyBear.Fast, which provides fast field arithmetic for the BabyBear field. This allows the test file to use BabyBear's fast implementation in its tests.
tests/CompPolyTests/Fields/BabyBear/Fast.lean: This file adds a new test suite tests/CompPolyTests/Fields/BabyBear/Fast.lean for the executable Montgomery representation of the BabyBear field. It imports CompPoly.Fields.BabyBear.Fast and uses #guard statements to regression-test core arithmetic operations (val, toUInt32, toNat, toField) and their properties, including zero, one, addition, subtraction, negation, multiplication, exponentiation (with both Nat and Int exponents), inverse, and division. The tests verify correct modular reduction, identity elements, and consistency with the non-fast BabyBear.Field for exponentiation and inverse, ensuring the fast Montgomery implementation matches the specification.
tests/CompPolyTests/Fields/KoalaBear/Fast.lean: This diff updates tests/CompPolyTests/Fields/KoalaBear/Fast.lean to rewrite all regression checks for the Montgomery representation of the KoalaBear field. Previously, each check used a mix of top-level functions (raw, toCanonicalUInt32, toNat, toField, square) applied to Field values; now all checks are expressed as methods on the Field type itself (.val, .toUInt32, .toNat, .toField) and the square test is replaced by a direct multiplication. The check for (1 : Field).val also changes from a constant rModModulus to an explicit invocation Montgomery.Native32.Mont32Field.rModModulus (modulus := KoalaBear.fieldSize). No sorry or admit is present in this diff.

Last updated: 2026-07-15 12:55 UTC.

Simplify 32-bit Montgomery fields

graikos added 6 commits June 24, 2026 11:41

feat(fields): Fast BabyBear impl, mirroring KB

192d094

feat(fields): minor changes and test

c7198bb

feat(fields): Split KoalaBear fast impl

c0607d8

feat(fields): Dedup KB/BB with shared Montgomery proof logic

2c58e80

feat(fields): Changed inv to pow instead of chain

6b87a34

chore(fields): doc changes

8d55443

graikos and others added 3 commits June 29, 2026 12:45

feat(fields): dedup & shared code for u32 fields (KoalaBear/BabyBear)

f5eb442

refactor(fields): clarify Montgomery core API

61ef5a8

refactor(fields): name native Montgomery quotient

e7032ba

mitschabaude mentioned this pull request Jul 13, 2026

Simplify 32-bit Montgomery fields graikos/CompPoly#1

Merged

mitschabaude added 19 commits July 13, 2026 10:58

docs(fields): shorten Native32 module overview

40a831d

refactor(fields): simplify Mont32Field assumptions

8947f22

refactor(fields): state Montgomery inverse by remainder

4ad9d93

rename modulus consistently

a218874

refactor(fields): index Mont32Field by modulus

71957d5

minor

8d73aa7

refactor(fields): trim native Montgomery API

3ec0105

refactor(fields): remove concrete Montgomery shims

12d8f43

remove redundant conversion definitions

f2434fc

refactor(fields): remove redundant theorem reexports

25e3f4f

refactor(fields): collapse concrete fast field modules

0dd17ae

fix(bench): update fast field conversion calls

e7488d9

refactor(bench): reuse KoalaBear fast NTT domains

6160d87

refactor(ntt): simplify concrete field domains

73efa51

refactor(fields): simplify KoalaBear root proofs

694893f

refactor(fields): separate native Montgomery reduction

4fca163

refactor(fields): streamline native Montgomery field

62611d2

simplify proofs

5305c7a

refactor(fields): simplify Montgomery field proofs

fc6b63f

mitschabaude and others added 5 commits July 14, 2026 17:24

refactor(fields): clarify Montgomery cast lemma names

f929586

make R2 a uint64 and simplify

c8b8e6b

refactor(fields): remove redundant fast field wrappers

0958afd

Merge pull request #1 from mitschabaude/fast_kb_bb_fields-gregor

e423dee

Simplify 32-bit Montgomery fields

Merge branch 'master' into fast_kb_bb_fields

a6ace46

mitschabaude approved these changes Jul 16, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(fields): add fast KoalaBear/BabyBear arithmetic#258

feat(fields): add fast KoalaBear/BabyBear arithmetic#258
graikos wants to merge 33 commits into
Verified-zkEVM:masterfrom
graikos:fast_kb_bb_fields

graikos commented Jun 24, 2026

Uh oh!

github-actions Bot commented Jun 24, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

graikos commented Jun 24, 2026

Uh oh!

github-actions Bot commented Jun 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Jun 24, 2026 •

edited

Loading