Simplify 32-bit Montgomery fields

CompPoly.lean

@@ -68,9 +68,6 @@ import CompPoly.Fields.BN254
 import CompPoly.Fields.BabyBear
 import CompPoly.Fields.BabyBear.Basic
 import CompPoly.Fields.BabyBear.Fast
-import CompPoly.Fields.BabyBear.Fast.Convert
-import CompPoly.Fields.BabyBear.Fast.Montgomery
-import CompPoly.Fields.BabyBear.Fast.Prelude
 import CompPoly.Fields.Basic
 import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT
 import CompPoly.Fields.Binary.AdditiveNTT.Algorithm
@@ -107,9 +104,6 @@ import CompPoly.Fields.Goldilocks
 import CompPoly.Fields.KoalaBear
 import CompPoly.Fields.KoalaBear.Basic
 import CompPoly.Fields.KoalaBear.Fast
-import CompPoly.Fields.KoalaBear.Fast.Convert
-import CompPoly.Fields.KoalaBear.Fast.Montgomery
-import CompPoly.Fields.KoalaBear.Fast.Prelude
 import CompPoly.Fields.Mersenne
 import CompPoly.Fields.Montgomery.Basic
 import CompPoly.Fields.Montgomery.Native32

CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean

@@ -123,10 +123,9 @@ def fastKoalaBearFiniteFieldContext :
     simp [KoalaBear.Field, Nat.card_eq_fintype_card, ZMod.card]
   frobenius_fixed := by
     intro a
-    apply KoalaBear.Fast.toField_injective
-    rw [KoalaBear.Fast.toField_npow]
-    simpa [KoalaBear.Field, KoalaBear.fieldSize] using
-      ZMod.pow_card (KoalaBear.Fast.toField a)
+    apply Montgomery.Native32.toField_injective
+    rw [Montgomery.Native32.toField_npow]
+    simp [KoalaBear.fieldSize]
 
 /-- Primitive generator transported to native-word fast KoalaBear. -/
 def fastKoalaBearPrimitiveRoot : KoalaBear.Fast.Field :=
@@ -139,7 +138,7 @@ lemma fastKoalaBearPrimitiveRoot_order :
   have h := MulEquiv.orderOf_eq KoalaBear.Fast.ringEquiv.toMulEquiv
     (KoalaBear.Fast.ofField KoalaBear.primitiveRoot)
   rw [← h]
-  simpa [KoalaBear.Fast.ringEquiv_apply, KoalaBear.Fast.toField_ofField] using
+  simpa [KoalaBear.Fast.ringEquiv, KoalaBear.Fast.ofField] using
     KoalaBear.primitiveRoot_order
 
 /-- Smooth cyclic splitter context for native-word fast KoalaBear. -/

CompPoly/Fields/BabyBear/Basic.lean

@@ -47,12 +47,8 @@ def twoAdicity : Nat := 27
 
 instance : Fact (Nat.Prime fieldSize) := ⟨is_prime⟩
 
-instance : _root_.Field Field := ZMod.instField fieldSize
-
 instance : NonBinaryField Field where
-  char_neq_2 := by
-    simpa [Field, fieldSize] using
-      (by decide : (2 : ZMod (2 ^ 31 - 2 ^ 27 + 1)) ≠ 0)
+  char_neq_2 := by decide
 
 /-- Fermat-style inversion in `ZMod fieldSize`. -/
 lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2) := by

CompPoly/Fields/BabyBear/Fast.lean

@@ -4,185 +4,52 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Valerii Huhnin, Georgios Raikos
 -/
 
-import CompPoly.Fields.BabyBear.Fast.Convert
+import CompPoly.Fields.BabyBear.Basic
+import CompPoly.Fields.Montgomery.Native32Field
 
 /-!
-# Fast BabyBear Field Operations
+# Fast BabyBear Field
 
