diff --git a/CompPoly.lean b/CompPoly.lean index 61e7a4cd..7c13359f 100644 --- a/CompPoly.lean +++ b/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 diff --git a/CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean b/CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean index 867c2885..9af2e636 100644 --- a/CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean +++ b/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. -/ diff --git a/CompPoly/Fields/BabyBear/Basic.lean b/CompPoly/Fields/BabyBear/Basic.lean index 37a0729a..c0ed25de 100644 --- a/CompPoly/Fields/BabyBear/Basic.lean +++ b/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 diff --git a/CompPoly/Fields/BabyBear/Fast.lean b/CompPoly/Fields/BabyBear/Fast.lean index 2a313148..20cb5efd 100644 --- a/CompPoly/Fields/BabyBear/Fast.lean +++ b/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 diff --git a/CompPoly/Fields/BabyBear/Fast/Convert.lean b/CompPoly/Fields/BabyBear/Fast/Convert.lean deleted file mode 100644 index f02556e1..00000000 --- a/CompPoly/Fields/BabyBear/Fast/Convert.lean +++ /dev/null @@ -1,124 +0,0 @@ -/- -Copyright (c) 2026 CompPoly Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Valerii Huhnin, Georgios Raikos --/ - -import CompPoly.Fields.BabyBear.Fast.Montgomery - -/-! -# Fast BabyBear Field — Conversions - -Conversions between the fast Montgomery representation and the canonical -`BabyBear.Field` / `Nat` views, re-exported from the shared implementation in -`CompPoly.Fields.Montgomery.Native32Field` at the BabyBear instance. --/ - -namespace BabyBear -namespace Fast - -open Montgomery.Native32 - -/-- Build a fast element from a canonical natural representative. -/ -@[inline] -def ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : Field := - Montgomery.Native32.ofCanonicalNat (F := BabyBear.Field) n h - -/-- Reduce a `UInt64` modulo the BabyBear prime and return a Montgomery fast element. -/ -@[inline] -def reduceUInt64 (x : UInt64) : Field := - Montgomery.Native32.reduceUInt64 (F := BabyBear.Field) x - -/-- The zero fast BabyBear element. -/ -def zero : Field := Montgomery.Native32.zero (F := BabyBear.Field) - -/-- The one fast BabyBear element. -/ -def one : Field := Montgomery.Native32.one (F := BabyBear.Field) - -/-- Convert a natural number into fast Montgomery representation. -/ -@[inline] -def ofNat (n : Nat) : Field := - Montgomery.Native32.ofNat (F := BabyBear.Field) n - -/-- Convert a 32-bit word into fast Montgomery representation. -/ -@[inline] -def ofUInt32 (x : UInt32) : Field := - Montgomery.Native32.ofUInt32 (F := BabyBear.Field) x - -/-- Convert from the canonical `ZMod` BabyBear field into fast Montgomery form. -/ -@[inline] -def ofField (x : BabyBear.Field) : Field := - Montgomery.Native32.ofField (F := BabyBear.Field) x - -/-- Convert an integer into fast Montgomery representation. -/ -@[inline] -def ofInt (n : Int) : Field := - Montgomery.Native32.ofInt (F := BabyBear.Field) n - -/-- Convert a fast element to its canonical native-word representative. -/ -@[inline] -def toCanonicalUInt32 (x : Field) : UInt32 := - Montgomery.Native32.toCanonicalUInt32 x - -/-- Convert a fast BabyBear element to its canonical natural representative. -/ -@[inline] -def toNat (x : Field) : Nat := - Montgomery.Native32.toNat x - -/-- Convert a fast BabyBear element to the canonical `ZMod` BabyBear field. -/ -@[inline] -def toField (x : Field) : BabyBear.Field := - Montgomery.Native32.toField x - -theorem toNat_lt_fieldSize (x : Field) : toNat x < BabyBear.fieldSize := - Montgomery.Native32.toNat_lt_fieldSize x - -theorem toField_eq_raw_mul_inv (x : Field) : - toField x = (x.val.toNat : BabyBear.Field) * (UInt32.size : BabyBear.Field)⁻¹ := - Montgomery.Native32.toField_eq_raw_mul_inv x - -theorem raw_cast_eq_toField_mul (x : Field) : - (x.val.toNat : BabyBear.Field) = toField x * (UInt32.size : BabyBear.Field) := - Montgomery.Native32.raw_cast_eq_toField_mul x - -theorem nat_eq_of_field_eq {a b : Nat} (ha : a < BabyBear.fieldSize) - (hb : b < BabyBear.fieldSize) (h : (a : BabyBear.Field) = (b : BabyBear.Field)) : - a = b := - Montgomery.Native32.nat_eq_of_field_eq (F := BabyBear.Field) ha hb h - -theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < BabyBear.fieldSize) : - ((ofCanonicalNat n h).val.toNat : BabyBear.Field) = - (n : BabyBear.Field) * (UInt32.size : BabyBear.Field) := - Montgomery.Native32.ofCanonicalNat_raw_cast (F := BabyBear.Field) n h - -theorem reduceUInt64_raw_cast (x : UInt64) : - ((reduceUInt64 x).val.toNat : BabyBear.Field) = - (x.toNat : BabyBear.Field) * (UInt32.size : BabyBear.Field) := - Montgomery.Native32.reduceUInt64_raw_cast x - -/-- Converting a canonical natural representative to fast form preserves its value. -/ -@[simp] -theorem toNat_ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : - toNat (ofCanonicalNat n h) = n := - Montgomery.Native32.toNat_ofCanonicalNat n h - -/-- `ofCanonicalNat` embeds a canonical representative into the canonical field. -/ -@[simp] -theorem toField_ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : - toField (ofCanonicalNat n h) = (n : BabyBear.Field) := - Montgomery.Native32.toField_ofCanonicalNat n h - -/-- Reducing a `UInt64` gives the canonical natural residue modulo BabyBear. -/ -@[simp] -theorem toNat_reduceUInt64 (x : UInt64) : - toNat (reduceUInt64 x) = x.toNat % BabyBear.fieldSize := - Montgomery.Native32.toNat_reduceUInt64 x - -/-- Reducing a `UInt64` agrees with casting that word into the canonical field. -/ -@[simp] -theorem toField_reduceUInt64 (x : UInt64) : - toField (reduceUInt64 x) = (x.toNat : BabyBear.Field) := - Montgomery.Native32.toField_reduceUInt64 x - -end Fast -end BabyBear diff --git a/CompPoly/Fields/BabyBear/Fast/Montgomery.lean b/CompPoly/Fields/BabyBear/Fast/Montgomery.lean deleted file mode 100644 index f798d171..00000000 --- a/CompPoly/Fields/BabyBear/Fast/Montgomery.lean +++ /dev/null @@ -1,81 +0,0 @@ -/- -Copyright (c) 2026 CompPoly Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Valerii Huhnin, Georgios Raikos --/ - -import CompPoly.Fields.BabyBear.Fast.Prelude - -/-! -# Fast BabyBear Field — Montgomery Reduction - -The native-word Montgomery reducers specialized to BabyBear. The definitions and their -correctness proofs are shared across every fast 32-bit-word field; they live once in -`CompPoly.Fields.Montgomery.Native32Field`, parameterized by the `Mont32Field` instance -supplied in `CompPoly.Fields.BabyBear.Fast.Prelude`. This module just re-exports them at -the BabyBear instance. Because the shared definitions are `@[inline]`, fixing the instance -folds the constants to literals: the compiled code is identical to a hand-written -monomorphic reducer, with no `Mont32Field` dictionary at runtime. --/ - -namespace BabyBear -namespace Fast - -open Montgomery.Native32 - -/-- Reduce a native word known to be below twice the BabyBear prime. -/ -@[inline] -def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 := - Montgomery.Native32.reduceUInt32Lt2ModulusRaw (F := BabyBear.Field) x - -theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) - (h : x.toNat < 2 * BabyBear.fieldSize) : - (reduceUInt32Lt2ModulusRaw x).toNat < BabyBear.fieldSize := - Montgomery.Native32.reduceUInt32Lt2ModulusRaw_lt (F := BabyBear.Field) x h - -/-- Reduce a native word known to be below twice the BabyBear prime. -/ -@[inline] -def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * BabyBear.fieldSize) : - Field := - Montgomery.Native32.reduceUInt32Lt2Modulus (F := BabyBear.Field) x h - -theorem reduceUInt32Lt2Modulus_cast (x : UInt32) - (h : x.toNat < 2 * BabyBear.fieldSize) : - ((reduceUInt32Lt2Modulus x h).val.toNat : BabyBear.Field) = - (x.toNat : BabyBear.Field) := - Montgomery.Native32.reduceUInt32Lt2Modulus_cast (F := BabyBear.Field) x h - -/-- Reduce a native word below `2^32` modulo the BabyBear prime. -/ -@[inline] -def reduceUInt32 (x : UInt32) : Field := - Montgomery.Native32.reduceUInt32 (F := BabyBear.Field) x - -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 := - Montgomery.Native32.montgomeryReduceBoundedRaw (F := BabyBear.Field) x - -theorem montgomeryReduceBoundedRaw_lt (x : UInt64) - (h : x.toNat < BabyBear.fieldSize * UInt32.size) : - (montgomeryReduceBoundedRaw x).toNat < BabyBear.fieldSize := - Montgomery.Native32.montgomeryReduceBoundedRaw_lt (F := BabyBear.Field) x h - -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -def montgomeryReduceBounded (x : UInt64) - (h : x.toNat < BabyBear.fieldSize * UInt32.size) : Field := - Montgomery.Native32.montgomeryReduceBounded (F := BabyBear.Field) x h - -theorem montgomeryReduceBounded_cast (x : UInt64) - (h : x.toNat < BabyBear.fieldSize * UInt32.size) : - ((montgomeryReduceBounded x h).val.toNat : BabyBear.Field) = - (x.toNat : BabyBear.Field) * (UInt32.size : BabyBear.Field)⁻¹ := - Montgomery.Native32.montgomeryReduceBounded_cast (F := BabyBear.Field) x h - -/-- Montgomery reduction of a 64-bit word. Hot bounded callers use `montgomeryReduceBounded`. -/ -@[inline] -def montgomeryReduce (x : UInt64) : Field := - Montgomery.Native32.montgomeryReduce (F := BabyBear.Field) x - -end Fast -end BabyBear diff --git a/CompPoly/Fields/BabyBear/Fast/Prelude.lean b/CompPoly/Fields/BabyBear/Fast/Prelude.lean deleted file mode 100644 index 4ed200a1..00000000 --- a/CompPoly/Fields/BabyBear/Fast/Prelude.lean +++ /dev/null @@ -1,124 +0,0 @@ -/- -Copyright (c) 2026 CompPoly Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Valerii Huhnin, Georgios Raikos --/ - -import CompPoly.Fields.BabyBear.Basic -import CompPoly.Fields.Montgomery.Native32Field - -/-! -# Fast BabyBear Field — Basics - -The native-word constants and the `Field` carrier type for the fast BabyBear field. The -shared implementation lives in `CompPoly.Fields.Montgomery.Native32Field`; this module -supplies the per-field `Mont32Field` instance (the five word constants plus the -`decide`-checked numeric facts) and pins `Field := Native32.FastField BabyBear.Field`, so -the generic definitions, proofs, and algebraic instances specialize to BabyBear. - -The Montgomery reducers are re-exported in `CompPoly.Fields.BabyBear.Fast.Montgomery`; -conversions in `...Fast.Convert`; the field operations and instances in -`CompPoly.Fields.BabyBear.Fast`. --/ - -namespace BabyBear -namespace Fast - -open Montgomery.Native32 (Mont32Field FastField) - -/-- BabyBear modulus as a native word. -/ -def modulus : UInt32 := 0x78000001 - -/-- BabyBear modulus as a 64-bit word for modular reduction. -/ -def modulus64 : UInt64 := 0x78000001 - -/-- `2^32 mod BabyBear.fieldSize`. This is the Montgomery representation of one. -/ -def rModModulus : UInt32 := 0x0FFFFFFE - -/-- `(2^32)^2 mod BabyBear.fieldSize`, used to enter Montgomery representation. -/ -def r2ModModulus : UInt32 := 0x45DDDDE3 - -/-- `-BabyBear.fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ -def montgomeryNegInv : UInt32 := 0x77FFFFFF - -/-- The native `UInt32` modulus agrees with the mathematical BabyBear modulus. -/ -@[simp] theorem modulus_toNat : modulus.toNat = BabyBear.fieldSize := by decide - -/-- The native `UInt64` modulus agrees with the mathematical BabyBear modulus. -/ -@[simp] theorem modulus64_toNat : modulus64.toNat = BabyBear.fieldSize := by decide - -theorem fieldSize_pos : 0 < BabyBear.fieldSize := by decide - -theorem two_lt_fieldSize : 2 < BabyBear.fieldSize := by decide - -theorem fieldSize_lt_uint32Size : BabyBear.fieldSize < UInt32.size := by decide - -theorem fieldSize_add_fieldSize_lt_two64 : - BabyBear.fieldSize + BabyBear.fieldSize < 2 ^ 64 := by decide - -theorem fieldSize_add_fieldSize_lt_uint32Size : - BabyBear.fieldSize + BabyBear.fieldSize < UInt32.size := by decide - -theorem fieldSize_mul_fieldSize_lt_two64 : - BabyBear.fieldSize * BabyBear.fieldSize < 2 ^ 64 := by decide - -theorem uint32Size_lt_three_fieldSize : - UInt32.size < BabyBear.fieldSize + BabyBear.fieldSize + BabyBear.fieldSize := by decide - -theorem fieldSize_mul_uint32Size_lt_two64 : - BabyBear.fieldSize * UInt32.size < 2 ^ 64 := by decide - -theorem two_fieldSize_mul_uint32Size_lt_two64 : - 2 * BabyBear.fieldSize * UInt32.size < 2 ^ 64 := by decide - -theorem uint32Size_ne_zero_in_field : - (UInt32.size : BabyBear.Field) ≠ 0 := by decide - -theorem rModModulus_lt_fieldSize : rModModulus.toNat < BabyBear.fieldSize := by decide - -theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < BabyBear.fieldSize := by decide - -theorem rModModulus_cast : - (rModModulus.toNat : BabyBear.Field) = (UInt32.size : BabyBear.Field) := by decide - -theorem r2ModModulus_cast : - (r2ModModulus.toNat : BabyBear.Field) = (UInt32.size : BabyBear.Field) ^ 2 := by decide - -/-- The per-field data realizing BabyBear as a fast 32-bit-word Montgomery field. The five -word constants are the only runtime data; every other field is a `decide`-checked fact. -/ -instance instMont32Field : Mont32Field BabyBear.Field where - fieldSize := BabyBear.fieldSize - prime := inferInstance - modulus := modulus - modulus64 := modulus64 - rModModulus := rModModulus - r2ModModulus := r2ModModulus - montgomeryNegInv := montgomeryNegInv - modulus_toNat := modulus_toNat - modulus64_toNat := modulus64_toNat - fieldSize_pos := fieldSize_pos - two_lt_fieldSize := two_lt_fieldSize - fieldSize_lt_uint32Size := fieldSize_lt_uint32Size - fieldSize_add_fieldSize_lt_two64 := fieldSize_add_fieldSize_lt_two64 - fieldSize_add_fieldSize_lt_uint32Size := fieldSize_add_fieldSize_lt_uint32Size - fieldSize_mul_fieldSize_lt_two64 := fieldSize_mul_fieldSize_lt_two64 - uint32Size_lt_three_fieldSize := uint32Size_lt_three_fieldSize - fieldSize_mul_uint32Size_lt_two64 := fieldSize_mul_uint32Size_lt_two64 - two_fieldSize_mul_uint32Size_lt_two64 := two_fieldSize_mul_uint32Size_lt_two64 - uint32Size_ne_zero_in_field := uint32Size_ne_zero_in_field - rModModulus_lt_fieldSize := rModModulus_lt_fieldSize - r2ModModulus_lt_fieldSize := r2ModModulus_lt_fieldSize - rModModulus_cast := rModModulus_cast - r2ModModulus_cast := r2ModModulus_cast - negInv_congr := by decide - two_ne_zero_in_field := by decide - -/-- The fast native-word BabyBear field carrier, stored as a Montgomery residue. -/ -abbrev Field : Type := FastField BabyBear.Field - -/-- The raw Montgomery word backing a fast BabyBear element. -/ -@[inline] -def raw (x : Field) : UInt32 := x.val - -end Fast -end BabyBear diff --git a/CompPoly/Fields/KoalaBear/Basic.lean b/CompPoly/Fields/KoalaBear/Basic.lean index e32de202..45c6bf81 100644 --- a/CompPoly/Fields/KoalaBear/Basic.lean +++ b/CompPoly/Fields/KoalaBear/Basic.lean @@ -126,7 +126,6 @@ def twoAdicGenerators : List Field := /-! Statements requested by the Python spec translation. -/ -set_option maxRecDepth 4096 in /-- Fermat-style inversion in `ZMod fieldSize`. -/ lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2) := by have hcard : Fintype.card Field = fieldSize := ZMod.card fieldSize @@ -289,13 +288,11 @@ lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : /-- Primitive generator used by the smooth field-root splitter. -/ def primitiveRoot : Field := (3 : Field) -set_option maxRecDepth 100000 in /-- `primitiveRoot ^ 127` is the maximal two-adic generator. -/ private lemma primitiveRoot_pow_127_eq_twoAdicGenerator : - primitiveRoot ^ 127 = - twoAdicGenerators[(⟨twoAdicity, by omega⟩ : Fin (twoAdicity + 1))] := by - unfold primitiveRoot twoAdicity - decide + primitiveRoot ^ 127 = twoAdicGenerators[twoAdicity] := by + norm_num [primitiveRoot, twoAdicity, twoAdicGenerators] + rfl /-- `primitiveRoot ^ 2^twoAdicity` is nontrivial. -/ private lemma primitiveRoot_pow_twoAdicity_ne_one : diff --git a/CompPoly/Fields/KoalaBear/Fast.lean b/CompPoly/Fields/KoalaBear/Fast.lean index ea0f844b..8c1983c9 100644 --- a/CompPoly/Fields/KoalaBear/Fast.lean +++ b/CompPoly/Fields/KoalaBear/Fast.lean @@ -4,185 +4,89 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Valerii Huhnin -/ -import CompPoly.Fields.KoalaBear.Fast.Convert +import CompPoly.Fields.KoalaBear.Basic +import CompPoly.Fields.Montgomery.Native32Field /-! -# Fast KoalaBear Field Operations - -A native-word implementation of KoalaBear arithmetic as a sidecar to the canonical -`KoalaBear.Field := ZMod KoalaBear.fieldSize` model. Fast values are stored as Montgomery -`UInt32` residues below `KoalaBear.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.KoalaBear.Fast.Prelude`. Because `Field := Native32.FastField KoalaBear.Field`, -the generic algebraic instances resolve here automatically. This module re-exports the -named operations and `simp` lemmas at the KoalaBear instance. +# Fast KoalaBear Field + +A native-word Montgomery implementation of KoalaBear arithmetic. The shared algorithms and +proofs live in `CompPoly.Fields.Montgomery.Native32Field`; this module supplies the KoalaBear +constants and its concrete API. -/ -namespace KoalaBear -namespace Fast +namespace KoalaBear.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 KoalaBear as a fast 32-bit-word Montgomery field. -/ +instance instMont32Field : Mont32Field KoalaBear.fieldSize where + prime := KoalaBear.is_prime + modulus32 := 0x7F000001 + modulus64 := 0x7F000001 + rModModulus := 0x01FFFFFE + r2ModModulus := 0x17F7EFE4 + montgomeryNegInv := 0x7EFFFFFF -/-- Fast modular subtraction in Montgomery form. -/ -@[inline] -def sub (x y : Field) : Field := Montgomery.Native32.sub x y +/-- The fast native-word KoalaBear field carrier, stored as a Montgomery residue. -/ +abbrev Field : Type := FastField KoalaBear.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 KoalaBear.fieldSize x -/-- Exponentiation over the fast representation using repeated squaring. -/ +/-- Convert from the canonical `ZMod` KoalaBear field into fast Montgomery form. -/ @[inline] -def pow (x : Field) (n : Nat) : Field := Montgomery.Native32.pow x n +def ofField (x : KoalaBear.Field) : Field := + Montgomery.Native32.FastField.ofField x -/-- Fermat exponent used for inversion in the KoalaBear prime field. -/ -def invExponent : Nat := Montgomery.Native32.invExponent (F := KoalaBear.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 `KoalaBear.Field`. -/ def ringEquiv : Field ≃+* KoalaBear.Field := - Montgomery.Native32.ringEquiv (F := KoalaBear.Field) - -/-- Converting from the canonical field to fast form and back is the identity. -/ -@[simp] -theorem toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x := - Montgomery.Native32.toField_ofField (F := KoalaBear.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 KoalaBear values. -/ -theorem toField_injective : Function.Injective (toField : Field → KoalaBear.Field) := - Montgomery.Native32.toField_injective (F := KoalaBear.Field) - -/-- `toField` maps fast zero to canonical zero. -/ -@[simp] -theorem toField_zero : toField (0 : Field) = 0 := - Montgomery.Native32.toField_zero (F := KoalaBear.Field) - -/-- `toField` maps fast one to canonical one. -/ -@[simp] -theorem toField_one : toField (1 : Field) = 1 := - Montgomery.Native32.toField_one (F := KoalaBear.Field) - -/-- Fast addition agrees with addition in the canonical KoalaBear 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 KoalaBear 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 KoalaBear field. -/ -@[simp] -theorem toField_neg (x : Field) : toField (-x) = -toField x := - Montgomery.Native32.toField_neg x - -/-- Fast multiplication agrees with multiplication in the canonical KoalaBear 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 : KoalaBear.Field) : ringEquiv.symm x = ofField x := - Montgomery.Native32.ringEquiv_symm_apply (F := KoalaBear.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 KoalaBear field. -/ -@[simp] -theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ := - Montgomery.Native32.toField_inv x - -/-- Fast division agrees with division in the canonical KoalaBear 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 : KoalaBear.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 : KoalaBear.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 : KoalaBear.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 : KoalaBear.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 - -end Fast -end KoalaBear + Montgomery.Native32.ringEquiv KoalaBear.fieldSize + +/-! ## Two-adic roots -/ + +/-- Precomputed KoalaBear two-adic generators in Montgomery representation. -/ +def twoAdicGenerators : List Field := + [ + ⟨0x01FFFFFE, by decide⟩, + ⟨0x7D000003, by decide⟩, + ⟨0x7B020407, by decide⟩, + ⟨0x60F5EF4D, by decide⟩, + ⟨0x6D249C01, by decide⟩, + ⟨0x788529F3, by decide⟩, + ⟨0x07F7373E, by decide⟩, + ⟨0x6FE91D3C, by decide⟩, + ⟨0x3FD49211, by decide⟩, + ⟨0x1E056392, by decide⟩, + ⟨0x6D969BAB, by decide⟩, + ⟨0x439600CC, by decide⟩, + ⟨0x150276FC, by decide⟩, + ⟨0x68CACC36, by decide⟩, + ⟨0x42336C40, by decide⟩, + ⟨0x019B1972, by decide⟩, + ⟨0x34E52F6D, by decide⟩, + ⟨0x1C2EB437, by decide⟩, + ⟨0x7CB65829, by decide⟩, + ⟨0x29306FAE, by decide⟩, + ⟨0x351C7FA7, by decide⟩, + ⟨0x6E3E9A00, by decide⟩, + ⟨0x47C2BDF7, by decide⟩, + ⟨0x0C895820, by decide⟩, + ⟨0x13C85195, by decide⟩ + ] + +/-- The Montgomery root table represents the canonical KoalaBear roots. -/ +theorem twoAdicGenerators_eq_map : + twoAdicGenerators = KoalaBear.twoAdicGenerators.map ofField := by + decide + +end KoalaBear.Fast diff --git a/CompPoly/Fields/KoalaBear/Fast/Convert.lean b/CompPoly/Fields/KoalaBear/Fast/Convert.lean deleted file mode 100644 index f2409532..00000000 --- a/CompPoly/Fields/KoalaBear/Fast/Convert.lean +++ /dev/null @@ -1,124 +0,0 @@ -/- -Copyright (c) 2026 CompPoly Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Valerii Huhnin --/ - -import CompPoly.Fields.KoalaBear.Fast.Montgomery - -/-! -# Fast KoalaBear Field — Conversions - -Conversions between the fast Montgomery representation and the canonical -`KoalaBear.Field` / `Nat` views, re-exported from the shared implementation in -`CompPoly.Fields.Montgomery.Native32Field` at the KoalaBear instance. --/ - -namespace KoalaBear -namespace Fast - -open Montgomery.Native32 - -/-- Build a fast element from a canonical natural representative. -/ -@[inline] -def ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : Field := - Montgomery.Native32.ofCanonicalNat (F := KoalaBear.Field) n h - -/-- Reduce a `UInt64` modulo the KoalaBear prime and return a Montgomery fast element. -/ -@[inline] -def reduceUInt64 (x : UInt64) : Field := - Montgomery.Native32.reduceUInt64 (F := KoalaBear.Field) x - -/-- The zero fast KoalaBear element. -/ -def zero : Field := Montgomery.Native32.zero (F := KoalaBear.Field) - -/-- The one fast KoalaBear element. -/ -def one : Field := Montgomery.Native32.one (F := KoalaBear.Field) - -/-- Convert a natural number into fast Montgomery representation. -/ -@[inline] -def ofNat (n : Nat) : Field := - Montgomery.Native32.ofNat (F := KoalaBear.Field) n - -/-- Convert a 32-bit word into fast Montgomery representation. -/ -@[inline] -def ofUInt32 (x : UInt32) : Field := - Montgomery.Native32.ofUInt32 (F := KoalaBear.Field) x - -/-- Convert from the canonical `ZMod` KoalaBear field into fast Montgomery form. -/ -@[inline] -def ofField (x : KoalaBear.Field) : Field := - Montgomery.Native32.ofField (F := KoalaBear.Field) x - -/-- Convert an integer into fast Montgomery representation. -/ -@[inline] -def ofInt (n : Int) : Field := - Montgomery.Native32.ofInt (F := KoalaBear.Field) n - -/-- Convert a fast element to its canonical native-word representative. -/ -@[inline] -def toCanonicalUInt32 (x : Field) : UInt32 := - Montgomery.Native32.toCanonicalUInt32 x - -/-- Convert a fast KoalaBear element to its canonical natural representative. -/ -@[inline] -def toNat (x : Field) : Nat := - Montgomery.Native32.toNat x - -/-- Convert a fast KoalaBear element to the canonical `ZMod` KoalaBear field. -/ -@[inline] -def toField (x : Field) : KoalaBear.Field := - Montgomery.Native32.toField x - -theorem toNat_lt_fieldSize (x : Field) : toNat x < KoalaBear.fieldSize := - Montgomery.Native32.toNat_lt_fieldSize x - -theorem toField_eq_raw_mul_inv (x : Field) : - toField x = (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := - Montgomery.Native32.toField_eq_raw_mul_inv x - -theorem raw_cast_eq_toField_mul (x : Field) : - (x.val.toNat : KoalaBear.Field) = toField x * (UInt32.size : KoalaBear.Field) := - Montgomery.Native32.raw_cast_eq_toField_mul x - -theorem nat_eq_of_field_eq {a b : Nat} (ha : a < KoalaBear.fieldSize) - (hb : b < KoalaBear.fieldSize) (h : (a : KoalaBear.Field) = (b : KoalaBear.Field)) : - a = b := - Montgomery.Native32.nat_eq_of_field_eq (F := KoalaBear.Field) ha hb h - -theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < KoalaBear.fieldSize) : - ((ofCanonicalNat n h).val.toNat : KoalaBear.Field) = - (n : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) := - Montgomery.Native32.ofCanonicalNat_raw_cast (F := KoalaBear.Field) n h - -theorem reduceUInt64_raw_cast (x : UInt64) : - ((reduceUInt64 x).val.toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) := - Montgomery.Native32.reduceUInt64_raw_cast x - -/-- Converting a canonical natural representative to fast form preserves its value. -/ -@[simp] -theorem toNat_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : - toNat (ofCanonicalNat n h) = n := - Montgomery.Native32.toNat_ofCanonicalNat n h - -/-- `ofCanonicalNat` embeds a canonical representative into the canonical field. -/ -@[simp] -theorem toField_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : - toField (ofCanonicalNat n h) = (n : KoalaBear.Field) := - Montgomery.Native32.toField_ofCanonicalNat n h - -/-- Reducing a `UInt64` gives the canonical natural residue modulo KoalaBear. -/ -@[simp] -theorem toNat_reduceUInt64 (x : UInt64) : - toNat (reduceUInt64 x) = x.toNat % KoalaBear.fieldSize := - Montgomery.Native32.toNat_reduceUInt64 x - -/-- Reducing a `UInt64` agrees with casting that word into the canonical field. -/ -@[simp] -theorem toField_reduceUInt64 (x : UInt64) : - toField (reduceUInt64 x) = (x.toNat : KoalaBear.Field) := - Montgomery.Native32.toField_reduceUInt64 x - -end Fast -end KoalaBear diff --git a/CompPoly/Fields/KoalaBear/Fast/Montgomery.lean b/CompPoly/Fields/KoalaBear/Fast/Montgomery.lean deleted file mode 100644 index 4f9c94ca..00000000 --- a/CompPoly/Fields/KoalaBear/Fast/Montgomery.lean +++ /dev/null @@ -1,81 +0,0 @@ -/- -Copyright (c) 2026 CompPoly Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Valerii Huhnin --/ - -import CompPoly.Fields.KoalaBear.Fast.Prelude - -/-! -# Fast KoalaBear Field — Montgomery Reduction - -The native-word Montgomery reducers specialized to KoalaBear. The definitions and their -correctness proofs are shared across every fast 32-bit-word field; they live once in -`CompPoly.Fields.Montgomery.Native32Field`, parameterized by the `Mont32Field` instance -supplied in `CompPoly.Fields.KoalaBear.Fast.Prelude`. This module just re-exports them at -the KoalaBear instance. Because the shared definitions are `@[inline]`, fixing the instance -folds the constants to literals: the compiled code is identical to a hand-written -monomorphic reducer, with no `Mont32Field` dictionary at runtime. --/ - -namespace KoalaBear -namespace Fast - -open Montgomery.Native32 - -/-- Reduce a native word known to be below twice the KoalaBear prime. -/ -@[inline] -def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 := - Montgomery.Native32.reduceUInt32Lt2ModulusRaw (F := KoalaBear.Field) x - -theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) - (h : x.toNat < 2 * KoalaBear.fieldSize) : - (reduceUInt32Lt2ModulusRaw x).toNat < KoalaBear.fieldSize := - Montgomery.Native32.reduceUInt32Lt2ModulusRaw_lt (F := KoalaBear.Field) x h - -/-- Reduce a native word known to be below twice the KoalaBear prime. -/ -@[inline] -def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * KoalaBear.fieldSize) : - Field := - Montgomery.Native32.reduceUInt32Lt2Modulus (F := KoalaBear.Field) x h - -theorem reduceUInt32Lt2Modulus_cast (x : UInt32) - (h : x.toNat < 2 * KoalaBear.fieldSize) : - ((reduceUInt32Lt2Modulus x h).val.toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) := - Montgomery.Native32.reduceUInt32Lt2Modulus_cast (F := KoalaBear.Field) x h - -/-- Reduce a native word below `2^32` modulo the KoalaBear prime. -/ -@[inline] -def reduceUInt32 (x : UInt32) : Field := - Montgomery.Native32.reduceUInt32 (F := KoalaBear.Field) x - -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 := - Montgomery.Native32.montgomeryReduceBoundedRaw (F := KoalaBear.Field) x - -theorem montgomeryReduceBoundedRaw_lt (x : UInt64) - (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : - (montgomeryReduceBoundedRaw x).toNat < KoalaBear.fieldSize := - Montgomery.Native32.montgomeryReduceBoundedRaw_lt (F := KoalaBear.Field) x h - -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -def montgomeryReduceBounded (x : UInt64) - (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : Field := - Montgomery.Native32.montgomeryReduceBounded (F := KoalaBear.Field) x h - -theorem montgomeryReduceBounded_cast (x : UInt64) - (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : - ((montgomeryReduceBounded x h).val.toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := - Montgomery.Native32.montgomeryReduceBounded_cast (F := KoalaBear.Field) x h - -/-- Montgomery reduction of a 64-bit word. Hot bounded callers use `montgomeryReduceBounded`. -/ -@[inline] -def montgomeryReduce (x : UInt64) : Field := - Montgomery.Native32.montgomeryReduce (F := KoalaBear.Field) x - -end Fast -end KoalaBear diff --git a/CompPoly/Fields/KoalaBear/Fast/Prelude.lean b/CompPoly/Fields/KoalaBear/Fast/Prelude.lean deleted file mode 100644 index 0317685d..00000000 --- a/CompPoly/Fields/KoalaBear/Fast/Prelude.lean +++ /dev/null @@ -1,124 +0,0 @@ -/- -Copyright (c) 2026 CompPoly Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Valerii Huhnin --/ - -import CompPoly.Fields.KoalaBear.Basic -import CompPoly.Fields.Montgomery.Native32Field - -/-! -# Fast KoalaBear Field — Basics - -The native-word constants and the `Field` carrier type for the fast KoalaBear field. The -shared implementation lives in `CompPoly.Fields.Montgomery.Native32Field`; this module -supplies the per-field `Mont32Field` instance (the five word constants plus the -`decide`-checked numeric facts) and pins `Field := Native32.FastField KoalaBear.Field`, so -the generic definitions, proofs, and algebraic instances specialize to KoalaBear. - -The Montgomery reducers are re-exported in `CompPoly.Fields.KoalaBear.Fast.Montgomery`; -conversions in `...Fast.Convert`; the field operations and instances in -`CompPoly.Fields.KoalaBear.Fast`. --/ - -namespace KoalaBear -namespace Fast - -open Montgomery.Native32 (Mont32Field FastField) - -/-- KoalaBear modulus as a native word. -/ -def modulus : UInt32 := 0x7F000001 - -/-- KoalaBear modulus as a 64-bit word for modular reduction. -/ -def modulus64 : UInt64 := 0x7F000001 - -/-- `2^32 mod KoalaBear.fieldSize`. This is the Montgomery representation of one. -/ -def rModModulus : UInt32 := 0x01FFFFFE - -/-- `(2^32)^2 mod KoalaBear.fieldSize`, used to enter Montgomery representation. -/ -def r2ModModulus : UInt32 := 0x17F7EFE4 - -/-- `-KoalaBear.fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ -def montgomeryNegInv : UInt32 := 0x7EFFFFFF - -/-- The native `UInt32` modulus agrees with the mathematical KoalaBear modulus. -/ -@[simp] theorem modulus_toNat : modulus.toNat = KoalaBear.fieldSize := by decide - -/-- The native `UInt64` modulus agrees with the mathematical KoalaBear modulus. -/ -@[simp] theorem modulus64_toNat : modulus64.toNat = KoalaBear.fieldSize := by decide - -theorem fieldSize_pos : 0 < KoalaBear.fieldSize := by decide - -theorem two_lt_fieldSize : 2 < KoalaBear.fieldSize := by decide - -theorem fieldSize_lt_uint32Size : KoalaBear.fieldSize < UInt32.size := by decide - -theorem fieldSize_add_fieldSize_lt_two64 : - KoalaBear.fieldSize + KoalaBear.fieldSize < 2 ^ 64 := by decide - -theorem fieldSize_add_fieldSize_lt_uint32Size : - KoalaBear.fieldSize + KoalaBear.fieldSize < UInt32.size := by decide - -theorem fieldSize_mul_fieldSize_lt_two64 : - KoalaBear.fieldSize * KoalaBear.fieldSize < 2 ^ 64 := by decide - -theorem uint32Size_lt_three_fieldSize : - UInt32.size < KoalaBear.fieldSize + KoalaBear.fieldSize + KoalaBear.fieldSize := by decide - -theorem fieldSize_mul_uint32Size_lt_two64 : - KoalaBear.fieldSize * UInt32.size < 2 ^ 64 := by decide - -theorem two_fieldSize_mul_uint32Size_lt_two64 : - 2 * KoalaBear.fieldSize * UInt32.size < 2 ^ 64 := by decide - -theorem uint32Size_ne_zero_in_field : - (UInt32.size : KoalaBear.Field) ≠ 0 := by decide - -theorem rModModulus_lt_fieldSize : rModModulus.toNat < KoalaBear.fieldSize := by decide - -theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < KoalaBear.fieldSize := by decide - -theorem rModModulus_cast : - (rModModulus.toNat : KoalaBear.Field) = (UInt32.size : KoalaBear.Field) := by decide - -theorem r2ModModulus_cast : - (r2ModModulus.toNat : KoalaBear.Field) = (UInt32.size : KoalaBear.Field) ^ 2 := by decide - -/-- The per-field data realizing KoalaBear as a fast 32-bit-word Montgomery field. The five -word constants are the only runtime data; every other field is a `decide`-checked fact. -/ -instance instMont32Field : Mont32Field KoalaBear.Field where - fieldSize := KoalaBear.fieldSize - prime := inferInstance - modulus := modulus - modulus64 := modulus64 - rModModulus := rModModulus - r2ModModulus := r2ModModulus - montgomeryNegInv := montgomeryNegInv - modulus_toNat := modulus_toNat - modulus64_toNat := modulus64_toNat - fieldSize_pos := fieldSize_pos - two_lt_fieldSize := two_lt_fieldSize - fieldSize_lt_uint32Size := fieldSize_lt_uint32Size - fieldSize_add_fieldSize_lt_two64 := fieldSize_add_fieldSize_lt_two64 - fieldSize_add_fieldSize_lt_uint32Size := fieldSize_add_fieldSize_lt_uint32Size - fieldSize_mul_fieldSize_lt_two64 := fieldSize_mul_fieldSize_lt_two64 - uint32Size_lt_three_fieldSize := uint32Size_lt_three_fieldSize - fieldSize_mul_uint32Size_lt_two64 := fieldSize_mul_uint32Size_lt_two64 - two_fieldSize_mul_uint32Size_lt_two64 := two_fieldSize_mul_uint32Size_lt_two64 - uint32Size_ne_zero_in_field := uint32Size_ne_zero_in_field - rModModulus_lt_fieldSize := rModModulus_lt_fieldSize - r2ModModulus_lt_fieldSize := r2ModModulus_lt_fieldSize - rModModulus_cast := rModModulus_cast - r2ModModulus_cast := r2ModModulus_cast - negInv_congr := by decide - two_ne_zero_in_field := by decide - -/-- The fast native-word KoalaBear field carrier, stored as a Montgomery residue. -/ -abbrev Field : Type := FastField KoalaBear.Field - -/-- The raw Montgomery word backing a fast KoalaBear element. -/ -@[inline] -def raw (x : Field) : UInt32 := x.val - -end Fast -end KoalaBear diff --git a/CompPoly/Fields/Montgomery/Basic.lean b/CompPoly/Fields/Montgomery/Basic.lean index e6a8bce1..47336c85 100644 --- a/CompPoly/Fields/Montgomery/Basic.lean +++ b/CompPoly/Fields/Montgomery/Basic.lean @@ -10,110 +10,104 @@ import Mathlib.Algebra.Field.ZMod import Mathlib.Tactic.Ring /-! -# Montgomery Reduction — radix-generic core +# Montgomery Reduction -Field-agnostic number theory behind native-word Montgomery reduction, shared by every -fast prime field. Everything here is parameterized by an abstract radix `R : Nat` (the -Montgomery modulus, e.g. `2^32` for 32-bit-word fields) and the prime `p`; the proofs use -only that `gcd(R, p) = 1` — supplied as the congruence `negInv * p ≡ R - 1 [MOD R]` — and -that `0 < R`, so nothing here is tied to a particular word size. - -The concrete word-level bridges (e.g. the `UInt32 × UInt64`, `R = 2^32` reduction) live in -sibling modules such as `CompPoly.Fields.Montgomery.Native32`, which instantiate `R` and -call into this core. These lemmas are all `Prop`/spec level and erased at codegen, so -sharing them carries no runtime cost. +Radix-generic specification and correctness lemmas for single-word Montgomery reduction. +Word-specific implementations refine these results in sibling modules. -/ namespace Montgomery -/-- The Montgomery divisibility identity: if `negInv * p ≡ R - 1 [MOD R]` (i.e. -`negInv = -p⁻¹ mod R`), then `R ∣ x + ((x mod R)·negInv mod R)·p` for every `x`. This is -what makes Montgomery reduction integer-valued. -/ -theorem sum_dvd (R p negInv : Nat) (hR : 0 < R) - (hp : negInv * p ≡ R - 1 [MOD R]) (x : Nat) : - R ∣ x + ((x % R * negInv) % R) * p := by - rw [← Nat.modEq_zero_iff_dvd] - have hx : x ≡ x % R [MOD R] := (Nat.mod_modEq x R).symm - have hm : - ((x % R * negInv) % R) * p ≡ (x % R) * (R - 1) [MOD R] := by - have hmi : - (x % R * negInv) % R ≡ x % R * negInv [MOD R] := Nat.mod_modEq _ _ - calc - ((x % R * negInv) % R) * p - ≡ (x % R * negInv) * p [MOD R] := hmi.mul_right _ - _ = x % R * (negInv * p) := by ring - _ ≡ x % R * (R - 1) [MOD R] := hp.mul_left _ - calc - x + ((x % R * negInv) % R) * p - ≡ x % R + x % R * (R - 1) [MOD R] := hx.add hm - _ = x % R * R := by - rw [add_comm, ← Nat.mul_succ] - have hsucc : (R - 1).succ = R := by omega - rw [hsucc] - _ ≡ 0 [MOD R] := by - rw [Nat.modEq_zero_iff_dvd] - exact ⟨x % R, by rw [mul_comm]⟩ - -/-- Nat-level Montgomery reduction: specifies and is used to prove the native-word reducer. -/ -def reduceNat (R p negInv x : Nat) : Nat := +/-- Natural-number Montgomery reduction used to specify the native-word reducer. -/ +def reduceNat (R p negInv x : ℕ) : ℕ := let m := (x % R * negInv) % R let u := (x + m * p) / R if u < p then u else u - p -/-- Montgomery reduction descends to "multiply by `R⁻¹`" in `ZMod p`. -/ -theorem reduceNat_cast (R p negInv : Nat) [Fact (Nat.Prime p)] (hR : 0 < R) - (hp : negInv * p ≡ R - 1 [MOD R]) (hRne : (R : ZMod p) ≠ 0) (x : Nat) : - (reduceNat R p negInv x : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by +/-- The quotient before the final conditional subtraction in Montgomery reduction. -/ +def reduceNatQuotient (R p negInv x : ℕ) : ℕ := + let m := (x % R * negInv) % R + (x + m * p) / R + +/-- The pre-subtraction quotient is below twice the modulus. -/ +theorem reduceNatQuotient_lt_two_mul (R p negInv x : ℕ) + (hR : 0 < R) (hp : 0 < p) (hx : x < p * R) : + reduceNatQuotient R p negInv x < 2 * p := by + let m := x % R * negInv % R + have hm_lt : m < R := Nat.mod_lt _ hR + change (x + m * p) / R < 2 * p + rw [Nat.div_lt_iff_lt_mul] + · have hprod_lt : m * p < R * p := Nat.mul_lt_mul_of_pos_right hm_lt hp + have hprod_lt' : m * p < p * R := by + simpa only [Nat.mul_comm] using hprod_lt + calc + x + m * p < p * R + p * R := Nat.add_lt_add hx hprod_lt' + _ = 2 * p * R := by ring + · exact hR + +/-- Montgomery reduction returns a canonical representative. -/ +theorem reduceNat_lt (R p negInv x : ℕ) + (hR : 0 < R) (hp : 0 < p) (hx : x < p * R) : + reduceNat R p negInv x < p := by + change (if reduceNatQuotient R p negInv x < p then + reduceNatQuotient R p negInv x else reduceNatQuotient R p negInv x - p) < p + have hu := reduceNatQuotient_lt_two_mul R p negInv x hR hp hx + by_cases h : reduceNatQuotient R p negInv x < p + · rw [if_pos h] + exact h + · rw [if_neg h] + omega + +/-- The Montgomery divisibility identity: if `(negInv * p) % R = R - 1` (i.e. +`negInv = -p⁻¹ mod R`), then `R ∣ x + ((x mod R)·negInv mod R)·p` for every `x`. -/ +theorem dvd_add (R p negInv : ℕ) (hR : 0 < R) + (hnegInv : negInv * p % R = R - 1) (x : ℕ) : + R ∣ x + ((x % R * negInv) % R) * p := by + rw [Nat.dvd_iff_mod_eq_zero] + rw [Nat.add_mod, Nat.mod_mul_mod (x % R * negInv) p R, Nat.mul_assoc] + rw [← Nat.mul_mod_mod, hnegInv, Nat.add_mod_mod, add_comm, ← Nat.mul_add_one] + rw [show R - 1 + 1 = R by omega, Nat.mul_mod_left] + +/-- The pre-subtraction quotient represents multiplication by `R⁻¹` in `ZMod p`. -/ +theorem reduceNatQuotient_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R) + (hnegInv : negInv * p % R = R - 1) (hRne : (R : ZMod p) ≠ 0) (x : ℕ) : + (reduceNatQuotient R p negInv x : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by let m := x % R * negInv % R let u := (x + m * p) / R + change (u : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ have hdiv : R ∣ x + m * p := by - simpa [m] using sum_dvd R p negInv hR hp x + simpa [m] using dvd_add R p negInv hR hnegInv x have hu_mul : u * R = x + m * p := Nat.div_mul_cancel hdiv have hcast_mul : (u : ZMod p) * (R : ZMod p) = (x : ZMod p) := by rw [← Nat.cast_mul, hu_mul, Nat.cast_add, Nat.cast_mul] simp - by_cases hu : u < p - · have hmain : (u : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by - rw [← hcast_mul] - refine (mul_inv_cancel_right₀ ?_ (u : ZMod p)).symm - exact hRne - dsimp only [reduceNat] - rw [if_pos hu] - exact hmain - · have hfield : ((u - p : Nat) : ZMod p) = (u : ZMod p) := by - rw [Nat.cast_sub (Nat.le_of_not_gt hu)] - simp - have hmain : ((u - p : Nat) : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by - rw [hfield, ← hcast_mul] - refine (mul_inv_cancel_right₀ ?_ (u : ZMod p)).symm - exact hRne - dsimp only [reduceNat] - rw [if_neg hu] - exact hmain + rw [← hcast_mul] + exact (mul_inv_cancel_right₀ hRne (u : ZMod p)).symm -/-- The pre-conditional-subtract Montgomery quotient already casts to "multiply by `R⁻¹`" -in `ZMod p`. -/ -theorem quotient_cast (R p negInv : Nat) [Fact (Nat.Prime p)] (hR : 0 < R) - (hp : negInv * p ≡ R - 1 [MOD R]) (hRne : (R : ZMod p) ≠ 0) (x : Nat) : - (let m := x % R * negInv % R - let u := (x + m * p) / R - (u : ZMod p)) = (x : ZMod p) * (R : ZMod p)⁻¹ := by +/-- Montgomery reduction represents multiplication by `R⁻¹` in `ZMod p`. -/ +theorem reduceNat_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R) + (hnegInv : negInv * p % R = R - 1) (hRne : (R : ZMod p) ≠ 0) (x : ℕ) : + (reduceNat R p negInv x : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by let m := x % R * negInv % R let u := (x + m * p) / R - have hmr := reduceNat_cast R p negInv hR hp hRne x - unfold reduceNat at hmr - change (u : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ + have hu_cast : (u : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by + simpa only [reduceNatQuotient, m, u] using + reduceNatQuotient_cast R p negInv hR hnegInv hRne x + change ((if u < p then u else u - p : ℕ) : ZMod p) = + (x : ZMod p) * (R : ZMod p)⁻¹ by_cases hu : u < p - · simpa only [m, u, hu, if_true] using hmr - · have hfield : ((u - p : Nat) : ZMod p) = (u : ZMod p) := by + · rw [if_pos hu] + exact hu_cast + · have hfield : ((u - p : ℕ) : ZMod p) = (u : ZMod p) := by rw [Nat.cast_sub (Nat.le_of_not_gt hu)] simp - rw [← hfield] - simpa only [m, u, hu, if_false] using hmr + rw [if_neg hu] + rw [hfield] + exact hu_cast /-- Two naturals below `p` are equal once their `ZMod p` casts agree. -/ -theorem natCast_inj {p a b : Nat} (ha : a < p) (hb : b < p) - (h : (a : ZMod p) = (b : ZMod p)) : a = b := by +theorem natCast_inj_of_lt {p a b : ℕ} (h : (a : ZMod p) = (b : ZMod p)) + (ha : a < p) (hb : b < p) : a = b := by rw [ZMod.natCast_eq_natCast_iff] at h exact Nat.ModEq.eq_of_lt_of_lt h ha hb diff --git a/CompPoly/Fields/Montgomery/Native32.lean b/CompPoly/Fields/Montgomery/Native32.lean index 9cd9df29..bba0de97 100644 --- a/CompPoly/Fields/Montgomery/Native32.lean +++ b/CompPoly/Fields/Montgomery/Native32.lean @@ -7,68 +7,134 @@ Authors: Valerii Huhnin, Georgios Raikos import CompPoly.Fields.Montgomery.Basic /-! -# Montgomery Reduction — native `UInt32 × UInt64`, radix `R = 2^32` +# Native 32-bit Montgomery Reduction -The word-level bridge specialising `Montgomery.Basic` to 32-bit-word prime fields: the -Montgomery product fits in a `UInt64`, the radix is `R = UInt32.size = 2^32`, and the -high word is extracted with `>>> 32`. These lemmas relate the native-word computation to -the `Nat` formula proved generically in `Montgomery.Basic`, parameterized by the prime -`p`, the `UInt32` negated inverse `negInv`, and the `UInt64` modulus `modN`. - -A future 64-bit family would add a parallel `Native64` bridge (`>>> 64`, -`UInt64 × UInt128`) over the same `Montgomery.Basic` core. +Raw word operations for Montgomery reduction with radix `2 ^ 32`. -/ namespace Montgomery namespace Native32 -/-- The native high-word extraction agrees with the `Nat`-level Montgomery quotient. -/ -theorem u_eq_nat (negInv : UInt32) (modN : UInt64) (p : Nat) - (hmod : modN.toNat = p) (hp_pos : 0 < p) - (hbound : 2 * p * UInt32.size < 2 ^ 64) - (x : UInt64) (h : x.toNat < p * UInt32.size) : - ((((x + (x.toUInt32 * negInv).toUInt64 * modN) >>> 32).toUInt32).toNat) = - (x.toNat + ((x.toNat % UInt32.size * negInv.toNat) % UInt32.size) * p) / UInt32.size := by +/-- Montgomery reduction. -/ +@[inline] +def reduceRaw (p32 : UInt32) (p64 : UInt64) (negInv : UInt32) (x : UInt64) : UInt32 := + let m := (x.toUInt32 * negInv).toUInt64 + let u := ((x + m * p64) >>> 32).toUInt32 + if u < p32 then u else u - p32 + +/-- The native pre-subtraction quotient in 32-bit Montgomery reduction. -/ +def reduceQuotient (negInv : UInt32) (p x : UInt64) : UInt32 := + ((x + (x.toUInt32 * negInv).toUInt64 * p) >>> 32).toUInt32 + +/-- Conditional subtraction of the modulus in 32-bit Montgomery reduction. -/ +def conditionalSubtract (p32 : UInt32) (u : UInt32) : UInt32 := + if u < p32 then u else u - p32 + +variable {modulus : ℕ} {p32 negInv u : UInt32} {p64 x : UInt64} + +theorem reduceRaw_eq_conditionalSubtract : + reduceRaw p32 p64 negInv x = + conditionalSubtract p32 (reduceQuotient negInv p64 x) := rfl + +/-- The native quotient agrees with the `Nat`-level Montgomery quotient. -/ +theorem reduceQuotient_toNat (hp_pos : 0 < p64.toNat) (hbound : p64.toNat < 2 ^ 31) + (h : x.toNat < p64.toNat * 2 ^ 32) : + (reduceQuotient negInv p64 x).toNat = + reduceNatQuotient (2 ^ 32) p64.toNat negInv.toNat x.toNat := by simp only [UInt64.toNat_shiftRight, UInt64.toNat_toUInt32, UInt64.toNat_add, UInt64.toNat_mul, UInt32.toNat_toUInt64, UInt32.toNat_mul, UInt64.toNat_ofNat, - hmod, Nat.shiftRight_eq_div_pow] - norm_num [UInt32.size] at h hbound ⊢ - let mNat := x.toNat * negInv.toNat % 4294967296 - have hm_lt : mNat < 4294967296 := Nat.mod_lt _ (by decide) - have hsum_lt : x.toNat + mNat * p < 18446744073709551616 := by - have hprod_lt : mNat * p < p * 4294967296 := by + reduceQuotient, reduceNatQuotient, Nat.shiftRight_eq_div_pow] + let mNat := x.toNat * negInv.toNat % 2 ^ 32 + have hm_lt : mNat < 2 ^ 32 := Nat.mod_lt _ (by decide) + have hsum_lt : x.toNat + mNat * p64.toNat < 2 ^ 64 := by + have hprod_lt : mNat * p64.toNat < p64.toNat * 2 ^ 32 := by have := Nat.mul_lt_mul_of_pos_right hm_lt hp_pos simpa [Nat.mul_comm] using this - calc x.toNat + mNat * p < p * 4294967296 + p * 4294967296 := Nat.add_lt_add h hprod_lt - _ = 2 * p * 4294967296 := by ring - _ < 18446744073709551616 := hbound - change ((x.toNat + mNat * p) % 18446744073709551616 / 4294967296) % 4294967296 = - (x.toNat + mNat * p) / 4294967296 - rw [Nat.mod_eq_of_lt hsum_lt] - rw [Nat.mod_eq_of_lt] + calc + x.toNat + mNat * p64.toNat < + p64.toNat * 2 ^ 32 + p64.toNat * 2 ^ 32 := Nat.add_lt_add h hprod_lt + _ = 2 * p64.toNat * 2 ^ 32 := by ring + _ < 2 ^ 64 := by omega + norm_num [UInt32.size] + change ((x.toNat + mNat * p64.toNat) % 2 ^ 64 / 2 ^ 32) % 2 ^ 32 = + (x.toNat + mNat * p64.toNat) / 2 ^ 32 + rw [Nat.mod_eq_of_lt hsum_lt, Nat.mod_eq_of_lt] rw [Nat.div_lt_iff_lt_mul] · exact hsum_lt · decide -/-- The native Montgomery quotient stays below `2 * p`, so a single conditional subtract -canonicalises it. -/ -theorem u_lt_two_mul (negInv : UInt32) (modN : UInt64) (p : Nat) - (hmod : modN.toNat = p) (hp_pos : 0 < p) - (hbound : 2 * p * UInt32.size < 2 ^ 64) - (x : UInt64) (h : x.toNat < p * UInt32.size) : - ((((x + (x.toUInt32 * negInv).toUInt64 * modN) >>> 32).toUInt32).toNat) < 2 * p := by - rw [u_eq_nat negInv modN p hmod hp_pos hbound x h] - let mNat := x.toNat % UInt32.size * negInv.toNat % UInt32.size - have hm_lt : mNat < UInt32.size := Nat.mod_lt _ (by decide) - rw [Nat.div_lt_iff_lt_mul] - · have hprod_lt : mNat * p < UInt32.size * p := Nat.mul_lt_mul_of_pos_right hm_lt hp_pos - have hprod_lt' : mNat * p < p * UInt32.size := by - simpa [Nat.mul_comm] using hprod_lt - change x.toNat + mNat * p < 2 * p * UInt32.size - calc x.toNat + mNat * p < p * UInt32.size + p * UInt32.size := - Nat.add_lt_add h hprod_lt' - _ = 2 * p * UInt32.size := by ring - · decide +theorem conditionalSubtract_toNat : + (conditionalSubtract p32 u).toNat = + if u.toNat < p32.toNat then u.toNat else u.toNat - p32.toNat := by + simp only [conditionalSubtract, UInt32.lt_iff_toNat_lt] + by_cases hx : u.toNat < p32.toNat + · simp only [if_pos hx] + · have hp_le_x : p32 ≤ u := by + rw [UInt32.le_iff_toNat_le] + omega + simp only [if_neg hx, UInt32.toNat_sub_of_le _ _ hp_le_x] + +/-- Native Montgomery reduction agrees with the natural-number specification. -/ +theorem reduceRaw_toNat (hp32 : p32.toNat = modulus) (hp64 : p64.toNat = modulus) + (hp_pos : 0 < modulus) (hp_bound : modulus < 2 ^ 31) + (h : x.toNat < modulus * 2 ^ 32) : + (reduceRaw p32 p64 negInv x).toNat = + reduceNat (2 ^ 32) modulus negInv.toNat x.toNat := by + rw [reduceRaw_eq_conditionalSubtract, conditionalSubtract_toNat] + rw [reduceQuotient_toNat + (by simpa only [hp64] using hp_pos) + (by simpa only [hp64] using hp_bound) + (by simpa only [hp64] using h)] + rw [hp32, hp64] + rfl + +theorem conditionalSubtract_lt (h : u.toNat < 2 * p32.toNat) : + (conditionalSubtract p32 u).toNat < p32.toNat := by + simp only [conditionalSubtract, UInt32.lt_iff_toNat_lt] + by_cases hx : u.toNat < p32.toNat + · rw [if_pos hx] + exact hx + · have hp_le_x : p32 ≤ u := by + rw [UInt32.le_iff_toNat_le] + omega + rw [if_neg hx, UInt32.toNat_sub_of_le _ _ hp_le_x] + omega + +theorem conditionalSubtract_cast : + ((conditionalSubtract p32 u).toNat : ZMod p32.toNat) = + (u.toNat : ZMod p32.toNat) := by + simp only [conditionalSubtract] + by_cases hx : u < p32 + · rw [if_pos hx] + · have hp_le_x : p32 ≤ u := by + rw [UInt32.le_iff_toNat_le] + rw [UInt32.lt_iff_toNat_lt] at hx + exact Nat.le_of_not_gt hx + rw [if_neg hx, UInt32.toNat_sub_of_le _ _ hp_le_x] + rw [Nat.cast_sub (by + rw [UInt32.le_iff_toNat_le] at hp_le_x + exact hp_le_x)] + simp + +theorem reduceRaw_lt (hp : p32.toNat = p64.toNat) (hp_pos : 0 < p64.toNat) + (hp_bound : p64.toNat < 2 ^ 31) + (h : x.toNat < p64.toNat * 2 ^ 32) : + (reduceRaw p32 p64 negInv x).toNat < p32.toNat := by + rw [reduceRaw_toNat hp rfl hp_pos hp_bound h, hp] + exact reduceNat_lt (2 ^ 32) p64.toNat negInv.toNat x.toNat + (by decide) hp_pos h + +theorem reduceRaw_cast [Fact (Nat.Prime modulus)] + (hp32 : p32.toNat = modulus) (hp64 : p64.toNat = modulus) + (hp_pos : 0 < modulus) (hp_bound : modulus < 2 ^ 31) + (hnegInv : negInv.toNat * modulus % 2 ^ 32 = 2 ^ 32 - 1) + (hRne : ((2 ^ 32 : ℕ) : ZMod modulus) ≠ 0) + (h : x.toNat < modulus * 2 ^ 32) : + ((reduceRaw p32 p64 negInv x).toNat : ZMod modulus) = + (x.toNat : ZMod modulus) * ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ := by + rw [reduceRaw_toNat hp32 hp64 hp_pos hp_bound h] + exact reduceNat_cast (2 ^ 32) modulus negInv.toNat + (by decide) hnegInv hRne x.toNat end Native32 end Montgomery diff --git a/CompPoly/Fields/Montgomery/Native32Field.lean b/CompPoly/Fields/Montgomery/Native32Field.lean index 88f0e9a4..c8265181 100644 --- a/CompPoly/Fields/Montgomery/Native32Field.lean +++ b/CompPoly/Fields/Montgomery/Native32Field.lean @@ -8,718 +8,410 @@ import CompPoly.Fields.Basic import CompPoly.Fields.Montgomery.Native32 import Mathlib.Algebra.Field.TransferInstance import Mathlib.FieldTheory.Finite.Basic +import Mathlib.Tactic.Linarith /-! -# Fast 32-bit-word prime fields — shared implementation - -A `BabyBear`-style and `KoalaBear`-style fast field differ only in a handful of word -constants; their definitions, the proofs about them, and the resulting algebraic instances -are otherwise identical. This module captures that common content **once**, parameterized -by a `Mont32Field` instance that supplies the per-field data. - -* `Mont32Field F` bundles the prime (`fieldSize`), its native-word forms, the Montgomery - constants, and the small `decide`-checkable numeric/`ZMod` facts the proofs consume. - Everything except the five word constants is spec-level and erased at codegen. -* `FastField F` is the fast carrier `{ x : UInt32 // x.toNat < fieldSize }`, indexed by the - tag `F` so that the generic `Add`/`Mul`/`Field`/… instances below resolve for each - concrete field's `Field := FastField `. At runtime it erases to `UInt32`. -* The executable `def`s are `@[inline]`/`@[specialize]`, so once a concrete instance is - fixed the instance projections fold to literals and the compiled code is identical to a - hand-written monomorphic version — no `Mont32Field` dictionary survives to runtime. - -The radix-generic number theory lives in `CompPoly.Fields.Montgomery.Basic` and the -`R = 2^32` word bridge in `CompPoly.Fields.Montgomery.Native32`. A concrete fast field is -then just a `Mont32Field` instance plus thin re-export shims. +# Fast 32-bit Montgomery Fields + +The bounded carrier, conversions, arithmetic, and field instances built on `Native32` reduction. -/ namespace Montgomery namespace Native32 -/-- Per-field data for a fast 32-bit-word Montgomery prime field. - -The five word constants (`modulus`, `modulus64`, `rModModulus`, `r2ModModulus`, -`montgomeryNegInv`) are the only runtime data; the remaining fields are `Prop`s, all -dischargeable by `decide` for a concrete field, and are erased at codegen. `F` is a tag -(in practice the canonical `ZMod fieldSize` field) used for instance resolution. -/ -class Mont32Field (F : Type) where - /-- The field size / prime `p`. -/ - fieldSize : Nat - /-- `fieldSize` is prime — needed to reduce into `ZMod fieldSize` as a field. -/ - prime : Fact (Nat.Prime fieldSize) - /-- `fieldSize` as a 32-bit word. -/ - modulus : UInt32 - /-- `fieldSize` as a 64-bit word. -/ +/-- Per-field data for a fast 32-bit Montgomery field. -/ +class Mont32Field (modulus : ℕ) where + /-- `modulus` is prime. -/ + prime : modulus.Prime + /-- `modulus` as a 32-bit word. -/ + modulus32 : UInt32 + /-- `modulus` as a 64-bit word. -/ modulus64 : UInt64 - /-- `2^32 mod fieldSize`, the Montgomery representation of one. -/ + /-- `2^32 mod modulus`, the Montgomery representation of one. -/ rModModulus : UInt32 - /-- `(2^32)^2 mod fieldSize`, used to enter Montgomery form. -/ - r2ModModulus : UInt32 - /-- `-fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ + /-- `(2^32)^2 mod modulus`, used to enter Montgomery form. -/ + r2ModModulus : UInt64 + /-- `-modulus⁻¹ mod 2^32`, used by Montgomery reduction. -/ montgomeryNegInv : UInt32 - modulus_toNat : modulus.toNat = fieldSize - modulus64_toNat : modulus64.toNat = fieldSize - fieldSize_pos : 0 < fieldSize - two_lt_fieldSize : 2 < fieldSize - fieldSize_lt_uint32Size : fieldSize < UInt32.size - fieldSize_add_fieldSize_lt_two64 : fieldSize + fieldSize < 2 ^ 64 - fieldSize_add_fieldSize_lt_uint32Size : fieldSize + fieldSize < UInt32.size - fieldSize_mul_fieldSize_lt_two64 : fieldSize * fieldSize < 2 ^ 64 - uint32Size_lt_three_fieldSize : UInt32.size < fieldSize + fieldSize + fieldSize - fieldSize_mul_uint32Size_lt_two64 : fieldSize * UInt32.size < 2 ^ 64 - two_fieldSize_mul_uint32Size_lt_two64 : 2 * fieldSize * UInt32.size < 2 ^ 64 - uint32Size_ne_zero_in_field : (UInt32.size : ZMod fieldSize) ≠ 0 - rModModulus_lt_fieldSize : rModModulus.toNat < fieldSize - r2ModModulus_lt_fieldSize : r2ModModulus.toNat < fieldSize - rModModulus_cast : (rModModulus.toNat : ZMod fieldSize) = (UInt32.size : ZMod fieldSize) - r2ModModulus_cast : - (r2ModModulus.toNat : ZMod fieldSize) = (UInt32.size : ZMod fieldSize) ^ 2 - /-- The Montgomery inverse congruence `negInv * p ≡ 2^32 - 1 [MOD 2^32]`. -/ - negInv_congr : - montgomeryNegInv.toNat * fieldSize ≡ UInt32.size - 1 [MOD UInt32.size] - /-- Characteristic `≠ 2`, used to build the `NonBinaryField` instance. -/ - two_ne_zero_in_field : (2 : ZMod fieldSize) ≠ 0 - -attribute [instance] Mont32Field.prime - -/-- The fast carrier for the field tagged by `F`: a native word below `fieldSize`, + modulus32_toNat : modulus32.toNat = modulus := by decide + modulus64_toNat : modulus64.toNat = modulus := by decide + two_lt_modulus : 2 < modulus := by decide + modulus_lt_two_pow_31 : modulus < 2 ^ 31 := by decide + rModModulus_toNat : rModModulus.toNat = 2 ^ 32 % modulus := by decide + r2ModModulus_toNat : r2ModModulus.toNat = (2 ^ 32) ^ 2 % modulus := by decide + montgomeryNegInv_mul_modulus_mod_two_pow_32 : + (montgomeryNegInv.toNat * modulus) % 2 ^ 32 = 2 ^ 32 - 1 := by decide + +attribute [simp] Mont32Field.modulus32_toNat Mont32Field.modulus64_toNat + Mont32Field.rModModulus_toNat Mont32Field.r2ModModulus_toNat + Mont32Field.modulus_lt_two_pow_31 + +attribute [-simp] Nat.reducePow + +/-- The fast carrier for a prime modulus: a native word below `modulus`, interpreted as a Montgomery residue. At runtime this erases to `UInt32`. -/ -def FastField (F : Type) [Mont32Field F] : Type := - { x : UInt32 // x.toNat < Mont32Field.fieldSize F } - -instance (F : Type) [Mont32Field F] : DecidableEq (FastField F) := - inferInstanceAs (DecidableEq { x : UInt32 // x.toNat < Mont32Field.fieldSize F }) +def FastField (modulus : ℕ) [Mont32Field modulus] : Type := + { x : UInt32 // x.toNat < modulus } section -variable {F : Type} [P : Mont32Field F] +variable {modulus : ℕ} [P : Mont32Field modulus] -instance : NeZero P.fieldSize := ⟨P.fieldSize_pos.ne'⟩ +instance : DecidableEq (FastField modulus) := + inferInstanceAs (DecidableEq { x : UInt32 // x.toNat < modulus }) -/-- The raw Montgomery word backing a fast element. -/ -@[inline] -def raw (x : FastField F) : UInt32 := x.val +namespace Mont32Field -/-! ## Montgomery reduction -/ +instance : Fact (Nat.Prime modulus) := ⟨P.prime⟩ -/-- Reduce a native word known to be below twice the prime. -/ -@[inline] -def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 := - if x < P.modulus then x else x - P.modulus - -theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) - (h : x.toNat < 2 * P.fieldSize) : - (reduceUInt32Lt2ModulusRaw (F := F) x).toNat < P.fieldSize := by - unfold reduceUInt32Lt2ModulusRaw - by_cases hx : x < P.modulus - · rw [if_pos hx] - rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx - exact hx - · rw [if_neg hx] - have hmod_le_x : P.modulus ≤ x := by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx - exact Nat.le_of_not_gt hx - rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, P.modulus_toNat] - omega +@[simp] +theorem modulus_pos : 0 < modulus := Nat.zero_lt_of_lt P.two_lt_modulus -/-- Reduce a native word known to be below twice the prime. -/ -@[inline] -def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * P.fieldSize) : - FastField F := - ⟨reduceUInt32Lt2ModulusRaw (F := F) x, reduceUInt32Lt2ModulusRaw_lt x h⟩ - -theorem reduceUInt32Lt2Modulus_cast (x : UInt32) - (h : x.toNat < 2 * P.fieldSize) : - ((reduceUInt32Lt2Modulus (F := F) x h).val.toNat : ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) := by - change ((reduceUInt32Lt2ModulusRaw (F := F) x).toNat : ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) - unfold reduceUInt32Lt2ModulusRaw - by_cases hx : x < P.modulus - · rw [if_pos hx] - · have hmod_le_x : P.modulus ≤ x := by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx - exact Nat.le_of_not_gt hx - rw [if_neg hx] - rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, P.modulus_toNat] - rw [Nat.cast_sub (by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] at hmod_le_x - exact hmod_le_x)] - simp +@[simp] theorem modulus32_pos : 0 < P.modulus32.toNat := by simp +@[simp] theorem modulus64_pos : 0 < P.modulus64.toNat := by simp +@[simp] theorem modulus32_lt_two_pow_31 : P.modulus32.toNat < 2 ^ 31 := by simp +@[simp] theorem modulus64_lt_two_pow_31 : P.modulus64.toNat < 2 ^ 31 := by simp -/-- Reduce a native word below `2^32` modulo the prime. -/ -@[inline] -def reduceUInt32 (x : UInt32) : FastField F := - if hx : x < P.modulus then - ⟨x, by - rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx - exact hx⟩ - else - let y := x - P.modulus - if hy : y < P.modulus then - ⟨y, by - rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hy - exact hy⟩ - else - ⟨y - P.modulus, by - have hmod_le_x : P.modulus ≤ x := by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx - exact Nat.le_of_not_gt hx - have hy_eq : y.toNat = x.toNat - P.fieldSize := by - change (x - P.modulus).toNat = x.toNat - P.fieldSize - rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, P.modulus_toNat] - have hmod_le_y : P.modulus ≤ y := by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hy - exact Nat.le_of_not_gt hy - rw [UInt32.toNat_sub_of_le _ _ hmod_le_y, P.modulus_toNat, hy_eq] - have hx_lt := UInt32.toNat_lt_size x - have hthree := P.uint32Size_lt_three_fieldSize - omega⟩ +@[simp] theorem modulus_lt_two_pow_32 : modulus < 2 ^ 32 := by + linarith [P.modulus_lt_two_pow_31] -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 := - let m : UInt32 := x.toUInt32 * P.montgomeryNegInv - let u : UInt32 := ((x + m.toUInt64 * P.modulus64) >>> 32).toUInt32 - reduceUInt32Lt2ModulusRaw (F := F) u - -theorem montgomeryReduceBoundedRaw_lt (x : UInt64) - (h : x.toNat < P.fieldSize * UInt32.size) : - (montgomeryReduceBoundedRaw (F := F) x).toNat < P.fieldSize := by - unfold montgomeryReduceBoundedRaw - exact reduceUInt32Lt2ModulusRaw_lt _ - (Montgomery.Native32.u_lt_two_mul P.montgomeryNegInv P.modulus64 P.fieldSize - P.modulus64_toNat P.fieldSize_pos P.two_fieldSize_mul_uint32Size_lt_two64 x h) +theorem modulus_sq_lt_two_pow_64 : modulus ^ 2 < 2 ^ 64 := by + nlinarith [P.modulus_lt_two_pow_32] -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -def montgomeryReduceBounded (x : UInt64) - (h : x.toNat < P.fieldSize * UInt32.size) : FastField F := - ⟨montgomeryReduceBoundedRaw (F := F) x, montgomeryReduceBoundedRaw_lt x h⟩ - -theorem montgomeryReduceBounded_cast (x : UInt64) - (h : x.toNat < P.fieldSize * UInt32.size) : - ((montgomeryReduceBounded (F := F) x h).val.toNat : ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ := by - change ((montgomeryReduceBoundedRaw (F := F) x).toNat : ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - unfold montgomeryReduceBoundedRaw - let m : UInt32 := x.toUInt32 * P.montgomeryNegInv - let u : UInt32 := ((x + m.toUInt64 * P.modulus64) >>> 32).toUInt32 - change ((reduceUInt32Lt2ModulusRaw (F := F) u).toNat : ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - have hred := reduceUInt32Lt2Modulus_cast (F := F) u - (Montgomery.Native32.u_lt_two_mul P.montgomeryNegInv P.modulus64 P.fieldSize - P.modulus64_toNat P.fieldSize_pos P.two_fieldSize_mul_uint32Size_lt_two64 x h) - change ((reduceUInt32Lt2ModulusRaw (F := F) u).toNat : ZMod P.fieldSize) = - (u.toNat : ZMod P.fieldSize) at hred - rw [hred] - change (u.toNat : ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - rw [show u.toNat = - (x.toNat + ((x.toNat % UInt32.size * P.montgomeryNegInv.toNat) % UInt32.size) * - P.fieldSize) / UInt32.size by - exact Montgomery.Native32.u_eq_nat P.montgomeryNegInv P.modulus64 P.fieldSize - P.modulus64_toNat P.fieldSize_pos P.two_fieldSize_mul_uint32Size_lt_two64 x h] - exact Montgomery.quotient_cast UInt32.size P.fieldSize P.montgomeryNegInv.toNat - (by decide) P.negInv_congr P.uint32Size_ne_zero_in_field x.toNat - -/-- Montgomery reduction of a 64-bit word. Hot bounded callers use `montgomeryReduceBounded`. -/ -@[inline] -def montgomeryReduce (x : UInt64) : FastField F := - let m : UInt32 := x.toUInt32 * P.montgomeryNegInv - let u : UInt32 := ((x + m.toUInt64 * P.modulus64) >>> 32).toUInt32 - reduceUInt32 (F := F) u +theorem two_ne_zero : (2 : ZMod modulus) ≠ 0 := by + intro h + have hdvd : modulus ∣ 2 := (ZMod.natCast_eq_zero_iff 2 modulus).mp h + exact (Nat.not_le_of_gt P.two_lt_modulus) (Nat.le_of_dvd (by decide) hdvd) -/-! ## Conversions -/ +theorem two_pow_32_ne_zero : ((2 ^ 32 : ℕ) : ZMod modulus) ≠ 0 := by + simp [two_ne_zero] -/-- Build a fast element from a canonical natural representative. -/ -@[inline] -def ofCanonicalNat (n : Nat) (_h : n < P.fieldSize) : FastField F := - montgomeryReduceBounded (UInt64.ofNat n * P.r2ModModulus.toUInt64) (by - rw [UInt64.toNat_mul, UInt64.toNat_ofNat', UInt32.toNat_toUInt64] - have hnmod : n % 2 ^ 64 = n := by - apply Nat.mod_eq_of_lt - exact Nat.lt_trans _h (Nat.lt_trans P.fieldSize_lt_uint32Size (by decide)) - rw [hnmod] - have hprod : n * P.r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [P.r2ModModulus_lt_fieldSize]) +theorem r2ModModulus_lt_modulus : (2 ^ 32) ^ 2 % modulus < modulus := by + exact Nat.mod_lt _ P.modulus_pos + +end Mont32Field -/-- Reduce a `UInt64` modulo the prime and return a Montgomery fast element. -/ +instance : NeZero modulus := ⟨P.modulus_pos.ne'⟩ + +/-! ## Implementation -/ + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ @[inline] -def reduceUInt64 (x : UInt64) : FastField F := - let y := x % P.modulus64 - montgomeryReduceBounded (y * P.r2ModModulus.toUInt64) (by - rw [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hy_lt : (x % P.modulus64).toNat < P.fieldSize := by - rw [UInt64.toNat_mod, P.modulus64_toNat] - exact Nat.mod_lt _ P.fieldSize_pos - have hprod : (x % P.modulus64).toNat * P.r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [hy_lt, P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [P.r2ModModulus_lt_fieldSize]) +def reduce (x : UInt64) (h : x.toNat < modulus * 2 ^ 32) : FastField modulus := + .mk (reduceRaw P.modulus32 P.modulus64 P.montgomeryNegInv x) <| by + nth_rw 4 [← P.modulus32_toNat] + apply reduceRaw_lt <;> simp_all -/-- The zero fast element. -/ -def zero : FastField F := ⟨0, by - have h0 : (0 : UInt32).toNat = 0 := by decide - have hp := P.fieldSize_pos - omega⟩ +namespace FastField -/-- The one fast element. -/ -def one : FastField F := ⟨P.rModModulus, P.rModModulus_lt_fieldSize⟩ +/-! ### Conversions -/ + +/-- Build a fast element from a canonical natural representative. -/ +@[inline] +def ofCanonicalNat (n : ℕ) (h : n < modulus) : FastField modulus := + reduce (UInt64.ofNat n * P.r2ModModulus) <| by + simp only [UInt64.toNat_mul, UInt64.toNat_ofNat', P.r2ModModulus_toNat, + Nat.mod_mul_mod] + apply Nat.mod_lt_of_lt + grw [Nat.mod_lt _ P.modulus_pos] + apply mul_lt_mul <;> simp [h, le_of_lt] /-- Convert a natural number into fast Montgomery representation. -/ @[inline] -def ofNat (n : Nat) : FastField F := - ofCanonicalNat (n % P.fieldSize) (Nat.mod_lt _ P.fieldSize_pos) +def ofNat (modulus : ℕ) [P : Mont32Field modulus] (n : ℕ) : FastField modulus := + ofCanonicalNat (n % modulus) (Nat.mod_lt _ P.modulus_pos) /-- Convert a 32-bit word into fast Montgomery representation. -/ @[inline] -def ofUInt32 (x : UInt32) : FastField F := - reduceUInt64 x.toUInt64 +def ofUInt32 (modulus : ℕ) [P : Mont32Field modulus] (x : UInt32) : FastField modulus := + reduce (x.toUInt64 * P.r2ModModulus) <| by + simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64, P.r2ModModulus_toNat] + apply Nat.mod_lt_of_lt + grw [Nat.mod_lt _ P.modulus_pos, mul_comm modulus] + apply Nat.mul_lt_mul_of_pos_right <;> simp /-- Convert from the canonical `ZMod` field into fast Montgomery form. -/ @[inline] -def ofField (x : ZMod P.fieldSize) : FastField F := +def ofField (x : ZMod modulus) : FastField modulus := ofCanonicalNat x.val (ZMod.val_lt x) /-- Convert an integer into fast Montgomery representation. -/ @[inline] -def ofInt (n : Int) : FastField F := - ofField (n : ZMod P.fieldSize) +private def ofInt (modulus : ℕ) [P : Mont32Field modulus] (n : Int) : FastField modulus := + ofField (n : ZMod modulus) /-- Convert a fast element to its canonical native-word representative. -/ @[inline] -def toCanonicalUInt32 (x : FastField F) : UInt32 := - raw (montgomeryReduceBounded x.val.toUInt64 (by +def toUInt32 (x : FastField modulus) : UInt32 := Subtype.val <| + reduce (modulus := modulus) x.val.toUInt64 <| by rw [UInt32.toNat_toUInt64] - nlinarith [x.property, P.fieldSize_pos])) + nlinarith [x.property, P.modulus_pos] /-- Convert a fast element to its canonical natural representative. -/ @[inline] -def toNat (x : FastField F) : Nat := - (toCanonicalUInt32 x).toNat +def toNat (x : FastField modulus) : ℕ := x.toUInt32.toNat /-- Convert a fast element to the canonical `ZMod` field. -/ @[inline] -def toField (x : FastField F) : ZMod P.fieldSize := - (toNat x : ZMod P.fieldSize) +def toField (x : FastField modulus) : ZMod modulus := (x.toNat : ZMod modulus) +end FastField -theorem toNat_lt_fieldSize (x : FastField F) : toNat x < P.fieldSize := by - unfold toNat toCanonicalUInt32 raw - change (montgomeryReduceBoundedRaw (F := F) x.val.toUInt64).toNat < P.fieldSize - exact montgomeryReduceBoundedRaw_lt x.val.toUInt64 (by - rw [UInt32.toNat_toUInt64] - nlinarith [x.property, P.fieldSize_pos]) +open FastField -theorem toField_eq_raw_mul_inv (x : FastField F) : - toField x = - (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ := by - unfold toField toNat toCanonicalUInt32 raw - have hred := montgomeryReduceBounded_cast x.val.toUInt64 (by - rw [UInt32.toNat_toUInt64] - nlinarith [x.property, P.fieldSize_pos]) - change ((montgomeryReduceBoundedRaw (F := F) x.val.toUInt64).toNat : ZMod P.fieldSize) = - (x.val.toUInt64.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ at hred - change ((montgomeryReduceBoundedRaw (F := F) x.val.toUInt64).toNat : ZMod P.fieldSize) = - (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - rw [hred] - rw [UInt32.toNat_toUInt64] - -theorem raw_cast_eq_toField_mul (x : FastField F) : - (x.val.toNat : ZMod P.fieldSize) = - toField x * (UInt32.size : ZMod P.fieldSize) := by - rw [toField_eq_raw_mul_inv] - rw [mul_assoc] - rw [inv_mul_cancel₀ P.uint32Size_ne_zero_in_field] - rw [mul_one] - -theorem nat_eq_of_field_eq {a b : Nat} (ha : a < P.fieldSize) - (hb : b < P.fieldSize) (h : (a : ZMod P.fieldSize) = (b : ZMod P.fieldSize)) : - a = b := - Montgomery.natCast_inj ha hb h - -theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < P.fieldSize) : - ((ofCanonicalNat (F := F) n h).val.toNat : ZMod P.fieldSize) = - (n : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) := by - unfold ofCanonicalNat - have hred := montgomeryReduceBounded_cast - (UInt64.ofNat n * P.r2ModModulus.toUInt64) (by - rw [UInt64.toNat_mul, UInt64.toNat_ofNat', UInt32.toNat_toUInt64] - have hnmod : n % 2 ^ 64 = n := by - apply Nat.mod_eq_of_lt - exact Nat.lt_trans h (Nat.lt_trans P.fieldSize_lt_uint32Size (by decide)) - rw [hnmod] - have hprod : n * P.r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [P.r2ModModulus_lt_fieldSize]) - change ((montgomeryReduceBoundedRaw (F := F) - (UInt64.ofNat n * P.r2ModModulus.toUInt64)).toNat : ZMod P.fieldSize) = - ((UInt64.ofNat n * P.r2ModModulus.toUInt64).toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹ at hred - change ((montgomeryReduceBoundedRaw (F := F) - (UInt64.ofNat n * P.r2ModModulus.toUInt64)).toNat : ZMod P.fieldSize) = - (n : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) - rw [hred] - simp only [UInt64.toNat_mul, UInt64.toNat_ofNat', UInt32.toNat_toUInt64] - have hnmod : n % 2 ^ 64 = n := by - apply Nat.mod_eq_of_lt - exact Nat.lt_trans h (Nat.lt_trans P.fieldSize_lt_uint32Size (by decide)) - rw [hnmod] - have hprod : n * P.r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - rw [Nat.cast_mul, P.r2ModModulus_cast] - rw [pow_two] - rw [mul_assoc (n : ZMod P.fieldSize) ((UInt32.size : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)) ((UInt32.size : ZMod P.fieldSize)⁻¹)] - rw [mul_assoc (UInt32.size : ZMod P.fieldSize) (UInt32.size : ZMod P.fieldSize) - ((UInt32.size : ZMod P.fieldSize)⁻¹)] - rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] - rw [mul_one] - -theorem toField_ofCanonicalNat_aux (n : Nat) (h : n < P.fieldSize) : - toField (ofCanonicalNat (F := F) n h) = (n : ZMod P.fieldSize) := by - rw [toField_eq_raw_mul_inv, ofCanonicalNat_raw_cast] - rw [mul_assoc] - rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] - rw [mul_one] - -theorem reduceUInt64_raw_cast (x : UInt64) : - ((reduceUInt64 (F := F) x).val.toNat : ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) := by - unfold reduceUInt64 - let y := x % P.modulus64 - have hred := montgomeryReduceBounded_cast (y * P.r2ModModulus.toUInt64) (by - rw [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hy_lt : y.toNat < P.fieldSize := by - rw [show y = x % P.modulus64 by rfl, UInt64.toNat_mod, P.modulus64_toNat] - exact Nat.mod_lt _ P.fieldSize_pos - have hprod : y.toNat * P.r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [hy_lt, P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [P.r2ModModulus_lt_fieldSize]) - change ((montgomeryReduceBoundedRaw (F := F) (y * P.r2ModModulus.toUInt64)).toNat : - ZMod P.fieldSize) = - ((y * P.r2ModModulus.toUInt64).toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹ at hred - change ((montgomeryReduceBoundedRaw (F := F) (y * P.r2ModModulus.toUInt64)).toNat : - ZMod P.fieldSize) = - (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) - rw [hred] - simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hy_lt : y.toNat < P.fieldSize := by - rw [show y = x % P.modulus64 by rfl, UInt64.toNat_mod, P.modulus64_toNat] - exact Nat.mod_lt _ P.fieldSize_pos - have hprod : y.toNat * P.r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [hy_lt, P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - have hy_cast : (y.toNat : ZMod P.fieldSize) = (x.toNat : ZMod P.fieldSize) := by - rw [show y = x % P.modulus64 by rfl, UInt64.toNat_mod, P.modulus64_toNat] - rw [ZMod.natCast_eq_natCast_iff] - exact Nat.mod_modEq _ _ - rw [Nat.cast_mul, P.r2ModModulus_cast, hy_cast] - rw [pow_two] - rw [mul_assoc (x.toNat : ZMod P.fieldSize) ((UInt32.size : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)) ((UInt32.size : ZMod P.fieldSize)⁻¹)] - rw [mul_assoc (UInt32.size : ZMod P.fieldSize) (UInt32.size : ZMod P.fieldSize) - ((UInt32.size : ZMod P.fieldSize)⁻¹)] - rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] - rw [mul_one] - -@[simp] -theorem toNat_ofCanonicalNat (n : Nat) (h : n < P.fieldSize) : - toNat (ofCanonicalNat (F := F) n h) = n := - nat_eq_of_field_eq (toNat_lt_fieldSize _) h (toField_ofCanonicalNat_aux n h) - -@[simp] -theorem toField_ofCanonicalNat (n : Nat) (h : n < P.fieldSize) : - toField (ofCanonicalNat (F := F) n h) = (n : ZMod P.fieldSize) := - toField_ofCanonicalNat_aux n h +/-! ### Field operations -/ -@[simp] -theorem toNat_reduceUInt64 (x : UInt64) : - toNat (reduceUInt64 (F := F) x) = x.toNat % P.fieldSize := by - apply nat_eq_of_field_eq (toNat_lt_fieldSize _) (Nat.mod_lt _ P.fieldSize_pos) - change toField (reduceUInt64 (F := F) x) = ((x.toNat % P.fieldSize : Nat) : ZMod P.fieldSize) - rw [toField_eq_raw_mul_inv, reduceUInt64_raw_cast] - rw [mul_assoc] - rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] - rw [mul_one] - rw [ZMod.natCast_eq_natCast_iff] - exact (Nat.mod_modEq _ _).symm - -@[simp] -theorem toField_reduceUInt64 (x : UInt64) : - toField (reduceUInt64 (F := F) x) = (x.toNat : ZMod P.fieldSize) := by - rw [toField_eq_raw_mul_inv, reduceUInt64_raw_cast] - rw [mul_assoc] - rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] - rw [mul_one] +/-- The zero fast element. -/ +def zero (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus := .mk 0 <| by simp -/-! ## Field operations -/ +/-- The one fast element. -/ +def one (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus := .mk P.rModModulus <| by + simp [Nat.mod_lt _ P.modulus_pos] /-- Fast modular addition in Montgomery form. -/ @[inline] -def add (x y : FastField F) : FastField F := - reduceUInt32Lt2Modulus (x.val + y.val) (by - rw [UInt32.toNat_add] - exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) (by - have := x.property; have := y.property; omega)) +def add (x y : FastField modulus) : FastField modulus := + .mk (conditionalSubtract P.modulus32 (x.val + y.val)) <| by + simp_rw [← P.modulus32_toNat] + apply conditionalSubtract_lt + simp only [UInt32.toNat_add, P.modulus32_toNat] + apply Nat.lt_of_le_of_lt (Nat.mod_le _ _) + linarith [x.property, y.property] /-- Fast modular negation in Montgomery form. -/ @[inline] -def neg (x : FastField F) : FastField F := +def neg (x : FastField modulus) : FastField modulus := if hx : x.val = 0 then - zero + zero modulus else - ⟨P.modulus - x.val, by - have hle : x.val ≤ P.modulus := by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] - exact Nat.le_of_lt x.property - rw [UInt32.toNat_sub_of_le _ _ hle, P.modulus_toNat] - have hxpos : 0 < x.val.toNat := by - apply Nat.pos_of_ne_zero - intro hzero - apply hx - apply UInt32.toNat_inj.mp - simpa using hzero - have hp := P.fieldSize_pos - omega⟩ + .mk (P.modulus32 - x.val) <| by + have hle : x.val ≤ P.modulus32 := by + simp [Nat.le_of_lt, UInt32.le_iff_toNat_le, x.property] + simp [UInt32.toNat_sub_of_le _ _ hle] + rw [← UInt32.toNat_inj] at hx + change x.val.toNat ≠ 0 at hx + omega /-- Fast modular subtraction in Montgomery form. -/ @[inline] -def sub (x y : FastField F) : FastField F := +def sub (x y : FastField modulus) : FastField modulus := if hyx : y.val ≤ x.val then - ⟨x.val - y.val, by + .mk (x.val - y.val) <| by rw [UInt32.toNat_sub_of_le _ _ hyx] - have := x.property; omega⟩ + have := x.property + omega else - ⟨x.val + P.modulus - y.val, by - have hsum_lt : x.val.toNat + P.fieldSize < UInt32.size := by - have htwo := P.fieldSize_add_fieldSize_lt_uint32Size - have := x.property; omega - have hsum_eq : (x.val + P.modulus).toNat = x.val.toNat + P.fieldSize := by - rw [UInt32.toNat_add, P.modulus_toNat, Nat.mod_eq_of_lt hsum_lt] - have hyle : y.val ≤ x.val + P.modulus := by - rw [UInt32.le_iff_toNat_le, hsum_eq] - have := y.property; omega - rw [UInt32.toNat_sub_of_le _ _ hyle, hsum_eq] - have hyxNat : ¬y.val.toNat ≤ x.val.toNat := by - intro hle - apply hyx - rw [UInt32.le_iff_toNat_le] - exact hle - have := y.property; omega⟩ + .mk (x.val + P.modulus32 - y.val) <| by + simp only [UInt32.le_iff_toNat_le] at hyx + have hsum_lt : x.val.toNat + modulus < 2 ^ 32 := by + have := x.property + have := P.modulus_lt_two_pow_31 + omega + have hyle : y.val ≤ x.val + P.modulus32 := by + simp only [UInt32.le_iff_toNat_le, UInt32.toNat_add, P.modulus32_toNat, + Nat.mod_eq_of_lt hsum_lt] + have := y.property + omega + rw [UInt32.toNat_sub_of_le _ _ hyle, UInt32.toNat_add, P.modulus32_toNat, + Nat.mod_eq_of_lt hsum_lt] + have := y.property + omega /-- Fast modular multiplication in Montgomery form. -/ @[inline] -def mul (x y : FastField F) : FastField F := - montgomeryReduceBounded (x.val.toUInt64 * y.val.toUInt64) (by +def mul (x y : FastField modulus) : FastField modulus := + reduce (x.val.toUInt64 * y.val.toUInt64) (by simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] have hprod : x.val.toNat * y.val.toNat < 2 ^ 64 := by - nlinarith [x.property, y.property, P.fieldSize_mul_fieldSize_lt_two64] + nlinarith [x.property, y.property, P.modulus_sq_lt_two_pow_64] rw [Nat.mod_eq_of_lt hprod] - nlinarith [x.property, y.property, P.fieldSize_lt_uint32Size, P.fieldSize_pos]) + nlinarith [x.property, y.property, P.modulus_lt_two_pow_32, P.modulus_pos]) /-- Fast squaring. -/ @[inline] -def square (x : FastField F) : FastField F := - mul x x +def square (x : FastField modulus) : FastField modulus := mul x x /-- Exponentiation over the fast representation using repeated squaring. -/ @[specialize] -def pow (x : FastField F) (n : Nat) : FastField F := - @npowBinRec (FastField F) ⟨one⟩ ⟨mul⟩ n x - -/-- Fermat exponent used for inversion in the prime field. -/ -def invExponent : Nat := P.fieldSize - 2 +def pow (x : FastField modulus) (n : ℕ) : FastField modulus := + @npowBinRec (FastField modulus) ⟨one modulus⟩ ⟨mul⟩ n x /-- Inversion in Montgomery form via Fermat's little theorem (`x⁻¹ = x^(p-2)`), by binary exponentiation (`pow`). -/ @[inline] -def inv (x : FastField F) : FastField F := - pow x (invExponent (F := F)) +def inv (x : FastField modulus) : FastField modulus := + pow x (modulus - 2) /-- Division through inversion and fast multiplication. -/ @[inline] -def div (x y : FastField F) : FastField F := +def div (x y : FastField modulus) : FastField modulus := mul x (inv y) -instance instZero : Zero (FastField F) where - zero := zero - -instance instOne : One (FastField F) where - one := one - -instance instAdd : Add (FastField F) where - add := add - -instance instNeg : Neg (FastField F) where - neg := neg - -instance instSub : Sub (FastField F) where - sub := sub - -instance instMul : Mul (FastField F) where - mul := mul +instance : Zero (FastField modulus) := ⟨zero modulus⟩ +instance : One (FastField modulus) := ⟨one modulus⟩ +instance : Add (FastField modulus) where add +instance : Neg (FastField modulus) where neg +instance : Sub (FastField modulus) where sub +instance : Mul (FastField modulus) where mul +instance : Inv (FastField modulus) where inv +instance : Div (FastField modulus) where div + +theorem zero_def : (0 : FastField modulus) = zero modulus := rfl +theorem one_def : (1 : FastField modulus) = one modulus := rfl +theorem add_def (x y : FastField modulus) : x + y = add x y := rfl +theorem neg_def (x : FastField modulus) : -x = neg x := rfl +theorem sub_def (x y : FastField modulus) : x - y = sub x y := rfl +theorem mul_def (x y : FastField modulus) : x * y = mul x y := rfl +theorem inv_def (x : FastField modulus) : x⁻¹ = inv x := rfl +theorem div_def (x y : FastField modulus) : x / y = x * y⁻¹ := rfl +theorem square_def (x : FastField modulus) : square x = x * x := rfl + +instance : NatCast (FastField modulus) := ⟨ofNat modulus⟩ +instance : IntCast (FastField modulus) := ⟨ofInt modulus⟩ + +instance : SMul ℕ (FastField modulus) where + smul n x := ofNat modulus n * x + +instance : SMul Int (FastField modulus) where + smul n x := ofInt modulus n * x + +instance : Pow (FastField modulus) ℕ where pow + +instance : Pow (FastField modulus) Int where + pow x n := + match n with + | Int.ofNat k => pow x k + | Int.negSucc k => pow (inv x) (k + 1) -instance instInv : Inv (FastField F) where - inv := inv +instance : NNRatCast (FastField modulus) where + nnratCast q := ofField (q : ZMod modulus) -instance instDiv : Div (FastField F) where - div := div +instance : RatCast (FastField modulus) where + ratCast q := ofField (q : ZMod modulus) -instance instNatCast : NatCast (FastField F) where - natCast := ofNat +instance : SMul ℚ≥0 (FastField modulus) where + smul q x := ofField (q • toField x) -instance instIntCast : IntCast (FastField F) where - intCast := ofInt +instance : SMul ℚ (FastField modulus) where + smul q x := ofField (q • toField x) -instance instNatSMul : SMul Nat (FastField F) where - smul n x := ofNat n * x +/-! ## Correctness -/ -instance instIntSMul : SMul Int (FastField F) where - smul n x := ofInt n * x +/-! ### Reduction and conversions -/ -instance instPowNat : Pow (FastField F) Nat where - pow := pow +private theorem reduce_val_toNat_cast {x : UInt64} + (h : x.toNat < modulus * 2 ^ 32) : + ((reduce x h).val.toNat : ZMod modulus) = + (x.toNat : ZMod modulus) * ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ := by + apply reduceRaw_cast <;> + simp [P.montgomeryNegInv_mul_modulus_mod_two_pow_32, P.two_ne_zero, *] -instance instPowInt : Pow (FastField F) Int where - pow x n := - match n with - | Int.ofNat k => pow x k - | Int.negSucc k => pow (inv x) (k + 1) - -instance instNNRatCast : NNRatCast (FastField F) where - nnratCast q := ofField (q : ZMod P.fieldSize) +@[simp] +theorem FastField.val_toNat_lt (x : FastField modulus) : x.val.toNat < modulus := x.property -instance instRatCast : RatCast (FastField F) where - ratCast q := ofField (q : ZMod P.fieldSize) +theorem toNat_lt_modulus {x : FastField modulus} : toNat x < modulus := by + simp [FastField.toNat, FastField.toUInt32] -instance instNNRatSMul : SMul ℚ≥0 (FastField F) where - smul q x := ofField (q • toField x) +private theorem toField_eq_val_toNat_cast_mul_inv {x : FastField modulus} : + toField x = + (x.val.toNat : ZMod modulus) * ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ := by + convert reduce_val_toNat_cast ?_ using 1 + +private theorem val_toNat_cast_eq_toField_mul {x : FastField modulus} : + (x.val.toNat : ZMod modulus) = + toField x * ((2 ^ 32 : ℕ) : ZMod modulus) := by + rw [toField_eq_val_toNat_cast_mul_inv, mul_assoc] + rw [inv_mul_cancel₀ P.two_pow_32_ne_zero, mul_one] + +private theorem ofCanonicalNat_val_toNat_cast {n : ℕ} (h : n < modulus) : + ((ofCanonicalNat n h).val.toNat : ZMod modulus) = + (n : ZMod modulus) * ((2 ^ 32 : ℕ) : ZMod modulus) := by + convert reduce_val_toNat_cast ?_ using 1 + simp only [Nat.cast_pow, Nat.cast_ofNat, UInt64.toNat_mul, UInt64.toNat_ofNat', + P.r2ModModulus_toNat, Nat.mod_mul_mod] + have hprod : n * ((2 ^ 32) ^ 2 % modulus) < 2 ^ 64 := by + nlinarith [P.r2ModModulus_lt_modulus, P.modulus_sq_lt_two_pow_64] + rw [Nat.mod_eq_of_lt hprod] + grind -instance instRatSMul : SMul ℚ (FastField F) where - smul q x := ofField (q • toField x) +@[simp] +theorem toField_ofCanonicalNat {n : ℕ} (h : n < modulus) : + toField (ofCanonicalNat n h) = (n : ZMod modulus) := by + rw [toField_eq_val_toNat_cast_mul_inv, ofCanonicalNat_val_toNat_cast, mul_assoc] + rw [mul_inv_cancel₀ P.two_pow_32_ne_zero, mul_one] -/-- Fermat-style inversion in `ZMod fieldSize`. -/ -theorem inv_eq_pow_field (a : ZMod P.fieldSize) (ha : a ≠ 0) : - a⁻¹ = a ^ (P.fieldSize - 2) := by - have hcard : Fintype.card (ZMod P.fieldSize) = P.fieldSize := ZMod.card P.fieldSize - have h1 : a ^ (P.fieldSize - 1) = 1 := by - have h := FiniteField.pow_card_sub_one_eq_one a ha - rw [hcard] at h; exact h - have hmul : a * a ^ (P.fieldSize - 2) = 1 := by - rw [← pow_succ']; show a ^ (P.fieldSize - 2 + 1) = 1 - have : P.fieldSize - 2 + 1 = P.fieldSize - 1 := by - have := P.two_lt_fieldSize; omega - rw [this]; exact h1 - exact (eq_inv_of_mul_eq_one_left (by rwa [mul_comm])).symm +@[simp] +theorem toNat_ofCanonicalNat {n : ℕ} (h : n < modulus) : + toNat (ofCanonicalNat n h) = n := + natCast_inj_of_lt (toField_ofCanonicalNat h) toNat_lt_modulus h /-- Converting from the canonical field to fast form and back is the identity. -/ @[simp] -theorem toField_ofField (x : ZMod P.fieldSize) : toField (ofField (F := F) x) = x := by - unfold ofField - rw [toField_ofCanonicalNat] - exact ZMod.natCast_zmod_val x +theorem toField_ofField (x : ZMod modulus) : toField (ofField x) = x := by + simp [ofField, toField_ofCanonicalNat] /-- Converting from fast form to the canonical field and back is the identity. -/ @[simp] -theorem ofField_toField (x : FastField F) : ofField (toField x) = x := by +theorem ofField_toField (x : FastField modulus) : ofField (toField x) = x := by apply Subtype.ext apply UInt32.toNat_inj.mp - apply nat_eq_of_field_eq (F := F) - · exact (ofField (toField x)).property - · exact x.property - · rw [raw_cast_eq_toField_mul] - rw [toField_ofField] - rw [raw_cast_eq_toField_mul] + apply natCast_inj_of_lt + · rw [val_toNat_cast_eq_toField_mul, toField_ofField] + rw [val_toNat_cast_eq_toField_mul] + · simp + · simp /-- The canonical-field interpretation distinguishes fast values. -/ -theorem toField_injective : Function.Injective (toField (F := F)) := +theorem toField_injective : Function.Injective (toField (modulus := modulus)) := Function.LeftInverse.injective ofField_toField +/-! ### Field operations -/ + /-- `toField` maps fast zero to canonical zero. -/ @[simp] -theorem toField_zero : toField (0 : FastField F) = 0 := by - rw [toField_eq_raw_mul_inv] - change ((0 : Nat) : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ = 0 - rw [Nat.cast_zero, zero_mul] +theorem toField_zero : toField (0 : FastField modulus) = 0 := by + simp [toField_eq_val_toNat_cast_mul_inv, zero_def, zero] /-- `toField` maps fast one to canonical one. -/ @[simp] -theorem toField_one : toField (1 : FastField F) = 1 := by - rw [toField_eq_raw_mul_inv] - change (P.rModModulus.toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹ = 1 - rw [P.rModModulus_cast] - exact mul_inv_cancel₀ P.uint32Size_ne_zero_in_field +theorem toField_one : toField (1 : FastField modulus) = 1 := by + simp only [toField_eq_val_toNat_cast_mul_inv, one_def, one, + Mont32Field.rModModulus_toNat, ZMod.natCast_mod] + exact mul_inv_cancel₀ P.two_pow_32_ne_zero /-- Fast addition agrees with addition in the canonical field. -/ @[simp] -theorem toField_add (x y : FastField F) : toField (x + y) = toField x + toField y := by - rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x, toField_eq_raw_mul_inv y] - unfold instAdd add - have hred := reduceUInt32Lt2Modulus_cast (F := F) (x.val + y.val) (by - rw [UInt32.toNat_add] - exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) (by - have hx := x.property; have hy := y.property; omega)) - change ((reduceUInt32Lt2ModulusRaw (F := F) (x.val + y.val)).toNat : ZMod P.fieldSize) = - ((x.val + y.val).toNat : ZMod P.fieldSize) at hred - change ((reduceUInt32Lt2ModulusRaw (F := F) (x.val + y.val)).toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹ = - (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + - (y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - rw [hred] - rw [UInt32.toNat_add] - have hsum_lt : x.val.toNat + y.val.toNat < UInt32.size := by - nlinarith [x.property, y.property, P.fieldSize_add_fieldSize_lt_uint32Size] - rw [Nat.mod_eq_of_lt hsum_lt] - rw [Nat.cast_add] +theorem toField_add (x y : FastField modulus) : toField (x + y) = toField x + toField y := by + rw [toField_eq_val_toNat_cast_mul_inv, toField_eq_val_toNat_cast_mul_inv (x := x), + toField_eq_val_toNat_cast_mul_inv (x := y), add_def, add] + have hred := conditionalSubtract_cast (p32 := P.modulus32) (u := x.val + y.val) + rw [P.modulus32_toNat] at hred + rw [hred, UInt32.toNat_add] + have hsum_lt : x.val.toNat + y.val.toNat < 2 ^ 32 := by + nlinarith [x.property, y.property, P.modulus_lt_two_pow_31] + rw [Nat.mod_eq_of_lt hsum_lt, Nat.cast_add] ring /-- Fast subtraction agrees with subtraction in the canonical field. -/ @[simp] -theorem toField_sub (x y : FastField F) : toField (x - y) = toField x - toField y := by - rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x, toField_eq_raw_mul_inv y] +theorem toField_sub (x y : FastField modulus) : toField (x - y) = toField x - toField y := by + rw [toField_eq_val_toNat_cast_mul_inv, toField_eq_val_toNat_cast_mul_inv (x := x), + toField_eq_val_toNat_cast_mul_inv (x := y)] + simp only [sub_def] by_cases hyx : y.val ≤ x.val - · have hsubval : (x - y : FastField F).val = x.val - y.val := by - change (sub x y).val = x.val - y.val - unfold sub - rw [dif_pos hyx] - rw [hsubval] - change (((x.val - y.val).toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹) = - (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - - (y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + · simp only [sub, hyx, ↓reduceDIte] rw [UInt32.toNat_sub_of_le _ _ hyx] rw [Nat.cast_sub (by rw [UInt32.le_iff_toNat_le] at hyx exact hyx)] ring - · have hsum_lt : x.val.toNat + P.fieldSize < UInt32.size := by - have htwo := P.fieldSize_add_fieldSize_lt_uint32Size + · have hsum_lt : x.val.toNat + modulus < 2 ^ 32 := by + have htwo := P.modulus_lt_two_pow_31 have := x.property; omega - have hsum_eq : (x.val + P.modulus).toNat = x.val.toNat + P.fieldSize := by - rw [UInt32.toNat_add, P.modulus_toNat, Nat.mod_eq_of_lt hsum_lt] - have hyle : y.val ≤ x.val + P.modulus := by + have hsum_eq : (x.val + P.modulus32).toNat = x.val.toNat + modulus := by + rw [UInt32.toNat_add, P.modulus32_toNat, Nat.mod_eq_of_lt hsum_lt] + have hyle : y.val ≤ x.val + P.modulus32 := by rw [UInt32.le_iff_toNat_le, hsum_eq] have := y.property; omega - have hsubval : (x - y : FastField F).val = x.val + P.modulus - y.val := by - change (sub x y).val = x.val + P.modulus - y.val - unfold sub - rw [dif_neg hyx] - rw [hsubval] - change (((x.val + P.modulus - y.val).toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹) = - (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - - (y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + simp only [sub, hyx, ↓reduceDIte] rw [UInt32.toNat_sub_of_le _ _ hyle, hsum_eq] rw [Nat.cast_sub (by rw [UInt32.le_iff_toNat_le, hsum_eq] at hyle @@ -729,106 +421,59 @@ theorem toField_sub (x y : FastField F) : toField (x - y) = toField x - toField /-- Fast negation agrees with negation in the canonical field. -/ @[simp] -theorem toField_neg (x : FastField F) : toField (-x) = -toField x := by - rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x] +theorem toField_neg (x : FastField modulus) : toField (-x) = -toField x := by + rw [toField_eq_val_toNat_cast_mul_inv, toField_eq_val_toNat_cast_mul_inv (x := x)] + simp only [neg_def] by_cases hx : x.val = 0 - · have hnegval : (-x : FastField F).val = (zero : FastField F).val := by - change (neg x).val = (zero : FastField F).val - unfold neg - rw [dif_pos hx] - rw [hnegval] - change ((zero : FastField F).val.toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹ = - -((x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) - have hxNat : x.val.toNat = 0 := by - simpa using congrArg UInt32.toNat hx - rw [hxNat] - change ((0 : Nat) : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ = - -(((0 : Nat) : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) - simp - · have hle : x.val ≤ P.modulus := by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] + · simp only [neg, hx, ↓reduceDIte, zero] + have hxNat := congrArg UInt32.toNat hx + simp_all + · have hle : x.val ≤ P.modulus32 := by + rw [UInt32.le_iff_toNat_le, P.modulus32_toNat] exact Nat.le_of_lt x.property - have hnegval : (-x : FastField F).val = P.modulus - x.val := by - change (neg x).val = P.modulus - x.val - unfold neg - rw [dif_neg hx] - rw [hnegval] - change (((P.modulus - x.val).toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹) = - -((x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) - rw [UInt32.toNat_sub_of_le _ _ hle, P.modulus_toNat] + simp only [neg, hx, ↓reduceDIte] + rw [UInt32.toNat_sub_of_le _ _ hle, P.modulus32_toNat] rw [Nat.cast_sub (by - rw [UInt32.le_iff_toNat_le, P.modulus_toNat] at hle + rw [UInt32.le_iff_toNat_le, P.modulus32_toNat] at hle exact hle)] rw [ZMod.natCast_self] ring /-- Fast multiplication agrees with multiplication in the canonical field. -/ -@[simp] -theorem toField_mul (x y : FastField F) : toField (x * y) = toField x * toField y := by - rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x, toField_eq_raw_mul_inv y] - unfold instMul mul - have hred := montgomeryReduceBounded_cast (F := F) (x.val.toUInt64 * y.val.toUInt64) (by - simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hprod : x.val.toNat * y.val.toNat < 2 ^ 64 := by - nlinarith [x.property, y.property, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [x.property, y.property, P.fieldSize_lt_uint32Size, P.fieldSize_pos]) - change ((montgomeryReduceBoundedRaw (F := F) (x.val.toUInt64 * y.val.toUInt64)).toNat : - ZMod P.fieldSize) = - ((x.val.toUInt64 * y.val.toUInt64).toNat : ZMod P.fieldSize) * - (UInt32.size : ZMod P.fieldSize)⁻¹ at hred - change ((montgomeryReduceBoundedRaw (F := F) (x.val.toUInt64 * y.val.toUInt64)).toNat : - ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ = - (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ * - ((y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) - rw [hred] +private theorem mul_val_toNat_cast (x y : FastField modulus) : + ((mul x y).val.toNat : ZMod modulus) = + (x.val.toNat : ZMod modulus) * (y.val.toNat : ZMod modulus) * + ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ := by + convert reduce_val_toNat_cast ?_ using 1 simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] have hprod : x.val.toNat * y.val.toNat < 2 ^ 64 := by - nlinarith [x.property, y.property, P.fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - rw [Nat.cast_mul] - ring - -/-- Ring equivalence between the fast Montgomery representation and the canonical field. -/ -def ringEquiv : FastField F ≃+* ZMod P.fieldSize where - toFun := toField - invFun := ofField - left_inv := ofField_toField - right_inv := toField_ofField - map_add' := toField_add - map_mul' := toField_mul - -@[simp] -theorem ringEquiv_apply (x : FastField F) : ringEquiv x = toField x := rfl + nlinarith [x.property, y.property, P.modulus_sq_lt_two_pow_64] + rw [Nat.mod_eq_of_lt hprod, Nat.cast_mul] @[simp] -theorem ringEquiv_symm_apply (x : ZMod P.fieldSize) : - (ringEquiv (F := F)).symm x = ofField x := rfl +theorem toField_mul (x y : FastField modulus) : toField (x * y) = toField x * toField y := by + rw [toField_eq_val_toNat_cast_mul_inv, toField_eq_val_toNat_cast_mul_inv (x := x), + toField_eq_val_toNat_cast_mul_inv (x := y), mul_def, mul_val_toNat_cast] + ring -private theorem mul_assoc_field (x y z : FastField F) : (x * y) * z = x * (y * z) := by +private theorem mul_assoc (x y z : FastField modulus) : (x * y) * z = x * (y * z) := by apply toField_injective rw [toField_mul, toField_mul, toField_mul, toField_mul] ring -private theorem pow_succ_field (x : FastField F) (n : Nat) : pow x (n + 1) = pow x n * x := by +private theorem pow_succ_field (x : FastField modulus) (n : ℕ) : pow x (n + 1) = pow x n * x := by unfold pow - letI : Semigroup (FastField F) := { - mul := (· * ·) - mul_assoc := mul_assoc_field - } + letI : Semigroup (FastField modulus) := { mul, mul_assoc } exact npowBinRec_succ n x /-- Fast squaring agrees with multiplication by itself in the canonical field. -/ @[simp] -theorem toField_square (x : FastField F) : toField (square x) = toField x * toField x := by - change toField (x * x) = toField x * toField x - rw [toField_mul] +theorem toField_square (x : FastField modulus) : toField (square x) = toField x * toField x := by + simp only [square_def, toField_mul] /-- Fast natural-power computation agrees with powers in the canonical field. -/ @[simp] -theorem toField_pow (x : FastField F) (n : Nat) : toField (pow x n) = toField x ^ n := by +theorem toField_pow (x : FastField modulus) (n : ℕ) : toField (pow x n) = toField x ^ n := by induction n with | zero => unfold pow @@ -838,84 +483,70 @@ theorem toField_pow (x : FastField F) (n : Nat) : toField (pow x n) = toField x | succ n ih => rw [pow_succ_field, toField_mul, ih, _root_.pow_succ] -private theorem toField_inv_pow (x : FastField F) : - toField (inv x) = toField x ^ (invExponent (F := F)) := by - unfold inv - exact toField_pow x (invExponent (F := F)) - -private theorem toField_inv_raw (x : FastField F) : toField (inv x) = (toField x)⁻¹ := by - rw [toField_inv_pow] - by_cases hx : toField x = 0 - · rw [hx, inv_zero] - exact zero_pow (by unfold invExponent; have := P.two_lt_fieldSize; omega) - · simpa [invExponent] using (inv_eq_pow_field (toField x) hx).symm +/-- Fermat-style inversion in `ZMod modulus`. -/ +private theorem inv_eq_pow {a : ZMod modulus} (ha : a ≠ 0) : + a⁻¹ = a ^ (modulus - 2) := by + have hcard : Fintype.card (ZMod modulus) = modulus := ZMod.card modulus + have h1 : a ^ (modulus - 1) = 1 := by + have h := FiniteField.pow_card_sub_one_eq_one a ha + rw [hcard] at h; exact h + have hmul : a * a ^ (modulus - 2) = 1 := by + rw [← pow_succ']; show a ^ (modulus - 2 + 1) = 1 + have : modulus - 2 + 1 = modulus - 1 := by + have := P.two_lt_modulus; omega + rw [this]; exact h1 + exact (eq_inv_of_mul_eq_one_left (by rwa [mul_comm])).symm /-- Fast inversion agrees with inversion in the canonical field. -/ @[simp] -theorem toField_inv (x : FastField F) : toField x⁻¹ = (toField x)⁻¹ := by - change toField (inv x) = (toField x)⁻¹ - exact toField_inv_raw x - -private theorem toField_mul_raw (x y : FastField F) : - toField (mul x y) = toField x * toField y := by - change toField (x * y) = toField x * toField y - exact toField_mul x y - -private theorem toField_div_mul_inv (x y : FastField F) : - toField (div x y) = toField x * toField (inv y) := by - unfold div - exact toField_mul_raw x (inv y) +theorem toField_inv (x : FastField modulus) : toField x⁻¹ = (toField x)⁻¹ := by + simp only [inv_def, inv, toField_pow] + by_cases hx : toField x = 0 + · rw [hx, inv_zero, zero_pow] + have := P.two_lt_modulus + omega + · rw [inv_eq_pow hx] /-- Fast division agrees with division in the canonical field. -/ @[simp] -theorem toField_div (x y : FastField F) : toField (x / y) = toField x / toField y := by - change toField (div x y) = toField x / toField y - have h : ∀ a b c : ZMod P.fieldSize, c = b⁻¹ → a * c = a / b := by - intro a b c hc - rw [hc] - rfl - exact (toField_div_mul_inv x y).trans - (h (toField x) (toField y) (toField (inv y)) (toField_inv_raw y)) +theorem toField_div (x y : FastField modulus) : toField (x / y) = toField x / toField y := by + simp only [div_def, toField_mul, toField_inv] + rfl /-- Natural casts into fast form agree with natural casts into the canonical field. -/ @[simp] -theorem toField_natCast (n : Nat) : toField (n : FastField F) = (n : ZMod P.fieldSize) := by - change toField (ofNat n) = (n : ZMod P.fieldSize) - unfold ofNat - rw [toField_ofCanonicalNat] - rw [ZMod.natCast_eq_natCast_iff] +theorem toField_natCast (n : ℕ) : toField (n : FastField modulus) = (n : ZMod modulus) := by + change toField (ofNat modulus n) = (n : ZMod modulus) + rw [ofNat, toField_ofCanonicalNat, ZMod.natCast_eq_natCast_iff] exact Nat.mod_modEq _ _ /-- Integer casts into fast form agree with integer casts into the canonical field. -/ @[simp] -theorem toField_intCast (n : Int) : toField (n : FastField F) = (n : ZMod P.fieldSize) := by - change toField (ofInt n) = (n : ZMod P.fieldSize) - unfold ofInt +theorem toField_intCast (n : Int) : toField (n : FastField modulus) = (n : ZMod modulus) := by + change toField (ofField n) = (n : ZMod modulus) rw [toField_ofField] /-- Natural scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_nsmul (n : Nat) (x : FastField F) : toField (n • x) = n • toField x := by - change toField ((n : FastField F) * x) = n • toField x - rw [toField_mul, toField_natCast] - rw [nsmul_eq_mul] +theorem toField_nsmul (n : ℕ) (x : FastField modulus) : toField (n • x) = n • toField x := by + change toField ((n : FastField modulus) * x) = n • toField x + rw [toField_mul, toField_natCast, nsmul_eq_mul] /-- Integer scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_zsmul (n : Int) (x : FastField F) : toField (n • x) = n • toField x := by - change toField ((n : FastField F) * x) = n • toField x - rw [toField_mul, toField_intCast] - rw [zsmul_eq_mul] +theorem toField_zsmul (n : Int) (x : FastField modulus) : toField (n • x) = n • toField x := by + change toField ((n : FastField modulus) * x) = n • toField x + rw [toField_mul, toField_intCast, zsmul_eq_mul] /-- Natural powers through the `Pow` instance are preserved by `toField`. -/ @[simp] -theorem toField_npow (x : FastField F) (n : Nat) : toField (x ^ n) = toField x ^ n := by +theorem toField_npow (x : FastField modulus) (n : ℕ) : toField (x ^ n) = toField x ^ n := by change toField (pow x n) = toField x ^ n rw [toField_pow] /-- Integer powers through the `Pow` instance are preserved by `toField`. -/ @[simp] -theorem toField_zpow (x : FastField F) (n : Int) : toField (x ^ n) = toField x ^ n := by +theorem toField_zpow (x : FastField modulus) (n : Int) : toField (x ^ n) = toField x ^ n := by cases n with | ofNat n => change toField (pow x n) = toField x ^ (Int.ofNat n) @@ -930,65 +561,59 @@ theorem toField_zpow (x : FastField F) (n : Int) : toField (x ^ n) = toField x ^ /-- Nonnegative rational casts into fast form agree with canonical-field casts. -/ @[simp] -theorem toField_nnratCast (q : ℚ≥0) : toField (q : FastField F) = (q : ZMod P.fieldSize) := by - change toField (ofField (q : ZMod P.fieldSize)) = (q : ZMod P.fieldSize) +theorem toField_nnratCast (q : ℚ≥0) : toField (q : FastField modulus) = (q : ZMod modulus) := by + change toField (ofField (q : ZMod modulus)) = (q : ZMod modulus) rw [toField_ofField] /-- Rational casts into fast form agree with canonical-field casts. -/ @[simp] -theorem toField_ratCast (q : ℚ) : toField (q : FastField F) = (q : ZMod P.fieldSize) := by - change toField (ofField (q : ZMod P.fieldSize)) = (q : ZMod P.fieldSize) +theorem toField_ratCast (q : ℚ) : toField (q : FastField modulus) = (q : ZMod modulus) := by + change toField (ofField (q : ZMod modulus)) = (q : ZMod modulus) rw [toField_ofField] /-- Nonnegative rational scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_nnqsmul (q : ℚ≥0) (x : FastField F) : toField (q • x) = q • toField x := by +theorem toField_nnqsmul (q : ℚ≥0) (x : FastField modulus) : toField (q • x) = q • toField x := by change toField (ofField (q • toField x)) = q • toField x rw [toField_ofField] /-- Rational scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_qsmul (q : ℚ) (x : FastField F) : toField (q • x) = q • toField x := by +theorem toField_qsmul (q : ℚ) (x : FastField modulus) : toField (q • x) = q • toField x := by change toField (ofField (q • toField x)) = q • toField x rw [toField_ofField] +/-! ### Algebraic structure -/ + +/-- Ring equivalence between the fast Montgomery representation and the canonical field. -/ +def ringEquiv (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus ≃+* ZMod modulus where + toFun := toField + invFun := ofField + left_inv := ofField_toField + right_inv := toField_ofField + map_add' := toField_add + map_mul' := toField_mul + +@[simp] +theorem ringEquiv_apply {x : FastField modulus} : ringEquiv modulus x = toField x := rfl + +@[simp] +theorem ringEquiv_symm_apply {x : ZMod modulus} : + (ringEquiv modulus).symm x = ofField x := rfl + /-- Field instance transferred from the canonical field through `toField`. -/ -instance (priority := low) instField : _root_.Field (FastField F) := - toField_injective.field toField - toField_zero - toField_one - toField_add - toField_mul - toField_neg - toField_sub - toField_inv - toField_div - toField_nsmul - toField_zsmul - toField_nnqsmul - toField_qsmul - toField_npow - toField_zpow - toField_natCast - toField_intCast - toField_nnratCast - toField_ratCast - -/-- Commutative-ring instance inherited from the transferred field structure. -/ -instance (priority := low) instCommRing : CommRing (FastField F) := by - infer_instance +instance instField : _root_.Field (FastField modulus) := by + apply toField_injective.field toField <;> simp /-- A fast 32-bit-word field is non-binary. -/ -instance (priority := low) instNonBinaryField : NonBinaryField (FastField F) where +instance instNonBinaryField : NonBinaryField (FastField modulus) where char_neq_2 := by - change ((2 : Nat) : FastField F) ≠ 0 intro h - exact P.two_ne_zero_in_field (by - calc - (2 : ZMod P.fieldSize) = ((2 : Nat) : ZMod P.fieldSize) := by norm_cast - _ = toField ((2 : Nat) : FastField F) := (toField_natCast 2).symm - _ = toField (0 : FastField F) := congrArg toField h - _ = 0 := toField_zero) + apply P.two_ne_zero + calc + _ = toField ((2 : ℕ) : FastField modulus) := (toField_natCast 2).symm + _ = toField (0 : FastField modulus) := congrArg toField h + _ = 0 := toField_zero end diff --git a/CompPoly/Fields/README.md b/CompPoly/Fields/README.md index f7718c2a..6830d132 100644 --- a/CompPoly/Fields/README.md +++ b/CompPoly/Fields/README.md @@ -20,8 +20,8 @@ This directory contains formally verified field infrastructure used in zero-know | **KoalaBear/Fast.lean** | KoalaBear-namespaced API over the shared fast-field implementation (`Montgomery/Native32Field.lean`): thin wrappers forwarding the native `UInt32` Montgomery-residue operations and their `KoalaBear.Field` equivalence (`@[simp]`) lemmas. | | **Mersenne.lean** | \(2^{31} - 1\) — Circle STARKs. | | **Montgomery/Basic.lean** | Radix-generic Montgomery reduction, field-agnostic number theory shared by the fast prime fields. | -| **Montgomery/Native32.lean** | `UInt32 × UInt64`, radix `R = 2^32` word-level Montgomery bridge over the generic core. | -| **Montgomery/Native32Field.lean** | Shared 32-bit-word fast-field implementation over the word bridge: the `Mont32Field` per-field data class, the `FastField` carrier, every field operation, the algebraic instances, and the `toField`/`ofField` correctness bridge — written once and instantiated by both BabyBear and KoalaBear. | +| **Montgomery/Native32.lean** | Raw `UInt32`/`UInt64` Montgomery reduction over explicit word constants, including bounds and correctness. | +| **Montgomery/Native32Field.lean** | Per-field parameters, the shared `FastField` carrier, arithmetic, instances, and canonical-field bridge. | | **Secp256k1.lean** | Base and scalar fields for the Secp256k1 curve (used in Bitcoin/Ethereum). | ## Binary-field modules diff --git a/CompPoly/Univariate/NTT/BabyBear.lean b/CompPoly/Univariate/NTT/BabyBear.lean index f8c4d6d8..4464f689 100644 --- a/CompPoly/Univariate/NTT/BabyBear.lean +++ b/CompPoly/Univariate/NTT/BabyBear.lean @@ -22,23 +22,6 @@ def bitsOfLogN (logN : Nat) (hlogN : logN ≤ BabyBear.twoAdicity) : Fin (BabyBear.twoAdicity + 1) := ⟨logN, Nat.lt_succ_of_le hlogN⟩ -/-- The BabyBear NTT domain size is nonzero in the field for supported two-adic sizes. -/ -theorem twoPowNatCast_ne_zero - (logN : Nat) (hlogN : logN ≤ BabyBear.twoAdicity) : - (((2 ^ logN : Nat) : BabyBear.Field) ≠ 0) := by - intro hzero - have hpow_pos : 0 < 2 ^ logN := by - positivity - have hpow_le : 2 ^ logN ≤ 2 ^ BabyBear.twoAdicity := by - exact Nat.pow_le_pow_right (by decide : 1 ≤ 2) hlogN - have hpow_lt : 2 ^ logN < BabyBear.fieldSize := by - have htop : 2 ^ BabyBear.twoAdicity < BabyBear.fieldSize := by - simp [BabyBear.twoAdicity, BabyBear.fieldSize] - exact lt_of_le_of_lt hpow_le htop - have hdiv : BabyBear.fieldSize ∣ 2 ^ logN := by - exact (ZMod.natCast_eq_zero_iff (2 ^ logN) BabyBear.fieldSize).mp hzero - exact (not_le_of_gt hpow_lt) (Nat.le_of_dvd hpow_pos hdiv) - /-- BabyBear radix-2 NTT domain for a supported two-adic size. -/ def domainOfLogN (logN : Nat) (hlogN : logN ≤ BabyBear.twoAdicity) : Domain BabyBear.Field where @@ -47,7 +30,6 @@ def domainOfLogN (logN : Nat) (hlogN : logN ≤ BabyBear.twoAdicity) : primitive := by simpa [bitsOfLogN] using BabyBear.isPrimitiveRoot_twoAdicGenerator (bitsOfLogN logN hlogN) - natCast_ne_zero := twoPowNatCast_ne_zero logN hlogN end BabyBear end NTT diff --git a/CompPoly/Univariate/NTT/Domain.lean b/CompPoly/Univariate/NTT/Domain.lean index d99f2d6c..8e636c1a 100644 --- a/CompPoly/Univariate/NTT/Domain.lean +++ b/CompPoly/Univariate/NTT/Domain.lean @@ -26,7 +26,6 @@ structure Domain (R : Type*) [Field R] where logN : Nat omega : R primitive : IsPrimitiveRoot omega (2 ^ logN) - natCast_ne_zero : (((2 ^ logN : Nat) : R) ≠ 0) namespace Domain @@ -48,7 +47,6 @@ def inverse (D : Domain R) : Domain R where omega := D.omegaInv primitive := by simpa [omegaInv] using D.primitive.inv - natCast_ne_zero := D.natCast_ne_zero /-- Multiplicative inverse of the domain size in `R`. -/ @[inline] def nInv (D : Domain R) : R := ((D.n : Nat) : R)⁻¹ @@ -59,6 +57,11 @@ def inverse (D : Domain R) : Domain R where @[simp] lemma n_ne_zero (D : Domain R) : D.n ≠ 0 := by exact Nat.ne_of_gt D.n_pos +/-- The size of an NTT domain is nonzero in its coefficient field. -/ +theorem natCast_ne_zero (D : Domain R) : ((D.n : Nat) : R) ≠ 0 := by + letI : NeZero D.n := ⟨D.n_ne_zero⟩ + exact D.primitive.neZero'.out + section RawHelpers variable [BEq R] diff --git a/CompPoly/Univariate/NTT/KoalaBear.lean b/CompPoly/Univariate/NTT/KoalaBear.lean index aeba091b..edb4794f 100644 --- a/CompPoly/Univariate/NTT/KoalaBear.lean +++ b/CompPoly/Univariate/NTT/KoalaBear.lean @@ -22,23 +22,6 @@ def bitsOfLogN (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : Fin (KoalaBear.twoAdicity + 1) := ⟨logN, Nat.lt_succ_of_le hlogN⟩ -/-- The KoalaBear NTT domain size is nonzero in the field for supported two-adic sizes. -/ -theorem twoPowNatCast_ne_zero - (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : - (((2 ^ logN : Nat) : KoalaBear.Field) ≠ 0) := by - intro hzero - have hpow_pos : 0 < 2 ^ logN := by - positivity - have hpow_le : 2 ^ logN ≤ 2 ^ KoalaBear.twoAdicity := by - exact Nat.pow_le_pow_right (by decide : 1 ≤ 2) hlogN - have hpow_lt : 2 ^ logN < KoalaBear.fieldSize := by - have htop : 2 ^ KoalaBear.twoAdicity < KoalaBear.fieldSize := by - simp [KoalaBear.twoAdicity, KoalaBear.fieldSize] - exact lt_of_le_of_lt hpow_le htop - have hdiv : KoalaBear.fieldSize ∣ 2 ^ logN := by - exact (ZMod.natCast_eq_zero_iff (2 ^ logN) KoalaBear.fieldSize).mp hzero - exact (not_le_of_gt hpow_lt) (Nat.le_of_dvd hpow_pos hdiv) - /-- KoalaBear radix-2 NTT domain for a supported two-adic size. -/ def domainOfLogN (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : Domain KoalaBear.Field where @@ -47,7 +30,6 @@ def domainOfLogN (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : primitive := by simpa [bitsOfLogN] using KoalaBear.isPrimitiveRoot_twoAdicGenerator (bitsOfLogN logN hlogN) - natCast_ne_zero := twoPowNatCast_ne_zero logN hlogN /-- KoalaBear NTT domain lookup for dynamic multiplication contexts. -/ def bestDomainForLength? (requiredLen : Nat) : @@ -55,42 +37,15 @@ def bestDomainForLength? (requiredLen : Nat) : CPolynomial.NTT.bestDomainForLength? KoalaBear.twoAdicity domainOfLogN (by intro _ _; rfl) requiredLen -/-- Fast KoalaBear two-adic generators are primitive roots of the same orders. -/ -theorem fast_isPrimitiveRoot_twoAdicGenerator - (bits : Fin (KoalaBear.twoAdicity + 1)) : - IsPrimitiveRoot (KoalaBear.Fast.ofField KoalaBear.twoAdicGenerators[bits]) - (2 ^ (bits : Nat)) := by - have hbasic : IsPrimitiveRoot KoalaBear.twoAdicGenerators[bits] (2 ^ (bits : Nat)) := - KoalaBear.isPrimitiveRoot_twoAdicGenerator bits - have hfast : - IsPrimitiveRoot (KoalaBear.Fast.ringEquiv.symm KoalaBear.twoAdicGenerators[bits]) - (2 ^ (bits : Nat)) := by - exact hbasic.map_of_injective KoalaBear.Fast.ringEquiv.symm.injective - simpa using hfast - -/-- The fast KoalaBear NTT domain size is nonzero for supported two-adic sizes. -/ -theorem fast_twoPowNatCast_ne_zero - (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : - (((2 ^ logN : Nat) : KoalaBear.Fast.Field) ≠ 0) := by - intro hzero - exact twoPowNatCast_ne_zero logN hlogN (by - calc - (((2 ^ logN : Nat) : KoalaBear.Field)) = - KoalaBear.Fast.toField (((2 ^ logN : Nat) : KoalaBear.Fast.Field)) := by - rw [KoalaBear.Fast.toField_natCast] - _ = KoalaBear.Fast.toField 0 := congrArg KoalaBear.Fast.toField hzero - _ = 0 := KoalaBear.Fast.toField_zero) - /-- Fast KoalaBear radix-2 NTT domain for a supported two-adic size. -/ def fastDomainOfLogN (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : Domain KoalaBear.Fast.Field where logN := logN - omega := KoalaBear.Fast.ofField - KoalaBear.twoAdicGenerators[bitsOfLogN logN hlogN] + omega := KoalaBear.Fast.twoAdicGenerators[bitsOfLogN logN hlogN] primitive := by - simpa [bitsOfLogN] using - fast_isPrimitiveRoot_twoAdicGenerator (bitsOfLogN logN hlogN) - natCast_ne_zero := fast_twoPowNatCast_ne_zero logN hlogN + have h := (KoalaBear.isPrimitiveRoot_twoAdicGenerator (bitsOfLogN logN hlogN)).map_of_injective + KoalaBear.Fast.ringEquiv.symm.injective + simpa [KoalaBear.Fast.twoAdicGenerators_eq_map] using h /-- Fast KoalaBear NTT domain lookup for dynamic multiplication contexts. -/ def fastBestDomainForLength? (requiredLen : Nat) : diff --git a/bench/CompPolyBench/Common.lean b/bench/CompPolyBench/Common.lean index 0c885e5b..4e5ab3de 100644 --- a/bench/CompPolyBench/Common.lean +++ b/bench/CompPolyBench/Common.lean @@ -454,7 +454,7 @@ def checksumKoalaBear (x : KoalaBear.Field) : Nat := /-- Convert a fast KoalaBear element to a checksum word. -/ def checksumKoalaBearFast (x : KoalaBear.Fast.Field) : Nat := - KoalaBear.Fast.toNat x + x.toNat /-- Convert a `ZMod` element to a checksum word. -/ def checksumZMod {modulus : Nat} (x : ZMod modulus) : Nat := diff --git a/bench/CompPolyBench/Univariate/Common.lean b/bench/CompPolyBench/Univariate/Common.lean index 8a6ec4cb..2fd4ad0e 100644 --- a/bench/CompPolyBench/Univariate/Common.lean +++ b/bench/CompPolyBench/Univariate/Common.lean @@ -97,61 +97,13 @@ def koalaBearBestDomainForLength? (requiredLen : Nat) : CPolynomial.NTT.bestDomainForLength? KoalaBear.twoAdicity CPolynomial.NTT.KoalaBear.domainOfLogN (by intro _ _; rfl) requiredLen -/-- Ring equivalence from fast KoalaBear elements to the canonical `ZMod` model. -/ -noncomputable def koalaBearFastRingEquiv : KoalaBear.Fast.Field ≃+* KoalaBear.Field where - toFun := KoalaBear.Fast.toField - invFun := KoalaBear.Fast.ofField - left_inv := KoalaBear.Fast.ofField_toField - right_inv := KoalaBear.Fast.toField_ofField - map_mul' := KoalaBear.Fast.toField_mul - map_add' := KoalaBear.Fast.toField_add - -/-- Fast KoalaBear two-adic generators are primitive roots of the same orders. -/ -theorem koalaBearFast_isPrimitiveRoot_twoAdicGenerator - (bits : Fin (KoalaBear.twoAdicity + 1)) : - IsPrimitiveRoot (KoalaBear.Fast.ofField KoalaBear.twoAdicGenerators[bits]) - (2 ^ (bits : Nat)) := by - have hbasic : IsPrimitiveRoot KoalaBear.twoAdicGenerators[bits] (2 ^ (bits : Nat)) := - KoalaBear.isPrimitiveRoot_twoAdicGenerator bits - have hfast : - IsPrimitiveRoot (koalaBearFastRingEquiv.symm KoalaBear.twoAdicGenerators[bits]) - (2 ^ (bits : Nat)) := by - exact hbasic.map_of_injective koalaBearFastRingEquiv.symm.injective - simpa [koalaBearFastRingEquiv] using hfast - -/-- The fast KoalaBear NTT domain size is nonzero for supported two-adic sizes. -/ -theorem koalaBearFast_twoPowNatCast_ne_zero - (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : - (((2 ^ logN : Nat) : KoalaBear.Fast.Field) ≠ 0) := by - intro hzero - exact CPolynomial.NTT.KoalaBear.twoPowNatCast_ne_zero logN hlogN (by - calc - (((2 ^ logN : Nat) : KoalaBear.Field)) = - KoalaBear.Fast.toField (((2 ^ logN : Nat) : KoalaBear.Fast.Field)) := by - rw [KoalaBear.Fast.toField_natCast] - _ = KoalaBear.Fast.toField 0 := congrArg KoalaBear.Fast.toField hzero - _ = 0 := KoalaBear.Fast.toField_zero) - -/-- Fast KoalaBear radix-2 NTT domain for a supported two-adic size. -/ -def koalaBearFastDomainOfLogN (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) : - CPolynomial.NTT.Domain KoalaBear.Fast.Field where - logN := logN - omega := KoalaBear.Fast.ofField - KoalaBear.twoAdicGenerators[(⟨logN, Nat.lt_succ_of_le hlogN⟩ : - Fin (KoalaBear.twoAdicity + 1))] - primitive := by - simpa using koalaBearFast_isPrimitiveRoot_twoAdicGenerator - (⟨logN, Nat.lt_succ_of_le hlogN⟩ : Fin (KoalaBear.twoAdicity + 1)) - natCast_ne_zero := koalaBearFast_twoPowNatCast_ne_zero logN hlogN - /-- NTT domain for direct univariate fast KoalaBear multiplication benchmarks. -/ def koalaBearFastMulNttDomain : CPolynomial.NTT.Domain KoalaBear.Fast.Field := - koalaBearFastDomainOfLogN univariateMulLogN (by decide) + CPolynomial.NTT.KoalaBear.fastDomainOfLogN univariateMulLogN (by decide) /-- Fast KoalaBear NTT domain lookup for dynamic multiplication contexts. -/ def koalaBearFastBestDomainForLength? (requiredLen : Nat) : Option (CPolynomial.NTT.FittingDomain KoalaBear.Fast.Field requiredLen) := - CPolynomial.NTT.bestDomainForLength? KoalaBear.twoAdicity - koalaBearFastDomainOfLogN (by intro _ _; rfl) requiredLen + CPolynomial.NTT.KoalaBear.fastBestDomainForLength? requiredLen end CompPolyBench diff --git a/bench/CompPolyBench/Univariate/NTT/FastMul.lean b/bench/CompPolyBench/Univariate/NTT/FastMul.lean index d1465586..1c2c43a0 100644 --- a/bench/CompPolyBench/Univariate/NTT/FastMul.lean +++ b/bench/CompPolyBench/Univariate/NTT/FastMul.lean @@ -22,6 +22,11 @@ def univariateNttFastMulGroupInfos : List BenchGroupInfo := [ ⟨"univariate-mul-koalabear", "Univariate multiplication (KoalaBear)"⟩ ] +/-- Display and checksum operations associated with a benchmark field. -/ +private structure BenchField (F : Type*) where + id : String + checksum : F → Nat + /-- Benchmark KoalaBear direct univariate multiplication and root-of-unity NTT variants. -/ private def runKoalaBearUnivariateMul (preset : BenchPreset) (gen : StdGen) : IO (BenchGroup × StdGen) := do @@ -33,9 +38,14 @@ private def runKoalaBearUnivariateMul (preset : BenchPreset) (gen : StdGen) : let fastMulRhsCoeffs := koalaBearFastArray mulRhsCoeffs let fastMulLhsPoly := cpolyOfArray fastMulLhsCoeffs let fastMulRhsPoly := cpolyOfArray fastMulRhsCoeffs - let koalaBearMulNttFastPlan := CPolynomial.NTTFast.Plan.ofDomain koalaBearMulNttDomain - let koalaBearFastMulNttFastPlan := - CPolynomial.NTTFast.Plan.ofDomain koalaBearFastMulNttDomain + let canonicalPlan := CPolynomial.NTTFast.Plan.ofDomain koalaBearMulNttDomain + let fastPlan := CPolynomial.NTTFast.Plan.ofDomain koalaBearFastMulNttDomain + let canonicalField : BenchField KoalaBear.Field := + ⟨"KoalaBear.Field", checksumKoalaBear⟩ + let fastField : BenchField KoalaBear.Fast.Field := + ⟨"KoalaBear.Fast.Field", checksumKoalaBearFast⟩ + let canonicalChecksum := checksumCPolynomial canonicalField.checksum + let fastChecksum := checksumCPolynomial fastField.checksum let warmup := mulWarmupIterations preset let measured := mulMeasuredIterations preset let nttMeasured := preset.selectNat 200 30 5 @@ -49,66 +59,61 @@ private def runKoalaBearUnivariateMul (preset : BenchPreset) (gen : StdGen) : nttMeasured, nttFastMeasured, nttFastPlanMeasured, fastMeasured, fastNttMeasured, fastNttFastMeasured, fastNttFastPlanMeasured ] - let koalaBearMulNaive ← runTimed - "univariate-mul-naive" "CPolynomial" "mul" "KoalaBear.Field" + let canonicalNaive ← runTimed + "univariate-mul-naive" "CPolynomial" "mul" canonicalField.id univariateMulShape preset warmup measured - (fun _ ↦ mulLhsPoly * mulRhsPoly) - (checksumCPolynomial checksumKoalaBear) (checksumIterations := checksumIterations) - let koalaBearFastMulNaive ← runTimed - "univariate-mul-naive-fast" "CPolynomial" "mul" "KoalaBear.Fast.Field" + (fun _ ↦ mulLhsPoly * mulRhsPoly) canonicalChecksum + (checksumIterations := checksumIterations) + let fastNaive ← runTimed + "univariate-mul-naive-fast" "CPolynomial" "mul" fastField.id univariateMulShape preset warmup fastMeasured - (fun _ ↦ fastMulLhsPoly * fastMulRhsPoly) - (checksumCPolynomial checksumKoalaBearFast) (checksumIterations := checksumIterations) - let koalaBearMulNtt ← runTimed + (fun _ ↦ fastMulLhsPoly * fastMulRhsPoly) fastChecksum + (checksumIterations := checksumIterations) + let canonicalNtt ← runTimed "univariate-mul-ntt" "CPolynomial" (univariateMulNttMethod "FastMul.fastMulImpl") - "KoalaBear.Field" - univariateMulShape preset warmup nttMeasured - (fun _ ↦ CPolynomial.NTT.FastMul.fastMulImpl koalaBearMulNttDomain mulLhsPoly mulRhsPoly) - (checksumCPolynomial checksumKoalaBear) (checksumIterations := checksumIterations) - let koalaBearFastMulNtt ← runTimed + canonicalField.id univariateMulShape preset warmup nttMeasured + (fun _ ↦ + CPolynomial.NTT.FastMul.fastMulImpl koalaBearMulNttDomain mulLhsPoly mulRhsPoly) + canonicalChecksum (checksumIterations := checksumIterations) + let fastNtt ← runTimed "univariate-mul-ntt-koalabear-fast" "CPolynomial" - (univariateMulNttMethod "FastMul.fastMulImpl") "KoalaBear.Fast.Field" + (univariateMulNttMethod "FastMul.fastMulImpl") fastField.id univariateMulShape preset warmup fastNttMeasured - (fun _ ↦ CPolynomial.NTT.FastMul.fastMulImpl koalaBearFastMulNttDomain fastMulLhsPoly - fastMulRhsPoly) - (checksumCPolynomial checksumKoalaBearFast) (checksumIterations := checksumIterations) - let koalaBearMulNttFast ← runTimed + (fun _ ↦ CPolynomial.NTT.FastMul.fastMulImpl koalaBearFastMulNttDomain + fastMulLhsPoly fastMulRhsPoly) + fastChecksum (checksumIterations := checksumIterations) + let canonicalNttFast ← runTimed "univariate-mul-ntt-fast" "CPolynomial" (univariateMulNttMethod "NTTFast.fastMulImpl") - "KoalaBear.Field" - univariateMulShape preset warmup nttFastMeasured - (fun _ ↦ CPolynomial.NTTFast.fastMulImpl koalaBearMulNttDomain mulLhsPoly mulRhsPoly) - (checksumCPolynomial checksumKoalaBear) (checksumIterations := checksumIterations) - let koalaBearFastMulNttFast ← runTimed + canonicalField.id univariateMulShape preset warmup nttFastMeasured + (fun _ ↦ + CPolynomial.NTTFast.fastMulImpl koalaBearMulNttDomain mulLhsPoly mulRhsPoly) + canonicalChecksum (checksumIterations := checksumIterations) + let fastNttFast ← runTimed "univariate-mul-ntt-fast-koalabear-fast" "CPolynomial" - (univariateMulNttMethod "NTTFast.fastMulImpl") "KoalaBear.Fast.Field" + (univariateMulNttMethod "NTTFast.fastMulImpl") fastField.id univariateMulShape preset warmup fastNttFastMeasured - (fun _ ↦ CPolynomial.NTTFast.fastMulImpl koalaBearFastMulNttDomain fastMulLhsPoly - fastMulRhsPoly) - (checksumCPolynomial checksumKoalaBearFast) (checksumIterations := checksumIterations) - let koalaBearMulNttFastPlanRecord ← runTimed + (fun _ ↦ CPolynomial.NTTFast.fastMulImpl koalaBearFastMulNttDomain + fastMulLhsPoly fastMulRhsPoly) + fastChecksum (checksumIterations := checksumIterations) + let canonicalNttFastPlan ← runTimed "univariate-mul-ntt-fast-plan" "CPolynomial" (univariateMulNttMethod "NTTFast.Plan.fastMulImpl, cached twiddles, mixed radix-4 DIF/DIT, dual forward") - "KoalaBear.Field" - univariateMulShape preset warmup nttFastPlanMeasured - (fun _ ↦ CPolynomial.NTTFast.Plan.fastMulImpl koalaBearMulNttFastPlan mulLhsPoly - mulRhsPoly) - (checksumCPolynomial checksumKoalaBear) (checksumIterations := checksumIterations) - let koalaBearFastMulNttFastPlanRecord ← runTimed + canonicalField.id univariateMulShape preset warmup nttFastPlanMeasured + (fun _ ↦ CPolynomial.NTTFast.Plan.fastMulImpl canonicalPlan mulLhsPoly mulRhsPoly) + canonicalChecksum (checksumIterations := checksumIterations) + let fastNttFastPlan ← runTimed "univariate-mul-ntt-fast-plan-fast" "CPolynomial" (univariateMulNttMethod "NTTFast.Plan.fastMulImpl, cached twiddles, mixed radix-4 DIF/DIT, dual forward") - "KoalaBear.Fast.Field" - univariateMulShape preset warmup fastNttFastPlanMeasured - (fun _ ↦ CPolynomial.NTTFast.Plan.fastMulImpl koalaBearFastMulNttFastPlan - fastMulLhsPoly fastMulRhsPoly) - (checksumCPolynomial checksumKoalaBearFast) (checksumIterations := checksumIterations) + fastField.id univariateMulShape preset warmup fastNttFastPlanMeasured + (fun _ ↦ CPolynomial.NTTFast.Plan.fastMulImpl fastPlan fastMulLhsPoly fastMulRhsPoly) + fastChecksum (checksumIterations := checksumIterations) pure ({ groupKey := "univariate-mul-koalabear", title := "Univariate multiplication (KoalaBear)", - records := #[koalaBearMulNaive, koalaBearMulNtt, koalaBearMulNttFast, - koalaBearMulNttFastPlanRecord, koalaBearFastMulNaive, koalaBearFastMulNtt, - koalaBearFastMulNttFast, koalaBearFastMulNttFastPlanRecord] + records := #[canonicalNaive, canonicalNtt, canonicalNttFast, canonicalNttFastPlan, + fastNaive, fastNtt, fastNttFast, fastNttFastPlan] }, gen) /-- Runnable `CompPoly.Univariate.NTT.FastMul` benchmark tasks. -/ diff --git a/tests/CompPolyTests/Fields/BabyBear/Fast.lean b/tests/CompPolyTests/Fields/BabyBear/Fast.lean index 02b25071..909414df 100644 --- a/tests/CompPolyTests/Fields/BabyBear/Fast.lean +++ b/tests/CompPolyTests/Fields/BabyBear/Fast.lean @@ -14,28 +14,29 @@ Regression checks for the executable Montgomery representation. namespace BabyBear.Fast -#guard raw (0 : Field) = 0 -#guard raw (1 : Field) = rModModulus -#guard toCanonicalUInt32 (ofNat 37) = (37 : UInt32) -#guard toNat (ofNat BabyBear.fieldSize) = 0 -#guard toNat (ofNat (BabyBear.fieldSize + 37)) = 37 -#guard toNat ((ofNat (BabyBear.fieldSize - 1)) + (2 : Field)) = 1 -#guard toNat ((ofNat (BabyBear.fieldSize - 1)) + (ofNat (BabyBear.fieldSize - 1))) = +#guard (0 : Field).val = 0 +#guard (1 : Field).val = + Montgomery.Native32.Mont32Field.rModModulus BabyBear.fieldSize +#guard (37 : Field).toUInt32 = (37 : UInt32) +#guard (BabyBear.fieldSize : Field).toNat = 0 +#guard (BabyBear.fieldSize + 37 : Field).toNat = 37 +#guard ((BabyBear.fieldSize - 1 : Field) + 2).toNat = 1 +#guard ((BabyBear.fieldSize - 1 : Field) + (BabyBear.fieldSize - 1 : Field)).toNat = BabyBear.fieldSize - 2 -#guard toNat ((9 : Field) - (5 : Field)) = 4 -#guard toNat ((5 : Field) - (9 : Field)) = BabyBear.fieldSize - 4 -#guard toNat (-(0 : Field)) = 0 -#guard toNat (-(1 : Field)) = BabyBear.fieldSize - 1 -#guard toNat ((ofNat (BabyBear.fieldSize - 1)) * (ofNat (BabyBear.fieldSize - 1))) = 1 -#guard toNat (square (12345 : Field)) = 152399025 -#guard toNat ((37 : Field) ^ 0) = 1 -#guard toNat ((37 : Field) ^ 1) = 37 -#guard toField ((123456789 : Field) ^ 17) = ((123456789 : BabyBear.Field) ^ 17) -#guard toField ((123456789 : Field) ^ 255) = ((123456789 : BabyBear.Field) ^ 255) -#guard toNat ((0 : Field)⁻¹) = 0 -#guard toNat ((37 : Field)⁻¹ * (37 : Field)) = 1 -#guard toNat ((37 : Field) / (37 : Field)) = 1 -#guard toField ((37 : Field)⁻¹) = ((37 : BabyBear.Field)⁻¹) -#guard toField ((37 : Field) ^ (-3 : Int)) = ((37 : BabyBear.Field) ^ (-3 : Int)) +#guard ((9 : Field) - 5).toNat = 4 +#guard ((5 : Field) - 9).toNat = BabyBear.fieldSize - 4 +#guard (-(0 : Field)).toNat = 0 +#guard (-(1 : Field)).toNat = BabyBear.fieldSize - 1 +#guard ((BabyBear.fieldSize - 1 : Field) * (BabyBear.fieldSize - 1 : Field)).toNat = 1 +#guard ((12345 : Field) * 12345).toNat = 152399025 +#guard ((37 : Field) ^ 0).toNat = 1 +#guard ((37 : Field) ^ 1).toNat = 37 +#guard ((123456789 : Field) ^ 17).toField = ((123456789 : BabyBear.Field) ^ 17) +#guard ((123456789 : Field) ^ 255).toField = ((123456789 : BabyBear.Field) ^ 255) +#guard ((0 : Field)⁻¹).toNat = 0 +#guard ((37 : Field)⁻¹ * 37).toNat = 1 +#guard ((37 : Field) / 37).toNat = 1 +#guard ((37 : Field)⁻¹).toField = ((37 : BabyBear.Field)⁻¹) +#guard ((37 : Field) ^ (-3 : Int)).toField = ((37 : BabyBear.Field) ^ (-3 : Int)) end BabyBear.Fast diff --git a/tests/CompPolyTests/Fields/KoalaBear/Fast.lean b/tests/CompPolyTests/Fields/KoalaBear/Fast.lean index 5629a825..52f2d25a 100644 --- a/tests/CompPolyTests/Fields/KoalaBear/Fast.lean +++ b/tests/CompPolyTests/Fields/KoalaBear/Fast.lean @@ -14,28 +14,29 @@ Regression checks for the executable Montgomery representation. namespace KoalaBear.Fast -#guard raw (0 : Field) = 0 -#guard raw (1 : Field) = rModModulus -#guard toCanonicalUInt32 (ofNat 37) = (37 : UInt32) -#guard toNat (ofNat KoalaBear.fieldSize) = 0 -#guard toNat (ofNat (KoalaBear.fieldSize + 37)) = 37 -#guard toNat ((ofNat (KoalaBear.fieldSize - 1)) + (2 : Field)) = 1 -#guard toNat ((ofNat (KoalaBear.fieldSize - 1)) + (ofNat (KoalaBear.fieldSize - 1))) = +#guard (0 : Field).val = 0 +#guard (1 : Field).val = + Montgomery.Native32.Mont32Field.rModModulus (modulus := KoalaBear.fieldSize) +#guard (37 : Field).toUInt32 = (37 : UInt32) +#guard (KoalaBear.fieldSize : Field).toNat = 0 +#guard (KoalaBear.fieldSize + 37 : Field).toNat = 37 +#guard ((KoalaBear.fieldSize - 1 : Field) + 2).toNat = 1 +#guard ((KoalaBear.fieldSize - 1 : Field) + (KoalaBear.fieldSize - 1 : Field)).toNat = KoalaBear.fieldSize - 2 -#guard toNat ((9 : Field) - (5 : Field)) = 4 -#guard toNat ((5 : Field) - (9 : Field)) = KoalaBear.fieldSize - 4 -#guard toNat (-(0 : Field)) = 0 -#guard toNat (-(1 : Field)) = KoalaBear.fieldSize - 1 -#guard toNat ((ofNat (KoalaBear.fieldSize - 1)) * (ofNat (KoalaBear.fieldSize - 1))) = 1 -#guard toNat (square (12345 : Field)) = 152399025 -#guard toNat ((37 : Field) ^ 0) = 1 -#guard toNat ((37 : Field) ^ 1) = 37 -#guard toField ((123456789 : Field) ^ 17) = ((123456789 : KoalaBear.Field) ^ 17) -#guard toField ((123456789 : Field) ^ 255) = ((123456789 : KoalaBear.Field) ^ 255) -#guard toNat ((0 : Field)⁻¹) = 0 -#guard toNat ((37 : Field)⁻¹ * (37 : Field)) = 1 -#guard toNat ((37 : Field) / (37 : Field)) = 1 -#guard toField ((37 : Field)⁻¹) = ((37 : KoalaBear.Field)⁻¹) -#guard toField ((37 : Field) ^ (-3 : Int)) = ((37 : KoalaBear.Field) ^ (-3 : Int)) +#guard ((9 : Field) - 5).toNat = 4 +#guard ((5 : Field) - 9).toNat = KoalaBear.fieldSize - 4 +#guard (-(0 : Field)).toNat = 0 +#guard (-(1 : Field)).toNat = KoalaBear.fieldSize - 1 +#guard ((KoalaBear.fieldSize - 1 : Field) * (KoalaBear.fieldSize - 1 : Field)).toNat = 1 +#guard ((12345 : Field) * 12345).toNat = 152399025 +#guard ((37 : Field) ^ 0).toNat = 1 +#guard ((37 : Field) ^ 1).toNat = 37 +#guard ((123456789 : Field) ^ 17).toField = ((123456789 : KoalaBear.Field) ^ 17) +#guard ((123456789 : Field) ^ 255).toField = ((123456789 : KoalaBear.Field) ^ 255) +#guard ((0 : Field)⁻¹).toNat = 0 +#guard ((37 : Field)⁻¹ * 37).toNat = 1 +#guard ((37 : Field) / 37).toNat = 1 +#guard ((37 : Field)⁻¹).toField = ((37 : KoalaBear.Field)⁻¹) +#guard ((37 : Field) ^ (-3 : Int)).toField = ((37 : KoalaBear.Field) ^ (-3 : Int)) end KoalaBear.Fast