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

Mathematical Formalization

Proves primality of the BabyBear modulus ($2^{31} - 2^{27} + 1$) and provides verified tables for two-adic generators and primitive roots of unity.
Defines a radix-generic Montgomery reduction framework with proofs of functional correctness relative to ZMod p.
Verifies that native 32-bit and 64-bit word operations correctly implement Montgomery quotients and remain within modular bounds.

Field Implementation and Optimization

Implements Montgomery-form arithmetic for BabyBear and KoalaBear using native UInt32 and UInt64 operations.
Adds the Mont32Field typeclass and FastField carrier for monomorphic machine code generation via aggressive inlining.
Specializes 32-bit Montgomery reduction primitives for specific primes to optimize performance.

Architecture and Refactoring

Reorganizes the Fields library into Basic (canonical) and Fast (Montgomery) submodules.
Consolidates arithmetic logic into a shared Montgomery/ directory for logic reuse.
Updates CompPoly imports and field facade modules to re-export specialized components.

Documentation and Testing

Updates README and Wiki for the modular architecture and Montgomery framework.
Adds regression tests for BabyBear.Fast using #guard to verify operations against canonical definitions.

Statistics

Metric	Count
📝 Files Changed	18
✅ Lines Added	2444
❌ Lines Removed	1401

Lean Declarations

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