-A native-word implementation of BabyBear arithmetic as a sidecar to the canonical
-`BabyBear.Field := ZMod BabyBear.fieldSize` model. Fast values are stored as Montgomery
-`UInt32` residues below `BabyBear.fieldSize`, representing `x * 2^32` modulo the prime.
-
-The operations, their `Field`/`CommRing`/`NonBinaryField` instances, the `toField` bridge,
-and all correctness theorems are shared across every fast 32-bit-word field; they live once
-in `CompPoly.Fields.Montgomery.Native32Field`, parameterized by the `Mont32Field` instance
-in `CompPoly.Fields.BabyBear.Fast.Prelude`. Because `Field := Native32.FastField BabyBear.Field`,
-the generic algebraic instances resolve here automatically. This module re-exports the
-named operations and `simp` lemmas at the BabyBear instance.
+A native-word Montgomery implementation of BabyBear arithmetic. The shared algorithms and
+proofs live in `CompPoly.Fields.Montgomery.Native32Field`; this module supplies the BabyBear
+constants and its concrete API.
 -/
 
-namespace BabyBear
-namespace Fast
+namespace BabyBear.Fast
 
-open Montgomery.Native32
+open Montgomery.Native32 (Mont32Field FastField)
+open Montgomery.Native32.FastField
 
-/-- Fast modular addition in Montgomery form. -/
-@[inline]
-def add (x y : Field) : Field := Montgomery.Native32.add x y
+/-! ## Parameters and carrier -/
 
-/-- Fast modular negation in Montgomery form. -/
-@[inline]
-def neg (x : Field) : Field := Montgomery.Native32.neg x
+/-- The per-field data realizing BabyBear as a fast 32-bit-word Montgomery field. -/
+instance instMont32Field : Mont32Field BabyBear.fieldSize where
+  prime := BabyBear.is_prime
+  modulus32 := 0x78000001
+  modulus64 := 0x78000001
+  rModModulus := 0x0FFFFFFE
+  r2ModModulus := 0x45DDDDE3
+  montgomeryNegInv := 0x77FFFFFF
 
-/-- Fast modular subtraction in Montgomery form. -/
-@[inline]
-def sub (x y : Field) : Field := Montgomery.Native32.sub x y
+/-- The fast native-word BabyBear field carrier, stored as a Montgomery residue. -/
+abbrev Field : Type := FastField BabyBear.fieldSize
 
-/-- Fast modular multiplication in Montgomery form. -/
-@[inline]
-def mul (x y : Field) : Field := Montgomery.Native32.mul x y
+/-! ## Conversions -/
 
-/-- Fast squaring. -/
+/-- Convert a 32-bit word into fast Montgomery representation. -/
 @[inline]
-def square (x : Field) : Field := Montgomery.Native32.square x
+def ofUInt32 (x : UInt32) : Field :=
+  Montgomery.Native32.FastField.ofUInt32 BabyBear.fieldSize x
 
-/-- Exponentiation over the fast representation using repeated squaring. -/
+/-- Convert from the canonical `ZMod` BabyBear field into fast Montgomery form. -/
 @[inline]
-def pow (x : Field) (n : Nat) : Field := Montgomery.Native32.pow x n
+def ofField (x : BabyBear.Field) : Field :=
+  Montgomery.Native32.FastField.ofField x
 
-/-- Fermat exponent used for inversion in the BabyBear prime field. -/
-def invExponent : Nat := Montgomery.Native32.invExponent (F := BabyBear.Field)
-
-/-- Inversion in Montgomery form via Fermat's little theorem (`x⁻¹ = x^(p-2)`). -/
-@[inline]
-def inv (x : Field) : Field := Montgomery.Native32.inv x
-
-/-- Division through inversion and fast multiplication. -/
-@[inline]
-def div (x y : Field) : Field := Montgomery.Native32.div x y
+/-! ## Canonical bridge -/
 
 /-- Ring equivalence between the fast Montgomery representation and canonical `BabyBear.Field`. -/
 def ringEquiv : Field ≃+* BabyBear.Field :=
