Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta)

[mitschabaude-bot]

Proven multi-limb Montgomery field arithmetic, structured for fast interpreted/compiled evaluation. The new work is the top 4 commits (97464eb..28c8931); the branch is based on fast_kb_bb_fields (#258), so the diff includes that until it merges.

• Native64x8Defs / Native64x8Mul — raw eight-limb (64×8) CIOS Montgomery multiplication over straight-line accumulator code, with the fused blocks split into variable-input defs (mulAccum / mulReduce) so per-limb specs stay provable by narrow omega.
• Native64x8 / Native64x8Field — the carrier type, ring/field structure, and the toField bridge to ZMod p (proved, no axioms beyond the classical trio).
• Pasta — both Pasta primes instantiated (negInv = 0xffffffff for both), primality via Pratt certificates.

Downstream consumer already exists: the Zcash ironwood verifier-key certificate runs its Pippenger MSM + radix-2 FFT on this arithmetic (vendored copy for now; the vendored copy gets deleted in favor of the pin once this lands).

Update: the runtime definitions (word helpers, Limbs8, add/sub/neg, State9, and the CIOS multiplication) are now split out verbatim into Montgomery/Native64x8Defs.lean, a module with zero imports. Rationale: downstream consumers put this module into precompileModules native-compilation lanes, and precompileModules compiles the entire import closure — with the defs interleaved into Native64x8.lean, that closure includes mathlib. All theorems stay in Native64x8.lean, which imports the defs module. The ironwood consumer already uses exactly this shape (its vendored copy is a zero-import defs module).

Update 2: the PR now also carries the scalar radix-2 DIT FFT over Limbs8 Montgomery elements (Montgomery/ScalarFft.lean), generic over the modulus like the rest of the defs module. It imports only Native64x8Defs — zero-import for the same precompileModules reason — and is runtime definitions only; the correctness proofs live downstream in ironwood until upstreamed.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta)

Proven eight-limb Montgomery field arithmetic for 255-bit moduli, instantiated on the Pasta curves (Pallas/Vesta), with a zero-import runtime definitions module for native compilation. The PR also refactors the existing BabyBear and KoalaBear fast field implementations to use a shared 32-bit Montgomery library, consolidates NTT domain structures, and updates documentation and benchmarks. No new sorrys or admits are introduced.

---

Statistics

Metric	Count
📝 Files Changed	30
✅ Lines Added	3548
❌ 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: 320 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/Fields/Montgomery/Native64x8.lean (44)

• private theorem carry_top_zero {S A B Q c : ℕ} (h : S + 2 ^ 256 * c = A + B)
• private theorem cond_eq_mod {T Q : ℕ} (h : T < 2 * Q) :
• private theorem cond_of_borrow_one {M Q T : ℕ} (h : M + Q = T + 2 ^ 256) (hM : M < 2 ^ 256) :
• private theorem cond_of_borrow_zero {M Q T : ℕ} (h : M + Q = T) (hM : M < 2 ^ 256) :
• private theorem land_mask32 (x : ℕ) : x &&& 4294967295 = x % 4294967296
• private theorem sub_of_borrow_one {A B Q D E c : ℕ} (hD : D + B = A + 2 ^ 256 * 1)
• private theorem sub_of_borrow_zero {A B Q D : ℕ} (h : D + B = A + 2 ^ 256 * 0)
• private theorem toNat_zero : (0 : UInt64).toNat = 0
• theorem Limbs8.ext_of_toNat {x y : Limbs8} (hx : x.Bounded) (hy : y.Bounded)
• theorem Limbs8.toNat_lt {x : Limbs8} (hx : x.Bounded) : x.toNat < 2 ^ 256
• theorem adcLo_lt (x y c : UInt64) : (adcLo x y c).toNat < 2 ^ 32
• theorem adc_spec (x y c : UInt64) (hx : x.toNat < 2 ^ 32) (hy : y.toNat < 2 ^ 32)
• theorem adc_spec_wide (x y c : UInt64) (hx : x.toNat < 2 ^ 33) (hy : y.toNat < 2 ^ 32)
• theorem addLimbs_bounded (a b : Limbs8) : (addLimbs a b).Bounded
• theorem addLimbs_toNat (a b : Limbs8) (ha : a.Bounded) (hb : b.Bounded) :
• theorem add_bounded (q a b : Limbs8) : (add q a b).Bounded
• theorem add_lt (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
• theorem add_toNat (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
• theorem borrow_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 : ℕ}
• theorem carry_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 : ℕ}
• theorem condSub_bounded (q t : Limbs8) (ht : t.Bounded) : (condSub q t).Bounded
• theorem condSub_lt (q t : Limbs8) (hq : q.Bounded) (ht : t.Bounded)

