diff --git a/CompPoly.lean b/CompPoly.lean index 4c5463fe..5242903f 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -66,6 +66,8 @@ import CompPoly.Fields.BLS12_377 import CompPoly.Fields.BLS12_381 import CompPoly.Fields.BN254 import CompPoly.Fields.BabyBear +import CompPoly.Fields.BabyBear.Basic +import CompPoly.Fields.BabyBear.Fast import CompPoly.Fields.Basic import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT import CompPoly.Fields.Binary.AdditiveNTT.Algorithm @@ -103,6 +105,9 @@ import CompPoly.Fields.KoalaBear import CompPoly.Fields.KoalaBear.Basic import CompPoly.Fields.KoalaBear.Fast import CompPoly.Fields.Mersenne +import CompPoly.Fields.Montgomery.Basic +import CompPoly.Fields.Montgomery.Native32 +import CompPoly.Fields.Montgomery.Native32Field import CompPoly.Fields.PrattCertificate import CompPoly.Fields.Secp256k1 import CompPoly.LinearAlgebra.Dense diff --git a/CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean b/CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean index 50c2a460..e4ec9e87 100644 --- a/CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean +++ b/CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean @@ -127,10 +127,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 := @@ -143,7 +142,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.lean b/CompPoly/Fields/BabyBear.lean index 98d7abe8..bcc0bb89 100644 --- a/CompPoly/Fields/BabyBear.lean +++ b/CompPoly/Fields/BabyBear.lean @@ -4,252 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao, Valerii Huhnin -/ -import CompPoly.Fields.Basic -import CompPoly.Fields.PrattCertificate -import Mathlib.Algebra.Order.Ring.Star -import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots -/-! - # BabyBear Field `2^{31} - 2^{27} + 1` - - This is the field used by Risc Zero. --/ - -namespace BabyBear - -/-- The BabyBear field modulus, `2^31 - 2^27 + 1`. -/ -@[reducible] -def fieldSize : Nat := 2 ^ 31 - 2 ^ 27 + 1 - -/-- The BabyBear prime field as a `ZMod`. -/ -abbrev Field := ZMod fieldSize - -/-- The BabyBear modulus is prime. -/ -theorem is_prime : Nat.Prime fieldSize := by - unfold fieldSize - pratt - -/-! - ## Constants - - These are convenience constants for the BabyBear field: - - `pBits = 31` - - `twoAdicity = 27` with `fieldSize - 1 = 2^27 * 15` --/ - -/-- Bit width of the BabyBear modulus. -/ -@[reducible] -def pBits : Nat := 31 - -/-- The largest supported power-of-two root-of-unity exponent for BabyBear. -/ -@[reducible] -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) - -/-! - ## Two-adicity and roots of unity table - - We record the factorization of `fieldSize - 1` and provide a precomputed table - of `2^n`-th roots of unity for `0 ≤ n ≤ twoAdicity`. --/ - -/-- The factorization `fieldSize - 1 = 2^twoAdicity * 15`. -/ -lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15 := by - unfold fieldSize twoAdicity - decide +import CompPoly.Fields.BabyBear.Basic +import CompPoly.Fields.BabyBear.Fast /-! - A table of `2^n`-th roots of unity. The element at index `n` generates the - multiplicative subgroup of order `2^n`. +# BabyBear Field - The first entry n = 0 is 1. +Facade module for the BabyBear field. It re-exports the canonical `ZMod` model +from `CompPoly.Fields.BabyBear.Basic` and the native-word implementation from +`CompPoly.Fields.BabyBear.Fast`. -/ -/-- Precomputed generators for the BabyBear two-adic subgroups. -/ -def twoAdicGenerators : List Field := - [ - (0x1 : Field), - (0x78000000 : Field), - (0x67055C21 : Field), - (0x5EE99486 : Field), - (0xBB4C4E4 : Field), - (0x2D4CC4DA : Field), - (0x669D6090 : Field), - (0x17B56C64 : Field), - (0x67456167 : Field), - (0x688442F9 : Field), - (0x145E952D : Field), - (0x4FE61226 : Field), - (0x4C734715 : Field), - (0x11C33E2A : Field), - (0x62C3D2B1 : Field), - (0x77CAD399 : Field), - (0x54C131F4 : Field), - (0x4CABD6A6 : Field), - (0x5CF5713F : Field), - (0x3E9430E8 : Field), - (0xBA067A3 : Field), - (0x18ADC27D : Field), - (0x21FD55BC : Field), - (0x4B859B3D : Field), - (0x3BD57996 : Field), - (0x4483D85A : Field), - (0x3A26EEF8 : Field), - (0x1A427A41 : Field) - ] - -/-- The BabyBear two-adic generator table has one entry for each supported exponent. -/ -@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1 := by - decide - -/-- Consecutive BabyBear two-adic generators square to the previous generator. -/ -@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) : - twoAdicGenerators[idx.val + 1] ^ 2 = twoAdicGenerators[idx] := by - fin_cases idx - <;> simp [twoAdicGenerators] <;> decide - -/-- Consecutive BabyBear two-adic generators square to the previous generator. -/ -@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) : - haveI : idx + 1 < twoAdicGenerators.length := by simp [twoAdicGenerators_length, h] - twoAdicGenerators[idx + 1] ^ 2 = twoAdicGenerators[idx] := - twoAdicGenerators_succ_square_eq' ⟨idx, h⟩ - -/-- `twoAdicity` is maximal: `2^(twoAdicity+1)` does not divide `fieldSize - 1`. -/ -lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1) := by - decide - -/-- Repeated squaring: `sqChain g n = g ^ (2^n)`. - Does `n` multiplications instead of `2^n`, making it kernel-friendly. -/ -private def sqChain (g : Field) : Nat → Field - | 0 => g - | n + 1 => let h := sqChain g n; h * h - -/-- Repeated squaring agrees with exponentiation by a power of two. -/ -private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) : - sqChain g n = g ^ (2 ^ n) := by - induction n with - | zero => simp [sqChain] - | succ n ih => simp [sqChain, ih, pow_succ, pow_mul] - -/-- Repeated squaring walks backward through the precomputed two-adic generator table. -/ -private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) : - sqChain twoAdicGenerators[(⟨k + n, by omega⟩ : Fin (twoAdicity + 1))] n = - twoAdicGenerators[(⟨k, by omega⟩ : Fin (twoAdicity + 1))] := by - induction n generalizing k with - | zero => - simp [sqChain] - | succ n ih => - calc - sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : Fin (twoAdicity + 1))] - (n + 1) - = sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : - Fin (twoAdicity + 1))] n * - sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : - Fin (twoAdicity + 1))] n := by - simp [sqChain] - _ = twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] * - twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] := by - have hshift : - sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : - Fin (twoAdicity + 1))] n = - twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] := by - simpa [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using - (ih (k := k + 1) (by omega)) - exact congrArg (fun x ↦ x * x) hshift - _ = twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] ^ 2 := by - simp [pow_two] - _ = twoAdicGenerators[(⟨k, by omega⟩ : Fin (twoAdicity + 1))] := by - simpa [Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] - using (twoAdicGenerators_succ_square_eq k (by omega)) - -/-- Every nonzero index in the precomputed table is genuinely nontrivial. -/ -private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) : - twoAdicGenerators[n] ≠ (1 : Field) := by - fin_cases n <;> simp_all [twoAdicGenerators] <;> decide - -/-- The power `(twoAdicGenerators[bits])^(2^bits) = 1`. -/ -lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) : - twoAdicGenerators[bits] ^ (2 ^ (bits : Nat)) = 1 := by - rw [← sqChain_eq_pow_two_pow] - rcases bits with ⟨n, hn⟩ - have hshift : - sqChain twoAdicGenerators[(⟨n, hn⟩ : Fin (twoAdicity + 1))] n = - twoAdicGenerators[(⟨0, by omega⟩ : Fin (twoAdicity + 1))] := by - have hidx : (⟨0 + n, by omega⟩ : Fin (twoAdicity + 1)) = ⟨n, hn⟩ := by - ext - simp - convert sqChain_twoAdicGenerators_shift 0 n (by omega) using 2 - · exact (congrArg (fun i => twoAdicGenerators[i]) hidx).symm - simpa [twoAdicGenerators] using hshift - -/-- Helper: Fin-indexed version for computational verification of non-triviality. -/ -private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28) - (hm : m.val < n.val) : - twoAdicGenerators[n] ^ (2 ^ m.val) ≠ (1 : Field) := by - rw [← sqChain_eq_pow_two_pow] - let nMinus : Fin (twoAdicity + 1) := - ⟨n.val - m.val, lt_of_le_of_lt (Nat.sub_le _ _) n.isLt⟩ - have hshift : - sqChain twoAdicGenerators[n] m.val = twoAdicGenerators[nMinus] := by - have hn_le : n.val ≤ twoAdicity := by - simpa [twoAdicity] using Nat.le_of_lt_succ n.isLt - have hbound : (n.val - m.val) + m.val ≤ twoAdicity := by - simpa [Nat.sub_add_cancel (Nat.le_of_lt hm)] using hn_le - simpa [Nat.sub_add_cancel (Nat.le_of_lt hm)] using - (sqChain_twoAdicGenerators_shift (n.val - m.val) m.val hbound) - rw [hshift] - exact twoAdicGenerators_ne_one_of_pos nMinus (by - change 0 < n.val - m.val - exact Nat.sub_pos_of_lt hm) - -/-- If `m < bits`, then `(twoAdicGenerators[bits])^(2^m) ≠ 1`. -/ -lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt - {bits : Fin (twoAdicity + 1)} {m : Nat} (hm : m < bits) : - (twoAdicGenerators[bits]) ^ (2 ^ m) ≠ (1 : Field) := by - have hm_lt : m < 28 := Nat.lt_trans hm bits.isLt - exact twoAdicGenerators_pow_ne_one_aux bits ⟨m, hm_lt⟩ hm - -/-- The precomputed element at index `bits` is a primitive `2^bits`-th root of unity. -/ -lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) : - IsPrimitiveRoot (twoAdicGenerators[n]) (2 ^ (n : Nat)) := by - rw [IsPrimitiveRoot.iff_def] - rcases n with ⟨_ | k, hb⟩ - · simp [twoAdicGenerators] - · constructor - · exact twoAdicGenerators_pow_twoPow_eq_one ⟨k + 1, hb⟩ - · intro m hm - by_contra h - have hord := orderOf_eq_prime_pow - (twoAdicGenerators_pow_twoPow_ne_one_of_lt (bits := ⟨k + 1, hb⟩) (m := k) - (by simp)) - (twoAdicGenerators_pow_twoPow_eq_one ⟨k + 1, hb⟩) - have hdvd := orderOf_dvd_of_pow_eq_one hm - rw [hord] at hdvd - exact h hdvd - -/-- As a unit, the precomputed element is a member of `rootsOfUnity (2^bits)`. -/ -lemma twoAdicGenerator_unit_mem_rootsOfUnity - (bits : Fin (twoAdicity + 1)) (h : twoAdicGenerators[bits] ≠ 0) : - Units.mk0 (twoAdicGenerators[bits]) h ∈ rootsOfUnity (2 ^ (bits : Nat)) Field := by - rw [mem_rootsOfUnity] - rw [Units.ext_iff] - simp only [Units.val_pow_eq_pow_val, Units.val_mk0, Units.val_one] - exact twoAdicGenerators_pow_twoPow_eq_one bits - -/-- The order of `twoAdicGenerators[bits]` equals `2^bits`. -/ -lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : - orderOf (twoAdicGenerators[bits]) = 2 ^ (bits : Nat) := by - rcases bits with ⟨_ | n, hb⟩ - · simp [twoAdicGenerators, orderOf_one] - · exact orderOf_eq_prime_pow - (twoAdicGenerators_pow_twoPow_ne_one_of_lt (bits := ⟨n + 1, hb⟩) (m := n) - (by simp)) - (twoAdicGenerators_pow_twoPow_eq_one ⟨n + 1, hb⟩) - -end BabyBear diff --git a/CompPoly/Fields/BabyBear/Basic.lean b/CompPoly/Fields/BabyBear/Basic.lean new file mode 100644 index 00000000..757110fa --- /dev/null +++ b/CompPoly/Fields/BabyBear/Basic.lean @@ -0,0 +1,264 @@ +/- +Copyright (c) 2024 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Quang Dao, Valerii Huhnin +-/ + +import CompPoly.Fields.Basic +import CompPoly.Fields.PrattCertificate +import Mathlib.Algebra.Order.Ring.Star +import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots +import Mathlib.FieldTheory.Finite.Basic +/-! + # BabyBear Field `2^{31} - 2^{27} + 1` + + This is the field used by Risc Zero. +-/ + +namespace BabyBear + +/-- The BabyBear field modulus, `2^31 - 2^27 + 1`. -/ +@[reducible] +def fieldSize : Nat := 2 ^ 31 - 2 ^ 27 + 1 + +/-- The BabyBear prime field as a `ZMod`. -/ +abbrev Field := ZMod fieldSize + +/-- The BabyBear modulus is prime. -/ +theorem is_prime : Nat.Prime fieldSize := by + unfold fieldSize + pratt + +/-! + ## Constants + + These are convenience constants for the BabyBear field: + - `pBits = 31` + - `twoAdicity = 27` with `fieldSize - 1 = 2^27 * 15` +-/ + +/-- Bit width of the BabyBear modulus. -/ +@[reducible] +def pBits : Nat := 31 + +/-- The largest supported power-of-two root-of-unity exponent for BabyBear. -/ +@[reducible] +def twoAdicity : Nat := 27 + +instance : Fact (Nat.Prime fieldSize) := ⟨is_prime⟩ + +instance : NonBinaryField Field where + 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 + have hcard : Fintype.card Field = fieldSize := ZMod.card fieldSize + have h1 : a ^ (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 ^ (fieldSize - 2) = 1 := by + rw [← pow_succ']; show a ^ (fieldSize - 2 + 1) = 1 + have : fieldSize - 2 + 1 = fieldSize - 1 := by unfold fieldSize; omega + rw [this]; exact h1 + exact (eq_inv_of_mul_eq_one_left (by rwa [mul_comm])).symm + +/-! + ## Two-adicity and roots of unity table + + We record the factorization of `fieldSize - 1` and provide a precomputed table + of `2^n`-th roots of unity for `0 ≤ n ≤ twoAdicity`. +-/ + +/-- The factorization `fieldSize - 1 = 2^twoAdicity * 15`. -/ +lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15 := by + unfold fieldSize twoAdicity + decide + +/-! + A table of `2^n`-th roots of unity. The element at index `n` generates the + multiplicative subgroup of order `2^n`. + + The first entry n = 0 is 1. +-/ +/-- Precomputed generators for the BabyBear two-adic subgroups. -/ +def twoAdicGenerators : List Field := + [ + (0x1 : Field), + (0x78000000 : Field), + (0x67055C21 : Field), + (0x5EE99486 : Field), + (0xBB4C4E4 : Field), + (0x2D4CC4DA : Field), + (0x669D6090 : Field), + (0x17B56C64 : Field), + (0x67456167 : Field), + (0x688442F9 : Field), + (0x145E952D : Field), + (0x4FE61226 : Field), + (0x4C734715 : Field), + (0x11C33E2A : Field), + (0x62C3D2B1 : Field), + (0x77CAD399 : Field), + (0x54C131F4 : Field), + (0x4CABD6A6 : Field), + (0x5CF5713F : Field), + (0x3E9430E8 : Field), + (0xBA067A3 : Field), + (0x18ADC27D : Field), + (0x21FD55BC : Field), + (0x4B859B3D : Field), + (0x3BD57996 : Field), + (0x4483D85A : Field), + (0x3A26EEF8 : Field), + (0x1A427A41 : Field) + ] + +/-- The BabyBear two-adic generator table has one entry for each supported exponent. -/ +@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1 := by + decide + +/-- Consecutive BabyBear two-adic generators square to the previous generator. -/ +@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) : + twoAdicGenerators[idx.val + 1] ^ 2 = twoAdicGenerators[idx] := by + fin_cases idx + <;> simp [twoAdicGenerators] <;> decide + +/-- Consecutive BabyBear two-adic generators square to the previous generator. -/ +@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) : + haveI : idx + 1 < twoAdicGenerators.length := by simp [twoAdicGenerators_length, h] + twoAdicGenerators[idx + 1] ^ 2 = twoAdicGenerators[idx] := + twoAdicGenerators_succ_square_eq' ⟨idx, h⟩ + +/-- `twoAdicity` is maximal: `2^(twoAdicity+1)` does not divide `fieldSize - 1`. -/ +lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1) := by + decide + +/-- Repeated squaring: `sqChain g n = g ^ (2^n)`. + Does `n` multiplications instead of `2^n`, making it kernel-friendly. -/ +private def sqChain (g : Field) : Nat → Field + | 0 => g + | n + 1 => let h := sqChain g n; h * h + +/-- Repeated squaring agrees with exponentiation by a power of two. -/ +private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) : + sqChain g n = g ^ (2 ^ n) := by + induction n with + | zero => simp [sqChain] + | succ n ih => simp [sqChain, ih, pow_succ, pow_mul] + +/-- Repeated squaring walks backward through the precomputed two-adic generator table. -/ +private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) : + sqChain twoAdicGenerators[(⟨k + n, by omega⟩ : Fin (twoAdicity + 1))] n = + twoAdicGenerators[(⟨k, by omega⟩ : Fin (twoAdicity + 1))] := by + induction n generalizing k with + | zero => + simp [sqChain] + | succ n ih => + calc + sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : Fin (twoAdicity + 1))] + (n + 1) + = sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : + Fin (twoAdicity + 1))] n * + sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : + Fin (twoAdicity + 1))] n := by + simp [sqChain] + _ = twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] * + twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] := by + have hshift : + sqChain twoAdicGenerators[(⟨k + (n + 1), by omega⟩ : + Fin (twoAdicity + 1))] n = + twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] := by + simpa [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using + (ih (k := k + 1) (by omega)) + exact congrArg (fun x ↦ x * x) hshift + _ = twoAdicGenerators[(⟨k + 1, by omega⟩ : Fin (twoAdicity + 1))] ^ 2 := by + simp [pow_two] + _ = twoAdicGenerators[(⟨k, by omega⟩ : Fin (twoAdicity + 1))] := by + simpa [Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] + using (twoAdicGenerators_succ_square_eq k (by omega)) + +/-- Every nonzero index in the precomputed table is genuinely nontrivial. -/ +private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) : + twoAdicGenerators[n] ≠ (1 : Field) := by + fin_cases n <;> simp_all [twoAdicGenerators] <;> decide + +/-- The power `(twoAdicGenerators[bits])^(2^bits) = 1`. -/ +lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) : + twoAdicGenerators[bits] ^ (2 ^ (bits : Nat)) = 1 := by + rw [← sqChain_eq_pow_two_pow] + rcases bits with ⟨n, hn⟩ + have hshift : + sqChain twoAdicGenerators[(⟨n, hn⟩ : Fin (twoAdicity + 1))] n = + twoAdicGenerators[(⟨0, by omega⟩ : Fin (twoAdicity + 1))] := by + have hidx : (⟨0 + n, by omega⟩ : Fin (twoAdicity + 1)) = ⟨n, hn⟩ := by + ext + simp + convert sqChain_twoAdicGenerators_shift 0 n (by omega) using 2 + · exact (congrArg (fun i => twoAdicGenerators[i]) hidx).symm + simpa [twoAdicGenerators] using hshift + +/-- Helper: Fin-indexed version for computational verification of non-triviality. -/ +private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28) + (hm : m.val < n.val) : + twoAdicGenerators[n] ^ (2 ^ m.val) ≠ (1 : Field) := by + rw [← sqChain_eq_pow_two_pow] + let nMinus : Fin (twoAdicity + 1) := + ⟨n.val - m.val, lt_of_le_of_lt (Nat.sub_le _ _) n.isLt⟩ + have hshift : + sqChain twoAdicGenerators[n] m.val = twoAdicGenerators[nMinus] := by + have hn_le : n.val ≤ twoAdicity := by + simpa [twoAdicity] using Nat.le_of_lt_succ n.isLt + have hbound : (n.val - m.val) + m.val ≤ twoAdicity := by + simpa [Nat.sub_add_cancel (Nat.le_of_lt hm)] using hn_le + simpa [Nat.sub_add_cancel (Nat.le_of_lt hm)] using + (sqChain_twoAdicGenerators_shift (n.val - m.val) m.val hbound) + rw [hshift] + exact twoAdicGenerators_ne_one_of_pos nMinus (by + change 0 < n.val - m.val + exact Nat.sub_pos_of_lt hm) + +/-- If `m < bits`, then `(twoAdicGenerators[bits])^(2^m) ≠ 1`. -/ +lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt + {bits : Fin (twoAdicity + 1)} {m : Nat} (hm : m < bits) : + (twoAdicGenerators[bits]) ^ (2 ^ m) ≠ (1 : Field) := by + have hm_lt : m < 28 := Nat.lt_trans hm bits.isLt + exact twoAdicGenerators_pow_ne_one_aux bits ⟨m, hm_lt⟩ hm + +/-- The precomputed element at index `bits` is a primitive `2^bits`-th root of unity. -/ +lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) : + IsPrimitiveRoot (twoAdicGenerators[n]) (2 ^ (n : Nat)) := by + rw [IsPrimitiveRoot.iff_def] + rcases n with ⟨_ | k, hb⟩ + · simp [twoAdicGenerators] + · constructor + · exact twoAdicGenerators_pow_twoPow_eq_one ⟨k + 1, hb⟩ + · intro m hm + by_contra h + have hord := orderOf_eq_prime_pow + (twoAdicGenerators_pow_twoPow_ne_one_of_lt (bits := ⟨k + 1, hb⟩) (m := k) + (by simp)) + (twoAdicGenerators_pow_twoPow_eq_one ⟨k + 1, hb⟩) + have hdvd := orderOf_dvd_of_pow_eq_one hm + rw [hord] at hdvd + exact h hdvd + +/-- As a unit, the precomputed element is a member of `rootsOfUnity (2^bits)`. -/ +lemma twoAdicGenerator_unit_mem_rootsOfUnity + (bits : Fin (twoAdicity + 1)) (h : twoAdicGenerators[bits] ≠ 0) : + Units.mk0 (twoAdicGenerators[bits]) h ∈ rootsOfUnity (2 ^ (bits : Nat)) Field := by + rw [mem_rootsOfUnity] + rw [Units.ext_iff] + simp only [Units.val_pow_eq_pow_val, Units.val_mk0, Units.val_one] + exact twoAdicGenerators_pow_twoPow_eq_one bits + +/-- The order of `twoAdicGenerators[bits]` equals `2^bits`. -/ +lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : + orderOf (twoAdicGenerators[bits]) = 2 ^ (bits : Nat) := by + rcases bits with ⟨_ | n, hb⟩ + · simp [twoAdicGenerators, orderOf_one] + · exact orderOf_eq_prime_pow + (twoAdicGenerators_pow_twoPow_ne_one_of_lt (bits := ⟨n + 1, hb⟩) (m := n) + (by simp)) + (twoAdicGenerators_pow_twoPow_eq_one ⟨n + 1, hb⟩) + +end BabyBear diff --git a/CompPoly/Fields/BabyBear/Fast.lean b/CompPoly/Fields/BabyBear/Fast.lean new file mode 100644 index 00000000..20cb5efd --- /dev/null +++ b/CompPoly/Fields/BabyBear/Fast.lean @@ -0,0 +1,55 @@ +/- +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 + +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.Fast + +open Montgomery.Native32 (Mont32Field FastField) +open Montgomery.Native32.FastField + +/-! ## Parameters and carrier -/ + +/-- 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 + +/-- The fast native-word BabyBear field carrier, stored as a Montgomery residue. -/ +abbrev Field : Type := FastField BabyBear.fieldSize + +/-! ## Conversions -/ + +/-- Convert a 32-bit word into fast Montgomery representation. -/ +@[inline] +def ofUInt32 (x : UInt32) : Field := + Montgomery.Native32.FastField.ofUInt32 BabyBear.fieldSize x + +/-- Convert from the canonical `ZMod` BabyBear field into fast Montgomery form. -/ +@[inline] +def ofField (x : BabyBear.Field) : Field := + Montgomery.Native32.FastField.ofField x + +/-! ## Canonical bridge -/ + +/-- Ring equivalence between the fast Montgomery representation and canonical `BabyBear.Field`. -/ +def ringEquiv : Field ≃+* BabyBear.Field := + Montgomery.Native32.ringEquiv BabyBear.fieldSize + +end BabyBear.Fast diff --git a/CompPoly/Fields/KoalaBear/Basic.lean b/CompPoly/Fields/KoalaBear/Basic.lean index 8f09580e..4f2ea736 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 @@ -293,13 +292,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 e35308d0..8c1983c9 100644 --- a/CompPoly/Fields/KoalaBear/Fast.lean +++ b/CompPoly/Fields/KoalaBear/Fast.lean @@ -5,1270 +5,88 @@ Authors: Valerii Huhnin -/ import CompPoly.Fields.KoalaBear.Basic -import Mathlib.Algebra.Field.TransferInstance -import Mathlib.Data.Nat.ModEq +import CompPoly.Fields.Montgomery.Native32Field /-! -# Fast KoalaBear Field Operations +# Fast KoalaBear Field -This module provides a native-word implementation of KoalaBear arithmetic as a sidecar -to the canonical `KoalaBear.Field := ZMod KoalaBear.fieldSize` model. - -Fast field values are stored as Montgomery `UInt32` residues below `KoalaBear.fieldSize`, -representing `x * 2^32` modulo the KoalaBear prime. Addition, subtraction, and -negation operate directly on Montgomery words; multiplication uses Montgomery -reduction on a native `UInt64` product. +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 - -/-- KoalaBear modulus as a native word. -/ -def modulus : UInt32 := 0x7F000001 - -/-- KoalaBear modulus as a 64-bit word for modular reduction. -/ -def modulus64 : UInt64 := 0x7F000001 +namespace KoalaBear.Fast -/-- `2^32 mod KoalaBear.fieldSize`. This is the Montgomery representation of one. -/ -def rModModulus : UInt32 := 0x01FFFFFE +open Montgomery.Native32 (Mont32Field FastField) +open Montgomery.Native32.FastField -/-- `(2^32)^2 mod KoalaBear.fieldSize`, used to enter Montgomery representation. -/ -def r2ModModulus : UInt32 := 0x17F7EFE4 +/-! ## Parameters and carrier -/ -/-- `-KoalaBear.fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ -def montgomeryNegInv : UInt32 := 0x7EFFFFFF +/-- 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 /-- The fast native-word KoalaBear field carrier, stored as a Montgomery residue. -/ -abbrev Field : Type := { x : UInt32 // x.toNat < KoalaBear.fieldSize } - -instance : DecidableEq Field := inferInstance - -/-- The raw Montgomery word backing a fast KoalaBear element. -/ -@[inline] -def raw (x : Field) : UInt32 := x.val - -/-- 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 - -private theorem fieldSize_pos : 0 < KoalaBear.fieldSize := by - decide - -private theorem fieldSize_lt_uint32Size : KoalaBear.fieldSize < UInt32.size := by - decide - -private theorem fieldSize_add_fieldSize_lt_two64 : - KoalaBear.fieldSize + KoalaBear.fieldSize < 2 ^ 64 := by - decide - -private theorem fieldSize_add_fieldSize_lt_uint32Size : - KoalaBear.fieldSize + KoalaBear.fieldSize < UInt32.size := by - decide - -private theorem fieldSize_mul_fieldSize_lt_two64 : - KoalaBear.fieldSize * KoalaBear.fieldSize < 2 ^ 64 := by - decide - -private theorem uint32Size_lt_three_fieldSize : - UInt32.size < KoalaBear.fieldSize + KoalaBear.fieldSize + KoalaBear.fieldSize := by - decide - -private theorem fieldSize_mul_uint32Size_lt_two64 : - KoalaBear.fieldSize * UInt32.size < 2 ^ 64 := by - decide - -private theorem two_fieldSize_mul_uint32Size_lt_two64 : - 2 * KoalaBear.fieldSize * UInt32.size < 2 ^ 64 := by - decide - -private theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < KoalaBear.fieldSize := by - decide - -private theorem rModModulus_lt_fieldSize : rModModulus.toNat < KoalaBear.fieldSize := by - decide - -private theorem rModModulus_cast : - (rModModulus.toNat : KoalaBear.Field) = (UInt32.size : KoalaBear.Field) := by - decide - -private theorem r2ModModulus_cast : - (r2ModModulus.toNat : KoalaBear.Field) = (UInt32.size : KoalaBear.Field) ^ 2 := by - decide - -private theorem uint32Size_ne_zero_in_field : - (UInt32.size : KoalaBear.Field) ≠ 0 := by - decide - -private theorem montgomery_sum_dvd (x : Nat) : - UInt32.size ∣ - x + ((x % UInt32.size * montgomeryNegInv.toNat) % UInt32.size) * KoalaBear.fieldSize := by - rw [← Nat.modEq_zero_iff_dvd] - have hx : x ≡ x % UInt32.size [MOD UInt32.size] := - (Nat.mod_modEq x UInt32.size).symm - have hm : - ((x % UInt32.size * montgomeryNegInv.toNat) % UInt32.size) * KoalaBear.fieldSize ≡ - (x % UInt32.size) * (UInt32.size - 1) [MOD UInt32.size] := by - have hmi : - (x % UInt32.size * montgomeryNegInv.toNat) % UInt32.size ≡ - x % UInt32.size * montgomeryNegInv.toNat [MOD UInt32.size] := - Nat.mod_modEq _ _ - have hp : montgomeryNegInv.toNat * KoalaBear.fieldSize ≡ UInt32.size - 1 - [MOD UInt32.size] := by - decide - calc - ((x % UInt32.size * montgomeryNegInv.toNat) % UInt32.size) * KoalaBear.fieldSize - ≡ (x % UInt32.size * montgomeryNegInv.toNat) * KoalaBear.fieldSize - [MOD UInt32.size] := hmi.mul_right _ - _ = x % UInt32.size * (montgomeryNegInv.toNat * KoalaBear.fieldSize) := by ring - _ ≡ x % UInt32.size * (UInt32.size - 1) [MOD UInt32.size] := hp.mul_left _ - calc - x + ((x % UInt32.size * montgomeryNegInv.toNat) % UInt32.size) * KoalaBear.fieldSize - ≡ x % UInt32.size + x % UInt32.size * (UInt32.size - 1) [MOD UInt32.size] := - hx.add hm - _ = x % UInt32.size * UInt32.size := by - rw [add_comm, ← Nat.mul_succ] - have hsucc : (UInt32.size - 1).succ = UInt32.size := by decide - rw [hsucc] - _ ≡ 0 [MOD UInt32.size] := by - rw [Nat.modEq_zero_iff_dvd] - exact ⟨x % UInt32.size, by rw [mul_comm]⟩ - -/-- Nat-level Montgomery reduction used to specify and prove the native-word reducer. -/ -private def montgomeryReduceNat (x : Nat) : Nat := - let m := (x % UInt32.size * montgomeryNegInv.toNat) % UInt32.size - let u := (x + m * KoalaBear.fieldSize) / UInt32.size - if u < KoalaBear.fieldSize then u else u - KoalaBear.fieldSize - -private theorem montgomeryReduceNat_lt (x : Nat) - (h : x < KoalaBear.fieldSize * UInt32.size) : - montgomeryReduceNat x < KoalaBear.fieldSize := by - let m := x % UInt32.size * montgomeryNegInv.toNat % UInt32.size - let u := (x + m * KoalaBear.fieldSize) / UInt32.size - have hm_lt : m < UInt32.size := Nat.mod_lt _ (by decide) - have hu_lt : u < 2 * KoalaBear.fieldSize := by - rw [Nat.div_lt_iff_lt_mul] - · have hprod_lt : m * KoalaBear.fieldSize < UInt32.size * KoalaBear.fieldSize := by - exact Nat.mul_lt_mul_of_pos_right hm_lt fieldSize_pos - have hprod_lt' : m * KoalaBear.fieldSize < KoalaBear.fieldSize * UInt32.size := by - simpa [Nat.mul_comm] using hprod_lt - nlinarith - · decide - by_cases hu : u < KoalaBear.fieldSize - · unfold montgomeryReduceNat - change (if u < KoalaBear.fieldSize then u else u - KoalaBear.fieldSize) < - KoalaBear.fieldSize - rw [if_pos hu] - exact hu - · have hsub : u - KoalaBear.fieldSize < KoalaBear.fieldSize := by omega - unfold montgomeryReduceNat - change (if u < KoalaBear.fieldSize then u else u - KoalaBear.fieldSize) < - KoalaBear.fieldSize - rw [if_neg hu] - exact hsub - -private theorem montgomeryReduceNat_cast (x : Nat) : - (montgomeryReduceNat x : KoalaBear.Field) = - (x : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := by - let m := x % UInt32.size * montgomeryNegInv.toNat % UInt32.size - let u := (x + m * KoalaBear.fieldSize) / UInt32.size - have hdiv : UInt32.size ∣ x + m * KoalaBear.fieldSize := by - simpa [m] using montgomery_sum_dvd x - have hu_mul : u * UInt32.size = x + m * KoalaBear.fieldSize := by - exact Nat.div_mul_cancel hdiv - have hcast_mul : (u : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) = - (x : KoalaBear.Field) := by - rw [← Nat.cast_mul, hu_mul, Nat.cast_add, Nat.cast_mul] - simp - have hR := uint32Size_ne_zero_in_field - by_cases hu : u < KoalaBear.fieldSize - · have hmain : - (u : KoalaBear.Field) = (x : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ := by - calc - (u : KoalaBear.Field) = - (u : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ := by - rw [mul_assoc, mul_inv_cancel₀ hR, mul_one] - _ = (x : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := by - rw [hcast_mul] - dsimp only [montgomeryReduceNat] - rw [if_pos hu] - exact hmain - · have hfield : - ((u - KoalaBear.fieldSize : Nat) : KoalaBear.Field) = (u : KoalaBear.Field) := by - rw [Nat.cast_sub (Nat.le_of_not_gt hu)] - simp - have hmain : - ((u - KoalaBear.fieldSize : Nat) : KoalaBear.Field) = - (x : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := by - rw [hfield] - calc - (u : KoalaBear.Field) = - (u : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ := by - rw [mul_assoc, mul_inv_cancel₀ hR, mul_one] - _ = (x : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := by - rw [hcast_mul] - dsimp only [montgomeryReduceNat] - rw [if_neg hu] - exact hmain +abbrev Field : Type := FastField KoalaBear.fieldSize -private theorem montgomeryQuotient_cast (x : Nat) : - (let m := x % UInt32.size * montgomeryNegInv.toNat % UInt32.size - let u := (x + m * KoalaBear.fieldSize) / UInt32.size - (u : KoalaBear.Field)) = - (x : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := by - let m := x % UInt32.size * montgomeryNegInv.toNat % UInt32.size - let u := (x + m * KoalaBear.fieldSize) / UInt32.size - have hmr := montgomeryReduceNat_cast x - unfold montgomeryReduceNat at hmr - change (u : KoalaBear.Field) = - (x : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - by_cases hu : u < KoalaBear.fieldSize - · simpa only [m, u, hu, if_true] using hmr - · have hfield : ((u - KoalaBear.fieldSize : Nat) : KoalaBear.Field) = - (u : KoalaBear.Field) := by - rw [Nat.cast_sub (Nat.le_of_not_gt hu)] - simp - rw [← hfield] - simpa only [m, u, hu, if_false] using hmr - -private theorem montgomery_u_eq_nat (x : UInt64) - (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : - (let m : UInt32 := x.toUInt32 * montgomeryNegInv - (((x + m.toUInt64 * modulus64) >>> 32).toUInt32).toNat) = - (x.toNat + ((x.toNat % UInt32.size * montgomeryNegInv.toNat) % UInt32.size) * - KoalaBear.fieldSize) / UInt32.size := by - simp only [UInt64.toNat_shiftRight, UInt64.toNat_toUInt32, UInt64.toNat_add, - UInt64.toNat_mul, UInt32.toNat_toUInt64, UInt32.toNat_mul, UInt64.toNat_ofNat, - modulus64_toNat, Nat.shiftRight_eq_div_pow] - norm_num [KoalaBear.fieldSize, UInt32.size] at h ⊢ - let mNat := x.toNat * montgomeryNegInv.toNat % 4294967296 - have hm_lt : mNat < 4294967296 := Nat.mod_lt _ (by decide) - have hsum_lt : x.toNat + mNat * 2130706433 < 18446744073709551616 := by - have hprod_lt : mNat * 2130706433 < 2130706433 * 4294967296 := by nlinarith - nlinarith - change ((x.toNat + mNat * 2130706433) % 18446744073709551616 / 4294967296) % - 4294967296 = (x.toNat + mNat * 2130706433) / 4294967296 - rw [Nat.mod_eq_of_lt hsum_lt] - rw [Nat.mod_eq_of_lt] - rw [Nat.div_lt_iff_lt_mul] - · exact hsum_lt - · decide - -private theorem montgomery_u_lt_two_fieldSize (x : UInt64) - (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : - (let m : UInt32 := x.toUInt32 * montgomeryNegInv - (((x + m.toUInt64 * modulus64) >>> 32).toUInt32).toNat) < - 2 * KoalaBear.fieldSize := by - rw [montgomery_u_eq_nat x h] - let mNat := x.toNat % UInt32.size * montgomeryNegInv.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 * KoalaBear.fieldSize < UInt32.size * KoalaBear.fieldSize := by - exact Nat.mul_lt_mul_of_pos_right hm_lt fieldSize_pos - have hprod_lt' : - mNat * KoalaBear.fieldSize < KoalaBear.fieldSize * UInt32.size := by - simpa [Nat.mul_comm] using hprod_lt - change x.toNat + mNat * KoalaBear.fieldSize < 2 * KoalaBear.fieldSize * UInt32.size - nlinarith - · decide - -/-- Reduce a native word known to be below twice the KoalaBear prime. -/ -@[inline] -private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 := - if x < modulus then x else x - modulus - -private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) - (h : x.toNat < 2 * KoalaBear.fieldSize) : - (reduceUInt32Lt2ModulusRaw x).toNat < KoalaBear.fieldSize := by - unfold reduceUInt32Lt2ModulusRaw - by_cases hx : x < modulus - · rw [if_pos hx] - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact hx - · rw [if_neg hx] - have hmod_le_x : modulus ≤ x := by - rw [UInt32.le_iff_toNat_le, modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact Nat.le_of_not_gt hx - rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, modulus_toNat] - omega - -/-- Reduce a native word known to be below twice the KoalaBear prime. -/ -@[inline] -private def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * KoalaBear.fieldSize) : - Field := - ⟨reduceUInt32Lt2ModulusRaw x, reduceUInt32Lt2ModulusRaw_lt x h⟩ - -private theorem reduceUInt32Lt2Modulus_cast (x : UInt32) - (h : x.toNat < 2 * KoalaBear.fieldSize) : - ((reduceUInt32Lt2Modulus x h).val.toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) := by - change ((reduceUInt32Lt2ModulusRaw x).toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) - unfold reduceUInt32Lt2ModulusRaw - by_cases hx : x < modulus - · rw [if_pos hx] - · have hmod_le_x : modulus ≤ x := by - rw [UInt32.le_iff_toNat_le, modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact Nat.le_of_not_gt hx - rw [if_neg hx] - rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, modulus_toNat] - rw [Nat.cast_sub (by - rw [UInt32.le_iff_toNat_le, modulus_toNat] at hmod_le_x - exact hmod_le_x)] - simp - -private theorem reduceUInt32Lt2Modulus_val_eq_nat (x : UInt32) - (h : x.toNat < 2 * KoalaBear.fieldSize) : - (reduceUInt32Lt2Modulus x h).val.toNat = montgomeryReduceNat (x.toNat * UInt32.size) := by - change (reduceUInt32Lt2ModulusRaw x).toNat = montgomeryReduceNat (x.toNat * UInt32.size) - unfold reduceUInt32Lt2ModulusRaw montgomeryReduceNat - have hm_zero : - (x.toNat * UInt32.size % UInt32.size * montgomeryNegInv.toNat) % UInt32.size = 0 := by - simp - rw [hm_zero] - simp only [zero_mul, add_zero] - have hdiv : x.toNat * UInt32.size / UInt32.size = x.toNat := by - rw [Nat.mul_div_cancel _ (by decide : 0 < UInt32.size)] - rw [hdiv] - by_cases hx : x < modulus - · rw [if_pos] - · have hxNat : x.toNat < KoalaBear.fieldSize := by - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact hx - rw [if_pos hxNat] - · have hxNat : x.toNat < KoalaBear.fieldSize := by - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact hx - exact hxNat - · rw [if_neg] - · have hmod_le_x : modulus ≤ x := by - rw [UInt32.le_iff_toNat_le, modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact Nat.le_of_not_gt hx - have hxNat : ¬x.toNat < KoalaBear.fieldSize := by - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact hx - rw [if_neg hxNat] - rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, modulus_toNat] - · have hxNat : ¬x.toNat < KoalaBear.fieldSize := by - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact hx - exact hxNat - -/-- Reduce a native word below `2^32` modulo the KoalaBear prime. -/ -@[inline] -private def reduceUInt32 (x : UInt32) : Field := - if hx : x < modulus then - ⟨x, by - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact hx⟩ - else - let y := x - modulus - if hy : y < modulus then - ⟨y, by - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hy - exact hy⟩ - else - ⟨y - modulus, by - have hmod_le_x : modulus ≤ x := by - rw [UInt32.le_iff_toNat_le, modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hx - exact Nat.le_of_not_gt hx - have hy_eq : y.toNat = x.toNat - KoalaBear.fieldSize := by - change (x - modulus).toNat = x.toNat - KoalaBear.fieldSize - rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, modulus_toNat] - have hmod_le_y : modulus ≤ y := by - rw [UInt32.le_iff_toNat_le, modulus_toNat] - rw [UInt32.lt_iff_toNat_lt, modulus_toNat] at hy - exact Nat.le_of_not_gt hy - rw [UInt32.toNat_sub_of_le _ _ hmod_le_y, modulus_toNat, hy_eq] - have hx_lt := UInt32.toNat_lt_size x - have hthree := uint32Size_lt_three_fieldSize - omega⟩ - -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -private def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 := - let m : UInt32 := x.toUInt32 * montgomeryNegInv - let u : UInt32 := ((x + m.toUInt64 * modulus64) >>> 32).toUInt32 - reduceUInt32Lt2ModulusRaw u - -private theorem montgomeryReduceBoundedRaw_lt (x : UInt64) - (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : - (montgomeryReduceBoundedRaw x).toNat < KoalaBear.fieldSize := by - unfold montgomeryReduceBoundedRaw - exact reduceUInt32Lt2ModulusRaw_lt _ - (montgomery_u_lt_two_fieldSize x h) - -/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ -@[inline] -private def montgomeryReduceBounded (x : UInt64) - (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : Field := - ⟨montgomeryReduceBoundedRaw x, montgomeryReduceBoundedRaw_lt x h⟩ - -private 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)⁻¹ := by - change ((montgomeryReduceBoundedRaw x).toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - unfold montgomeryReduceBoundedRaw - let m : UInt32 := x.toUInt32 * montgomeryNegInv - let u : UInt32 := ((x + m.toUInt64 * modulus64) >>> 32).toUInt32 - change ((reduceUInt32Lt2ModulusRaw u).toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - have hred := reduceUInt32Lt2Modulus_cast u (montgomery_u_lt_two_fieldSize x h) - change ((reduceUInt32Lt2ModulusRaw u).toNat : KoalaBear.Field) = - (u.toNat : KoalaBear.Field) at hred - rw [hred] - change (u.toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - rw [show u.toNat = - (x.toNat + ((x.toNat % UInt32.size * montgomeryNegInv.toNat) % UInt32.size) * - KoalaBear.fieldSize) / UInt32.size by - exact montgomery_u_eq_nat x h] - exact montgomeryQuotient_cast x.toNat - -/-- Montgomery reduction of a 64-bit word. Hot bounded callers use `montgomeryReduceBounded`. -/ -@[inline] -def montgomeryReduce (x : UInt64) : Field := - let m : UInt32 := x.toUInt32 * montgomeryNegInv - let u : UInt32 := ((x + m.toUInt64 * modulus64) >>> 32).toUInt32 - reduceUInt32 u - -/-- Build a fast element from a canonical natural representative. -/ -@[inline] -def ofCanonicalNat (n : Nat) (_h : n < KoalaBear.fieldSize) : Field := - montgomeryReduceBounded (UInt64.ofNat n * 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 fieldSize_lt_uint32Size (by decide)) - rw [hnmod] - have hprod : n * r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [r2ModModulus_lt_fieldSize, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [r2ModModulus_lt_fieldSize]) - -/-- Reduce a `UInt64` modulo the KoalaBear prime and return a Montgomery fast element. -/ -@[inline] -def reduceUInt64 (x : UInt64) : Field := - let y := x % modulus64 - montgomeryReduceBounded (y * r2ModModulus.toUInt64) (by - rw [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hy_lt : (x % modulus64).toNat < KoalaBear.fieldSize := by - rw [UInt64.toNat_mod, modulus64_toNat] - exact Nat.mod_lt _ fieldSize_pos - have hprod : (x % modulus64).toNat * r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [hy_lt, r2ModModulus_lt_fieldSize, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [r2ModModulus_lt_fieldSize]) - -/-- The zero fast KoalaBear element. -/ -def zero : Field := ⟨0, by decide⟩ - -/-- The one fast KoalaBear element. -/ -def one : Field := ⟨rModModulus, by decide⟩ - -/-- Convert a natural number into fast Montgomery representation. -/ -@[inline] -def ofNat (n : Nat) : Field := - ofCanonicalNat (n % KoalaBear.fieldSize) (Nat.mod_lt _ fieldSize_pos) +/-! ## Conversions -/ /-- Convert a 32-bit word into fast Montgomery representation. -/ @[inline] def ofUInt32 (x : UInt32) : Field := - reduceUInt64 x.toUInt64 + Montgomery.Native32.FastField.ofUInt32 KoalaBear.fieldSize x /-- Convert from the canonical `ZMod` KoalaBear field into fast Montgomery form. -/ @[inline] def ofField (x : KoalaBear.Field) : Field := - ofCanonicalNat x.val (ZMod.val_lt x) - -/-- Convert an integer into fast Montgomery representation. -/ -@[inline] -def ofInt (n : Int) : Field := - ofField (n : KoalaBear.Field) - -/-- Convert a fast element to its canonical native-word representative. -/ -@[inline] -def toCanonicalUInt32 (x : Field) : UInt32 := - raw (montgomeryReduceBounded x.val.toUInt64 (by - rw [UInt32.toNat_toUInt64] - nlinarith [x.property, fieldSize_pos])) - -/-- Convert a fast KoalaBear element to its canonical natural representative. -/ -@[inline] -def toNat (x : Field) : Nat := - (toCanonicalUInt32 x).toNat - -/-- Convert a fast KoalaBear element to the canonical `ZMod` KoalaBear field. -/ -@[inline] -def toField (x : Field) : KoalaBear.Field := - (toNat x : KoalaBear.Field) - -private theorem toNat_lt_fieldSize (x : Field) : toNat x < KoalaBear.fieldSize := by - unfold toNat toCanonicalUInt32 raw - change (montgomeryReduceBoundedRaw x.val.toUInt64).toNat < KoalaBear.fieldSize - exact montgomeryReduceBoundedRaw_lt x.val.toUInt64 (by - rw [UInt32.toNat_toUInt64] - nlinarith [x.property, fieldSize_pos]) - -private theorem toField_eq_raw_mul_inv (x : Field) : - toField x = - (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := by - unfold toField toNat toCanonicalUInt32 raw - have hred := montgomeryReduceBounded_cast x.val.toUInt64 (by - rw [UInt32.toNat_toUInt64] - nlinarith [x.property, fieldSize_pos]) - change ((montgomeryReduceBoundedRaw x.val.toUInt64).toNat : KoalaBear.Field) = - (x.val.toUInt64.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ at hred - change ((montgomeryReduceBoundedRaw x.val.toUInt64).toNat : KoalaBear.Field) = - (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - rw [hred] - rw [UInt32.toNat_toUInt64] - -private theorem raw_cast_eq_toField_mul (x : Field) : - (x.val.toNat : KoalaBear.Field) = - toField x * (UInt32.size : KoalaBear.Field) := by - rw [toField_eq_raw_mul_inv] - rw [mul_assoc] - rw [inv_mul_cancel₀ uint32Size_ne_zero_in_field] - rw [mul_one] - -private 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 := by - rw [ZMod.natCast_eq_natCast_iff] at h - exact Nat.ModEq.eq_of_lt_of_lt h ha hb - -private theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < KoalaBear.fieldSize) : - ((ofCanonicalNat n h).val.toNat : KoalaBear.Field) = - (n : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) := by - unfold ofCanonicalNat - have hred := montgomeryReduceBounded_cast - (UInt64.ofNat n * 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 fieldSize_lt_uint32Size (by decide)) - rw [hnmod] - have hprod : n * r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [r2ModModulus_lt_fieldSize, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [r2ModModulus_lt_fieldSize]) - change ((montgomeryReduceBoundedRaw - (UInt64.ofNat n * r2ModModulus.toUInt64)).toNat : KoalaBear.Field) = - ((UInt64.ofNat n * r2ModModulus.toUInt64).toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ at hred - change ((montgomeryReduceBoundedRaw - (UInt64.ofNat n * r2ModModulus.toUInt64)).toNat : KoalaBear.Field) = - (n : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) - 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 fieldSize_lt_uint32Size (by decide)) - rw [hnmod] - have hprod : n * r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [r2ModModulus_lt_fieldSize, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - rw [Nat.cast_mul, r2ModModulus_cast] - rw [pow_two] - rw [mul_assoc (n : KoalaBear.Field) ((UInt32.size : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)) ((UInt32.size : KoalaBear.Field)⁻¹)] - rw [mul_assoc (UInt32.size : KoalaBear.Field) (UInt32.size : KoalaBear.Field) - ((UInt32.size : KoalaBear.Field)⁻¹)] - rw [mul_inv_cancel₀ uint32Size_ne_zero_in_field] - rw [mul_one] + Montgomery.Native32.FastField.ofField x -private theorem toField_ofCanonicalNat_aux (n : Nat) (h : n < KoalaBear.fieldSize) : - toField (ofCanonicalNat n h) = (n : KoalaBear.Field) := by - rw [toField_eq_raw_mul_inv, ofCanonicalNat_raw_cast] - rw [mul_assoc] - rw [mul_inv_cancel₀ uint32Size_ne_zero_in_field] - rw [mul_one] - -private theorem reduceUInt64_raw_cast (x : UInt64) : - ((reduceUInt64 x).val.toNat : KoalaBear.Field) = - (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) := by - unfold reduceUInt64 - let y := x % modulus64 - have hred := montgomeryReduceBounded_cast (y * r2ModModulus.toUInt64) (by - rw [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hy_lt : y.toNat < KoalaBear.fieldSize := by - rw [show y = x % modulus64 by rfl, UInt64.toNat_mod, modulus64_toNat] - exact Nat.mod_lt _ fieldSize_pos - have hprod : y.toNat * r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [hy_lt, r2ModModulus_lt_fieldSize, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [r2ModModulus_lt_fieldSize]) - change ((montgomeryReduceBoundedRaw (y * r2ModModulus.toUInt64)).toNat : - KoalaBear.Field) = - ((y * r2ModModulus.toUInt64).toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ at hred - change ((montgomeryReduceBoundedRaw (y * r2ModModulus.toUInt64)).toNat : - KoalaBear.Field) = - (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) - rw [hred] - simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hy_lt : y.toNat < KoalaBear.fieldSize := by - rw [show y = x % modulus64 by rfl, UInt64.toNat_mod, modulus64_toNat] - exact Nat.mod_lt _ fieldSize_pos - have hprod : y.toNat * r2ModModulus.toNat < 2 ^ 64 := by - nlinarith [hy_lt, r2ModModulus_lt_fieldSize, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - have hy_cast : (y.toNat : KoalaBear.Field) = (x.toNat : KoalaBear.Field) := by - rw [show y = x % modulus64 by rfl, UInt64.toNat_mod, modulus64_toNat] - rw [ZMod.natCast_eq_natCast_iff] - exact Nat.mod_modEq _ _ - rw [Nat.cast_mul, r2ModModulus_cast, hy_cast] - rw [pow_two] - rw [mul_assoc (x.toNat : KoalaBear.Field) ((UInt32.size : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)) ((UInt32.size : KoalaBear.Field)⁻¹)] - rw [mul_assoc (UInt32.size : KoalaBear.Field) (UInt32.size : KoalaBear.Field) - ((UInt32.size : KoalaBear.Field)⁻¹)] - rw [mul_inv_cancel₀ uint32Size_ne_zero_in_field] - rw [mul_one] - -/-- 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 := by - exact nat_eq_of_field_eq (toNat_lt_fieldSize _) h (toField_ofCanonicalNat_aux 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) := by - exact toField_ofCanonicalNat_aux 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 := by - apply nat_eq_of_field_eq (toNat_lt_fieldSize _) (Nat.mod_lt _ fieldSize_pos) - change toField (reduceUInt64 x) = ((x.toNat % KoalaBear.fieldSize : Nat) : KoalaBear.Field) - rw [toField_eq_raw_mul_inv, reduceUInt64_raw_cast] - rw [mul_assoc] - rw [mul_inv_cancel₀ uint32Size_ne_zero_in_field] - rw [mul_one] - rw [ZMod.natCast_eq_natCast_iff] - exact (Nat.mod_modEq _ _).symm - -/-- 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) := by - rw [toField_eq_raw_mul_inv, reduceUInt64_raw_cast] - rw [mul_assoc] - rw [mul_inv_cancel₀ uint32Size_ne_zero_in_field] - rw [mul_one] - -/-- Fast modular addition in Montgomery form. -/ -@[inline] -def add (x y : Field) : Field := - reduceUInt32Lt2Modulus (x.val + y.val) (by - rw [UInt32.toNat_add] - exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) (by omega)) - -/-- Fast modular negation in Montgomery form. -/ -@[inline] -def neg (x : Field) : Field := - if hx : x.val = 0 then - zero - else - ⟨modulus - x.val, by - have hle : x.val ≤ modulus := by - rw [UInt32.le_iff_toNat_le, modulus_toNat] - exact Nat.le_of_lt x.property - rw [UInt32.toNat_sub_of_le _ _ hle, 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 - omega⟩ - -/-- Fast modular subtraction in Montgomery form. -/ -@[inline] -def sub (x y : Field) : Field := - if hyx : y.val ≤ x.val then - ⟨x.val - y.val, by - rw [UInt32.toNat_sub_of_le _ _ hyx] - omega⟩ - else - ⟨x.val + modulus - y.val, by - have hsum_lt : x.val.toNat + KoalaBear.fieldSize < UInt32.size := by - have htwo := fieldSize_add_fieldSize_lt_uint32Size - omega - have hsum_eq : (x.val + modulus).toNat = x.val.toNat + KoalaBear.fieldSize := by - rw [UInt32.toNat_add, modulus_toNat, Nat.mod_eq_of_lt hsum_lt] - have hyle : y.val ≤ x.val + modulus := by - rw [UInt32.le_iff_toNat_le, hsum_eq] - 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 - omega⟩ - -/-- Fast modular multiplication in Montgomery form. -/ -@[inline] -def mul (x y : Field) : Field := - montgomeryReduceBounded (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, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [x.property, y.property, fieldSize_lt_uint32Size, fieldSize_pos]) - -/-- Fast squaring. -/ -@[inline] -def square (x : Field) : Field := - mul x x - -/-- Exponentiation over the fast representation using repeated squaring. -/ -@[inline] -def pow (x : Field) (n : Nat) : Field := - @npowBinRec Field ⟨one⟩ ⟨mul⟩ n x - -/-- Fermat exponent used for inversion in the KoalaBear prime field. -/ -def invExponent : Nat := KoalaBear.fieldSize - 2 - -/-- Four squarings followed by multiplication by the next 4-bit exponent digit. -/ -@[inline] -private def shift4Mul (acc digit : Field) : Field := - mul (square (square (square (square acc)))) digit - -/-- Inversion in Montgomery form by a fixed 4-bit Fermat chain. -/ -@[inline] -def inv (x : Field) : Field := - let x2 := square x - let x3 := mul x2 x - let x5 := mul x3 x2 - let x7 := mul x5 x2 - let x14 := square x7 - let x15 := mul x14 x - let acc := shift4Mul x7 x14 - let acc := shift4Mul acc x15 - let acc := shift4Mul acc x15 - let acc := shift4Mul acc x15 - let acc := shift4Mul acc x15 - let acc := shift4Mul acc x15 - shift4Mul acc x15 - -/-- Division through inversion and fast multiplication. -/ -@[inline] -def div (x y : Field) : Field := - mul x (inv y) - -instance instZeroField : Zero Field where - zero := zero - -instance instOneField : One Field where - one := one - -instance instAddField : Add Field where - add := add - -instance instNegField : Neg Field where - neg := neg - -instance instSubField : Sub Field where - sub := sub - -instance instMulField : Mul Field where - mul := mul - -instance instInvField : Inv Field where - inv := inv - -instance instDivField : Div Field where - div := div - -instance instNatCastField : NatCast Field where - natCast := ofNat - -instance instIntCastField : IntCast Field where - intCast := ofInt - -instance instNatSMulField : SMul Nat Field where - smul n x := ofNat n * x - -instance instIntSMulField : SMul Int Field where - smul n x := ofInt n * x - -instance instPowFieldNat : Pow Field Nat where - pow := pow - -instance instPowFieldInt : Pow Field Int where - pow x n := - match n with - | Int.ofNat k => pow x k - | Int.negSucc k => pow (inv x) (k + 1) - -instance instNNRatCastField : NNRatCast Field where - nnratCast q := ofField (q : KoalaBear.Field) - -instance instRatCastField : RatCast Field where - ratCast q := ofField (q : KoalaBear.Field) - -instance instNNRatSMulField : SMul ℚ≥0 Field where - smul q x := ofField (q • toField x) - -instance instRatSMulField : SMul ℚ Field where - smul q x := ofField (q • toField x) - -/-- Converting from the canonical field to fast form and back is the identity. -/ -@[simp] -theorem toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x := by - unfold ofField - rw [toField_ofCanonicalNat] - exact ZMod.natCast_zmod_val x - -/-- Converting from fast form to the canonical field and back is the identity. -/ -@[simp] -theorem ofField_toField (x : Field) : ofField (toField x) = x := by - apply Subtype.ext - apply UInt32.toNat_inj.mp - apply nat_eq_of_field_eq - · exact (ofField (toField x)).property - · exact x.property - · rw [raw_cast_eq_toField_mul] - rw [toField_ofField] - rw [raw_cast_eq_toField_mul] - -/-- The canonical-field interpretation distinguishes fast KoalaBear values. -/ -theorem toField_injective : Function.Injective toField := - Function.LeftInverse.injective ofField_toField - -/-- `toField` maps fast zero to canonical zero. -/ -@[simp] -theorem toField_zero : toField (0 : Field) = 0 := by - rw [toField_eq_raw_mul_inv] - change ((0 : Nat) : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ = 0 - exact zero_mul _ - -/-- `toField` maps fast one to canonical one. -/ -@[simp] -theorem toField_one : toField (1 : Field) = 1 := by - rw [toField_eq_raw_mul_inv] - change (rModModulus.toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ = 1 - rw [rModModulus_cast] - exact mul_inv_cancel₀ uint32Size_ne_zero_in_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 := by - rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x, toField_eq_raw_mul_inv y] - unfold instAddField add - have hred := reduceUInt32Lt2Modulus_cast (x.val + y.val) (by - rw [UInt32.toNat_add] - exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) (by omega)) - change ((reduceUInt32Lt2ModulusRaw (x.val + y.val)).toNat : KoalaBear.Field) = - ((x.val + y.val).toNat : KoalaBear.Field) at hred - change ((reduceUInt32Lt2ModulusRaw (x.val + y.val)).toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ = - (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ + - (y.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - rw [hred] - rw [UInt32.toNat_add] - have hsum_lt : x.val.toNat + y.val.toNat < UInt32.size := by - nlinarith [x.property, y.property, fieldSize_add_fieldSize_lt_uint32Size] - rw [Nat.mod_eq_of_lt hsum_lt] - rw [Nat.cast_add] - ring - -/-- Fast subtraction agrees with subtraction in the canonical KoalaBear field. -/ -@[simp] -theorem toField_sub (x y : Field) : 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] - by_cases hyx : y.val ≤ x.val - · have hsubval : (x - y : Field).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 : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹) = - (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - - (y.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - 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 + KoalaBear.fieldSize < UInt32.size := by - have htwo := fieldSize_add_fieldSize_lt_uint32Size - omega - have hsum_eq : (x.val + modulus).toNat = x.val.toNat + KoalaBear.fieldSize := by - rw [UInt32.toNat_add, modulus_toNat, Nat.mod_eq_of_lt hsum_lt] - have hyle : y.val ≤ x.val + modulus := by - rw [UInt32.le_iff_toNat_le, hsum_eq] - omega - have hsubval : (x - y : Field).val = x.val + modulus - y.val := by - change (sub x y).val = x.val + modulus - y.val - unfold sub - rw [dif_neg hyx] - rw [hsubval] - change (((x.val + modulus - y.val).toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹) = - (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - - (y.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ - rw [UInt32.toNat_sub_of_le _ _ hyle, hsum_eq] - rw [Nat.cast_sub (by - rw [UInt32.le_iff_toNat_le, hsum_eq] at hyle - exact hyle)] - rw [Nat.cast_add, ZMod.natCast_self] - ring - -/-- Fast negation agrees with negation in the canonical KoalaBear field. -/ -@[simp] -theorem toField_neg (x : Field) : toField (-x) = -toField x := by - rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x] - by_cases hx : x.val = 0 - · have hnegval : (-x : Field).val = zero.val := by - change (neg x).val = zero.val - unfold neg - rw [dif_pos hx] - rw [hnegval] - change ((zero.val.toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹) = - -((x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹) - have hxNat : x.val.toNat = 0 := by - simpa using congrArg UInt32.toNat hx - rw [hxNat] - change ((0 : Nat) : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ = - -(((0 : Nat) : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹) - simp - · have hle : x.val ≤ modulus := by - rw [UInt32.le_iff_toNat_le, modulus_toNat] - exact Nat.le_of_lt x.property - have hnegval : (-x : Field).val = modulus - x.val := by - change (neg x).val = modulus - x.val - unfold neg - rw [dif_neg hx] - rw [hnegval] - change (((modulus - x.val).toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹) = - -((x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹) - rw [UInt32.toNat_sub_of_le _ _ hle, modulus_toNat] - rw [Nat.cast_sub (by - rw [UInt32.le_iff_toNat_le, modulus_toNat] at hle - exact hle)] - rw [ZMod.natCast_self] - ring - -/-- Fast multiplication agrees with multiplication in the canonical KoalaBear field. -/ -@[simp] -theorem toField_mul (x y : Field) : 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 instMulField mul - have hred := montgomeryReduceBounded_cast (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, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - nlinarith [x.property, y.property, fieldSize_lt_uint32Size, fieldSize_pos]) - change ((montgomeryReduceBoundedRaw (x.val.toUInt64 * y.val.toUInt64)).toNat : - KoalaBear.Field) = - ((x.val.toUInt64 * y.val.toUInt64).toNat : KoalaBear.Field) * - (UInt32.size : KoalaBear.Field)⁻¹ at hred - change ((montgomeryReduceBoundedRaw (x.val.toUInt64 * y.val.toUInt64)).toNat : - KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ = - (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ * - ((y.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹) - rw [hred] - simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] - have hprod : x.val.toNat * y.val.toNat < 2 ^ 64 := by - nlinarith [x.property, y.property, fieldSize_mul_fieldSize_lt_two64] - rw [Nat.mod_eq_of_lt hprod] - rw [Nat.cast_mul] - ring +/-! ## Canonical bridge -/ /-- Ring equivalence between the fast Montgomery representation and canonical `KoalaBear.Field`. -/ -def ringEquiv : Field ≃+* KoalaBear.Field where - toFun := toField - invFun := ofField - left_inv := ofField_toField - right_inv := toField_ofField - map_add' := toField_add - map_mul' := toField_mul - -/-- Applying `ringEquiv` is the same as interpreting a fast value canonically. -/ -@[simp] -theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x := rfl - -/-- Applying the inverse `ringEquiv` is conversion into fast Montgomery form. -/ -@[simp] -theorem ringEquiv_symm_apply (x : KoalaBear.Field) : ringEquiv.symm x = ofField x := rfl - -private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z) := by - apply toField_injective - rw [toField_mul, toField_mul, toField_mul, toField_mul] - ring - -private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x := by - unfold pow - letI : Semigroup Field := { - mul := (· * ·) - mul_assoc := mul_assoc_field - } - exact npowBinRec_succ n 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 := by - change toField (x * x) = toField x * toField x - rw [toField_mul] - -/-- Fast natural-power computation agrees with powers in the canonical field. -/ -@[simp] -theorem toField_pow (x : Field) (n : Nat) : toField (pow x n) = toField x ^ n := by - induction n with - | zero => - unfold pow - rw [npowBinRec_zero] - rw [toField_one] - simp - | succ n ih => - rw [pow_succ, toField_mul, ih, _root_.pow_succ] - -private theorem toField_mul_pow (base x y : Field) (m n : Nat) - (hx : toField x = toField base ^ m) (hy : toField y = toField base ^ n) : - toField (mul x y) = toField base ^ (m + n) := by - change toField (x * y) = toField base ^ (m + n) - rw [toField_mul, hx, hy, ← pow_add] - -private theorem toField_shift4Mul (acc digit : Field) : - toField (shift4Mul acc digit) = toField acc ^ 16 * toField digit := by - unfold shift4Mul - change toField (square (square (square (square acc))) * digit) = - toField acc ^ 16 * toField digit - rw [toField_mul] - repeat rw [toField_square] - ring - -private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat) - (hacc : toField acc = toField base ^ e) (hdigit : toField digit = toField base ^ d) : - toField (shift4Mul acc digit) = toField base ^ (16 * e + d) := by - rw [toField_shift4Mul, hacc, hdigit] - rw [← pow_mul, ← pow_add] - congr 1 - omega - -private theorem toField_inv_pow (x : Field) : - toField (inv x) = toField x ^ invExponent := by - unfold inv - let x2 := square x - let x3 := mul x2 x - let x5 := mul x3 x2 - let x7 := mul x5 x2 - let x14 := square x7 - let x15 := mul x14 x - let acc1 := shift4Mul x7 x14 - let acc2 := shift4Mul acc1 x15 - let acc3 := shift4Mul acc2 x15 - let acc4 := shift4Mul acc3 x15 - let acc5 := shift4Mul acc4 x15 - let acc6 := shift4Mul acc5 x15 - have hx1 : toField x = toField x ^ 1 := by simp - have hx2 : toField x2 = toField x ^ 2 := by - dsimp [x2] - rw [toField_square, pow_two] - have hx3 : toField x3 = toField x ^ 3 := by - dsimp [x3] - simpa using toField_mul_pow x x2 x 2 1 hx2 hx1 - have hx5 : toField x5 = toField x ^ 5 := by - dsimp [x5] - simpa using toField_mul_pow x x3 x2 3 2 hx3 hx2 - have hx7 : toField x7 = toField x ^ 7 := by - dsimp [x7] - simpa using toField_mul_pow x x5 x2 5 2 hx5 hx2 - have hx14 : toField x14 = toField x ^ 14 := by - dsimp [x14] - rw [toField_square, hx7, ← pow_add] - have hx15 : toField x15 = toField x ^ 15 := by - dsimp [x15] - simpa using toField_mul_pow x x14 x 14 1 hx14 hx1 - have hacc1 : toField acc1 = toField x ^ 126 := by - dsimp [acc1] - simpa using toField_shift4Mul_pow x x7 x14 7 14 hx7 hx14 - have hacc2 : toField acc2 = toField x ^ 2031 := by - dsimp [acc2] - simpa using toField_shift4Mul_pow x acc1 x15 126 15 hacc1 hx15 - have hacc3 : toField acc3 = toField x ^ 32511 := by - dsimp [acc3] - simpa using toField_shift4Mul_pow x acc2 x15 2031 15 hacc2 hx15 - have hacc4 : toField acc4 = toField x ^ 520191 := by - dsimp [acc4] - simpa using toField_shift4Mul_pow x acc3 x15 32511 15 hacc3 hx15 - have hacc5 : toField acc5 = toField x ^ 8323071 := by - dsimp [acc5] - simpa using toField_shift4Mul_pow x acc4 x15 520191 15 hacc4 hx15 - have hacc6 : toField acc6 = toField x ^ 133169151 := by - dsimp [acc6] - simpa using toField_shift4Mul_pow x acc5 x15 8323071 15 hacc5 hx15 - have hfinal := toField_shift4Mul_pow x acc6 x15 133169151 15 hacc6 hx15 - simpa [invExponent, KoalaBear.fieldSize] using hfinal - -private theorem toField_inv_raw (x : Field) : toField (inv x) = (toField x)⁻¹ := by - rw [toField_inv_pow] - by_cases hx : toField x = 0 - · rw [hx] - simp [invExponent, KoalaBear.fieldSize] - · simpa [invExponent] using (KoalaBear.inv_eq_pow (toField x) hx).symm - -/-- Fast inversion agrees with inversion in the canonical KoalaBear field. -/ -@[simp] -theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ := by - change toField (inv x) = (toField x)⁻¹ - exact toField_inv_raw x - -private theorem toField_mul_raw (x y : Field) : 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 : Field) : - toField (div x y) = toField x * toField (inv y) := by - unfold div - exact toField_mul_raw x (inv y) - -/-- Fast division agrees with division in the canonical KoalaBear field. -/ -@[simp] -theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y := by - change toField (div x y) = toField x / toField y - have h : ∀ a b c : KoalaBear.Field, 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)) - -/-- 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) := by - change toField (ofNat n) = (n : KoalaBear.Field) - unfold ofNat - rw [toField_ofCanonicalNat] - rw [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 : Field) = (n : KoalaBear.Field) := by - change toField (ofInt n) = (n : KoalaBear.Field) - unfold ofInt - rw [toField_ofField] - -/-- Natural scalar multiplication is preserved by `toField`. -/ -@[simp] -theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x := by - change toField ((n : Field) * x) = n • toField x - rw [toField_mul, toField_natCast] - rw [nsmul_eq_mul] - -/-- Integer scalar multiplication is preserved by `toField`. -/ -@[simp] -theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x := by - change toField ((n : Field) * x) = n • toField x - rw [toField_mul, toField_intCast] - rw [zsmul_eq_mul] - -/-- Natural powers through the `Pow` instance are preserved by `toField`. -/ -@[simp] -theorem toField_npow (x : Field) (n : Nat) : 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 : Field) (n : Int) : toField (x ^ n) = toField x ^ n := by - cases n with - | ofNat n => - change toField (pow x n) = toField x ^ (Int.ofNat n) - rw [toField_pow] - exact (zpow_natCast (toField x) n).symm - | negSucc n => - change toField (pow (inv x) (n + 1)) = toField x ^ (Int.negSucc n) - have hinv : toField (inv x) = (toField x)⁻¹ := by - change toField x⁻¹ = (toField x)⁻¹ - rw [toField_inv] - rw [toField_pow, hinv, zpow_negSucc, inv_pow] - -/-- Nonnegative rational casts into fast form agree with canonical-field casts. -/ -@[simp] -theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : KoalaBear.Field) := by - change toField (ofField (q : KoalaBear.Field)) = (q : KoalaBear.Field) - rw [toField_ofField] - -/-- Rational casts into fast form agree with canonical-field casts. -/ -@[simp] -theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : KoalaBear.Field) := by - change toField (ofField (q : KoalaBear.Field)) = (q : KoalaBear.Field) - rw [toField_ofField] - -/-- Nonnegative rational scalar multiplication is preserved by `toField`. -/ -@[simp] -theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : 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 : Field) : toField (q • x) = q • toField x := by - change toField (ofField (q • toField x)) = q • toField x - rw [toField_ofField] - -/-- Field instance transferred from canonical KoalaBear through `toField`. -/ -instance (priority := low) instField : _root_.Field Field := - 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 Field := by - infer_instance - -/-- Fast KoalaBear is a non-binary field. -/ -instance (priority := low) instNonBinaryField : NonBinaryField Field where - char_neq_2 := by - change ((2 : Nat) : Field) ≠ 0 - intro h - exact NonBinaryField.char_neq_2 (F := KoalaBear.Field) (by - calc - (2 : KoalaBear.Field) = toField ((2 : Nat) : Field) := (toField_natCast 2).symm - _ = toField (0 : Field) := congrArg toField h - _ = 0 := toField_zero) +def ringEquiv : Field ≃+* KoalaBear.Field := + 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 Fast -end KoalaBear +end KoalaBear.Fast diff --git a/CompPoly/Fields/Montgomery/Basic.lean b/CompPoly/Fields/Montgomery/Basic.lean new file mode 100644 index 00000000..47336c85 --- /dev/null +++ b/CompPoly/Fields/Montgomery/Basic.lean @@ -0,0 +1,114 @@ +/- +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 Mathlib.Data.Nat.ModEq +import Mathlib.Data.ZMod.Basic +import Mathlib.Algebra.Field.ZMod +import Mathlib.Tactic.Ring + +/-! +# Montgomery Reduction + +Radix-generic specification and correctness lemmas for single-word Montgomery reduction. +Word-specific implementations refine these results in sibling modules. +-/ + +namespace Montgomery + +/-- 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 + +/-- 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 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 + rw [← hcast_mul] + exact (mul_inv_cancel_right₀ hRne (u : ZMod p)).symm + +/-- 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 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 + · 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 [if_neg hu] + rw [hfield] + exact hu_cast + +/-- Two naturals below `p` are equal once their `ZMod p` casts agree. -/ +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 + +end Montgomery diff --git a/CompPoly/Fields/Montgomery/Native32.lean b/CompPoly/Fields/Montgomery/Native32.lean new file mode 100644 index 00000000..bba0de97 --- /dev/null +++ b/CompPoly/Fields/Montgomery/Native32.lean @@ -0,0 +1,140 @@ +/- +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.Montgomery.Basic + +/-! +# Native 32-bit Montgomery Reduction + +Raw word operations for Montgomery reduction with radix `2 ^ 32`. +-/ + +namespace Montgomery +namespace Native32 + +/-- 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, + 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 * 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 + +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 new file mode 100644 index 00000000..89e88d51 --- /dev/null +++ b/CompPoly/Fields/Montgomery/Native32Field.lean @@ -0,0 +1,642 @@ +/- +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.Basic +import CompPoly.Fields.Montgomery.Native32 +import Mathlib.Algebra.Field.TransferInstance +import Mathlib.FieldTheory.Finite.Basic +import Mathlib.Tactic.Linarith + +/-! +# 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 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 modulus`, the Montgomery representation of one. -/ + rModModulus : UInt32 + /-- `(2^32)^2 mod modulus`, used to enter Montgomery form. -/ + r2ModModulus : UInt64 + /-- `-modulus⁻¹ mod 2^32`, used by Montgomery reduction. -/ + montgomeryNegInv : UInt32 + 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 (modulus : ℕ) [Mont32Field modulus] : Type := + { x : UInt32 // x.toNat < modulus } + +section +variable {modulus : ℕ} [P : Mont32Field modulus] + +instance : DecidableEq (FastField modulus) := + inferInstanceAs (DecidableEq { x : UInt32 // x.toNat < modulus }) + +namespace Mont32Field + +instance : Fact (Nat.Prime modulus) := ⟨P.prime⟩ + +@[simp] +theorem modulus_pos : 0 < modulus := Nat.zero_lt_of_lt P.two_lt_modulus + +@[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 + +@[simp] theorem modulus_lt_two_pow_32 : modulus < 2 ^ 32 := by + linarith [P.modulus_lt_two_pow_31] + +theorem modulus_sq_lt_two_pow_64 : modulus ^ 2 < 2 ^ 64 := by + nlinarith [P.modulus_lt_two_pow_32] + +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) + +theorem two_pow_32_ne_zero : ((2 ^ 32 : ℕ) : ZMod modulus) ≠ 0 := by + simp [two_ne_zero] + +theorem r2ModModulus_lt_modulus : (2 ^ 32) ^ 2 % modulus < modulus := by + exact Nat.mod_lt _ P.modulus_pos + +end Mont32Field + +instance : NeZero modulus := ⟨P.modulus_pos.ne'⟩ + +/-! ## Implementation -/ + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ +@[inline] +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 + +namespace FastField + +/-! ### 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 (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 (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 modulus) : FastField modulus := + ofCanonicalNat x.val (ZMod.val_lt x) + +/-- Convert an integer into fast Montgomery representation. -/ +@[inline] +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 toUInt32 (x : FastField modulus) : UInt32 := Subtype.val <| + reduce (modulus := modulus) x.val.toUInt64 <| by + rw [UInt32.toNat_toUInt64] + nlinarith [x.property, P.modulus_pos] + +/-- Convert a fast element to its canonical natural representative. -/ +@[inline] +def toNat (x : FastField modulus) : ℕ := x.toUInt32.toNat + +/-- Convert a fast element to the canonical `ZMod` field. -/ +@[inline] +def toField (x : FastField modulus) : ZMod modulus := (x.toNat : ZMod modulus) +end FastField + +open FastField + +/-! ### Field operations -/ + +/-- The zero fast element. -/ +def zero (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus := .mk 0 <| by simp + +/-- 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 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 modulus) : FastField modulus := + if hx : x.val = 0 then + zero modulus + else + .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 modulus) : FastField modulus := + if hyx : y.val ≤ x.val then + .mk (x.val - y.val) <| by + rw [UInt32.toNat_sub_of_le _ _ hyx] + have := x.property + omega + else + .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 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.modulus_sq_lt_two_pow_64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [x.property, y.property, P.modulus_lt_two_pow_32, P.modulus_pos]) + +/-- Fast squaring. -/ +@[inline] +def square (x : FastField modulus) : FastField modulus := mul x x + +/-- Exponentiation over the fast representation using repeated squaring. -/ +@[specialize] +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 modulus) : FastField modulus := + pow x (modulus - 2) + +/-- Division through inversion and fast multiplication. -/ +@[inline] +def div (x y : FastField modulus) : FastField modulus := + mul x (inv y) + +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 : NNRatCast (FastField modulus) where + nnratCast q := ofField (q : ZMod modulus) + +instance : RatCast (FastField modulus) where + ratCast q := ofField (q : ZMod modulus) + +instance : SMul ℚ≥0 (FastField modulus) where + smul q x := ofField (q • toField x) + +instance : SMul ℚ (FastField modulus) where + smul q x := ofField (q • toField x) + +/-! ## Correctness -/ + +/-! ### Reduction and conversions -/ + +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, *] + +@[simp] +theorem FastField.val_toNat_lt (x : FastField modulus) : x.val.toNat < modulus := x.property + +theorem toNat_lt_modulus {x : FastField modulus} : toNat x < modulus := by + simp [FastField.toNat, FastField.toUInt32] + +private theorem toField_eq_val_toNat_cast_mul_inv {x : FastField modulus} : + toField x = + (x.val.toNat : ZMod modulus) * ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ := by + have hb : (x.val.toUInt64).toNat < modulus * 2 ^ 32 := by + rw [UInt32.toNat_toUInt64]; nlinarith [x.property, P.modulus_pos] + rw [show toField x + = (x.val.toUInt64.toNat : ZMod modulus) * ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ from + reduce_val_toNat_cast (P := P) (x := x.val.toUInt64) hb, UInt32.toNat_toUInt64] + +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 + have hb : (UInt64.ofNat n * P.r2ModModulus).toNat < modulus * 2 ^ 32 := 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] + rw [show ((ofCanonicalNat n h).val.toNat : ZMod modulus) + = ((UInt64.ofNat n * P.r2ModModulus).toNat : ZMod modulus) + * ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ from + reduce_val_toNat_cast (P := P) (x := UInt64.ofNat n * P.r2ModModulus) hb] + 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 + +@[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] + +@[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 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 modulus) : ofField (toField x) = x := by + apply Subtype.ext + apply UInt32.toNat_inj.mp + 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 (modulus := modulus)) := + Function.LeftInverse.injective ofField_toField + +/-! ### Field operations -/ + +/-- `toField` maps fast zero to canonical zero. -/ +@[simp] +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 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 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 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 + · 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 + modulus < 2 ^ 32 := by + have htwo := P.modulus_lt_two_pow_31 + have := x.property; omega + 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 + 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 + exact hyle)] + rw [Nat.cast_add, ZMod.natCast_self] + ring + +/-- Fast negation agrees with negation in the canonical field. -/ +@[simp] +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 + · 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 + 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.modulus32_toNat] at hle + exact hle)] + rw [ZMod.natCast_self] + ring + +/-- Fast multiplication agrees with multiplication in the canonical field. -/ +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 + have hb : (x.val.toUInt64 * y.val.toUInt64).toNat < modulus * 2 ^ 32 := 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.modulus_sq_lt_two_pow_64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [x.property, y.property, P.modulus_lt_two_pow_32, P.modulus_pos] + rw [show ((mul x y).val.toNat : ZMod modulus) + = ((x.val.toUInt64 * y.val.toUInt64).toNat : ZMod modulus) + * ((2 ^ 32 : ℕ) : ZMod modulus)⁻¹ from + reduce_val_toNat_cast (P := P) (x := x.val.toUInt64 * y.val.toUInt64) hb] + 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.modulus_sq_lt_two_pow_64] + rw [Nat.mod_eq_of_lt hprod, Nat.cast_mul] + +@[simp] +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 (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 modulus) (n : ℕ) : pow x (n + 1) = pow x n * x := by + unfold pow + 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 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 modulus) (n : ℕ) : toField (pow x n) = toField x ^ n := by + induction n with + | zero => + unfold pow + rw [npowBinRec_zero] + rw [toField_one] + simp + | succ n ih => + rw [pow_succ_field, toField_mul, ih, _root_.pow_succ] + +/-- 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 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 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 : ℕ) : 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 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 : ℕ) (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 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 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 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) + rw [toField_pow] + exact (zpow_natCast (toField x) n).symm + | negSucc n => + change toField (pow (inv x) (n + 1)) = toField x ^ (Int.negSucc n) + have hinv : toField (inv x) = (toField x)⁻¹ := by + change toField x⁻¹ = (toField x)⁻¹ + rw [toField_inv] + rw [toField_pow, hinv, zpow_negSucc, inv_pow] + +/-- Nonnegative rational casts into fast form agree with canonical-field casts. -/ +@[simp] +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 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 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 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 instField : _root_.Field (FastField modulus) := by + apply toField_injective.field toField <;> simp + +/-- A fast 32-bit-word field is non-binary. -/ +instance instNonBinaryField : NonBinaryField (FastField modulus) where + char_neq_2 := by + intro h + 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 + +end Native32 +end Montgomery diff --git a/CompPoly/Fields/README.md b/CompPoly/Fields/README.md index ef884b31..6830d132 100644 --- a/CompPoly/Fields/README.md +++ b/CompPoly/Fields/README.md @@ -8,15 +8,20 @@ This directory contains formally verified field infrastructure used in zero-know |--------|-------------| | **Basic.lean** | `NonBinaryField` type class (char ≠ 2), polynomial composition lemmas (`coeffs_of_comp_minus_x`, `comp_x_square_coeff`). | | **PrattCertificate.lean** | Lucas test for primality and Pratt certificate infrastructure (`PrattCertificate`, `PrattCertificate'`) for proving concrete primality goals. | -| **BabyBear.lean** | \(2^{31} - 2^{27} + 1\) — Risc Zero. | +| **BabyBear.lean** | Facade for BabyBear modules, re-exporting the canonical field and fast native-word implementation. | +| **BabyBear/Basic.lean** | \(2^{31} - 2^{27} + 1\) — Risc Zero. | +| **BabyBear/Fast.lean** | BabyBear-namespaced API over the shared fast-field implementation (`Montgomery/Native32Field.lean`): thin wrappers forwarding the native `UInt32` Montgomery-residue operations and their `BabyBear.Field` equivalence (`@[simp]`) lemmas. | | **BLS12_377.lean** | Scalar field of BLS12-377 (253-bit, 2-adicity 47) — Zexe. | | **BLS12_381.lean** | Scalar field of BLS12-381 (253-bit, 2-adicity 47). | | **BN254.lean** | Scalar field of BN254 curve. | | **Goldilocks.lean** | \(2^{64} - 2^{32} + 1\) — Plonky2/3. | | **KoalaBear.lean** | Facade for KoalaBear modules, re-exporting the canonical field and fast native-word implementation. | | **KoalaBear/Basic.lean** | \(2^{31} - 2^{24} + 1\) — lean Ethereum spec. | -| **KoalaBear/Fast.lean** | Native `UInt32` Montgomery-residue operations for KoalaBear, with conversion and operation equivalence statements against `KoalaBear.Field`. | +| **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** | 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 03ac92a4..aaeb94c8 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..6990fa09 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,16 @@ 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, bitsOfLogN, KoalaBear.Fast.ringEquiv, + KoalaBear.Fast.ofField] 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 022cf51c..fd314efd 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/docs/wiki/binary-fields-and-ntt.md b/docs/wiki/binary-fields-and-ntt.md index 958477d6..feedc80d 100644 --- a/docs/wiki/binary-fields-and-ntt.md +++ b/docs/wiki/binary-fields-and-ntt.md @@ -12,9 +12,15 @@ CompPoly/Fields/ BabyBear/ Basic.lean Fast.lean + Fast/ (Prelude.lean, Montgomery.lean, Convert.lean) KoalaBear/ Basic.lean Fast.lean + Fast/ (Prelude.lean, Montgomery.lean, Convert.lean) + Montgomery/ + Basic.lean + Native32.lean + Native32Field.lean Binary/ Common.lean BF128Ghash/ diff --git a/tests/CompPolyTests.lean b/tests/CompPolyTests.lean index 0321cad5..1c627ad7 100644 --- a/tests/CompPolyTests.lean +++ b/tests/CompPolyTests.lean @@ -21,6 +21,7 @@ import CompPolyTests.Bivariate.GuruswamiSudan.Root.RothRuckenstein import CompPolyTests.Bivariate.Multiplicity import CompPolyTests.Bivariate.WeightedDegree import CompPolyTests.Data.MvPolynomial.Notation +import CompPolyTests.Fields.BabyBear.Fast import CompPolyTests.Fields.Binary.AdditiveNTT.NovelPolynomialBasis import CompPolyTests.Fields.Binary.BF128Ghash.Prelude import CompPolyTests.Fields.KoalaBear.Fast diff --git a/tests/CompPolyTests/Fields/BabyBear/Fast.lean b/tests/CompPolyTests/Fields/BabyBear/Fast.lean new file mode 100644 index 00000000..909414df --- /dev/null +++ b/tests/CompPolyTests/Fields/BabyBear/Fast.lean @@ -0,0 +1,42 @@ +/- +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 + +/-! +# Fast BabyBear Field Tests + +Regression checks for the executable Montgomery representation. +-/ + +namespace BabyBear.Fast + +#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 ((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