private theorem fieldSize_add_fieldSize_lt_uint32Size : in CompPoly/Fields/KoalaBear/Fast.lean
@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) : in CompPoly/Fields/BabyBear.lean
private theorem rModModulus_cast : in CompPoly/Fields/KoalaBear/Fast.lean
instance instOneField : One Field where in CompPoly/Fields/KoalaBear/Fast.lean
lemma twoAdicGenerator_unit_mem_rootsOfUnity in CompPoly/Fields/BabyBear.lean
private theorem uint32Size_ne_zero_in_field : in CompPoly/Fields/KoalaBear/Fast.lean
def toNat (x : Field) : Nat in CompPoly/Fields/KoalaBear/Fast.lean
private theorem montgomery_u_eq_nat (x : UInt64) in CompPoly/Fields/KoalaBear/Fast.lean
instance instAddField : Add Field where in CompPoly/Fields/KoalaBear/Fast.lean
theorem toNat_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem reduceUInt32Lt2Modulus_cast (x : UInt32) in CompPoly/Fields/KoalaBear/Fast.lean
instance instPowFieldNat : Pow Field Nat where in CompPoly/Fields/KoalaBear/Fast.lean
theorem toNat_reduceUInt64 (x : UInt64) : in CompPoly/Fields/KoalaBear/Fast.lean
lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/BabyBear.lean
private theorem nat_eq_of_field_eq {a b : Nat} (ha : a < KoalaBear.fieldSize) in CompPoly/Fields/KoalaBear/Fast.lean
instance instNegField : Neg Field where in CompPoly/Fields/KoalaBear/Fast.lean
theorem toField_pow (x : Field) (n : Nat) : toField (pow x n) = toField x ^ n in CompPoly/Fields/KoalaBear/Fast.lean
def twoAdicity : Nat in CompPoly/Fields/BabyBear.lean
lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1) in CompPoly/Fields/BabyBear.lean
private theorem toField_eq_raw_mul_inv (x : Field) : in CompPoly/Fields/KoalaBear/Fast.lean
private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) : in CompPoly/Fields/BabyBear.lean
instance instMulField : Mul Field where in CompPoly/Fields/KoalaBear/Fast.lean
private def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem r2ModModulus_cast : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem reduceUInt64_raw_cast (x : UInt64) : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem reduceUInt32Lt2Modulus_val_eq_nat (x : UInt32) in CompPoly/Fields/KoalaBear/Fast.lean
private theorem raw_cast_eq_toField_mul (x : Field) : in CompPoly/Fields/KoalaBear/Fast.lean
def twoAdicGenerators : List Field in CompPoly/Fields/BabyBear.lean
def one : Field in CompPoly/Fields/KoalaBear/Fast.lean
theorem toField_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem montgomeryReduceBoundedRaw_lt (x : UInt64) in CompPoly/Fields/KoalaBear/Fast.lean
private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) in CompPoly/Fields/KoalaBear/Fast.lean
def modulus : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
instance instInvField : Inv Field where in CompPoly/Fields/KoalaBear/Fast.lean
private def montgomeryReduceBounded (x : UInt64) in CompPoly/Fields/KoalaBear/Fast.lean
private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x in CompPoly/Fields/KoalaBear/Fast.lean
instance instZeroField : Zero Field where in CompPoly/Fields/KoalaBear/Fast.lean
lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) : in CompPoly/Fields/BabyBear.lean
def reduceUInt64 (x : UInt64) : Field in CompPoly/Fields/KoalaBear/Fast.lean
def r2ModModulus : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
def modulus64 : UInt64 in CompPoly/Fields/KoalaBear/Fast.lean
private theorem montgomeryReduceBounded_cast (x : UInt64) in CompPoly/Fields/KoalaBear/Fast.lean
private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28) in CompPoly/Fields/BabyBear.lean
def ofUInt32 (x : UInt32) : Field in CompPoly/Fields/KoalaBear/Fast.lean
private theorem montgomery_u_lt_two_fieldSize (x : UInt64) in CompPoly/Fields/KoalaBear/Fast.lean
private theorem fieldSize_mul_fieldSize_lt_two64 : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem rModModulus_lt_fieldSize : rModModulus.toNat < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast.lean
@[simp] theorem modulus_toNat : modulus.toNat = KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast.lean
@[simp] theorem modulus64_toNat : modulus64.toNat = KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_shift4Mul (acc digit : Field) : in CompPoly/Fields/KoalaBear/Fast.lean
instance instNNRatSMulField : SMul ℚ≥0 Field where in CompPoly/Fields/KoalaBear/Fast.lean
private theorem two_fieldSize_mul_uint32Size_lt_two64 : in CompPoly/Fields/KoalaBear/Fast.lean
theorem is_prime : Nat.Prime fieldSize in CompPoly/Fields/BabyBear.lean
private def sqChain (g : Field) : Nat → Field in CompPoly/Fields/BabyBear.lean
private theorem montgomeryReduceNat_lt (x : Nat) in CompPoly/Fields/KoalaBear/Fast.lean
private theorem fieldSize_pos : 0 < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast.lean
private theorem montgomery_sum_dvd (x : Nat) : in CompPoly/Fields/KoalaBear/Fast.lean
private def shift4Mul (acc digit : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_inv_raw (x : Field) : toField (inv x) = (toField x)⁻¹ in CompPoly/Fields/KoalaBear/Fast.lean
def ofNat (n : Nat) : Field in CompPoly/Fields/KoalaBear/Fast.lean
private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) : in CompPoly/Fields/BabyBear.lean
def ofField (x : KoalaBear.Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean
private def montgomeryReduceNat (x : Nat) : Nat in CompPoly/Fields/KoalaBear/Fast.lean
private theorem montgomeryReduceNat_cast (x : Nat) : in CompPoly/Fields/KoalaBear/Fast.lean
def montgomeryNegInv : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat) in CompPoly/Fields/KoalaBear/Fast.lean
private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) : in CompPoly/Fields/BabyBear.lean
def rModModulus : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
private theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_inv_pow (x : Field) : in CompPoly/Fields/KoalaBear/Fast.lean
def zero : Field in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_mul_pow (base x y : Field) (m n : Nat) in CompPoly/Fields/KoalaBear/Fast.lean
instance instIntSMulField : SMul Int Field where in CompPoly/Fields/KoalaBear/Fast.lean
theorem toField_reduceUInt64 (x : UInt64) : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast.lean
instance instPowFieldInt : Pow Field Int where in CompPoly/Fields/KoalaBear/Fast.lean
def ofInt (n : Int) : Field in CompPoly/Fields/KoalaBear/Fast.lean
private theorem fieldSize_lt_uint32Size : KoalaBear.fieldSize < UInt32.size in CompPoly/Fields/KoalaBear/Fast.lean
instance instRatSMulField : SMul ℚ Field where in CompPoly/Fields/KoalaBear/Fast.lean
def ofCanonicalNat (n : Nat) (_h : n < KoalaBear.fieldSize) : Field in CompPoly/Fields/KoalaBear/Fast.lean
private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z) in CompPoly/Fields/KoalaBear/Fast.lean
@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) : in CompPoly/Fields/BabyBear.lean
instance instNNRatCastField : NNRatCast Field where in CompPoly/Fields/KoalaBear/Fast.lean
abbrev Field : Type in CompPoly/Fields/KoalaBear/Fast.lean
private def reduceUInt32 (x : UInt32) : Field in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_div_mul_inv (x y : Field) : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem uint32Size_lt_three_fieldSize : in CompPoly/Fields/KoalaBear/Fast.lean
instance instRatCastField : RatCast Field where in CompPoly/Fields/KoalaBear/Fast.lean
def montgomeryReduce (x : UInt64) : Field in CompPoly/Fields/KoalaBear/Fast.lean
def pBits : Nat in CompPoly/Fields/BabyBear.lean
instance instSubField : Sub Field where in CompPoly/Fields/KoalaBear/Fast.lean
private theorem montgomeryQuotient_cast (x : Nat) : in CompPoly/Fields/KoalaBear/Fast.lean
lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/BabyBear.lean
instance instIntCastField : IntCast Field where in CompPoly/Fields/KoalaBear/Fast.lean
@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1 in CompPoly/Fields/BabyBear.lean
private theorem fieldSize_mul_uint32Size_lt_two64 : in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toNat_lt_fieldSize (x : Field) : toNat x < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast.lean
instance instNatSMulField : SMul Nat Field where in CompPoly/Fields/KoalaBear/Fast.lean
def raw (x : Field) : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_mul_raw (x y : Field) : toField (mul x y) = toField x * toField y in CompPoly/Fields/KoalaBear/Fast.lean
def toCanonicalUInt32 (x : Field) : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
private theorem toField_ofCanonicalNat_aux (n : Nat) (h : n < KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast.lean
def fieldSize : Nat in CompPoly/Fields/BabyBear.lean
instance instDivField : Div Field where in CompPoly/Fields/KoalaBear/Fast.lean
def toField (x : Field) : KoalaBear.Field in CompPoly/Fields/KoalaBear/Fast.lean
lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt in CompPoly/Fields/BabyBear.lean
lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15 in CompPoly/Fields/BabyBear.lean
private def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 in CompPoly/Fields/KoalaBear/Fast.lean
instance instNatCastField : NatCast Field where in CompPoly/Fields/KoalaBear/Fast.lean
private theorem fieldSize_add_fieldSize_lt_two64 : in CompPoly/Fields/KoalaBear/Fast.lean
abbrev Field in CompPoly/Fields/BabyBear.lean

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

theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x in CompPoly/Fields/BabyBear/Fast.lean
def montgomeryReduceBounded (x : UInt64) in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
def rModModulus : UInt32 in CompPoly/Fields/BabyBear/Fast/Prelude.lean
def reduceUInt32 (x : UInt32) : Field in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
theorem montgomeryReduceBoundedRaw_lt (x : UInt64) in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
def one : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2) in CompPoly/Fields/BabyBear/Basic.lean
theorem fieldSize_lt_uint32Size : BabyBear.fieldSize < UInt32.size in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem raw_cast_eq_toField_mul (x : Field) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem ofField_toField (x : FastField F) : ofField (toField x) = x in CompPoly/Fields/Montgomery/Native32Field.lean
theorem ringEquiv_symm_apply (x : BabyBear.Field) : ringEquiv.symm x = ofField x in CompPoly/Fields/BabyBear/Fast.lean
def toField (x : Field) : BabyBear.Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem fieldSize_add_fieldSize_lt_uint32Size : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem ringEquiv_symm_apply (x : ZMod P.fieldSize) : in CompPoly/Fields/Montgomery/Native32Field.lean
def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
def div (x y : FastField F) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
def modulus : UInt32 in CompPoly/Fields/BabyBear/Fast/Prelude.lean
def montgomeryNegInv : UInt32 in CompPoly/Fields/BabyBear/Fast/Prelude.lean
def r2ModModulus : UInt32 in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem toField_add (x y : FastField F) : toField (x + y) = toField x + toField y in CompPoly/Fields/Montgomery/Native32Field.lean
theorem uint32Size_ne_zero_in_field : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem toField_intCast (n : Int) : toField (n : FastField F) = (n : ZMod P.fieldSize) in CompPoly/Fields/Montgomery/Native32Field.lean
theorem montgomeryReduceBounded_cast (x : UInt64) in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
theorem u_lt_two_mul (negInv : UInt32) (modN : UInt64) (p : Nat) in CompPoly/Fields/Montgomery/Native32.lean
theorem toField_zpow (x : FastField F) (n : Int) : toField (x ^ n) = toField x ^ n in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toNat_lt_fieldSize (x : Field) : toNat x < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) in CompPoly/Fields/Montgomery/Native32Field.lean
def ofNat (n : Nat) : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem toField_zero : toField (0 : FastField F) = 0 in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x in CompPoly/Fields/BabyBear/Fast.lean
def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
theorem toNat_ofCanonicalNat (n : Nat) (h : n < P.fieldSize) : in CompPoly/Fields/Montgomery/Native32Field.lean
theorem ringEquiv_apply (x : FastField F) : ringEquiv x = toField x in CompPoly/Fields/Montgomery/Native32Field.lean
def ringEquiv : FastField F ≃+* ZMod P.fieldSize where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toNat_reduceUInt64 (x : UInt64) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem toField_injective : Function.Injective (toField (F in CompPoly/Fields/Montgomery/Native32Field.lean
def add (x y : FastField F) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 in CompPoly/Fields/Montgomery/Native32Field.lean
def neg (x : FastField F) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem two_fieldSize_mul_uint32Size_lt_two64 : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def zero : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem toField_reduceUInt64 (x : UInt64) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
def invExponent : Nat in CompPoly/Fields/BabyBear/Fast.lean
theorem toNat_lt_fieldSize (x : FastField F) : toNat x < P.fieldSize in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toNat_lt_fieldSize (x : Field) : toNat x < BabyBear.fieldSize in CompPoly/Fields/BabyBear/Fast/Convert.lean
instance instMont32Field : Mont32Field BabyBear.Field where in CompPoly/Fields/BabyBear/Fast/Prelude.lean
lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15 in CompPoly/Fields/BabyBear/Basic.lean
instance instMul : Mul (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_one : toField (1 : FastField F) = 1 in CompPoly/Fields/Montgomery/Native32Field.lean
def reduceUInt64 (x : UInt64) : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem fieldSize_pos : 0 < BabyBear.fieldSize in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem toField_natCast (n : Nat) : toField (n : Field) = (n : BabyBear.Field) in CompPoly/Fields/BabyBear/Fast.lean
theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x in CompPoly/Fields/BabyBear/Fast.lean
@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) : in CompPoly/Fields/BabyBear/Basic.lean
abbrev Field : Type in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem reduceNat_cast (R p negInv : Nat) [Fact (Nat.Prime p)] (hR : 0 < R) in CompPoly/Fields/Montgomery/Basic.lean
instance instPowInt : Pow (FastField F) Int where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toNat_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
def ofInt (n : Int) : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
private theorem toField_div_mul_inv (x y : FastField F) : in CompPoly/Fields/Montgomery/Native32Field.lean
private theorem pow_succ_field (x : FastField F) (n : Nat) : pow x (n + 1) = pow x n * x in CompPoly/Fields/Montgomery/Native32Field.lean
instance instPowNat : Pow (FastField F) Nat where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem u_eq_nat (negInv : UInt32) (modN : UInt64) (p : Nat) in CompPoly/Fields/Montgomery/Native32.lean
def reduceUInt64 (x : UInt64) : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
def reduceUInt32 (x : UInt32) : Field in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
def reduceNat (R p negInv x : Nat) : Nat in CompPoly/Fields/Montgomery/Basic.lean
theorem inv_eq_pow_field (a : ZMod P.fieldSize) (ha : a ≠ 0) : in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_square (x : FastField F) : toField (square x) = toField x * toField x in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem toField_nnqsmul (q : ℚ≥0) (x : FastField F) : toField (q • x) = q • toField x in CompPoly/Fields/Montgomery/Native32Field.lean
def zero : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem toField_one : toField (1 : Field) = 1 in CompPoly/Fields/BabyBear/Fast.lean
theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n in CompPoly/Fields/BabyBear/Fast.lean
private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) : in CompPoly/Fields/BabyBear/Basic.lean
theorem toField_nnratCast (q : ℚ≥0) : toField (q : FastField F) = (q : ZMod P.fieldSize) in CompPoly/Fields/Montgomery/Native32Field.lean
@[simp] theorem modulus64_toNat : modulus64.toNat = KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
theorem toField_injective : Function.Injective (toField : Field → BabyBear.Field) in CompPoly/Fields/BabyBear/Fast.lean
def square (x : Field) : Field in CompPoly/Fields/BabyBear/Fast.lean
def toField (x : FastField F) : ZMod P.fieldSize in CompPoly/Fields/Montgomery/Native32Field.lean
theorem r2ModModulus_cast : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem toField_qsmul (q : ℚ) (x : FastField F) : toField (q • x) = q • toField x in CompPoly/Fields/Montgomery/Native32Field.lean
instance instNNRatCast : NNRatCast (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_eq_raw_mul_inv (x : FastField F) : in CompPoly/Fields/Montgomery/Native32Field.lean
theorem raw_cast_eq_toField_mul (x : FastField F) : in CompPoly/Fields/Montgomery/Native32Field.lean
def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 in CompPoly/Fields/Montgomery/Native32Field.lean
def pBits : Nat in CompPoly/Fields/BabyBear/Basic.lean
def raw (x : Field) : UInt32 in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def reduceUInt32 (x : UInt32) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
def square (x : FastField F) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_zero : toField (0 : Field) = 0 in CompPoly/Fields/BabyBear/Fast.lean
abbrev Field in CompPoly/Fields/BabyBear/Basic.lean
def modulus64 : UInt64 in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def ofInt (n : Int) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
def montgomeryReduce (x : UInt64) : Field in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
theorem toField_ratCast (q : ℚ) : toField (q : FastField F) = (q : ZMod P.fieldSize) in CompPoly/Fields/Montgomery/Native32Field.lean
def ofUInt32 (x : UInt32) : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem uint32Size_ne_zero_in_field : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) : in CompPoly/Fields/BabyBear/Basic.lean
def FastField (F : Type) [Mont32Field F] : Type in CompPoly/Fields/Montgomery/Native32Field.lean
private def sqChain (g : Field) : Nat → Field in CompPoly/Fields/BabyBear/Basic.lean
theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : BabyBear.Field) in CompPoly/Fields/BabyBear/Fast.lean
def div (x y : Field) : Field in CompPoly/Fields/BabyBear/Fast.lean
def ofField (x : BabyBear.Field) : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem ofField_toField (x : Field) : ofField (toField x) = x in CompPoly/Fields/BabyBear/Fast.lean
theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def ofNat (n : Nat) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
@[simp] theorem modulus_toNat : modulus.toNat = BabyBear.fieldSize in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem sum_dvd (R p negInv : Nat) (hR : 0 < R) in CompPoly/Fields/Montgomery/Basic.lean
theorem toField_neg (x : FastField F) : toField (-x) = -toField x in CompPoly/Fields/Montgomery/Native32Field.lean
def pow (x : Field) (n : Nat) : Field in CompPoly/Fields/BabyBear/Fast.lean
instance instMont32Field : Mont32Field KoalaBear.Field where in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem fieldSize_mul_uint32Size_lt_two64 : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem montgomeryReduceBounded_cast (x : UInt64) in CompPoly/Fields/Montgomery/Native32Field.lean
private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28) in CompPoly/Fields/BabyBear/Basic.lean
theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
theorem toField_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
def rModModulus : UInt32 in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem montgomeryReduceBounded_cast (x : UInt64) in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
theorem toField_ofField (x : BabyBear.Field) : toField (ofField x) = x in CompPoly/Fields/BabyBear/Fast.lean
def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
private theorem mul_assoc_field (x y z : FastField F) : (x * y) * z = x * (y * z) in CompPoly/Fields/Montgomery/Native32Field.lean
theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
def montgomeryReduce (x : UInt64) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
def toCanonicalUInt32 (x : Field) : UInt32 in CompPoly/Fields/BabyBear/Fast/Convert.lean
instance instSub : Sub (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) : in CompPoly/Fields/BabyBear/Basic.lean
def ringEquiv : Field ≃+* BabyBear.Field in CompPoly/Fields/BabyBear/Fast.lean
def ofUInt32 (x : UInt32) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
@[simp] theorem modulus_toNat : modulus.toNat = KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
instance instNatSMul : SMul Nat (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ in CompPoly/Fields/BabyBear/Fast.lean
theorem toNat_reduceUInt64 (x : UInt64) : in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_square (x : Field) : toField (square x) = toField x * toField x in CompPoly/Fields/BabyBear/Fast.lean
def sub (x y : FastField F) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < BabyBear.fieldSize) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
def add (x y : Field) : Field in CompPoly/Fields/BabyBear/Fast.lean
theorem rModModulus_lt_fieldSize : rModModulus.toNat < BabyBear.fieldSize in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem fieldSize_add_fieldSize_lt_uint32Size : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y in CompPoly/Fields/BabyBear/Fast.lean
theorem toField_ofCanonicalNat_aux (n : Nat) (h : n < P.fieldSize) : in CompPoly/Fields/Montgomery/Native32Field.lean
instance instRatSMul : SMul ℚ (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
def twoAdicGenerators : List Field in CompPoly/Fields/BabyBear/Basic.lean
theorem rModModulus_cast : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem fieldSize_mul_uint32Size_lt_two64 : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
instance instInv : Inv (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1) in CompPoly/Fields/BabyBear/Basic.lean
theorem rModModulus_lt_fieldSize : rModModulus.toNat < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
instance instNatCast : NatCast (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
instance instIntSMul : SMul Int (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem fieldSize_mul_fieldSize_lt_two64 : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem fieldSize_pos : 0 < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def ofField (x : ZMod P.fieldSize) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem reduceUInt64_raw_cast (x : UInt64) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
instance instOne : One (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem nat_eq_of_field_eq {a b : Nat} (ha : a < BabyBear.fieldSize) in CompPoly/Fields/BabyBear/Fast/Convert.lean
def one : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
instance instDiv : Div (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_inv (x : FastField F) : toField x⁻¹ = (toField x)⁻¹ in CompPoly/Fields/Montgomery/Native32Field.lean
lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/BabyBear/Basic.lean
def toNat (x : Field) : Nat in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem raw_cast_eq_toField_mul (x : Field) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
def ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem reduceUInt32Lt2Modulus_cast (x : UInt32) in CompPoly/Fields/Montgomery/Native32Field.lean
def toNat (x : Field) : Nat in CompPoly/Fields/KoalaBear/Fast/Convert.lean
def reduceUInt64 (x : UInt64) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
instance instNNRatSMul : SMul ℚ≥0 (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
def ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem montgomeryReduceBoundedRaw_lt (x : UInt64) in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : BabyBear.Field) in CompPoly/Fields/BabyBear/Fast.lean
theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x in CompPoly/Fields/BabyBear/Fast.lean
private theorem toField_inv_pow (x : FastField F) : in CompPoly/Fields/Montgomery/Native32Field.lean
def sub (x y : Field) : Field in CompPoly/Fields/BabyBear/Fast.lean
theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y in CompPoly/Fields/BabyBear/Fast.lean
def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * BabyBear.fieldSize) : in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) : in CompPoly/Fields/BabyBear/Basic.lean
def mul (x y : FastField F) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_div (x y : FastField F) : toField (x / y) = toField x / toField y in CompPoly/Fields/Montgomery/Native32Field.lean
def toNat (x : FastField F) : Nat in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_reduceUInt64 (x : UInt64) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
def montgomeryReduceBounded (x : UInt64) in CompPoly/Fields/Montgomery/Native32Field.lean
instance instZero : Zero (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem quotient_cast (R p negInv : Nat) [Fact (Nat.Prime p)] (hR : 0 < R) in CompPoly/Fields/Montgomery/Basic.lean
theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n in CompPoly/Fields/BabyBear/Fast.lean
theorem uint32Size_lt_three_fieldSize : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem toField_eq_raw_mul_inv (x : Field) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem reduceUInt32Lt2Modulus_cast (x : UInt32) in CompPoly/Fields/BabyBear/Fast/Montgomery.lean
theorem toField_intCast (n : Int) : toField (n : Field) = (n : BabyBear.Field) in CompPoly/Fields/BabyBear/Fast.lean
theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y in CompPoly/Fields/BabyBear/Fast.lean
theorem two_lt_fieldSize : 2 < KoalaBear.fieldSize in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def toCanonicalUInt32 (x : FastField F) : UInt32 in CompPoly/Fields/Montgomery/Native32Field.lean
def ofInt (n : Int) : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
def raw (x : FastField F) : UInt32 in CompPoly/Fields/Montgomery/Native32Field.lean
@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1 in CompPoly/Fields/BabyBear/Basic.lean
theorem natCast_inj {p a b : Nat} (ha : a < p) (hb : b < p) in CompPoly/Fields/Montgomery/Basic.lean
theorem uint32Size_lt_three_fieldSize : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y in CompPoly/Fields/BabyBear/Fast.lean
def pow (x : FastField F) (n : Nat) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem rModModulus_cast : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem toField_ofCanonicalNat (n : Nat) (h : n < P.fieldSize) : in CompPoly/Fields/Montgomery/Native32Field.lean
private theorem toField_inv_raw (x : FastField F) : toField (inv x) = (toField x)⁻¹ in CompPoly/Fields/Montgomery/Native32Field.lean
theorem is_prime : Nat.Prime fieldSize in CompPoly/Fields/BabyBear/Basic.lean
theorem toField_reduceUInt64 (x : UInt64) : in CompPoly/Fields/Montgomery/Native32Field.lean
private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) : in CompPoly/Fields/BabyBear/Basic.lean
theorem toField_npow (x : FastField F) (n : Nat) : toField (x ^ n) = toField x ^ n in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_sub (x y : FastField F) : toField (x - y) = toField x - toField y in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toNat_reduceUInt64 (x : UInt64) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem toField_ofField (x : ZMod P.fieldSize) : toField (ofField (F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_neg (x : Field) : toField (-x) = -toField x in CompPoly/Fields/BabyBear/Fast.lean
def montgomeryNegInv : UInt32 in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem fieldSize_add_fieldSize_lt_two64 : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def ofField (x : KoalaBear.Field) : Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
def modulus64 : UInt64 in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem fieldSize_lt_uint32Size : KoalaBear.fieldSize < UInt32.size in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < P.fieldSize) : in CompPoly/Fields/Montgomery/Native32Field.lean
instance instAdd : Add (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toNat_ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : in CompPoly/Fields/BabyBear/Fast/Convert.lean
def toCanonicalUInt32 (x : Field) : UInt32 in CompPoly/Fields/KoalaBear/Fast/Convert.lean
def zero : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem nat_eq_of_field_eq {a b : Nat} (ha : a < KoalaBear.fieldSize) in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem r2ModModulus_cast : in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
theorem nat_eq_of_field_eq {a b : Nat} (ha : a < P.fieldSize) in CompPoly/Fields/Montgomery/Native32Field.lean
def neg (x : Field) : Field in CompPoly/Fields/BabyBear/Fast.lean
theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < KoalaBear.fieldSize) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem toField_mul (x y : FastField F) : toField (x * y) = toField x * toField y in CompPoly/Fields/Montgomery/Native32Field.lean
theorem two_lt_fieldSize : 2 < BabyBear.fieldSize in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < BabyBear.fieldSize in CompPoly/Fields/BabyBear/Fast/Prelude.lean
instance instNeg : Neg (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
theorem reduceUInt64_raw_cast (x : UInt64) : in CompPoly/Fields/Montgomery/Native32Field.lean
theorem fieldSize_add_fieldSize_lt_two64 : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
def invExponent : Nat in CompPoly/Fields/Montgomery/Native32Field.lean
instance instIntCast : IntCast (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
instance instRatCast : RatCast (FastField F) where in CompPoly/Fields/Montgomery/Native32Field.lean
def r2ModModulus : UInt32 in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
private theorem toField_mul_raw (x y : FastField F) : in CompPoly/Fields/Montgomery/Native32Field.lean
def twoAdicity : Nat in CompPoly/Fields/BabyBear/Basic.lean
theorem toField_eq_raw_mul_inv (x : Field) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem reduceUInt32Lt2Modulus_cast (x : UInt32) in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
def one : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
theorem toField_natCast (n : Nat) : toField (n : FastField F) = (n : ZMod P.fieldSize) in CompPoly/Fields/Montgomery/Native32Field.lean
def raw (x : Field) : UInt32 in CompPoly/Fields/BabyBear/Fast/Prelude.lean
theorem two_fieldSize_mul_uint32Size_lt_two64 : in CompPoly/Fields/BabyBear/Fast/Prelude.lean
lemma twoAdicGenerator_unit_mem_rootsOfUnity in CompPoly/Fields/BabyBear/Basic.lean
def mul (x y : Field) : Field in CompPoly/Fields/BabyBear/Fast.lean
def ofUInt32 (x : UInt32) : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
def toField (x : Field) : KoalaBear.Field in CompPoly/Fields/KoalaBear/Fast/Convert.lean
theorem reduceUInt64_raw_cast (x : UInt64) : in CompPoly/Fields/KoalaBear/Fast/Convert.lean
lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/BabyBear/Basic.lean
@[simp] theorem modulus64_toNat : modulus64.toNat = BabyBear.fieldSize in CompPoly/Fields/BabyBear/Fast/Prelude.lean
abbrev Field : Type in CompPoly/Fields/BabyBear/Fast/Prelude.lean
def montgomeryReduce (x : UInt64) : Field in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
theorem toField_zsmul (n : Int) (x : FastField F) : toField (n • x) = n • toField x in CompPoly/Fields/Montgomery/Native32Field.lean
def modulus : UInt32 in CompPoly/Fields/KoalaBear/Fast/Prelude.lean
def ofCanonicalNat (n : Nat) (_h : n < P.fieldSize) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
def montgomeryReduceBounded (x : UInt64) in CompPoly/Fields/KoalaBear/Fast/Montgomery.lean
theorem montgomeryReduceBoundedRaw_lt (x : UInt64) in CompPoly/Fields/Montgomery/Native32Field.lean
def inv (x : Field) : Field in CompPoly/Fields/BabyBear/Fast.lean
theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x in CompPoly/Fields/BabyBear/Fast.lean
def ofNat (n : Nat) : Field in CompPoly/Fields/BabyBear/Fast/Convert.lean
def fieldSize : Nat in CompPoly/Fields/BabyBear/Basic.lean
lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt in CompPoly/Fields/BabyBear/Basic.lean
theorem toField_pow (x : FastField F) (n : Nat) : toField (pow x n) = toField x ^ n in CompPoly/Fields/Montgomery/Native32Field.lean
def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * P.fieldSize) : in CompPoly/Fields/Montgomery/Native32Field.lean
def inv (x : FastField F) : FastField F in CompPoly/Fields/Montgomery/Native32Field.lean
theorem toField_nsmul (n : Nat) (x : FastField F) : toField (n • x) = n • toField x in CompPoly/Fields/Montgomery/Native32Field.lean
theorem fieldSize_mul_fieldSize_lt_two64 : in CompPoly/Fields/BabyBear/Fast/Prelude.lean

✏️ **Affected:** 34 declaration(s) (line number changed)

def div (x y : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L774 to L62
def invExponent : Nat in CompPoly/Fields/KoalaBear/Fast.lean moved from L748 to L54
def ringEquiv : Field ≃+* KoalaBear.Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L1003 to L65
theorem ofField_toField (x : Field) : ofField (toField x) = x in CompPoly/Fields/KoalaBear/Fast.lean moved from L843 to L75
theorem toField_square (x : Field) : toField (square x) = toField x * toField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L1034 to L124
theorem toField_one : toField (1 : Field) = 1 in CompPoly/Fields/KoalaBear/Fast.lean moved from L866 to L89
def add (x y : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L678 to L31
theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y in CompPoly/Fields/KoalaBear/Fast.lean moved from L897 to L99
def pow (x : Field) (n : Nat) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L744 to L51
theorem toField_intCast (n : Int) : toField (n : Field) = (n : KoalaBear.Field) in CompPoly/Fields/KoalaBear/Fast.lean moved from L1172 to L144
theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L1186 to L154
theorem toField_neg (x : Field) : toField (-x) = -toField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L940 to L104
theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : KoalaBear.Field) in CompPoly/Fields/KoalaBear/Fast.lean moved from L1220 to L174
theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y in CompPoly/Fields/KoalaBear/Fast.lean moved from L1152 to L134
def neg (x : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L685 to L35
theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L1232 to L184
theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y in CompPoly/Fields/KoalaBear/Fast.lean moved from L977 to L109
theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n in CompPoly/Fields/KoalaBear/Fast.lean moved from L1199 to L164
theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n in CompPoly/Fields/KoalaBear/Fast.lean moved from L1193 to L159
theorem ringEquiv_symm_apply (x : KoalaBear.Field) : ringEquiv.symm x = ofField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L1017 to L119
theorem toField_zero : toField (0 : Field) = 0 in CompPoly/Fields/KoalaBear/Fast.lean moved from L859 to L84
theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L1226 to L179
theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : KoalaBear.Field) in CompPoly/Fields/KoalaBear/Fast.lean moved from L1214 to L169
theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L1179 to L149
theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x in CompPoly/Fields/KoalaBear/Fast.lean moved from L1013 to L114
theorem toField_natCast (n : Nat) : toField (n : Field) = (n : KoalaBear.Field) in CompPoly/Fields/KoalaBear/Fast.lean moved from L1163 to L139
def mul (x y : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L729 to L43
theorem toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x in CompPoly/Fields/KoalaBear/Fast.lean moved from L836 to L70
def sub (x y : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L704 to L39
theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y in CompPoly/Fields/KoalaBear/Fast.lean moved from L875 to L94
def square (x : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L739 to L47
theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ in CompPoly/Fields/KoalaBear/Fast.lean moved from L1137 to L129
def inv (x : Field) : Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L757 to L58
theorem toField_injective : Function.Injective (toField : Field → KoalaBear.Field) in CompPoly/Fields/KoalaBear/Fast.lean moved from L854 to L79

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

Review Findings for CompPoly Pull Request

1. Adherence to Style and Naming Guidelines

Naming Conventions: The PR successfully follows the project's naming dictionary and conventions. Files use UpperCamelCase (e.g., Native32Field.lean), types/classes use UpperCamelCase (e.g., Mont32Field), and theorems use snake_case (e.g., u_eq_nat).
Hypotheses and Binders: Hypotheses are correctly placed to the left of the colon (e.g., in reduceNat_cast), and there is a consistent space after binders (e.g., ∀ x,).
Formatting: The diff adheres to the 2-space indentation rule and places by and infix operators (=, :=) at the end of lines before breaks, as required.
Modern Syntax: The code correctly prefers fun x ↦ and the where syntax for instances.

2. Documentation Standards

LaTeX Delimiters: Some mathematical expressions in docstrings and file headers (e.g., 2^31 - 2^27 + 1 in CompPoly/Fields/BabyBear/Basic.lean and gcd(R, p) = 1 in CompPoly/Fields/Montgomery/Basic.lean) are written in plaintext. These should be wrapped in LaTeX delimiters ( $ ... $ ) to comply with the citation and documentation standards.
Theorem Docstrings: While definitions are well-documented, several significant correctness theorems (e.g., toField_eq_raw_mul_inv, reduceUInt64_raw_cast, and montgomeryReduceBounded_cast) lack docstrings. The project guidelines request docstrings for every definition and major theorem.

3. Progress and Framework Adherence

Shared Implementation: This PR makes significant progress by abstracting 32-bit-word Montgomery arithmetic into a shared framework in CompPoly/Fields/Montgomery/. This reduces logic duplication across the BabyBear and KoalaBear modules.
Handbook and Wiki: The update to docs/wiki/binary-fields-and-ntt.md correctly reflects the structural changes in the Fields/ directory.
Module Layout: The split into Basic.lean and Fast.lean with a facade module in the parent file correctly follows the project's layout for optimized field implementations.

📄 **Per-File Summaries**

CompPoly.lean: This update expands the CompPoly library's top-level imports to include specialized submodules for BabyBear and KoalaBear fields, as well as native 32-bit Montgomery arithmetic implementations.
CompPoly/Fields/BabyBear.lean: Refactors the BabyBear.lean file into a facade module that re-exports the BabyBear field implementation from the newly created Basic and Fast submodules. The change moves explicit definitions, primality proofs, and root-of-unity tables to these specialized components while maintaining a central entry point.
CompPoly/Fields/BabyBear/Basic.lean: This file defines the BabyBear prime field ($2^{31} - 2^{27} + 1$) used by Risc Zero and formally proves the primality of its modulus. It provides a precomputed table of two-adic generators and includes theorems verifying that these elements are primitive $2^n$-th roots of unity.
CompPoly/Fields/BabyBear/Fast.lean: This new file implements optimized Montgomery-form arithmetic for the BabyBear field using 32-bit native words. It defines standard field operations and provides correctness theorems—re-exported from a generic framework—to ensure consistency with the canonical BabyBear.Field representation.
CompPoly/Fields/BabyBear/Fast/Convert.lean: This file introduces definitions and theorems for converting between canonical representations (such as Nat, UInt64, and ZMod) and the fast Montgomery representation for the BabyBear field. It instantiates generic logic from the Montgomery.Native32 module to provide verified conversion utilities, and contains no sorry placeholders.
CompPoly/Fields/BabyBear/Fast/Montgomery.lean: This file introduces specialized Montgomery reduction definitions and correctness theorems for the BabyBear field by instantiating generic 32-bit native-word reduction primitives. These functions are designed for high performance via inlining and include no sorry or admit placeholders.
CompPoly/Fields/BabyBear/Fast/Prelude.lean: Introduces the BabyBear.Fast namespace, providing native UInt32 constants and an instMont32Field instance to enable high-performance Montgomery arithmetic for the BabyBear field. The file includes new definitions and verified theorems that link hardware-level representations to mathematical field properties without any sorry placeholders.
CompPoly/Fields/KoalaBear/Fast.lean: This refactor significantly simplifies the KoalaBear fast field implementation by delegating modular arithmetic operations, field instances, and correctness proofs to the generic Montgomery.Native32 module. The changes replace manual low-level proofs and definitions with calls to shared generic theorems, maintaining the existing field properties without introducing any sorry or admit placeholders.
CompPoly/Fields/KoalaBear/Fast/Convert.lean: This new file introduces definitions and theorems for converting between the fast Montgomery representation and canonical forms (such as Nat and ZMod) for the KoalaBear field. These conversions are implemented by specializing the generic Montgomery.Native32 implementation to the KoalaBear prime and do not contain any sorry placeholders.
CompPoly/Fields/KoalaBear/Fast/Montgomery.lean: This new file introduces specialized Montgomery reduction definitions and correctness theorems for the KoalaBear field by re-exporting generic routines from the Montgomery.Native32 framework. The implementation uses inlining to ensure efficient, monomorphic machine code for high-performance 32-bit field arithmetic, and it contains no sorry placeholders.
CompPoly/Fields/KoalaBear/Fast/Prelude.lean: Introduces the basic definitions and numeric constants for a fast, native 32-bit Montgomery implementation of the KoalaBear field. It establishes the Mont32Field instance through several theorems verified via decide and defines the core Field carrier type.
CompPoly/Fields/Montgomery/Basic.lean: This file introduces the core definitions and theorems for radix-generic Montgomery reduction, including the fundamental divisibility identity and the functional reduceNat algorithm. It establishes that Nat-level Montgomery reduction correctly implements multiplication by the inverse of the Montgomery modulus in ZMod p and contains no sorry or admit placeholders.
CompPoly/Fields/Montgomery/Native32.lean: This file introduces a bridge between generic Montgomery reduction and native 32-bit implementations using UInt32 and UInt64. It provides theorems u_eq_nat and u_lt_two_mul to prove that native bitwise operations correctly implement the Montgomery quotient and remain within expected bounds.
CompPoly/Fields/Montgomery/Native32Field.lean: This new file introduces the Mont32Field typeclass and FastField carrier to provide a unified, performant implementation of 32-bit prime fields using Montgomery reduction. It defines specialized arithmetic operations and establishes a full Field instance by proving their equivalence to the canonical ZMod representation. No sorry or admit placeholders are used in the definitions or proofs.
CompPoly/Fields/README.md: The documentation was updated to reflect a modular refactoring of field implementations, specifically reorganizing BabyBear and KoalaBear into submodules. It introduces a new shared Montgomery reduction framework in the Montgomery/ directory, which provides a generic, word-level bridge for efficient 32-bit field operations.
docs/wiki/binary-fields-and-ntt.md: This documentation update reflects the reorganization and expansion of field implementations by adding subdirectories for optimized 'Fast' operations in BabyBear and KoalaBear fields, alongside the introduction of a dedicated Montgomery reduction module.
tests/CompPolyTests.lean: This update integrates the fast implementation of the BabyBear field into the test suite by adding the relevant import to the main test aggregator file. No new theorems, definitions, or 'sorry' placeholders were introduced in this specific file.
tests/CompPolyTests/Fields/BabyBear/Fast.lean: This new file introduces a regression test suite for the BabyBear.Fast field implementation, providing checks for Montgomery-represented arithmetic operations and conversions. The tests use #guard statements to verify results against both constant values and the standard BabyBear.Field definition.

Last updated: 2026-06-29 12:47 UTC.

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

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

f5eb442

mitschabaude mentioned this pull request Jul 13, 2026

refactor(fields): clarify Montgomery reduction core graikos/CompPoly#1

Draft

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 7 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

Review Findings for CompPoly Pull Request

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

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

Mathematical Formalization

Field Implementation and Optimization

Architecture and Refactoring

Documentation and Testing

Review Findings for CompPoly Pull Request

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Jun 24, 2026 •

edited

Loading