…and 170 more not listed.

✏️ 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.

---

📄 **Per-File Summaries**

• CompPoly.lean: This change adds import statements for three sets of field-related submodules: CompPoly.Fields.BabyBear.Basic and Fast; a suite of CompPoly.Fields.Montgomery files (Basic, Native32, Native32Field, Native64x8, Native64x8Defs, Native64x8Field, Native64x8Mul, ScalarFft); and CompPoly.Fields.Pasta.Basic and Fast. These new imports expose additional field arithmetic implementations and supporting definitions for use throughout the CompPoly library.
• CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean: The change modifies how frobenius_fixed is proved in fastKoalaBearFiniteFieldContext. Instead of using KoalaBear.Fast.toField_injective and KoalaBear.Fast.toField_npow, it now uses Montgomery.Native32.toField_injective and Montgomery.Native32.toField_npow, and simplifies the simpa by dropping the call to ZMod.pow_card. Furthermore, the proof of fastKoalaBearPrimitiveRoot_order is updated: it replaces KoalaBear.Fast.ringEquiv_apply and KoalaBear.Fast.toField_ofField with KoalaBear.Fast.ringEquiv and KoalaBear.Fast.ofField in the simpa.
• CompPoly/Fields/BabyBear.lean: This file was completely rewritten from a standalone definition of the BabyBear field (with its own modulus, prime proof, two-adic generator table, and root-of-unity lemmas) into a thin facade module that re-exports the canonical ZMod model from CompPoly.Fields.BabyBear.Basic and a native-word implementation from CompPoly.Fields.BabyBear.Fast. All previously defined content — including the field size, primality theorem, precomputed two-adic generators, and lemmas about their order and primitivity — has been removed; the new module no longer defines any field structure or root-of-unity properties itself.
• CompPoly/Fields/BabyBear/Basic.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This new file defines th...oAdicGenerators_order`.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• CompPoly/Fields/BabyBear/Fast.lean: This new file provides a fast Montgomery-arithmetic implementation of the BabyBear field using 32-bit native words. It defines an instMont32Field instance of Mont32Field for BabyBear.fieldSize with the concrete BabyBear constants (modulus32, modulus64, rModModulus, r2ModModulus, montgomeryNegInv), an abbreviation Field for the carrier type FastField BabyBear.fieldSize, and two conversion functions (ofUInt32 from UInt32, ofField from the canonical BabyBear.Field). It also supplies a ringEquiv that establishes a ring isomorphism between the fast Montgomery representation and the canonical BabyBear.Field.
• CompPoly/Fields/KoalaBear/Basic.lean: The diff removes two set_option maxRecDepth pragmas (previously set to 4096 and 100000) from the file. It also simplifies both the statement and proof of primitiveRoot_pow_127_eq_twoAdicGenerator: the index is now given directly as twoAdicity instead of a cast Fin (twoAdicity+1) via ⟨twoAdicity, by omega⟩, and the proof is rewritten using norm_num followed by rfl in place of unfold primitiveRoot twoAdicity; decide.
• CompPoly/Fields/KoalaBear/Fast.lean: This file was rewritten to delegate all fast KoalaBear field arithmetic to the shared CompPoly/Fields/Montgomery.Native32Field library. The old custom constants (modulus, rModModulus, etc.), private correctness lemmas, and hand-written add/mul/inv operations are replaced by a single instMont32Field instance that supplies the KoalaBear prime’s parameters. The carrier type is now FastField KoalaBear.fieldSize (an abbreviation from the shared library), and conversions (ofUInt32, ofField) delegate to the shared API. The ring equivalence ringEquiv is obtained from Montgomery.Native32.ringEquiv. Additionally, a new section adds twoAdicGenerators, a List Field of precomputed Montgomery two-adic roots, together with the theorem twoAdicGenerators_eq_map showing they match the canonical generators under ofField.
• CompPoly/Fields/Montgomery/Basic.lean: This diff adds a new file CompPoly/Fields/Montgomery/Basic.lean, which introduces the Montgomery namespace and defines two core functions (reduceNat and reduceNatQuotient) for natural-number Montgomery reduction, along with five supporting lemmas. The lemma reduceNatQuotient_lt_two_mul bounds the pre-subtraction quotient below 2*p, reduceNat_lt proves the final result is below the modulus p, dvd_add establishes the key divisibility R ∣ x + ((x%R * negInv)%R) * p under the hypothesis negInv * p % R = R-1, and reduceNatQuotient_cast/reduceNat_cast show that both the quotient and the final reduced value correspond to (x : ZMod p) * (R : ZMod p)⁻¹. A final lemma natCast_inj_of_lt provides an injectivity result for Nat.cast into ZMod p for values below p. No sorry or admit are present.
• CompPoly/Fields/Montgomery/Native32.lean: This file introduces CompPoly/Fields/Montgomery/Native32.lean, a new module providing raw 32-bit word-level operations for Montgomery reduction, using a radix of 2^32 and lowering to UInt32 and UInt64. It defines the core functions reduceRaw, reduceQuotient, and conditionalSubtract, along with a series of theorems (reduceRaw_eq_conditionalSubtract, reduceQuotient_toNat, conditionalSubtract_toNat, reduceRaw_toNat, conditionalSubtract_lt, conditionalSubtract_cast, reduceRaw_lt, and reduceRaw_cast) that prove these functions agree with the existing Nat-level specification in Montgomery.Basic (e.g., reduceNatQuotient, reduceNat, reduceNat_lt, reduceNat_cast). The final theorem reduceRaw_cast additionally shows that reduceRaw correctly computes the multiplication by the inverse of the radix in ZMod modulus under the standard Montgomery conditions, given Fact (Nat.Prime modulus) and a suitable negInv. The file contains no sorry or admit statements.
• CompPoly/Fields/Montgomery/Native32Field.lean: Summary unavailable — error: Model 'deepseek/deepseek-v4-flash' returned no parseable structured output (finish_reason=error)
• CompPoly/Fields/Montgomery/Native64x8.lean: This new file provides the correctness proofs for Montgomery arithmetic over eight 32-bit limbs (Limbs8), the multi-limb sibling of Native32.lean. It states and proves the toNat specifications for every raw word helper: adc_spec, adc_spec_wide, sbb_spec, mac_spec, and montM_toNat give existential or equational characterizations of the carry/borrow/multiply-accumulate helpers; adcLo_lt, sbbLo_lt, macLo_lt, montM_lt give bound lemmas. For the limb vector itself, it proves Limbs8.zero_bounded, Limbs8.zero_toNat, Limbs8.one_bounded, Limbs8.one_toNat, Limbs8.ofNat_bounded, Limbs8.ofNat_toNat, the extensionality lemma Limbs8.ext_of_toNat, and the value bound Limbs8.toNat_lt. It then proves the two telescoping chain lemmas carry_chain_sum and borrow_chain_sum that combine eight-step carry/borrow chains into a single identity. Finally, it proves the correctness of the field operations: addLimbs_toNat and subLimbs_spec for the underlying carry/borrow chains, and then condSub_toNat, add_toNat, sub_toNat, neg_toNat (with companion bound lemmas) for conditional subtraction, modular addition, modular subtraction, and modular negation on Limbs8, all under the assumption that 2 * q.toNat < 2^256 (i.e., the modulus is below 2^255).
• CompPoly/Fields/Montgomery/Native64x8Defs.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This new file provides z... that imports this one.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• CompPoly/Fields/Montgomery/Native64x8Field.lean: This new file defines a fast eight-limb Montgomery field for prime moduli below 2^255, serving as the multi-limb analogue of Native32Field. It introduces the Mont64x8Field typeclass (containing per-field constants such as modulusLimbs, rModModulus, r2ModModulus, and montgomeryNegInv, with side conditions discharged by decide), the FastField carrier (a subtype of Limbs8 with a boundedness and a < modulus proof), and its arithmetic (add, sub, neg, mul, square, pow, inv, div) built on the raw operations from Native64x8Mul. It provides conversion functions (toLimbs8, toNat, toField, ofCanonicalNat, ofNat, ofField), a suite of @[simp] correctness theorems (e.g., toField_add, toField_mul, toField_inv, toField_pow, toField_natCast) establishing that toField is a ring homomorphism, and the ringEquiv FastField modulus ≃+* ZMod modulus together with the transferred instField and instNonBinaryField instances.
• CompPoly/Fields/Montgomery/Native64x8Mul.lean: Added the file CompPoly/Fields/Montgomery/Native64x8Mul.lean containing a correctness proof for eight-limb CIOS Montgomery multiplication. New theorems include: sum8_mul and mul_sum8 distributing scalar multiplication over limb recomposition; Limbs8.toNat_mod extracting the low limb; State9.zero_bounded, State9.zero_toNat, and State9.toNat_eq for the accumulator; mulAccum_spec stating that mulAccum exactly adds a * bi to the accumulator while preserving limb bounds; mulReduce_spec stating that mulReduce adds a multiple of the modulus to cancel the low limb and that division by 2^32 is exact; mulRound_spec giving the round invariant, bound below 2*q, and an existence claim; and mul_spec asserting that mul is canonical and satisfies 2 ^ 256 * ⟦mul a b⟧ ≡ ⟦a⟧ * ⟦b⟧ [MOD q]. Several private helper lemmas (montM_low_zero, round_bound, accum_assemble, reduce_assemble, fold8, mul_finish) support the main proofs.
• CompPoly/Fields/Montgomery/ScalarFft.lean: Adds CompPoly/Fields/Montgomery/ScalarFft.lean, which defines two runtime-only functions for a radix-2 decimation-in-time FFT over eight-limb Montgomery residues: bitreverse (n l : Nat) : Nat (bit-reversal permutation index) and fft (q : Limbs8) (negInv : UInt64) (a0 : Array Limbs8) (tw : Array Limbs8) (logN : Nat) : Array Limbs8 (in-place FFT using the add, sub, mul primitives from Native64x8). The file deliberately imports only CompPoly.Fields.Montgomery.Native64x8Defs (itself zero-import) to keep the precompileModules closure small; no sorry or admit appear.
• CompPoly/Fields/Pasta.lean: Created a new facade module CompPoly/Fields/Pasta.lean that re-exports the Pasta (Pallas/Vesta) base field implementations from CompPoly.Fields.Pasta.Basic and CompPoly.Fields.Pasta.Fast, providing a single import point for both the canonical ZMod models with primality certificates and the native-word eight-limb Montgomery representations.
• CompPoly/Fields/Pasta/Basic.lean: This new file CompPoly/Fields/Pasta/Basic.lean defines the two 255-bit primes underlying the Pallas and Vesta curves and provides their primality certificates. It introduces Pallas.baseFieldSize and Vesta.baseFieldSize as Nat constants (each equal to 1 mod 2^32 with 2-adicity 32), and uses the PrattCertificate' API from CompPoly.Fields.PrattCertificate to provide Pallas.baseFieldSize_is_prime and Vesta.baseFieldSize_is_prime along with Fact instances, enabling the Field instance for each ZMod base field (Pallas.BaseField and Vesta.BaseField, both defined as abbrevs). The file also defines Pallas.scalarFieldSize as Vesta.baseFieldSize, Vesta.scalarFieldSize as Pallas.baseFieldSize, and corresponding ScalarField abbreviations that alias the other curve's base field, establishing the 2-cycle relationship. No sorry or admit is present.
• CompPoly/Fields/Pasta/Fast.lean: This new file adds fast, native-word Montgomery implementations for the Pallas and Vesta base fields (the Pasta curves) using CompPoly.Fields.Montgomery.Native64x8Field. For each (Pallas.Fast and Vesta.Fast) it provides: an instMont64x8Field instance with the eight‑limb modulus, R, R², and the Montgomery inverse constant (montgomeryNegInv = 0xffffffff); the carrier type Field (an abbreviation of FastField); conversion functions ofField, toField, toNat; a ringEquiv showing the structure is equivalent to the canonical BaseField; and the two simp theorems toField_ofField / ofField_toField. No sorry or admit are present.
• CompPoly/Fields/README.md: The README was reorganized to document a new Montgomery subdirectory containing generic radix reduction (Montgomery/Basic.lean), raw UInt32/UInt64 word-level operations (Montgomery/Native32.lean), a shared FastField carrier and canonical-field bridge for 32-bit moduli (Montgomery/Native32Field.lean), eight-limb Montgomery word operations for moduli below 2^255 (Montgomery/Native64x8.lean), correctness of eight-limb CIOS multiplication (Montgomery/Native64x8Mul.lean), and the per-field bounded carrier and bridge for 255-bit moduli (Montgomery/Native64x8Field.lean). A new Pasta facade (Pasta.lean) re-exports the Pallas/Vesta base fields, detailed in Pasta/Basic.lean with Pratt primality certificates, and their fast implementations in Pasta/Fast.lean as wrappers over Montgomery/Native64x8Field.lean. BabyBear and KoalaBear were split into submodules: BabyBear/Basic.lean and BabyBear/Fast.lean (and similarly for KoalaBear), with the fast modules now described as namespaced APIs forwarding Montgomery/Native32Field.lean operations and providing @[simp] equivalence lemmas. The entries for BabyBear.lean and KoalaBear.lean were updated to describe them as facades.
• CompPoly/Univariate/NTT/Domain.lean: This change removes the natCast_ne_zero field from the Domain structure (which was a proof obligation that (2^logN : R) ≠ 0) and promotes it to a standalone theorem natCast_ne_zero in the Domain namespace. The Domain.inverse definition is simplified by deleting its corresponding natCast_ne_zero argument. The new theorem leverages the existing primitive witness, IsPrimitiveRoot, to derive the nonzeroness using D.primitive.neZero'.out, thereby eliminating the redundant bookkeeping field and making the Domain structure leaner.
• CompPoly/Univariate/NTT/KoalaBear.lean: This diff removes two theorems and adds significant refactoring to the KoalaBear NTT domain definitions. Specifically, the file deletes twoPowNatCast_ne_zero and fast_twoPowNatCast_ne_zero (along with fast_isPrimitiveRoot_twoAdicGenerator), and eliminates the natCast_ne_zero field from the Domain structures domainOfLogN and fastDomainOfLogN. It also changes fastDomainOfLogN.omega from KoalaBear.Fast.ofField KoalaBear.twoAdicGenerators[...] to directly KoalaBear.Fast.twoAdicGenerators[...], and rewrites the primitive proof for the fast domain to use map_of_injective on the original generator's primitive root property, now relying on an equality KoalaBear.Fast.twoAdicGenerators_eq_map rather than the removed helper lemma.
• bench/CompPolyBench/Common.lean: In checksumKoalaBearFast, the explicit call KoalaBear.Fast.toNat x was replaced with the method-style x.toNat. This is a syntactic refactor that does not change the function's behavior but improves consistency with other similar conversions in the file.
• bench/CompPolyBench/Univariate/Common.lean: The diff removes the locally-defined ring equivalence koalaBearFastRingEquiv, the theorems koalaBearFast_isPrimitiveRoot_twoAdicGenerator and koalaBearFast_twoPowNatCast_ne_zero, and the NTT domain definition koalaBearFastDomainOfLogN. It then refactors koalaBearFastMulNttDomain and koalaBearFastBestDomainForLength? to use the corresponding centralized definitions CPolynomial.NTT.KoalaBear.fastDomainOfLogN and CPolynomial.NTT.KoalaBear.fastBestDomainForLength? respectively. This eliminates duplicate code and consolidates fast KoalaBear NTT support into the shared CPolynomial.NTT.KoalaBear module.
• bench/CompPolyBench/Univariate/NTT/FastMul.lean: This pull request refactors the KoalaBear univariate multiplication benchmark. Key changes include: adding a private BenchField structure (with id and checksum fields) to encapsulate a benchmark field; renaming local variables (e.g., koalaBearMulNttFastPlan to canonicalPlan, and each benchmark record from koalaBearMul... to the more generic canonicalNtt/fastNtt); introducing canonicalField and fastField values of type BenchField for the canonical and fast fields, and computing canonicalChecksum/fastChecksum via checksumCPolynomial. All benchmark registrations (runTimed calls) were updated to use these new variable names and the BenchField.id and checksum references. This change standardizes the benchmark structure and prepares for potential extraction of field-specific configuration. No sorry or admit were introduced.
• docs/wiki/binary-fields-and-ntt.md: This documentation file (docs/wiki/binary-fields-and-ntt.md) has been updated to reflect the restructuring of the project's directory layout under CompPoly/Fields/. New subdirectories and files have been added to the tree diagram: for BabyBear/Fast/ and KoalaBear/Fast/, the files Prelude.lean, Montgomery.lean, and Convert.lean are now listed; additionally, a new top-level Montgomery/ directory has been introduced, containing Basic.lean, Native32.lean, and Native32Field.lean. The Binary/ directory and its contents remain unchanged.
• tests/CompPolyTests.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The file now imports `Co... field implementations.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• tests/CompPolyTests/Fields/BabyBear/Fast.lean: This new file (tests/CompPolyTests/Fields/BabyBear/Fast.lean) adds a test suite for the executable Montgomery representation of the BabyBear field. It imports CompPoly.Fields.BabyBear.Fast and, within the BabyBear.Fast namespace, uses a series of #guard commands to verify concrete arithmetic properties — including zero, one, addition/subtraction wraparound, negation, multiplication, exponentiation, inversion, and division — by comparing the .toNat (or .toField / .toUInt32) of results against expected values. These tests serve as regression checks ensuring that the fast field implementation behaves identically to the reference BabyBear.Field across a range of operations.
• tests/CompPolyTests/Fields/KoalaBear/Fast.lean: This diff updates the #guard regression checks in tests/CompPolyTests/Fields/KoalaBear/Fast.lean to use the new explicit .val, .toUInt32, .toNat, and .toField accessor methods instead of the previous raw, toCanonicalUInt32, toNat, and toField top-level functions. The check for the representation of 1 : Field now directly references Montgomery.Native32.Mont32Field.rModModulus with an explicit modulus := binder for KoalaBear.fieldSize. The squaring test is also simplified from square (12345 : Field) to (12345 : Field) * 12345. These changes reflect a refactor of the low-level field API to use field projections and remove the earlier standalone helper functions.
• tests/CompPolyTests/Fields/Montgomery/Native64x8.lean: This file adds regression tests for the eight-limb Montgomery arithmetic operations (Limbs8) for both the Vesta and Pallas base fields. It defines constants for the modulus (q, pq), the Montgomery negative inverse (negInv, pNegInv), the Montgomery radix (rMod), and sample limbs (a, b, montA, montB, montAB, pMontA, pMontB, pMontAB). The #guard statements verify that core operations—condSub, add, sub, neg, mul, and square—produce expected results (e.g., mul q negInv montA montB = montAB). It also tests the field arithmetic via the carrier types F (Vesta.Fast.Field) and G (Pallas.Fast.Field) and confirms that the canonical bridge functions Vesta.Fast.toField, Vesta.Fast.ofField, Pallas.Fast.toField, and Pallas.Fast.ofField align with ZMod arithmetic.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): CompPoly/Univariate/NTT/BabyBear.lean

---

Last updated: 2026-07-26 07:01 UTC.