-  Montgomery.Native32.ringEquiv (F := BabyBear.Field)
-
-/-- Converting from the canonical field to fast form and back is the identity. -/
-@[simp]
-theorem toField_ofField (x : BabyBear.Field) : toField (ofField x) = x :=
-  Montgomery.Native32.toField_ofField (F := BabyBear.Field) x
-
-/-- Converting from fast form to the canonical field and back is the identity. -/
-@[simp]
-theorem ofField_toField (x : Field) : ofField (toField x) = x :=
-  Montgomery.Native32.ofField_toField x
-
-/-- The canonical-field interpretation distinguishes fast BabyBear values. -/
-theorem toField_injective : Function.Injective (toField : Field → BabyBear.Field) :=
-  Montgomery.Native32.toField_injective (F := BabyBear.Field)
-
-/-- `toField` maps fast zero to canonical zero. -/
-@[simp]
-theorem toField_zero : toField (0 : Field) = 0 :=
-  Montgomery.Native32.toField_zero (F := BabyBear.Field)
-
-/-- `toField` maps fast one to canonical one. -/
-@[simp]
-theorem toField_one : toField (1 : Field) = 1 :=
-  Montgomery.Native32.toField_one (F := BabyBear.Field)
-
-/-- Fast addition agrees with addition in the canonical BabyBear field. -/
-@[simp]
-theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y :=
-  Montgomery.Native32.toField_add x y
-
-/-- Fast subtraction agrees with subtraction in the canonical BabyBear field. -/
-@[simp]
-theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y :=
-  Montgomery.Native32.toField_sub x y
-
-/-- Fast negation agrees with negation in the canonical BabyBear field. -/
-@[simp]
-theorem toField_neg (x : Field) : toField (-x) = -toField x :=
-  Montgomery.Native32.toField_neg x
-
-/-- Fast multiplication agrees with multiplication in the canonical BabyBear field. -/
-@[simp]
-theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y :=
-  Montgomery.Native32.toField_mul x y
-
-/-- Applying `ringEquiv` is the same as interpreting a fast value canonically. -/
-@[simp]
-theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x :=
-  Montgomery.Native32.ringEquiv_apply x
-
-/-- Applying the inverse `ringEquiv` is conversion into fast Montgomery form. -/
-@[simp]
-theorem ringEquiv_symm_apply (x : BabyBear.Field) : ringEquiv.symm x = ofField x :=
-  Montgomery.Native32.ringEquiv_symm_apply (F := BabyBear.Field) x
-
-/-- Fast squaring agrees with multiplication by itself in the canonical field. -/
-@[simp]
-theorem toField_square (x : Field) : toField (square x) = toField x * toField x :=
-  Montgomery.Native32.toField_square x
-
-/-- Fast inversion agrees with inversion in the canonical BabyBear field. -/
-@[simp]
-theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ :=
-  Montgomery.Native32.toField_inv x
-
-/-- Fast division agrees with division in the canonical BabyBear field. -/
-@[simp]
-theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y :=
-  Montgomery.Native32.toField_div x y
-
-/-- Natural casts into fast form agree with natural casts into the canonical field. -/
-@[simp]
-theorem toField_natCast (n : Nat) : toField (n : Field) = (n : BabyBear.Field) :=
-  Montgomery.Native32.toField_natCast n
-
-/-- Integer casts into fast form agree with integer casts into the canonical field. -/
-@[simp]
-theorem toField_intCast (n : Int) : toField (n : Field) = (n : BabyBear.Field) :=
-  Montgomery.Native32.toField_intCast n
-
-/-- Natural scalar multiplication is preserved by `toField`. -/
-@[simp]
-theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x :=
-  Montgomery.Native32.toField_nsmul n x
-
-/-- Integer scalar multiplication is preserved by `toField`. -/
-@[simp]
-theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x :=
-  Montgomery.Native32.toField_zsmul n x
-
-/-- Natural powers through the `Pow` instance are preserved by `toField`. -/
-@[simp]
-theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n :=
-  Montgomery.Native32.toField_npow x n
-
-/-- Integer powers through the `Pow` instance are preserved by `toField`. -/
-@[simp]
-theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n :=
-  Montgomery.Native32.toField_zpow x n
-
-/-- Nonnegative rational casts into fast form agree with canonical-field casts. -/
-@[simp]
-theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : BabyBear.Field) :=
-  Montgomery.Native32.toField_nnratCast q
-
-/-- Rational casts into fast form agree with canonical-field casts. -/
-@[simp]
-theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : BabyBear.Field) :=
-  Montgomery.Native32.toField_ratCast q
-
-/-- Nonnegative rational scalar multiplication is preserved by `toField`. -/
-@[simp]
-theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x :=
-  Montgomery.Native32.toField_nnqsmul q x
-
-/-- Rational scalar multiplication is preserved by `toField`. -/
-@[simp]
-theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x :=
-  Montgomery.Native32.toField_qsmul q x
+  Montgomery.Native32.ringEquiv BabyBear.fieldSize
 
-end Fast
-end BabyBear
+end BabyBear.Fast