diff --git a/CompPoly.lean b/CompPoly.lean index 58d6f008..61e7a4cd 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -66,6 +66,11 @@ 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.BabyBear.Fast.Convert +import CompPoly.Fields.BabyBear.Fast.Montgomery +import CompPoly.Fields.BabyBear.Fast.Prelude import CompPoly.Fields.Basic import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT import CompPoly.Fields.Binary.AdditiveNTT.Algorithm @@ -102,7 +107,13 @@ import CompPoly.Fields.Goldilocks import CompPoly.Fields.KoalaBear import CompPoly.Fields.KoalaBear.Basic import CompPoly.Fields.KoalaBear.Fast +import CompPoly.Fields.KoalaBear.Fast.Convert +import CompPoly.Fields.KoalaBear.Fast.Montgomery +import CompPoly.Fields.KoalaBear.Fast.Prelude import CompPoly.Fields.Mersenne +import CompPoly.Fields.Montgomery.Basic +import CompPoly.Fields.Montgomery.Native32 +import CompPoly.Fields.Montgomery.Native32Field import CompPoly.Fields.PrattCertificate import CompPoly.Fields.Secp256k1 import CompPoly.LinearAlgebra.Dense diff --git a/CompPoly/Fields/BabyBear.lean b/CompPoly/Fields/BabyBear.lean index e0bf3e60..bcc0bb89 100644 --- a/CompPoly/Fields/BabyBear.lean +++ b/CompPoly/Fields/BabyBear.lean @@ -4,248 +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 - simpa using sqChain_twoAdicGenerators_shift 0 n (by omega) - 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..37a0729a --- /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 : _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) + +/-- 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 + simpa using sqChain_twoAdicGenerators_shift 0 n (by omega) + 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..2a313148 --- /dev/null +++ b/CompPoly/Fields/BabyBear/Fast.lean @@ -0,0 +1,188 @@ +/- +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.Convert + +/-! +# Fast BabyBear Field Operations + +A native-word implementation of BabyBear arithmetic as a sidecar to the canonical +`BabyBear.Field := ZMod BabyBear.fieldSize` model. Fast values are stored as Montgomery +`UInt32` residues below `BabyBear.fieldSize`, representing `x * 2^32` modulo the prime. + +The operations, their `Field`/`CommRing`/`NonBinaryField` instances, the `toField` bridge, +and all correctness theorems are shared across every fast 32-bit-word field; they live once +in `CompPoly.Fields.Montgomery.Native32Field`, parameterized by the `Mont32Field` instance +in `CompPoly.Fields.BabyBear.Fast.Prelude`. Because `Field := Native32.FastField BabyBear.Field`, +the generic algebraic instances resolve here automatically. This module re-exports the +named operations and `simp` lemmas at the BabyBear instance. +-/ + +namespace BabyBear +namespace Fast + +open Montgomery.Native32 + +/-- Fast modular addition in Montgomery form. -/ +@[inline] +def add (x y : Field) : Field := Montgomery.Native32.add x y + +/-- Fast modular negation in Montgomery form. -/ +@[inline] +def neg (x : Field) : Field := Montgomery.Native32.neg x + +/-- Fast modular subtraction in Montgomery form. -/ +@[inline] +def sub (x y : Field) : Field := Montgomery.Native32.sub x y + +/-- Fast modular multiplication in Montgomery form. -/ +@[inline] +def mul (x y : Field) : Field := Montgomery.Native32.mul x y + +/-- Fast squaring. -/ +@[inline] +def square (x : Field) : Field := Montgomery.Native32.square x + +/-- Exponentiation over the fast representation using repeated squaring. -/ +@[inline] +def pow (x : Field) (n : Nat) : Field := Montgomery.Native32.pow x n + +/-- Fermat exponent used for inversion in the BabyBear prime field. -/ +def invExponent : Nat := Montgomery.Native32.invExponent (F := BabyBear.Field) + +/-- Inversion in Montgomery form via Fermat's little theorem (`x⁻¹ = x^(p-2)`). -/ +@[inline] +def inv (x : Field) : Field := Montgomery.Native32.inv x + +/-- Division through inversion and fast multiplication. -/ +@[inline] +def div (x y : Field) : Field := Montgomery.Native32.div x y + +/-- Ring equivalence between the fast Montgomery representation and canonical `BabyBear.Field`. -/ +def ringEquiv : Field ≃+* BabyBear.Field := + Montgomery.Native32.ringEquiv (F := BabyBear.Field) + +/-- Converting from the canonical field to fast form and back is the identity. -/ +@[simp] +theorem toField_ofField (x : BabyBear.Field) : toField (ofField x) = x := + Montgomery.Native32.toField_ofField (F := BabyBear.Field) x + +/-- Converting from fast form to the canonical field and back is the identity. -/ +@[simp] +theorem ofField_toField (x : Field) : ofField (toField x) = x := + Montgomery.Native32.ofField_toField x + +/-- The canonical-field interpretation distinguishes fast BabyBear values. -/ +theorem toField_injective : Function.Injective (toField : Field → BabyBear.Field) := + Montgomery.Native32.toField_injective (F := BabyBear.Field) + +/-- `toField` maps fast zero to canonical zero. -/ +@[simp] +theorem toField_zero : toField (0 : Field) = 0 := + Montgomery.Native32.toField_zero (F := BabyBear.Field) + +/-- `toField` maps fast one to canonical one. -/ +@[simp] +theorem toField_one : toField (1 : Field) = 1 := + Montgomery.Native32.toField_one (F := BabyBear.Field) + +/-- Fast addition agrees with addition in the canonical BabyBear field. -/ +@[simp] +theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y := + Montgomery.Native32.toField_add x y + +/-- Fast subtraction agrees with subtraction in the canonical BabyBear field. -/ +@[simp] +theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y := + Montgomery.Native32.toField_sub x y + +/-- Fast negation agrees with negation in the canonical BabyBear field. -/ +@[simp] +theorem toField_neg (x : Field) : toField (-x) = -toField x := + Montgomery.Native32.toField_neg x + +/-- Fast multiplication agrees with multiplication in the canonical BabyBear field. -/ +@[simp] +theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y := + Montgomery.Native32.toField_mul x y + +/-- Applying `ringEquiv` is the same as interpreting a fast value canonically. -/ +@[simp] +theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x := + Montgomery.Native32.ringEquiv_apply x + +/-- Applying the inverse `ringEquiv` is conversion into fast Montgomery form. -/ +@[simp] +theorem ringEquiv_symm_apply (x : BabyBear.Field) : ringEquiv.symm x = ofField x := + Montgomery.Native32.ringEquiv_symm_apply (F := BabyBear.Field) x + +/-- Fast squaring agrees with multiplication by itself in the canonical field. -/ +@[simp] +theorem toField_square (x : Field) : toField (square x) = toField x * toField x := + Montgomery.Native32.toField_square x + +/-- Fast inversion agrees with inversion in the canonical BabyBear field. -/ +@[simp] +theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ := + Montgomery.Native32.toField_inv x + +/-- Fast division agrees with division in the canonical BabyBear field. -/ +@[simp] +theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y := + Montgomery.Native32.toField_div x y + +/-- Natural casts into fast form agree with natural casts into the canonical field. -/ +@[simp] +theorem toField_natCast (n : Nat) : toField (n : Field) = (n : BabyBear.Field) := + Montgomery.Native32.toField_natCast n + +/-- Integer casts into fast form agree with integer casts into the canonical field. -/ +@[simp] +theorem toField_intCast (n : Int) : toField (n : Field) = (n : BabyBear.Field) := + Montgomery.Native32.toField_intCast n + +/-- Natural scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x := + Montgomery.Native32.toField_nsmul n x + +/-- Integer scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x := + Montgomery.Native32.toField_zsmul n x + +/-- Natural powers through the `Pow` instance are preserved by `toField`. -/ +@[simp] +theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n := + Montgomery.Native32.toField_npow x n + +/-- Integer powers through the `Pow` instance are preserved by `toField`. -/ +@[simp] +theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n := + Montgomery.Native32.toField_zpow x n + +/-- Nonnegative rational casts into fast form agree with canonical-field casts. -/ +@[simp] +theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : BabyBear.Field) := + Montgomery.Native32.toField_nnratCast q + +/-- Rational casts into fast form agree with canonical-field casts. -/ +@[simp] +theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : BabyBear.Field) := + Montgomery.Native32.toField_ratCast q + +/-- Nonnegative rational scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x := + Montgomery.Native32.toField_nnqsmul q x + +/-- Rational scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x := + Montgomery.Native32.toField_qsmul q x + +end Fast +end BabyBear diff --git a/CompPoly/Fields/BabyBear/Fast/Convert.lean b/CompPoly/Fields/BabyBear/Fast/Convert.lean new file mode 100644 index 00000000..f02556e1 --- /dev/null +++ b/CompPoly/Fields/BabyBear/Fast/Convert.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 CompPoly Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Valerii Huhnin, Georgios Raikos +-/ + +import CompPoly.Fields.BabyBear.Fast.Montgomery + +/-! +# Fast BabyBear Field — Conversions + +Conversions between the fast Montgomery representation and the canonical +`BabyBear.Field` / `Nat` views, re-exported from the shared implementation in +`CompPoly.Fields.Montgomery.Native32Field` at the BabyBear instance. +-/ + +namespace BabyBear +namespace Fast + +open Montgomery.Native32 + +/-- Build a fast element from a canonical natural representative. -/ +@[inline] +def ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : Field := + Montgomery.Native32.ofCanonicalNat (F := BabyBear.Field) n h + +/-- Reduce a `UInt64` modulo the BabyBear prime and return a Montgomery fast element. -/ +@[inline] +def reduceUInt64 (x : UInt64) : Field := + Montgomery.Native32.reduceUInt64 (F := BabyBear.Field) x + +/-- The zero fast BabyBear element. -/ +def zero : Field := Montgomery.Native32.zero (F := BabyBear.Field) + +/-- The one fast BabyBear element. -/ +def one : Field := Montgomery.Native32.one (F := BabyBear.Field) + +/-- Convert a natural number into fast Montgomery representation. -/ +@[inline] +def ofNat (n : Nat) : Field := + Montgomery.Native32.ofNat (F := BabyBear.Field) n + +/-- Convert a 32-bit word into fast Montgomery representation. -/ +@[inline] +def ofUInt32 (x : UInt32) : Field := + Montgomery.Native32.ofUInt32 (F := BabyBear.Field) x + +/-- Convert from the canonical `ZMod` BabyBear field into fast Montgomery form. -/ +@[inline] +def ofField (x : BabyBear.Field) : Field := + Montgomery.Native32.ofField (F := BabyBear.Field) x + +/-- Convert an integer into fast Montgomery representation. -/ +@[inline] +def ofInt (n : Int) : Field := + Montgomery.Native32.ofInt (F := BabyBear.Field) n + +/-- Convert a fast element to its canonical native-word representative. -/ +@[inline] +def toCanonicalUInt32 (x : Field) : UInt32 := + Montgomery.Native32.toCanonicalUInt32 x + +/-- Convert a fast BabyBear element to its canonical natural representative. -/ +@[inline] +def toNat (x : Field) : Nat := + Montgomery.Native32.toNat x + +/-- Convert a fast BabyBear element to the canonical `ZMod` BabyBear field. -/ +@[inline] +def toField (x : Field) : BabyBear.Field := + Montgomery.Native32.toField x + +theorem toNat_lt_fieldSize (x : Field) : toNat x < BabyBear.fieldSize := + Montgomery.Native32.toNat_lt_fieldSize x + +theorem toField_eq_raw_mul_inv (x : Field) : + toField x = (x.val.toNat : BabyBear.Field) * (UInt32.size : BabyBear.Field)⁻¹ := + Montgomery.Native32.toField_eq_raw_mul_inv x + +theorem raw_cast_eq_toField_mul (x : Field) : + (x.val.toNat : BabyBear.Field) = toField x * (UInt32.size : BabyBear.Field) := + Montgomery.Native32.raw_cast_eq_toField_mul x + +theorem nat_eq_of_field_eq {a b : Nat} (ha : a < BabyBear.fieldSize) + (hb : b < BabyBear.fieldSize) (h : (a : BabyBear.Field) = (b : BabyBear.Field)) : + a = b := + Montgomery.Native32.nat_eq_of_field_eq (F := BabyBear.Field) ha hb h + +theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < BabyBear.fieldSize) : + ((ofCanonicalNat n h).val.toNat : BabyBear.Field) = + (n : BabyBear.Field) * (UInt32.size : BabyBear.Field) := + Montgomery.Native32.ofCanonicalNat_raw_cast (F := BabyBear.Field) n h + +theorem reduceUInt64_raw_cast (x : UInt64) : + ((reduceUInt64 x).val.toNat : BabyBear.Field) = + (x.toNat : BabyBear.Field) * (UInt32.size : BabyBear.Field) := + Montgomery.Native32.reduceUInt64_raw_cast x + +/-- Converting a canonical natural representative to fast form preserves its value. -/ +@[simp] +theorem toNat_ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : + toNat (ofCanonicalNat n h) = n := + Montgomery.Native32.toNat_ofCanonicalNat n h + +/-- `ofCanonicalNat` embeds a canonical representative into the canonical field. -/ +@[simp] +theorem toField_ofCanonicalNat (n : Nat) (h : n < BabyBear.fieldSize) : + toField (ofCanonicalNat n h) = (n : BabyBear.Field) := + Montgomery.Native32.toField_ofCanonicalNat n h + +/-- Reducing a `UInt64` gives the canonical natural residue modulo BabyBear. -/ +@[simp] +theorem toNat_reduceUInt64 (x : UInt64) : + toNat (reduceUInt64 x) = x.toNat % BabyBear.fieldSize := + Montgomery.Native32.toNat_reduceUInt64 x + +/-- Reducing a `UInt64` agrees with casting that word into the canonical field. -/ +@[simp] +theorem toField_reduceUInt64 (x : UInt64) : + toField (reduceUInt64 x) = (x.toNat : BabyBear.Field) := + Montgomery.Native32.toField_reduceUInt64 x + +end Fast +end BabyBear diff --git a/CompPoly/Fields/BabyBear/Fast/Montgomery.lean b/CompPoly/Fields/BabyBear/Fast/Montgomery.lean new file mode 100644 index 00000000..f798d171 --- /dev/null +++ b/CompPoly/Fields/BabyBear/Fast/Montgomery.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 CompPoly Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Valerii Huhnin, Georgios Raikos +-/ + +import CompPoly.Fields.BabyBear.Fast.Prelude + +/-! +# Fast BabyBear Field — Montgomery Reduction + +The native-word Montgomery reducers specialized to BabyBear. The definitions and their +correctness proofs are shared across every fast 32-bit-word field; they live once in +`CompPoly.Fields.Montgomery.Native32Field`, parameterized by the `Mont32Field` instance +supplied in `CompPoly.Fields.BabyBear.Fast.Prelude`. This module just re-exports them at +the BabyBear instance. Because the shared definitions are `@[inline]`, fixing the instance +folds the constants to literals: the compiled code is identical to a hand-written +monomorphic reducer, with no `Mont32Field` dictionary at runtime. +-/ + +namespace BabyBear +namespace Fast + +open Montgomery.Native32 + +/-- Reduce a native word known to be below twice the BabyBear prime. -/ +@[inline] +def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 := + Montgomery.Native32.reduceUInt32Lt2ModulusRaw (F := BabyBear.Field) x + +theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) + (h : x.toNat < 2 * BabyBear.fieldSize) : + (reduceUInt32Lt2ModulusRaw x).toNat < BabyBear.fieldSize := + Montgomery.Native32.reduceUInt32Lt2ModulusRaw_lt (F := BabyBear.Field) x h + +/-- Reduce a native word known to be below twice the BabyBear prime. -/ +@[inline] +def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * BabyBear.fieldSize) : + Field := + Montgomery.Native32.reduceUInt32Lt2Modulus (F := BabyBear.Field) x h + +theorem reduceUInt32Lt2Modulus_cast (x : UInt32) + (h : x.toNat < 2 * BabyBear.fieldSize) : + ((reduceUInt32Lt2Modulus x h).val.toNat : BabyBear.Field) = + (x.toNat : BabyBear.Field) := + Montgomery.Native32.reduceUInt32Lt2Modulus_cast (F := BabyBear.Field) x h + +/-- Reduce a native word below `2^32` modulo the BabyBear prime. -/ +@[inline] +def reduceUInt32 (x : UInt32) : Field := + Montgomery.Native32.reduceUInt32 (F := BabyBear.Field) x + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ +@[inline] +def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 := + Montgomery.Native32.montgomeryReduceBoundedRaw (F := BabyBear.Field) x + +theorem montgomeryReduceBoundedRaw_lt (x : UInt64) + (h : x.toNat < BabyBear.fieldSize * UInt32.size) : + (montgomeryReduceBoundedRaw x).toNat < BabyBear.fieldSize := + Montgomery.Native32.montgomeryReduceBoundedRaw_lt (F := BabyBear.Field) x h + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ +@[inline] +def montgomeryReduceBounded (x : UInt64) + (h : x.toNat < BabyBear.fieldSize * UInt32.size) : Field := + Montgomery.Native32.montgomeryReduceBounded (F := BabyBear.Field) x h + +theorem montgomeryReduceBounded_cast (x : UInt64) + (h : x.toNat < BabyBear.fieldSize * UInt32.size) : + ((montgomeryReduceBounded x h).val.toNat : BabyBear.Field) = + (x.toNat : BabyBear.Field) * (UInt32.size : BabyBear.Field)⁻¹ := + Montgomery.Native32.montgomeryReduceBounded_cast (F := BabyBear.Field) x h + +/-- Montgomery reduction of a 64-bit word. Hot bounded callers use `montgomeryReduceBounded`. -/ +@[inline] +def montgomeryReduce (x : UInt64) : Field := + Montgomery.Native32.montgomeryReduce (F := BabyBear.Field) x + +end Fast +end BabyBear diff --git a/CompPoly/Fields/BabyBear/Fast/Prelude.lean b/CompPoly/Fields/BabyBear/Fast/Prelude.lean new file mode 100644 index 00000000..4ed200a1 --- /dev/null +++ b/CompPoly/Fields/BabyBear/Fast/Prelude.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 CompPoly Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Valerii Huhnin, Georgios Raikos +-/ + +import CompPoly.Fields.BabyBear.Basic +import CompPoly.Fields.Montgomery.Native32Field + +/-! +# Fast BabyBear Field — Basics + +The native-word constants and the `Field` carrier type for the fast BabyBear field. The +shared implementation lives in `CompPoly.Fields.Montgomery.Native32Field`; this module +supplies the per-field `Mont32Field` instance (the five word constants plus the +`decide`-checked numeric facts) and pins `Field := Native32.FastField BabyBear.Field`, so +the generic definitions, proofs, and algebraic instances specialize to BabyBear. + +The Montgomery reducers are re-exported in `CompPoly.Fields.BabyBear.Fast.Montgomery`; +conversions in `...Fast.Convert`; the field operations and instances in +`CompPoly.Fields.BabyBear.Fast`. +-/ + +namespace BabyBear +namespace Fast + +open Montgomery.Native32 (Mont32Field FastField) + +/-- BabyBear modulus as a native word. -/ +def modulus : UInt32 := 0x78000001 + +/-- BabyBear modulus as a 64-bit word for modular reduction. -/ +def modulus64 : UInt64 := 0x78000001 + +/-- `2^32 mod BabyBear.fieldSize`. This is the Montgomery representation of one. -/ +def rModModulus : UInt32 := 0x0FFFFFFE + +/-- `(2^32)^2 mod BabyBear.fieldSize`, used to enter Montgomery representation. -/ +def r2ModModulus : UInt32 := 0x45DDDDE3 + +/-- `-BabyBear.fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ +def montgomeryNegInv : UInt32 := 0x77FFFFFF + +/-- The native `UInt32` modulus agrees with the mathematical BabyBear modulus. -/ +@[simp] theorem modulus_toNat : modulus.toNat = BabyBear.fieldSize := by decide + +/-- The native `UInt64` modulus agrees with the mathematical BabyBear modulus. -/ +@[simp] theorem modulus64_toNat : modulus64.toNat = BabyBear.fieldSize := by decide + +theorem fieldSize_pos : 0 < BabyBear.fieldSize := by decide + +theorem two_lt_fieldSize : 2 < BabyBear.fieldSize := by decide + +theorem fieldSize_lt_uint32Size : BabyBear.fieldSize < UInt32.size := by decide + +theorem fieldSize_add_fieldSize_lt_two64 : + BabyBear.fieldSize + BabyBear.fieldSize < 2 ^ 64 := by decide + +theorem fieldSize_add_fieldSize_lt_uint32Size : + BabyBear.fieldSize + BabyBear.fieldSize < UInt32.size := by decide + +theorem fieldSize_mul_fieldSize_lt_two64 : + BabyBear.fieldSize * BabyBear.fieldSize < 2 ^ 64 := by decide + +theorem uint32Size_lt_three_fieldSize : + UInt32.size < BabyBear.fieldSize + BabyBear.fieldSize + BabyBear.fieldSize := by decide + +theorem fieldSize_mul_uint32Size_lt_two64 : + BabyBear.fieldSize * UInt32.size < 2 ^ 64 := by decide + +theorem two_fieldSize_mul_uint32Size_lt_two64 : + 2 * BabyBear.fieldSize * UInt32.size < 2 ^ 64 := by decide + +theorem uint32Size_ne_zero_in_field : + (UInt32.size : BabyBear.Field) ≠ 0 := by decide + +theorem rModModulus_lt_fieldSize : rModModulus.toNat < BabyBear.fieldSize := by decide + +theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < BabyBear.fieldSize := by decide + +theorem rModModulus_cast : + (rModModulus.toNat : BabyBear.Field) = (UInt32.size : BabyBear.Field) := by decide + +theorem r2ModModulus_cast : + (r2ModModulus.toNat : BabyBear.Field) = (UInt32.size : BabyBear.Field) ^ 2 := by decide + +/-- The per-field data realizing BabyBear as a fast 32-bit-word Montgomery field. The five +word constants are the only runtime data; every other field is a `decide`-checked fact. -/ +instance instMont32Field : Mont32Field BabyBear.Field where + fieldSize := BabyBear.fieldSize + prime := inferInstance + modulus := modulus + modulus64 := modulus64 + rModModulus := rModModulus + r2ModModulus := r2ModModulus + montgomeryNegInv := montgomeryNegInv + modulus_toNat := modulus_toNat + modulus64_toNat := modulus64_toNat + fieldSize_pos := fieldSize_pos + two_lt_fieldSize := two_lt_fieldSize + fieldSize_lt_uint32Size := fieldSize_lt_uint32Size + fieldSize_add_fieldSize_lt_two64 := fieldSize_add_fieldSize_lt_two64 + fieldSize_add_fieldSize_lt_uint32Size := fieldSize_add_fieldSize_lt_uint32Size + fieldSize_mul_fieldSize_lt_two64 := fieldSize_mul_fieldSize_lt_two64 + uint32Size_lt_three_fieldSize := uint32Size_lt_three_fieldSize + fieldSize_mul_uint32Size_lt_two64 := fieldSize_mul_uint32Size_lt_two64 + two_fieldSize_mul_uint32Size_lt_two64 := two_fieldSize_mul_uint32Size_lt_two64 + uint32Size_ne_zero_in_field := uint32Size_ne_zero_in_field + rModModulus_lt_fieldSize := rModModulus_lt_fieldSize + r2ModModulus_lt_fieldSize := r2ModModulus_lt_fieldSize + rModModulus_cast := rModModulus_cast + r2ModModulus_cast := r2ModModulus_cast + negInv_congr := by decide + two_ne_zero_in_field := by decide + +/-- The fast native-word BabyBear field carrier, stored as a Montgomery residue. -/ +abbrev Field : Type := FastField BabyBear.Field + +/-- The raw Montgomery word backing a fast BabyBear element. -/ +@[inline] +def raw (x : Field) : UInt32 := x.val + +end Fast +end BabyBear diff --git a/CompPoly/Fields/KoalaBear/Fast.lean b/CompPoly/Fields/KoalaBear/Fast.lean index e35308d0..ea0f844b 100644 --- a/CompPoly/Fields/KoalaBear/Fast.lean +++ b/CompPoly/Fields/KoalaBear/Fast.lean @@ -4,1271 +4,185 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Valerii Huhnin -/ -import CompPoly.Fields.KoalaBear.Basic -import Mathlib.Algebra.Field.TransferInstance -import Mathlib.Data.Nat.ModEq +import CompPoly.Fields.KoalaBear.Fast.Convert /-! # Fast KoalaBear Field Operations -This module provides a native-word implementation of KoalaBear arithmetic as a sidecar -to the canonical `KoalaBear.Field := ZMod KoalaBear.fieldSize` model. +A native-word implementation of KoalaBear arithmetic as a sidecar to the canonical +`KoalaBear.Field := ZMod KoalaBear.fieldSize` model. Fast values are stored as Montgomery +`UInt32` residues below `KoalaBear.fieldSize`, representing `x * 2^32` modulo the prime. -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. +The operations, their `Field`/`CommRing`/`NonBinaryField` instances, the `toField` bridge, +and all correctness theorems are shared across every fast 32-bit-word field; they live once +in `CompPoly.Fields.Montgomery.Native32Field`, parameterized by the `Mont32Field` instance +in `CompPoly.Fields.KoalaBear.Fast.Prelude`. Because `Field := Native32.FastField KoalaBear.Field`, +the generic algebraic instances resolve here automatically. This module re-exports the +named operations and `simp` lemmas at the KoalaBear instance. -/ 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 - -/-- `2^32 mod KoalaBear.fieldSize`. This is the Montgomery representation of one. -/ -def rModModulus : UInt32 := 0x01FFFFFE - -/-- `(2^32)^2 mod KoalaBear.fieldSize`, used to enter Montgomery representation. -/ -def r2ModModulus : UInt32 := 0x17F7EFE4 - -/-- `-KoalaBear.fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ -def montgomeryNegInv : UInt32 := 0x7EFFFFFF - -/-- The 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 - -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) - -/-- Convert a 32-bit word into fast Montgomery representation. -/ -@[inline] -def ofUInt32 (x : UInt32) : Field := - reduceUInt64 x.toUInt64 - -/-- 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] - -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] +open Montgomery.Native32 /-- 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)) +def add (x y : Field) : Field := Montgomery.Native32.add x y /-- 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⟩ +def neg (x : Field) : Field := Montgomery.Native32.neg x /-- 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⟩ +def sub (x y : Field) : Field := Montgomery.Native32.sub x y /-- 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]) +def mul (x y : Field) : Field := Montgomery.Native32.mul x y /-- Fast squaring. -/ @[inline] -def square (x : Field) : Field := - mul x x +def square (x : Field) : Field := Montgomery.Native32.square x /-- Exponentiation over the fast representation using repeated squaring. -/ @[inline] -def pow (x : Field) (n : Nat) : Field := - @npowBinRec Field ⟨one⟩ ⟨mul⟩ n x +def pow (x : Field) (n : Nat) : Field := Montgomery.Native32.pow x n /-- Fermat exponent used for inversion in the KoalaBear prime field. -/ -def invExponent : Nat := KoalaBear.fieldSize - 2 +def invExponent : Nat := Montgomery.Native32.invExponent (F := KoalaBear.Field) -/-- Four squarings followed by multiplication by the next 4-bit exponent digit. -/ +/-- Inversion in Montgomery form via Fermat's little theorem (`x⁻¹ = x^(p-2)`). -/ @[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 +def inv (x : Field) : Field := Montgomery.Native32.inv x /-- 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 +def div (x y : Field) : Field := Montgomery.Native32.div x y -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) +/-- Ring equivalence between the fast Montgomery representation and canonical `KoalaBear.Field`. -/ +def ringEquiv : Field ≃+* KoalaBear.Field := + Montgomery.Native32.ringEquiv (F := KoalaBear.Field) /-- Converting from the canonical field to fast form and back is the identity. -/ @[simp] -theorem toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x := by - unfold ofField - rw [toField_ofCanonicalNat] - exact ZMod.natCast_zmod_val x +theorem toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x := + Montgomery.Native32.toField_ofField (F := KoalaBear.Field) x /-- Converting from fast form to the canonical field and back is the identity. -/ @[simp] -theorem ofField_toField (x : Field) : ofField (toField x) = x := 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] +theorem ofField_toField (x : Field) : ofField (toField x) = x := + Montgomery.Native32.ofField_toField x /-- The canonical-field interpretation distinguishes fast KoalaBear values. -/ -theorem toField_injective : Function.Injective toField := - Function.LeftInverse.injective ofField_toField +theorem toField_injective : Function.Injective (toField : Field → KoalaBear.Field) := + Montgomery.Native32.toField_injective (F := KoalaBear.Field) /-- `toField` maps fast zero to canonical zero. -/ @[simp] -theorem toField_zero : toField (0 : Field) = 0 := by - rw [toField_eq_raw_mul_inv] - change ((0 : Nat) : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ = 0 - exact zero_mul _ +theorem toField_zero : toField (0 : Field) = 0 := + Montgomery.Native32.toField_zero (F := KoalaBear.Field) /-- `toField` maps fast one to canonical one. -/ @[simp] -theorem toField_one : toField (1 : Field) = 1 := 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 +theorem toField_one : toField (1 : Field) = 1 := + Montgomery.Native32.toField_one (F := KoalaBear.Field) /-- Fast addition agrees with addition in the canonical KoalaBear field. -/ @[simp] -theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y := 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 +theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y := + Montgomery.Native32.toField_add x y /-- Fast subtraction agrees with subtraction in the canonical KoalaBear field. -/ @[simp] -theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y := 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 +theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y := + Montgomery.Native32.toField_sub x y /-- Fast negation agrees with negation in the canonical KoalaBear field. -/ @[simp] -theorem toField_neg (x : Field) : toField (-x) = -toField x := 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 +theorem toField_neg (x : Field) : toField (-x) = -toField x := + Montgomery.Native32.toField_neg x /-- Fast multiplication agrees with multiplication in the canonical KoalaBear field. -/ @[simp] -theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y := 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 - -/-- 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 +theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y := + Montgomery.Native32.toField_mul x y /-- Applying `ringEquiv` is the same as interpreting a fast value canonically. -/ @[simp] -theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x := rfl +theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x := + Montgomery.Native32.ringEquiv_apply x /-- Applying the inverse `ringEquiv` is conversion into fast Montgomery form. -/ @[simp] -theorem ringEquiv_symm_apply (x : KoalaBear.Field) : ringEquiv.symm x = ofField x := 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 +theorem ringEquiv_symm_apply (x : KoalaBear.Field) : ringEquiv.symm x = ofField x := + Montgomery.Native32.ringEquiv_symm_apply (F := KoalaBear.Field) x /-- Fast squaring agrees with multiplication by itself in the canonical field. -/ @[simp] -theorem toField_square (x : Field) : toField (square x) = toField x * toField x := 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 +theorem toField_square (x : Field) : toField (square x) = toField x * toField x := + Montgomery.Native32.toField_square x /-- Fast inversion agrees with inversion in the canonical KoalaBear field. -/ @[simp] -theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ := 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) +theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹ := + Montgomery.Native32.toField_inv x /-- Fast division agrees with division in the canonical KoalaBear field. -/ @[simp] -theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y := 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)) +theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y := + Montgomery.Native32.toField_div x y /-- Natural casts into fast form agree with natural casts into the canonical field. -/ @[simp] -theorem toField_natCast (n : Nat) : toField (n : Field) = (n : KoalaBear.Field) := by - change toField (ofNat n) = (n : KoalaBear.Field) - unfold ofNat - rw [toField_ofCanonicalNat] - rw [ZMod.natCast_eq_natCast_iff] - exact Nat.mod_modEq _ _ +theorem toField_natCast (n : Nat) : toField (n : Field) = (n : KoalaBear.Field) := + Montgomery.Native32.toField_natCast n /-- Integer casts into fast form agree with integer casts into the canonical field. -/ @[simp] -theorem toField_intCast (n : Int) : toField (n : Field) = (n : KoalaBear.Field) := by - change toField (ofInt n) = (n : KoalaBear.Field) - unfold ofInt - rw [toField_ofField] +theorem toField_intCast (n : Int) : toField (n : Field) = (n : KoalaBear.Field) := + Montgomery.Native32.toField_intCast n /-- Natural scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x := by - change toField ((n : Field) * x) = n • toField x - rw [toField_mul, toField_natCast] - rw [nsmul_eq_mul] +theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x := + Montgomery.Native32.toField_nsmul n x /-- Integer scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x := by - change toField ((n : Field) * x) = n • toField x - rw [toField_mul, toField_intCast] - rw [zsmul_eq_mul] +theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x := + Montgomery.Native32.toField_zsmul n x /-- Natural powers through the `Pow` instance are preserved by `toField`. -/ @[simp] -theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n := by - change toField (pow x n) = toField x ^ n - rw [toField_pow] +theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n := + Montgomery.Native32.toField_npow x n /-- Integer powers through the `Pow` instance are preserved by `toField`. -/ @[simp] -theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n := 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] +theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n := + Montgomery.Native32.toField_zpow x n /-- Nonnegative rational casts into fast form agree with canonical-field casts. -/ @[simp] -theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : KoalaBear.Field) := by - change toField (ofField (q : KoalaBear.Field)) = (q : KoalaBear.Field) - rw [toField_ofField] +theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : KoalaBear.Field) := + Montgomery.Native32.toField_nnratCast q /-- Rational casts into fast form agree with canonical-field casts. -/ @[simp] -theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : KoalaBear.Field) := by - change toField (ofField (q : KoalaBear.Field)) = (q : KoalaBear.Field) - rw [toField_ofField] +theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : KoalaBear.Field) := + Montgomery.Native32.toField_ratCast q /-- Nonnegative rational scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x := by - change toField (ofField (q • toField x)) = q • toField x - rw [toField_ofField] +theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x := + Montgomery.Native32.toField_nnqsmul q x /-- Rational scalar multiplication is preserved by `toField`. -/ @[simp] -theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x := 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) +theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x := + Montgomery.Native32.toField_qsmul q x end Fast end KoalaBear diff --git a/CompPoly/Fields/KoalaBear/Fast/Convert.lean b/CompPoly/Fields/KoalaBear/Fast/Convert.lean new file mode 100644 index 00000000..f2409532 --- /dev/null +++ b/CompPoly/Fields/KoalaBear/Fast/Convert.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 CompPoly Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Valerii Huhnin +-/ + +import CompPoly.Fields.KoalaBear.Fast.Montgomery + +/-! +# Fast KoalaBear Field — Conversions + +Conversions between the fast Montgomery representation and the canonical +`KoalaBear.Field` / `Nat` views, re-exported from the shared implementation in +`CompPoly.Fields.Montgomery.Native32Field` at the KoalaBear instance. +-/ + +namespace KoalaBear +namespace Fast + +open Montgomery.Native32 + +/-- Build a fast element from a canonical natural representative. -/ +@[inline] +def ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : Field := + Montgomery.Native32.ofCanonicalNat (F := KoalaBear.Field) n h + +/-- Reduce a `UInt64` modulo the KoalaBear prime and return a Montgomery fast element. -/ +@[inline] +def reduceUInt64 (x : UInt64) : Field := + Montgomery.Native32.reduceUInt64 (F := KoalaBear.Field) x + +/-- The zero fast KoalaBear element. -/ +def zero : Field := Montgomery.Native32.zero (F := KoalaBear.Field) + +/-- The one fast KoalaBear element. -/ +def one : Field := Montgomery.Native32.one (F := KoalaBear.Field) + +/-- Convert a natural number into fast Montgomery representation. -/ +@[inline] +def ofNat (n : Nat) : Field := + Montgomery.Native32.ofNat (F := KoalaBear.Field) n + +/-- Convert a 32-bit word into fast Montgomery representation. -/ +@[inline] +def ofUInt32 (x : UInt32) : Field := + Montgomery.Native32.ofUInt32 (F := KoalaBear.Field) x + +/-- Convert from the canonical `ZMod` KoalaBear field into fast Montgomery form. -/ +@[inline] +def ofField (x : KoalaBear.Field) : Field := + Montgomery.Native32.ofField (F := KoalaBear.Field) x + +/-- Convert an integer into fast Montgomery representation. -/ +@[inline] +def ofInt (n : Int) : Field := + Montgomery.Native32.ofInt (F := KoalaBear.Field) n + +/-- Convert a fast element to its canonical native-word representative. -/ +@[inline] +def toCanonicalUInt32 (x : Field) : UInt32 := + Montgomery.Native32.toCanonicalUInt32 x + +/-- Convert a fast KoalaBear element to its canonical natural representative. -/ +@[inline] +def toNat (x : Field) : Nat := + Montgomery.Native32.toNat x + +/-- Convert a fast KoalaBear element to the canonical `ZMod` KoalaBear field. -/ +@[inline] +def toField (x : Field) : KoalaBear.Field := + Montgomery.Native32.toField x + +theorem toNat_lt_fieldSize (x : Field) : toNat x < KoalaBear.fieldSize := + Montgomery.Native32.toNat_lt_fieldSize x + +theorem toField_eq_raw_mul_inv (x : Field) : + toField x = (x.val.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := + Montgomery.Native32.toField_eq_raw_mul_inv x + +theorem raw_cast_eq_toField_mul (x : Field) : + (x.val.toNat : KoalaBear.Field) = toField x * (UInt32.size : KoalaBear.Field) := + Montgomery.Native32.raw_cast_eq_toField_mul x + +theorem nat_eq_of_field_eq {a b : Nat} (ha : a < KoalaBear.fieldSize) + (hb : b < KoalaBear.fieldSize) (h : (a : KoalaBear.Field) = (b : KoalaBear.Field)) : + a = b := + Montgomery.Native32.nat_eq_of_field_eq (F := KoalaBear.Field) ha hb h + +theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < KoalaBear.fieldSize) : + ((ofCanonicalNat n h).val.toNat : KoalaBear.Field) = + (n : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) := + Montgomery.Native32.ofCanonicalNat_raw_cast (F := KoalaBear.Field) n h + +theorem reduceUInt64_raw_cast (x : UInt64) : + ((reduceUInt64 x).val.toNat : KoalaBear.Field) = + (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field) := + Montgomery.Native32.reduceUInt64_raw_cast x + +/-- Converting a canonical natural representative to fast form preserves its value. -/ +@[simp] +theorem toNat_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : + toNat (ofCanonicalNat n h) = n := + Montgomery.Native32.toNat_ofCanonicalNat n h + +/-- `ofCanonicalNat` embeds a canonical representative into the canonical field. -/ +@[simp] +theorem toField_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) : + toField (ofCanonicalNat n h) = (n : KoalaBear.Field) := + Montgomery.Native32.toField_ofCanonicalNat n h + +/-- Reducing a `UInt64` gives the canonical natural residue modulo KoalaBear. -/ +@[simp] +theorem toNat_reduceUInt64 (x : UInt64) : + toNat (reduceUInt64 x) = x.toNat % KoalaBear.fieldSize := + Montgomery.Native32.toNat_reduceUInt64 x + +/-- Reducing a `UInt64` agrees with casting that word into the canonical field. -/ +@[simp] +theorem toField_reduceUInt64 (x : UInt64) : + toField (reduceUInt64 x) = (x.toNat : KoalaBear.Field) := + Montgomery.Native32.toField_reduceUInt64 x + +end Fast +end KoalaBear diff --git a/CompPoly/Fields/KoalaBear/Fast/Montgomery.lean b/CompPoly/Fields/KoalaBear/Fast/Montgomery.lean new file mode 100644 index 00000000..4f9c94ca --- /dev/null +++ b/CompPoly/Fields/KoalaBear/Fast/Montgomery.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 CompPoly Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Valerii Huhnin +-/ + +import CompPoly.Fields.KoalaBear.Fast.Prelude + +/-! +# Fast KoalaBear Field — Montgomery Reduction + +The native-word Montgomery reducers specialized to KoalaBear. The definitions and their +correctness proofs are shared across every fast 32-bit-word field; they live once in +`CompPoly.Fields.Montgomery.Native32Field`, parameterized by the `Mont32Field` instance +supplied in `CompPoly.Fields.KoalaBear.Fast.Prelude`. This module just re-exports them at +the KoalaBear instance. Because the shared definitions are `@[inline]`, fixing the instance +folds the constants to literals: the compiled code is identical to a hand-written +monomorphic reducer, with no `Mont32Field` dictionary at runtime. +-/ + +namespace KoalaBear +namespace Fast + +open Montgomery.Native32 + +/-- Reduce a native word known to be below twice the KoalaBear prime. -/ +@[inline] +def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 := + Montgomery.Native32.reduceUInt32Lt2ModulusRaw (F := KoalaBear.Field) x + +theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) + (h : x.toNat < 2 * KoalaBear.fieldSize) : + (reduceUInt32Lt2ModulusRaw x).toNat < KoalaBear.fieldSize := + Montgomery.Native32.reduceUInt32Lt2ModulusRaw_lt (F := KoalaBear.Field) x h + +/-- Reduce a native word known to be below twice the KoalaBear prime. -/ +@[inline] +def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * KoalaBear.fieldSize) : + Field := + Montgomery.Native32.reduceUInt32Lt2Modulus (F := KoalaBear.Field) x h + +theorem reduceUInt32Lt2Modulus_cast (x : UInt32) + (h : x.toNat < 2 * KoalaBear.fieldSize) : + ((reduceUInt32Lt2Modulus x h).val.toNat : KoalaBear.Field) = + (x.toNat : KoalaBear.Field) := + Montgomery.Native32.reduceUInt32Lt2Modulus_cast (F := KoalaBear.Field) x h + +/-- Reduce a native word below `2^32` modulo the KoalaBear prime. -/ +@[inline] +def reduceUInt32 (x : UInt32) : Field := + Montgomery.Native32.reduceUInt32 (F := KoalaBear.Field) x + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ +@[inline] +def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 := + Montgomery.Native32.montgomeryReduceBoundedRaw (F := KoalaBear.Field) x + +theorem montgomeryReduceBoundedRaw_lt (x : UInt64) + (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : + (montgomeryReduceBoundedRaw x).toNat < KoalaBear.fieldSize := + Montgomery.Native32.montgomeryReduceBoundedRaw_lt (F := KoalaBear.Field) x h + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ +@[inline] +def montgomeryReduceBounded (x : UInt64) + (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : Field := + Montgomery.Native32.montgomeryReduceBounded (F := KoalaBear.Field) x h + +theorem montgomeryReduceBounded_cast (x : UInt64) + (h : x.toNat < KoalaBear.fieldSize * UInt32.size) : + ((montgomeryReduceBounded x h).val.toNat : KoalaBear.Field) = + (x.toNat : KoalaBear.Field) * (UInt32.size : KoalaBear.Field)⁻¹ := + Montgomery.Native32.montgomeryReduceBounded_cast (F := KoalaBear.Field) x h + +/-- Montgomery reduction of a 64-bit word. Hot bounded callers use `montgomeryReduceBounded`. -/ +@[inline] +def montgomeryReduce (x : UInt64) : Field := + Montgomery.Native32.montgomeryReduce (F := KoalaBear.Field) x + +end Fast +end KoalaBear diff --git a/CompPoly/Fields/KoalaBear/Fast/Prelude.lean b/CompPoly/Fields/KoalaBear/Fast/Prelude.lean new file mode 100644 index 00000000..0317685d --- /dev/null +++ b/CompPoly/Fields/KoalaBear/Fast/Prelude.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 CompPoly Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Valerii Huhnin +-/ + +import CompPoly.Fields.KoalaBear.Basic +import CompPoly.Fields.Montgomery.Native32Field + +/-! +# Fast KoalaBear Field — Basics + +The native-word constants and the `Field` carrier type for the fast KoalaBear field. The +shared implementation lives in `CompPoly.Fields.Montgomery.Native32Field`; this module +supplies the per-field `Mont32Field` instance (the five word constants plus the +`decide`-checked numeric facts) and pins `Field := Native32.FastField KoalaBear.Field`, so +the generic definitions, proofs, and algebraic instances specialize to KoalaBear. + +The Montgomery reducers are re-exported in `CompPoly.Fields.KoalaBear.Fast.Montgomery`; +conversions in `...Fast.Convert`; the field operations and instances in +`CompPoly.Fields.KoalaBear.Fast`. +-/ + +namespace KoalaBear +namespace Fast + +open Montgomery.Native32 (Mont32Field FastField) + +/-- KoalaBear modulus as a native word. -/ +def modulus : UInt32 := 0x7F000001 + +/-- KoalaBear modulus as a 64-bit word for modular reduction. -/ +def modulus64 : UInt64 := 0x7F000001 + +/-- `2^32 mod KoalaBear.fieldSize`. This is the Montgomery representation of one. -/ +def rModModulus : UInt32 := 0x01FFFFFE + +/-- `(2^32)^2 mod KoalaBear.fieldSize`, used to enter Montgomery representation. -/ +def r2ModModulus : UInt32 := 0x17F7EFE4 + +/-- `-KoalaBear.fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ +def montgomeryNegInv : UInt32 := 0x7EFFFFFF + +/-- The native `UInt32` modulus agrees with the mathematical KoalaBear modulus. -/ +@[simp] theorem modulus_toNat : modulus.toNat = KoalaBear.fieldSize := by decide + +/-- The native `UInt64` modulus agrees with the mathematical KoalaBear modulus. -/ +@[simp] theorem modulus64_toNat : modulus64.toNat = KoalaBear.fieldSize := by decide + +theorem fieldSize_pos : 0 < KoalaBear.fieldSize := by decide + +theorem two_lt_fieldSize : 2 < KoalaBear.fieldSize := by decide + +theorem fieldSize_lt_uint32Size : KoalaBear.fieldSize < UInt32.size := by decide + +theorem fieldSize_add_fieldSize_lt_two64 : + KoalaBear.fieldSize + KoalaBear.fieldSize < 2 ^ 64 := by decide + +theorem fieldSize_add_fieldSize_lt_uint32Size : + KoalaBear.fieldSize + KoalaBear.fieldSize < UInt32.size := by decide + +theorem fieldSize_mul_fieldSize_lt_two64 : + KoalaBear.fieldSize * KoalaBear.fieldSize < 2 ^ 64 := by decide + +theorem uint32Size_lt_three_fieldSize : + UInt32.size < KoalaBear.fieldSize + KoalaBear.fieldSize + KoalaBear.fieldSize := by decide + +theorem fieldSize_mul_uint32Size_lt_two64 : + KoalaBear.fieldSize * UInt32.size < 2 ^ 64 := by decide + +theorem two_fieldSize_mul_uint32Size_lt_two64 : + 2 * KoalaBear.fieldSize * UInt32.size < 2 ^ 64 := by decide + +theorem uint32Size_ne_zero_in_field : + (UInt32.size : KoalaBear.Field) ≠ 0 := by decide + +theorem rModModulus_lt_fieldSize : rModModulus.toNat < KoalaBear.fieldSize := by decide + +theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < KoalaBear.fieldSize := by decide + +theorem rModModulus_cast : + (rModModulus.toNat : KoalaBear.Field) = (UInt32.size : KoalaBear.Field) := by decide + +theorem r2ModModulus_cast : + (r2ModModulus.toNat : KoalaBear.Field) = (UInt32.size : KoalaBear.Field) ^ 2 := by decide + +/-- The per-field data realizing KoalaBear as a fast 32-bit-word Montgomery field. The five +word constants are the only runtime data; every other field is a `decide`-checked fact. -/ +instance instMont32Field : Mont32Field KoalaBear.Field where + fieldSize := KoalaBear.fieldSize + prime := inferInstance + modulus := modulus + modulus64 := modulus64 + rModModulus := rModModulus + r2ModModulus := r2ModModulus + montgomeryNegInv := montgomeryNegInv + modulus_toNat := modulus_toNat + modulus64_toNat := modulus64_toNat + fieldSize_pos := fieldSize_pos + two_lt_fieldSize := two_lt_fieldSize + fieldSize_lt_uint32Size := fieldSize_lt_uint32Size + fieldSize_add_fieldSize_lt_two64 := fieldSize_add_fieldSize_lt_two64 + fieldSize_add_fieldSize_lt_uint32Size := fieldSize_add_fieldSize_lt_uint32Size + fieldSize_mul_fieldSize_lt_two64 := fieldSize_mul_fieldSize_lt_two64 + uint32Size_lt_three_fieldSize := uint32Size_lt_three_fieldSize + fieldSize_mul_uint32Size_lt_two64 := fieldSize_mul_uint32Size_lt_two64 + two_fieldSize_mul_uint32Size_lt_two64 := two_fieldSize_mul_uint32Size_lt_two64 + uint32Size_ne_zero_in_field := uint32Size_ne_zero_in_field + rModModulus_lt_fieldSize := rModModulus_lt_fieldSize + r2ModModulus_lt_fieldSize := r2ModModulus_lt_fieldSize + rModModulus_cast := rModModulus_cast + r2ModModulus_cast := r2ModModulus_cast + negInv_congr := by decide + two_ne_zero_in_field := by decide + +/-- The fast native-word KoalaBear field carrier, stored as a Montgomery residue. -/ +abbrev Field : Type := FastField KoalaBear.Field + +/-- The raw Montgomery word backing a fast KoalaBear element. -/ +@[inline] +def raw (x : Field) : UInt32 := x.val + +end Fast +end KoalaBear diff --git a/CompPoly/Fields/Montgomery/Basic.lean b/CompPoly/Fields/Montgomery/Basic.lean new file mode 100644 index 00000000..e6a8bce1 --- /dev/null +++ b/CompPoly/Fields/Montgomery/Basic.lean @@ -0,0 +1,120 @@ +/- +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 core + +Field-agnostic number theory behind native-word Montgomery reduction, shared by every +fast prime field. Everything here is parameterized by an abstract radix `R : Nat` (the +Montgomery modulus, e.g. `2^32` for 32-bit-word fields) and the prime `p`; the proofs use +only that `gcd(R, p) = 1` — supplied as the congruence `negInv * p ≡ R - 1 [MOD R]` — and +that `0 < R`, so nothing here is tied to a particular word size. + +The concrete word-level bridges (e.g. the `UInt32 × UInt64`, `R = 2^32` reduction) live in +sibling modules such as `CompPoly.Fields.Montgomery.Native32`, which instantiate `R` and +call into this core. These lemmas are all `Prop`/spec level and erased at codegen, so +sharing them carries no runtime cost. +-/ + +namespace Montgomery + +/-- The Montgomery divisibility identity: if `negInv * p ≡ R - 1 [MOD R]` (i.e. +`negInv = -p⁻¹ mod R`), then `R ∣ x + ((x mod R)·negInv mod R)·p` for every `x`. This is +what makes Montgomery reduction integer-valued. -/ +theorem sum_dvd (R p negInv : Nat) (hR : 0 < R) + (hp : negInv * p ≡ R - 1 [MOD R]) (x : Nat) : + R ∣ x + ((x % R * negInv) % R) * p := by + rw [← Nat.modEq_zero_iff_dvd] + have hx : x ≡ x % R [MOD R] := (Nat.mod_modEq x R).symm + have hm : + ((x % R * negInv) % R) * p ≡ (x % R) * (R - 1) [MOD R] := by + have hmi : + (x % R * negInv) % R ≡ x % R * negInv [MOD R] := Nat.mod_modEq _ _ + calc + ((x % R * negInv) % R) * p + ≡ (x % R * negInv) * p [MOD R] := hmi.mul_right _ + _ = x % R * (negInv * p) := by ring + _ ≡ x % R * (R - 1) [MOD R] := hp.mul_left _ + calc + x + ((x % R * negInv) % R) * p + ≡ x % R + x % R * (R - 1) [MOD R] := hx.add hm + _ = x % R * R := by + rw [add_comm, ← Nat.mul_succ] + have hsucc : (R - 1).succ = R := by omega + rw [hsucc] + _ ≡ 0 [MOD R] := by + rw [Nat.modEq_zero_iff_dvd] + exact ⟨x % R, by rw [mul_comm]⟩ + +/-- Nat-level Montgomery reduction: specifies and is used to prove the native-word reducer. -/ +def reduceNat (R p negInv x : Nat) : Nat := + let m := (x % R * negInv) % R + let u := (x + m * p) / R + if u < p then u else u - p + +/-- Montgomery reduction descends to "multiply by `R⁻¹`" in `ZMod p`. -/ +theorem reduceNat_cast (R p negInv : Nat) [Fact (Nat.Prime p)] (hR : 0 < R) + (hp : negInv * p ≡ R - 1 [MOD R]) (hRne : (R : ZMod p) ≠ 0) (x : Nat) : + (reduceNat R p negInv x : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by + let m := x % R * negInv % R + let u := (x + m * p) / R + have hdiv : R ∣ x + m * p := by + simpa [m] using sum_dvd R p negInv hR hp x + have hu_mul : u * R = x + m * p := Nat.div_mul_cancel hdiv + have hcast_mul : (u : ZMod p) * (R : ZMod p) = (x : ZMod p) := by + rw [← Nat.cast_mul, hu_mul, Nat.cast_add, Nat.cast_mul] + simp + by_cases hu : u < p + · have hmain : (u : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by + rw [← hcast_mul] + refine (mul_inv_cancel_right₀ ?_ (u : ZMod p)).symm + exact hRne + dsimp only [reduceNat] + rw [if_pos hu] + exact hmain + · have hfield : ((u - p : Nat) : ZMod p) = (u : ZMod p) := by + rw [Nat.cast_sub (Nat.le_of_not_gt hu)] + simp + have hmain : ((u - p : Nat) : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ := by + rw [hfield, ← hcast_mul] + refine (mul_inv_cancel_right₀ ?_ (u : ZMod p)).symm + exact hRne + dsimp only [reduceNat] + rw [if_neg hu] + exact hmain + +/-- The pre-conditional-subtract Montgomery quotient already casts to "multiply by `R⁻¹`" +in `ZMod p`. -/ +theorem quotient_cast (R p negInv : Nat) [Fact (Nat.Prime p)] (hR : 0 < R) + (hp : negInv * p ≡ R - 1 [MOD R]) (hRne : (R : ZMod p) ≠ 0) (x : Nat) : + (let m := x % R * negInv % R + let u := (x + m * p) / R + (u : ZMod p)) = (x : ZMod p) * (R : ZMod p)⁻¹ := by + let m := x % R * negInv % R + let u := (x + m * p) / R + have hmr := reduceNat_cast R p negInv hR hp hRne x + unfold reduceNat at hmr + change (u : ZMod p) = (x : ZMod p) * (R : ZMod p)⁻¹ + by_cases hu : u < p + · simpa only [m, u, hu, if_true] using hmr + · have hfield : ((u - p : Nat) : ZMod p) = (u : ZMod p) := by + rw [Nat.cast_sub (Nat.le_of_not_gt hu)] + simp + rw [← hfield] + simpa only [m, u, hu, if_false] using hmr + +/-- Two naturals below `p` are equal once their `ZMod p` casts agree. -/ +theorem natCast_inj {p a b : Nat} (ha : a < p) (hb : b < p) + (h : (a : ZMod p) = (b : ZMod p)) : a = b := by + 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..9cd9df29 --- /dev/null +++ b/CompPoly/Fields/Montgomery/Native32.lean @@ -0,0 +1,74 @@ +/- +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 + +/-! +# Montgomery Reduction — native `UInt32 × UInt64`, radix `R = 2^32` + +The word-level bridge specialising `Montgomery.Basic` to 32-bit-word prime fields: the +Montgomery product fits in a `UInt64`, the radix is `R = UInt32.size = 2^32`, and the +high word is extracted with `>>> 32`. These lemmas relate the native-word computation to +the `Nat` formula proved generically in `Montgomery.Basic`, parameterized by the prime +`p`, the `UInt32` negated inverse `negInv`, and the `UInt64` modulus `modN`. + +A future 64-bit family would add a parallel `Native64` bridge (`>>> 64`, +`UInt64 × UInt128`) over the same `Montgomery.Basic` core. +-/ + +namespace Montgomery +namespace Native32 + +/-- The native high-word extraction agrees with the `Nat`-level Montgomery quotient. -/ +theorem u_eq_nat (negInv : UInt32) (modN : UInt64) (p : Nat) + (hmod : modN.toNat = p) (hp_pos : 0 < p) + (hbound : 2 * p * UInt32.size < 2 ^ 64) + (x : UInt64) (h : x.toNat < p * UInt32.size) : + ((((x + (x.toUInt32 * negInv).toUInt64 * modN) >>> 32).toUInt32).toNat) = + (x.toNat + ((x.toNat % UInt32.size * negInv.toNat) % UInt32.size) * p) / UInt32.size := by + simp only [UInt64.toNat_shiftRight, UInt64.toNat_toUInt32, UInt64.toNat_add, + UInt64.toNat_mul, UInt32.toNat_toUInt64, UInt32.toNat_mul, UInt64.toNat_ofNat, + hmod, Nat.shiftRight_eq_div_pow] + norm_num [UInt32.size] at h hbound ⊢ + let mNat := x.toNat * negInv.toNat % 4294967296 + have hm_lt : mNat < 4294967296 := Nat.mod_lt _ (by decide) + have hsum_lt : x.toNat + mNat * p < 18446744073709551616 := by + have hprod_lt : mNat * p < p * 4294967296 := by + have := Nat.mul_lt_mul_of_pos_right hm_lt hp_pos + simpa [Nat.mul_comm] using this + calc x.toNat + mNat * p < p * 4294967296 + p * 4294967296 := Nat.add_lt_add h hprod_lt + _ = 2 * p * 4294967296 := by ring + _ < 18446744073709551616 := hbound + change ((x.toNat + mNat * p) % 18446744073709551616 / 4294967296) % 4294967296 = + (x.toNat + mNat * p) / 4294967296 + rw [Nat.mod_eq_of_lt hsum_lt] + rw [Nat.mod_eq_of_lt] + rw [Nat.div_lt_iff_lt_mul] + · exact hsum_lt + · decide + +/-- The native Montgomery quotient stays below `2 * p`, so a single conditional subtract +canonicalises it. -/ +theorem u_lt_two_mul (negInv : UInt32) (modN : UInt64) (p : Nat) + (hmod : modN.toNat = p) (hp_pos : 0 < p) + (hbound : 2 * p * UInt32.size < 2 ^ 64) + (x : UInt64) (h : x.toNat < p * UInt32.size) : + ((((x + (x.toUInt32 * negInv).toUInt64 * modN) >>> 32).toUInt32).toNat) < 2 * p := by + rw [u_eq_nat negInv modN p hmod hp_pos hbound x h] + let mNat := x.toNat % UInt32.size * negInv.toNat % UInt32.size + have hm_lt : mNat < UInt32.size := Nat.mod_lt _ (by decide) + rw [Nat.div_lt_iff_lt_mul] + · have hprod_lt : mNat * p < UInt32.size * p := Nat.mul_lt_mul_of_pos_right hm_lt hp_pos + have hprod_lt' : mNat * p < p * UInt32.size := by + simpa [Nat.mul_comm] using hprod_lt + change x.toNat + mNat * p < 2 * p * UInt32.size + calc x.toNat + mNat * p < p * UInt32.size + p * UInt32.size := + Nat.add_lt_add h hprod_lt' + _ = 2 * p * UInt32.size := by ring + · decide + +end Native32 +end Montgomery diff --git a/CompPoly/Fields/Montgomery/Native32Field.lean b/CompPoly/Fields/Montgomery/Native32Field.lean new file mode 100644 index 00000000..88f0e9a4 --- /dev/null +++ b/CompPoly/Fields/Montgomery/Native32Field.lean @@ -0,0 +1,996 @@ +/- +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 + +/-! +# Fast 32-bit-word prime fields — shared implementation + +A `BabyBear`-style and `KoalaBear`-style fast field differ only in a handful of word +constants; their definitions, the proofs about them, and the resulting algebraic instances +are otherwise identical. This module captures that common content **once**, parameterized +by a `Mont32Field` instance that supplies the per-field data. + +* `Mont32Field F` bundles the prime (`fieldSize`), its native-word forms, the Montgomery + constants, and the small `decide`-checkable numeric/`ZMod` facts the proofs consume. + Everything except the five word constants is spec-level and erased at codegen. +* `FastField F` is the fast carrier `{ x : UInt32 // x.toNat < fieldSize }`, indexed by the + tag `F` so that the generic `Add`/`Mul`/`Field`/… instances below resolve for each + concrete field's `Field := FastField `. At runtime it erases to `UInt32`. +* The executable `def`s are `@[inline]`/`@[specialize]`, so once a concrete instance is + fixed the instance projections fold to literals and the compiled code is identical to a + hand-written monomorphic version — no `Mont32Field` dictionary survives to runtime. + +The radix-generic number theory lives in `CompPoly.Fields.Montgomery.Basic` and the +`R = 2^32` word bridge in `CompPoly.Fields.Montgomery.Native32`. A concrete fast field is +then just a `Mont32Field` instance plus thin re-export shims. +-/ + +namespace Montgomery +namespace Native32 + +/-- Per-field data for a fast 32-bit-word Montgomery prime field. + +The five word constants (`modulus`, `modulus64`, `rModModulus`, `r2ModModulus`, +`montgomeryNegInv`) are the only runtime data; the remaining fields are `Prop`s, all +dischargeable by `decide` for a concrete field, and are erased at codegen. `F` is a tag +(in practice the canonical `ZMod fieldSize` field) used for instance resolution. -/ +class Mont32Field (F : Type) where + /-- The field size / prime `p`. -/ + fieldSize : Nat + /-- `fieldSize` is prime — needed to reduce into `ZMod fieldSize` as a field. -/ + prime : Fact (Nat.Prime fieldSize) + /-- `fieldSize` as a 32-bit word. -/ + modulus : UInt32 + /-- `fieldSize` as a 64-bit word. -/ + modulus64 : UInt64 + /-- `2^32 mod fieldSize`, the Montgomery representation of one. -/ + rModModulus : UInt32 + /-- `(2^32)^2 mod fieldSize`, used to enter Montgomery form. -/ + r2ModModulus : UInt32 + /-- `-fieldSize⁻¹ mod 2^32`, used by Montgomery reduction. -/ + montgomeryNegInv : UInt32 + modulus_toNat : modulus.toNat = fieldSize + modulus64_toNat : modulus64.toNat = fieldSize + fieldSize_pos : 0 < fieldSize + two_lt_fieldSize : 2 < fieldSize + fieldSize_lt_uint32Size : fieldSize < UInt32.size + fieldSize_add_fieldSize_lt_two64 : fieldSize + fieldSize < 2 ^ 64 + fieldSize_add_fieldSize_lt_uint32Size : fieldSize + fieldSize < UInt32.size + fieldSize_mul_fieldSize_lt_two64 : fieldSize * fieldSize < 2 ^ 64 + uint32Size_lt_three_fieldSize : UInt32.size < fieldSize + fieldSize + fieldSize + fieldSize_mul_uint32Size_lt_two64 : fieldSize * UInt32.size < 2 ^ 64 + two_fieldSize_mul_uint32Size_lt_two64 : 2 * fieldSize * UInt32.size < 2 ^ 64 + uint32Size_ne_zero_in_field : (UInt32.size : ZMod fieldSize) ≠ 0 + rModModulus_lt_fieldSize : rModModulus.toNat < fieldSize + r2ModModulus_lt_fieldSize : r2ModModulus.toNat < fieldSize + rModModulus_cast : (rModModulus.toNat : ZMod fieldSize) = (UInt32.size : ZMod fieldSize) + r2ModModulus_cast : + (r2ModModulus.toNat : ZMod fieldSize) = (UInt32.size : ZMod fieldSize) ^ 2 + /-- The Montgomery inverse congruence `negInv * p ≡ 2^32 - 1 [MOD 2^32]`. -/ + negInv_congr : + montgomeryNegInv.toNat * fieldSize ≡ UInt32.size - 1 [MOD UInt32.size] + /-- Characteristic `≠ 2`, used to build the `NonBinaryField` instance. -/ + two_ne_zero_in_field : (2 : ZMod fieldSize) ≠ 0 + +attribute [instance] Mont32Field.prime + +/-- The fast carrier for the field tagged by `F`: a native word below `fieldSize`, +interpreted as a Montgomery residue. At runtime this erases to `UInt32`. -/ +def FastField (F : Type) [Mont32Field F] : Type := + { x : UInt32 // x.toNat < Mont32Field.fieldSize F } + +instance (F : Type) [Mont32Field F] : DecidableEq (FastField F) := + inferInstanceAs (DecidableEq { x : UInt32 // x.toNat < Mont32Field.fieldSize F }) + +section +variable {F : Type} [P : Mont32Field F] + +instance : NeZero P.fieldSize := ⟨P.fieldSize_pos.ne'⟩ + +/-- The raw Montgomery word backing a fast element. -/ +@[inline] +def raw (x : FastField F) : UInt32 := x.val + +/-! ## Montgomery reduction -/ + +/-- Reduce a native word known to be below twice the prime. -/ +@[inline] +def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32 := + if x < P.modulus then x else x - P.modulus + +theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32) + (h : x.toNat < 2 * P.fieldSize) : + (reduceUInt32Lt2ModulusRaw (F := F) x).toNat < P.fieldSize := by + unfold reduceUInt32Lt2ModulusRaw + by_cases hx : x < P.modulus + · rw [if_pos hx] + rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx + exact hx + · rw [if_neg hx] + have hmod_le_x : P.modulus ≤ x := by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] + rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx + exact Nat.le_of_not_gt hx + rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, P.modulus_toNat] + omega + +/-- Reduce a native word known to be below twice the prime. -/ +@[inline] +def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * P.fieldSize) : + FastField F := + ⟨reduceUInt32Lt2ModulusRaw (F := F) x, reduceUInt32Lt2ModulusRaw_lt x h⟩ + +theorem reduceUInt32Lt2Modulus_cast (x : UInt32) + (h : x.toNat < 2 * P.fieldSize) : + ((reduceUInt32Lt2Modulus (F := F) x h).val.toNat : ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) := by + change ((reduceUInt32Lt2ModulusRaw (F := F) x).toNat : ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) + unfold reduceUInt32Lt2ModulusRaw + by_cases hx : x < P.modulus + · rw [if_pos hx] + · have hmod_le_x : P.modulus ≤ x := by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] + rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx + exact Nat.le_of_not_gt hx + rw [if_neg hx] + rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, P.modulus_toNat] + rw [Nat.cast_sub (by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] at hmod_le_x + exact hmod_le_x)] + simp + +/-- Reduce a native word below `2^32` modulo the prime. -/ +@[inline] +def reduceUInt32 (x : UInt32) : FastField F := + if hx : x < P.modulus then + ⟨x, by + rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx + exact hx⟩ + else + let y := x - P.modulus + if hy : y < P.modulus then + ⟨y, by + rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hy + exact hy⟩ + else + ⟨y - P.modulus, by + have hmod_le_x : P.modulus ≤ x := by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] + rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hx + exact Nat.le_of_not_gt hx + have hy_eq : y.toNat = x.toNat - P.fieldSize := by + change (x - P.modulus).toNat = x.toNat - P.fieldSize + rw [UInt32.toNat_sub_of_le _ _ hmod_le_x, P.modulus_toNat] + have hmod_le_y : P.modulus ≤ y := by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] + rw [UInt32.lt_iff_toNat_lt, P.modulus_toNat] at hy + exact Nat.le_of_not_gt hy + rw [UInt32.toNat_sub_of_le _ _ hmod_le_y, P.modulus_toNat, hy_eq] + have hx_lt := UInt32.toNat_lt_size x + have hthree := P.uint32Size_lt_three_fieldSize + omega⟩ + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ +@[inline] +def montgomeryReduceBoundedRaw (x : UInt64) : UInt32 := + let m : UInt32 := x.toUInt32 * P.montgomeryNegInv + let u : UInt32 := ((x + m.toUInt64 * P.modulus64) >>> 32).toUInt32 + reduceUInt32Lt2ModulusRaw (F := F) u + +theorem montgomeryReduceBoundedRaw_lt (x : UInt64) + (h : x.toNat < P.fieldSize * UInt32.size) : + (montgomeryReduceBoundedRaw (F := F) x).toNat < P.fieldSize := by + unfold montgomeryReduceBoundedRaw + exact reduceUInt32Lt2ModulusRaw_lt _ + (Montgomery.Native32.u_lt_two_mul P.montgomeryNegInv P.modulus64 P.fieldSize + P.modulus64_toNat P.fieldSize_pos P.two_fieldSize_mul_uint32Size_lt_two64 x h) + +/-- Montgomery reduction for inputs known to be below `p * 2^32`. -/ +@[inline] +def montgomeryReduceBounded (x : UInt64) + (h : x.toNat < P.fieldSize * UInt32.size) : FastField F := + ⟨montgomeryReduceBoundedRaw (F := F) x, montgomeryReduceBoundedRaw_lt x h⟩ + +theorem montgomeryReduceBounded_cast (x : UInt64) + (h : x.toNat < P.fieldSize * UInt32.size) : + ((montgomeryReduceBounded (F := F) x h).val.toNat : ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ := by + change ((montgomeryReduceBoundedRaw (F := F) x).toNat : ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + unfold montgomeryReduceBoundedRaw + let m : UInt32 := x.toUInt32 * P.montgomeryNegInv + let u : UInt32 := ((x + m.toUInt64 * P.modulus64) >>> 32).toUInt32 + change ((reduceUInt32Lt2ModulusRaw (F := F) u).toNat : ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + have hred := reduceUInt32Lt2Modulus_cast (F := F) u + (Montgomery.Native32.u_lt_two_mul P.montgomeryNegInv P.modulus64 P.fieldSize + P.modulus64_toNat P.fieldSize_pos P.two_fieldSize_mul_uint32Size_lt_two64 x h) + change ((reduceUInt32Lt2ModulusRaw (F := F) u).toNat : ZMod P.fieldSize) = + (u.toNat : ZMod P.fieldSize) at hred + rw [hred] + change (u.toNat : ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + rw [show u.toNat = + (x.toNat + ((x.toNat % UInt32.size * P.montgomeryNegInv.toNat) % UInt32.size) * + P.fieldSize) / UInt32.size by + exact Montgomery.Native32.u_eq_nat P.montgomeryNegInv P.modulus64 P.fieldSize + P.modulus64_toNat P.fieldSize_pos P.two_fieldSize_mul_uint32Size_lt_two64 x h] + exact Montgomery.quotient_cast UInt32.size P.fieldSize P.montgomeryNegInv.toNat + (by decide) P.negInv_congr P.uint32Size_ne_zero_in_field x.toNat + +/-- Montgomery reduction of a 64-bit word. Hot bounded callers use `montgomeryReduceBounded`. -/ +@[inline] +def montgomeryReduce (x : UInt64) : FastField F := + let m : UInt32 := x.toUInt32 * P.montgomeryNegInv + let u : UInt32 := ((x + m.toUInt64 * P.modulus64) >>> 32).toUInt32 + reduceUInt32 (F := F) u + +/-! ## Conversions -/ + +/-- Build a fast element from a canonical natural representative. -/ +@[inline] +def ofCanonicalNat (n : Nat) (_h : n < P.fieldSize) : FastField F := + montgomeryReduceBounded (UInt64.ofNat n * P.r2ModModulus.toUInt64) (by + rw [UInt64.toNat_mul, UInt64.toNat_ofNat', UInt32.toNat_toUInt64] + have hnmod : n % 2 ^ 64 = n := by + apply Nat.mod_eq_of_lt + exact Nat.lt_trans _h (Nat.lt_trans P.fieldSize_lt_uint32Size (by decide)) + rw [hnmod] + have hprod : n * P.r2ModModulus.toNat < 2 ^ 64 := by + nlinarith [P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [P.r2ModModulus_lt_fieldSize]) + +/-- Reduce a `UInt64` modulo the prime and return a Montgomery fast element. -/ +@[inline] +def reduceUInt64 (x : UInt64) : FastField F := + let y := x % P.modulus64 + montgomeryReduceBounded (y * P.r2ModModulus.toUInt64) (by + rw [UInt64.toNat_mul, UInt32.toNat_toUInt64] + have hy_lt : (x % P.modulus64).toNat < P.fieldSize := by + rw [UInt64.toNat_mod, P.modulus64_toNat] + exact Nat.mod_lt _ P.fieldSize_pos + have hprod : (x % P.modulus64).toNat * P.r2ModModulus.toNat < 2 ^ 64 := by + nlinarith [hy_lt, P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [P.r2ModModulus_lt_fieldSize]) + +/-- The zero fast element. -/ +def zero : FastField F := ⟨0, by + have h0 : (0 : UInt32).toNat = 0 := by decide + have hp := P.fieldSize_pos + omega⟩ + +/-- The one fast element. -/ +def one : FastField F := ⟨P.rModModulus, P.rModModulus_lt_fieldSize⟩ + +/-- Convert a natural number into fast Montgomery representation. -/ +@[inline] +def ofNat (n : Nat) : FastField F := + ofCanonicalNat (n % P.fieldSize) (Nat.mod_lt _ P.fieldSize_pos) + +/-- Convert a 32-bit word into fast Montgomery representation. -/ +@[inline] +def ofUInt32 (x : UInt32) : FastField F := + reduceUInt64 x.toUInt64 + +/-- Convert from the canonical `ZMod` field into fast Montgomery form. -/ +@[inline] +def ofField (x : ZMod P.fieldSize) : FastField F := + ofCanonicalNat x.val (ZMod.val_lt x) + +/-- Convert an integer into fast Montgomery representation. -/ +@[inline] +def ofInt (n : Int) : FastField F := + ofField (n : ZMod P.fieldSize) + +/-- Convert a fast element to its canonical native-word representative. -/ +@[inline] +def toCanonicalUInt32 (x : FastField F) : UInt32 := + raw (montgomeryReduceBounded x.val.toUInt64 (by + rw [UInt32.toNat_toUInt64] + nlinarith [x.property, P.fieldSize_pos])) + +/-- Convert a fast element to its canonical natural representative. -/ +@[inline] +def toNat (x : FastField F) : Nat := + (toCanonicalUInt32 x).toNat + +/-- Convert a fast element to the canonical `ZMod` field. -/ +@[inline] +def toField (x : FastField F) : ZMod P.fieldSize := + (toNat x : ZMod P.fieldSize) + +theorem toNat_lt_fieldSize (x : FastField F) : toNat x < P.fieldSize := by + unfold toNat toCanonicalUInt32 raw + change (montgomeryReduceBoundedRaw (F := F) x.val.toUInt64).toNat < P.fieldSize + exact montgomeryReduceBoundedRaw_lt x.val.toUInt64 (by + rw [UInt32.toNat_toUInt64] + nlinarith [x.property, P.fieldSize_pos]) + +theorem toField_eq_raw_mul_inv (x : FastField F) : + toField x = + (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ := by + unfold toField toNat toCanonicalUInt32 raw + have hred := montgomeryReduceBounded_cast x.val.toUInt64 (by + rw [UInt32.toNat_toUInt64] + nlinarith [x.property, P.fieldSize_pos]) + change ((montgomeryReduceBoundedRaw (F := F) x.val.toUInt64).toNat : ZMod P.fieldSize) = + (x.val.toUInt64.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ at hred + change ((montgomeryReduceBoundedRaw (F := F) x.val.toUInt64).toNat : ZMod P.fieldSize) = + (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + rw [hred] + rw [UInt32.toNat_toUInt64] + +theorem raw_cast_eq_toField_mul (x : FastField F) : + (x.val.toNat : ZMod P.fieldSize) = + toField x * (UInt32.size : ZMod P.fieldSize) := by + rw [toField_eq_raw_mul_inv] + rw [mul_assoc] + rw [inv_mul_cancel₀ P.uint32Size_ne_zero_in_field] + rw [mul_one] + +theorem nat_eq_of_field_eq {a b : Nat} (ha : a < P.fieldSize) + (hb : b < P.fieldSize) (h : (a : ZMod P.fieldSize) = (b : ZMod P.fieldSize)) : + a = b := + Montgomery.natCast_inj ha hb h + +theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < P.fieldSize) : + ((ofCanonicalNat (F := F) n h).val.toNat : ZMod P.fieldSize) = + (n : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) := by + unfold ofCanonicalNat + have hred := montgomeryReduceBounded_cast + (UInt64.ofNat n * P.r2ModModulus.toUInt64) (by + rw [UInt64.toNat_mul, UInt64.toNat_ofNat', UInt32.toNat_toUInt64] + have hnmod : n % 2 ^ 64 = n := by + apply Nat.mod_eq_of_lt + exact Nat.lt_trans h (Nat.lt_trans P.fieldSize_lt_uint32Size (by decide)) + rw [hnmod] + have hprod : n * P.r2ModModulus.toNat < 2 ^ 64 := by + nlinarith [P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [P.r2ModModulus_lt_fieldSize]) + change ((montgomeryReduceBoundedRaw (F := F) + (UInt64.ofNat n * P.r2ModModulus.toUInt64)).toNat : ZMod P.fieldSize) = + ((UInt64.ofNat n * P.r2ModModulus.toUInt64).toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹ at hred + change ((montgomeryReduceBoundedRaw (F := F) + (UInt64.ofNat n * P.r2ModModulus.toUInt64)).toNat : ZMod P.fieldSize) = + (n : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) + rw [hred] + simp only [UInt64.toNat_mul, UInt64.toNat_ofNat', UInt32.toNat_toUInt64] + have hnmod : n % 2 ^ 64 = n := by + apply Nat.mod_eq_of_lt + exact Nat.lt_trans h (Nat.lt_trans P.fieldSize_lt_uint32Size (by decide)) + rw [hnmod] + have hprod : n * P.r2ModModulus.toNat < 2 ^ 64 := by + nlinarith [P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + rw [Nat.cast_mul, P.r2ModModulus_cast] + rw [pow_two] + rw [mul_assoc (n : ZMod P.fieldSize) ((UInt32.size : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)) ((UInt32.size : ZMod P.fieldSize)⁻¹)] + rw [mul_assoc (UInt32.size : ZMod P.fieldSize) (UInt32.size : ZMod P.fieldSize) + ((UInt32.size : ZMod P.fieldSize)⁻¹)] + rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] + rw [mul_one] + +theorem toField_ofCanonicalNat_aux (n : Nat) (h : n < P.fieldSize) : + toField (ofCanonicalNat (F := F) n h) = (n : ZMod P.fieldSize) := by + rw [toField_eq_raw_mul_inv, ofCanonicalNat_raw_cast] + rw [mul_assoc] + rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] + rw [mul_one] + +theorem reduceUInt64_raw_cast (x : UInt64) : + ((reduceUInt64 (F := F) x).val.toNat : ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) := by + unfold reduceUInt64 + let y := x % P.modulus64 + have hred := montgomeryReduceBounded_cast (y * P.r2ModModulus.toUInt64) (by + rw [UInt64.toNat_mul, UInt32.toNat_toUInt64] + have hy_lt : y.toNat < P.fieldSize := by + rw [show y = x % P.modulus64 by rfl, UInt64.toNat_mod, P.modulus64_toNat] + exact Nat.mod_lt _ P.fieldSize_pos + have hprod : y.toNat * P.r2ModModulus.toNat < 2 ^ 64 := by + nlinarith [hy_lt, P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [P.r2ModModulus_lt_fieldSize]) + change ((montgomeryReduceBoundedRaw (F := F) (y * P.r2ModModulus.toUInt64)).toNat : + ZMod P.fieldSize) = + ((y * P.r2ModModulus.toUInt64).toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹ at hred + change ((montgomeryReduceBoundedRaw (F := F) (y * P.r2ModModulus.toUInt64)).toNat : + ZMod P.fieldSize) = + (x.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize) + rw [hred] + simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] + have hy_lt : y.toNat < P.fieldSize := by + rw [show y = x % P.modulus64 by rfl, UInt64.toNat_mod, P.modulus64_toNat] + exact Nat.mod_lt _ P.fieldSize_pos + have hprod : y.toNat * P.r2ModModulus.toNat < 2 ^ 64 := by + nlinarith [hy_lt, P.r2ModModulus_lt_fieldSize, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + have hy_cast : (y.toNat : ZMod P.fieldSize) = (x.toNat : ZMod P.fieldSize) := by + rw [show y = x % P.modulus64 by rfl, UInt64.toNat_mod, P.modulus64_toNat] + rw [ZMod.natCast_eq_natCast_iff] + exact Nat.mod_modEq _ _ + rw [Nat.cast_mul, P.r2ModModulus_cast, hy_cast] + rw [pow_two] + rw [mul_assoc (x.toNat : ZMod P.fieldSize) ((UInt32.size : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)) ((UInt32.size : ZMod P.fieldSize)⁻¹)] + rw [mul_assoc (UInt32.size : ZMod P.fieldSize) (UInt32.size : ZMod P.fieldSize) + ((UInt32.size : ZMod P.fieldSize)⁻¹)] + rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] + rw [mul_one] + +@[simp] +theorem toNat_ofCanonicalNat (n : Nat) (h : n < P.fieldSize) : + toNat (ofCanonicalNat (F := F) n h) = n := + nat_eq_of_field_eq (toNat_lt_fieldSize _) h (toField_ofCanonicalNat_aux n h) + +@[simp] +theorem toField_ofCanonicalNat (n : Nat) (h : n < P.fieldSize) : + toField (ofCanonicalNat (F := F) n h) = (n : ZMod P.fieldSize) := + toField_ofCanonicalNat_aux n h + +@[simp] +theorem toNat_reduceUInt64 (x : UInt64) : + toNat (reduceUInt64 (F := F) x) = x.toNat % P.fieldSize := by + apply nat_eq_of_field_eq (toNat_lt_fieldSize _) (Nat.mod_lt _ P.fieldSize_pos) + change toField (reduceUInt64 (F := F) x) = ((x.toNat % P.fieldSize : Nat) : ZMod P.fieldSize) + rw [toField_eq_raw_mul_inv, reduceUInt64_raw_cast] + rw [mul_assoc] + rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] + rw [mul_one] + rw [ZMod.natCast_eq_natCast_iff] + exact (Nat.mod_modEq _ _).symm + +@[simp] +theorem toField_reduceUInt64 (x : UInt64) : + toField (reduceUInt64 (F := F) x) = (x.toNat : ZMod P.fieldSize) := by + rw [toField_eq_raw_mul_inv, reduceUInt64_raw_cast] + rw [mul_assoc] + rw [mul_inv_cancel₀ P.uint32Size_ne_zero_in_field] + rw [mul_one] + +/-! ## Field operations -/ + +/-- Fast modular addition in Montgomery form. -/ +@[inline] +def add (x y : FastField F) : FastField F := + reduceUInt32Lt2Modulus (x.val + y.val) (by + rw [UInt32.toNat_add] + exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) (by + have := x.property; have := y.property; omega)) + +/-- Fast modular negation in Montgomery form. -/ +@[inline] +def neg (x : FastField F) : FastField F := + if hx : x.val = 0 then + zero + else + ⟨P.modulus - x.val, by + have hle : x.val ≤ P.modulus := by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] + exact Nat.le_of_lt x.property + rw [UInt32.toNat_sub_of_le _ _ hle, P.modulus_toNat] + have hxpos : 0 < x.val.toNat := by + apply Nat.pos_of_ne_zero + intro hzero + apply hx + apply UInt32.toNat_inj.mp + simpa using hzero + have hp := P.fieldSize_pos + omega⟩ + +/-- Fast modular subtraction in Montgomery form. -/ +@[inline] +def sub (x y : FastField F) : FastField F := + if hyx : y.val ≤ x.val then + ⟨x.val - y.val, by + rw [UInt32.toNat_sub_of_le _ _ hyx] + have := x.property; omega⟩ + else + ⟨x.val + P.modulus - y.val, by + have hsum_lt : x.val.toNat + P.fieldSize < UInt32.size := by + have htwo := P.fieldSize_add_fieldSize_lt_uint32Size + have := x.property; omega + have hsum_eq : (x.val + P.modulus).toNat = x.val.toNat + P.fieldSize := by + rw [UInt32.toNat_add, P.modulus_toNat, Nat.mod_eq_of_lt hsum_lt] + have hyle : y.val ≤ x.val + P.modulus := by + rw [UInt32.le_iff_toNat_le, hsum_eq] + have := y.property; omega + rw [UInt32.toNat_sub_of_le _ _ hyle, hsum_eq] + have hyxNat : ¬y.val.toNat ≤ x.val.toNat := by + intro hle + apply hyx + rw [UInt32.le_iff_toNat_le] + exact hle + have := y.property; omega⟩ + +/-- Fast modular multiplication in Montgomery form. -/ +@[inline] +def mul (x y : FastField F) : FastField F := + 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, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [x.property, y.property, P.fieldSize_lt_uint32Size, P.fieldSize_pos]) + +/-- Fast squaring. -/ +@[inline] +def square (x : FastField F) : FastField F := + mul x x + +/-- Exponentiation over the fast representation using repeated squaring. -/ +@[specialize] +def pow (x : FastField F) (n : Nat) : FastField F := + @npowBinRec (FastField F) ⟨one⟩ ⟨mul⟩ n x + +/-- Fermat exponent used for inversion in the prime field. -/ +def invExponent : Nat := P.fieldSize - 2 + +/-- Inversion in Montgomery form via Fermat's little theorem (`x⁻¹ = x^(p-2)`), +by binary exponentiation (`pow`). -/ +@[inline] +def inv (x : FastField F) : FastField F := + pow x (invExponent (F := F)) + +/-- Division through inversion and fast multiplication. -/ +@[inline] +def div (x y : FastField F) : FastField F := + mul x (inv y) + +instance instZero : Zero (FastField F) where + zero := zero + +instance instOne : One (FastField F) where + one := one + +instance instAdd : Add (FastField F) where + add := add + +instance instNeg : Neg (FastField F) where + neg := neg + +instance instSub : Sub (FastField F) where + sub := sub + +instance instMul : Mul (FastField F) where + mul := mul + +instance instInv : Inv (FastField F) where + inv := inv + +instance instDiv : Div (FastField F) where + div := div + +instance instNatCast : NatCast (FastField F) where + natCast := ofNat + +instance instIntCast : IntCast (FastField F) where + intCast := ofInt + +instance instNatSMul : SMul Nat (FastField F) where + smul n x := ofNat n * x + +instance instIntSMul : SMul Int (FastField F) where + smul n x := ofInt n * x + +instance instPowNat : Pow (FastField F) Nat where + pow := pow + +instance instPowInt : Pow (FastField F) Int where + pow x n := + match n with + | Int.ofNat k => pow x k + | Int.negSucc k => pow (inv x) (k + 1) + +instance instNNRatCast : NNRatCast (FastField F) where + nnratCast q := ofField (q : ZMod P.fieldSize) + +instance instRatCast : RatCast (FastField F) where + ratCast q := ofField (q : ZMod P.fieldSize) + +instance instNNRatSMul : SMul ℚ≥0 (FastField F) where + smul q x := ofField (q • toField x) + +instance instRatSMul : SMul ℚ (FastField F) where + smul q x := ofField (q • toField x) + +/-- Fermat-style inversion in `ZMod fieldSize`. -/ +theorem inv_eq_pow_field (a : ZMod P.fieldSize) (ha : a ≠ 0) : + a⁻¹ = a ^ (P.fieldSize - 2) := by + have hcard : Fintype.card (ZMod P.fieldSize) = P.fieldSize := ZMod.card P.fieldSize + have h1 : a ^ (P.fieldSize - 1) = 1 := by + have h := FiniteField.pow_card_sub_one_eq_one a ha + rw [hcard] at h; exact h + have hmul : a * a ^ (P.fieldSize - 2) = 1 := by + rw [← pow_succ']; show a ^ (P.fieldSize - 2 + 1) = 1 + have : P.fieldSize - 2 + 1 = P.fieldSize - 1 := by + have := P.two_lt_fieldSize; omega + rw [this]; exact h1 + exact (eq_inv_of_mul_eq_one_left (by rwa [mul_comm])).symm + +/-- Converting from the canonical field to fast form and back is the identity. -/ +@[simp] +theorem toField_ofField (x : ZMod P.fieldSize) : toField (ofField (F := F) x) = x := by + unfold ofField + rw [toField_ofCanonicalNat] + exact ZMod.natCast_zmod_val x + +/-- Converting from fast form to the canonical field and back is the identity. -/ +@[simp] +theorem ofField_toField (x : FastField F) : ofField (toField x) = x := by + apply Subtype.ext + apply UInt32.toNat_inj.mp + apply nat_eq_of_field_eq (F := F) + · exact (ofField (toField x)).property + · exact x.property + · rw [raw_cast_eq_toField_mul] + rw [toField_ofField] + rw [raw_cast_eq_toField_mul] + +/-- The canonical-field interpretation distinguishes fast values. -/ +theorem toField_injective : Function.Injective (toField (F := F)) := + Function.LeftInverse.injective ofField_toField + +/-- `toField` maps fast zero to canonical zero. -/ +@[simp] +theorem toField_zero : toField (0 : FastField F) = 0 := by + rw [toField_eq_raw_mul_inv] + change ((0 : Nat) : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ = 0 + rw [Nat.cast_zero, zero_mul] + +/-- `toField` maps fast one to canonical one. -/ +@[simp] +theorem toField_one : toField (1 : FastField F) = 1 := by + rw [toField_eq_raw_mul_inv] + change (P.rModModulus.toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹ = 1 + rw [P.rModModulus_cast] + exact mul_inv_cancel₀ P.uint32Size_ne_zero_in_field + +/-- Fast addition agrees with addition in the canonical field. -/ +@[simp] +theorem toField_add (x y : FastField F) : toField (x + y) = toField x + toField y := by + rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x, toField_eq_raw_mul_inv y] + unfold instAdd add + have hred := reduceUInt32Lt2Modulus_cast (F := F) (x.val + y.val) (by + rw [UInt32.toNat_add] + exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) (by + have hx := x.property; have hy := y.property; omega)) + change ((reduceUInt32Lt2ModulusRaw (F := F) (x.val + y.val)).toNat : ZMod P.fieldSize) = + ((x.val + y.val).toNat : ZMod P.fieldSize) at hred + change ((reduceUInt32Lt2ModulusRaw (F := F) (x.val + y.val)).toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹ = + (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + + (y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + rw [hred] + rw [UInt32.toNat_add] + have hsum_lt : x.val.toNat + y.val.toNat < UInt32.size := by + nlinarith [x.property, y.property, P.fieldSize_add_fieldSize_lt_uint32Size] + rw [Nat.mod_eq_of_lt hsum_lt] + rw [Nat.cast_add] + ring + +/-- Fast subtraction agrees with subtraction in the canonical field. -/ +@[simp] +theorem toField_sub (x y : FastField F) : toField (x - y) = toField x - toField y := by + rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x, toField_eq_raw_mul_inv y] + by_cases hyx : y.val ≤ x.val + · have hsubval : (x - y : FastField F).val = x.val - y.val := by + change (sub x y).val = x.val - y.val + unfold sub + rw [dif_pos hyx] + rw [hsubval] + change (((x.val - y.val).toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹) = + (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - + (y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + rw [UInt32.toNat_sub_of_le _ _ hyx] + rw [Nat.cast_sub (by + rw [UInt32.le_iff_toNat_le] at hyx + exact hyx)] + ring + · have hsum_lt : x.val.toNat + P.fieldSize < UInt32.size := by + have htwo := P.fieldSize_add_fieldSize_lt_uint32Size + have := x.property; omega + have hsum_eq : (x.val + P.modulus).toNat = x.val.toNat + P.fieldSize := by + rw [UInt32.toNat_add, P.modulus_toNat, Nat.mod_eq_of_lt hsum_lt] + have hyle : y.val ≤ x.val + P.modulus := by + rw [UInt32.le_iff_toNat_le, hsum_eq] + have := y.property; omega + have hsubval : (x - y : FastField F).val = x.val + P.modulus - y.val := by + change (sub x y).val = x.val + P.modulus - y.val + unfold sub + rw [dif_neg hyx] + rw [hsubval] + change (((x.val + P.modulus - y.val).toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹) = + (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ - + (y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ + 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 F) : 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 : FastField F).val = (zero : FastField F).val := by + change (neg x).val = (zero : FastField F).val + unfold neg + rw [dif_pos hx] + rw [hnegval] + change ((zero : FastField F).val.toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹ = + -((x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) + have hxNat : x.val.toNat = 0 := by + simpa using congrArg UInt32.toNat hx + rw [hxNat] + change ((0 : Nat) : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ = + -(((0 : Nat) : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) + simp + · have hle : x.val ≤ P.modulus := by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] + exact Nat.le_of_lt x.property + have hnegval : (-x : FastField F).val = P.modulus - x.val := by + change (neg x).val = P.modulus - x.val + unfold neg + rw [dif_neg hx] + rw [hnegval] + change (((P.modulus - x.val).toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹) = + -((x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) + rw [UInt32.toNat_sub_of_le _ _ hle, P.modulus_toNat] + rw [Nat.cast_sub (by + rw [UInt32.le_iff_toNat_le, P.modulus_toNat] at hle + exact hle)] + rw [ZMod.natCast_self] + ring + +/-- Fast multiplication agrees with multiplication in the canonical field. -/ +@[simp] +theorem toField_mul (x y : FastField F) : toField (x * y) = toField x * toField y := by + rw [toField_eq_raw_mul_inv, toField_eq_raw_mul_inv x, toField_eq_raw_mul_inv y] + unfold instMul mul + have hred := montgomeryReduceBounded_cast (F := F) (x.val.toUInt64 * y.val.toUInt64) (by + simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] + have hprod : x.val.toNat * y.val.toNat < 2 ^ 64 := by + nlinarith [x.property, y.property, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + nlinarith [x.property, y.property, P.fieldSize_lt_uint32Size, P.fieldSize_pos]) + change ((montgomeryReduceBoundedRaw (F := F) (x.val.toUInt64 * y.val.toUInt64)).toNat : + ZMod P.fieldSize) = + ((x.val.toUInt64 * y.val.toUInt64).toNat : ZMod P.fieldSize) * + (UInt32.size : ZMod P.fieldSize)⁻¹ at hred + change ((montgomeryReduceBoundedRaw (F := F) (x.val.toUInt64 * y.val.toUInt64)).toNat : + ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ = + (x.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹ * + ((y.val.toNat : ZMod P.fieldSize) * (UInt32.size : ZMod P.fieldSize)⁻¹) + rw [hred] + simp only [UInt64.toNat_mul, UInt32.toNat_toUInt64] + have hprod : x.val.toNat * y.val.toNat < 2 ^ 64 := by + nlinarith [x.property, y.property, P.fieldSize_mul_fieldSize_lt_two64] + rw [Nat.mod_eq_of_lt hprod] + rw [Nat.cast_mul] + ring + +/-- Ring equivalence between the fast Montgomery representation and the canonical field. -/ +def ringEquiv : FastField F ≃+* ZMod P.fieldSize where + toFun := toField + invFun := ofField + left_inv := ofField_toField + right_inv := toField_ofField + map_add' := toField_add + map_mul' := toField_mul + +@[simp] +theorem ringEquiv_apply (x : FastField F) : ringEquiv x = toField x := rfl + +@[simp] +theorem ringEquiv_symm_apply (x : ZMod P.fieldSize) : + (ringEquiv (F := F)).symm x = ofField x := rfl + +private theorem mul_assoc_field (x y z : FastField F) : (x * y) * z = x * (y * z) := by + apply toField_injective + rw [toField_mul, toField_mul, toField_mul, toField_mul] + ring + +private theorem pow_succ_field (x : FastField F) (n : Nat) : pow x (n + 1) = pow x n * x := by + unfold pow + letI : Semigroup (FastField F) := { + 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 : FastField F) : 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 : FastField F) (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_field, toField_mul, ih, _root_.pow_succ] + +private theorem toField_inv_pow (x : FastField F) : + toField (inv x) = toField x ^ (invExponent (F := F)) := by + unfold inv + exact toField_pow x (invExponent (F := F)) + +private theorem toField_inv_raw (x : FastField F) : toField (inv x) = (toField x)⁻¹ := by + rw [toField_inv_pow] + by_cases hx : toField x = 0 + · rw [hx, inv_zero] + exact zero_pow (by unfold invExponent; have := P.two_lt_fieldSize; omega) + · simpa [invExponent] using (inv_eq_pow_field (toField x) hx).symm + +/-- Fast inversion agrees with inversion in the canonical field. -/ +@[simp] +theorem toField_inv (x : FastField F) : toField x⁻¹ = (toField x)⁻¹ := by + change toField (inv x) = (toField x)⁻¹ + exact toField_inv_raw x + +private theorem toField_mul_raw (x y : FastField F) : + toField (mul x y) = toField x * toField y := by + change toField (x * y) = toField x * toField y + exact toField_mul x y + +private theorem toField_div_mul_inv (x y : FastField F) : + toField (div x y) = toField x * toField (inv y) := by + unfold div + exact toField_mul_raw x (inv y) + +/-- Fast division agrees with division in the canonical field. -/ +@[simp] +theorem toField_div (x y : FastField F) : toField (x / y) = toField x / toField y := by + change toField (div x y) = toField x / toField y + have h : ∀ a b c : ZMod P.fieldSize, c = b⁻¹ → a * c = a / b := by + intro a b c hc + rw [hc] + rfl + exact (toField_div_mul_inv x y).trans + (h (toField x) (toField y) (toField (inv y)) (toField_inv_raw y)) + +/-- Natural casts into fast form agree with natural casts into the canonical field. -/ +@[simp] +theorem toField_natCast (n : Nat) : toField (n : FastField F) = (n : ZMod P.fieldSize) := by + change toField (ofNat n) = (n : ZMod P.fieldSize) + unfold ofNat + rw [toField_ofCanonicalNat] + rw [ZMod.natCast_eq_natCast_iff] + exact Nat.mod_modEq _ _ + +/-- Integer casts into fast form agree with integer casts into the canonical field. -/ +@[simp] +theorem toField_intCast (n : Int) : toField (n : FastField F) = (n : ZMod P.fieldSize) := by + change toField (ofInt n) = (n : ZMod P.fieldSize) + unfold ofInt + rw [toField_ofField] + +/-- Natural scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_nsmul (n : Nat) (x : FastField F) : toField (n • x) = n • toField x := by + change toField ((n : FastField F) * x) = n • toField x + rw [toField_mul, toField_natCast] + rw [nsmul_eq_mul] + +/-- Integer scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_zsmul (n : Int) (x : FastField F) : toField (n • x) = n • toField x := by + change toField ((n : FastField F) * x) = n • toField x + rw [toField_mul, toField_intCast] + rw [zsmul_eq_mul] + +/-- Natural powers through the `Pow` instance are preserved by `toField`. -/ +@[simp] +theorem toField_npow (x : FastField F) (n : Nat) : toField (x ^ n) = toField x ^ n := by + change toField (pow x n) = toField x ^ n + rw [toField_pow] + +/-- Integer powers through the `Pow` instance are preserved by `toField`. -/ +@[simp] +theorem toField_zpow (x : FastField F) (n : Int) : toField (x ^ n) = toField x ^ n := by + 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 F) = (q : ZMod P.fieldSize) := by + change toField (ofField (q : ZMod P.fieldSize)) = (q : ZMod P.fieldSize) + rw [toField_ofField] + +/-- Rational casts into fast form agree with canonical-field casts. -/ +@[simp] +theorem toField_ratCast (q : ℚ) : toField (q : FastField F) = (q : ZMod P.fieldSize) := by + change toField (ofField (q : ZMod P.fieldSize)) = (q : ZMod P.fieldSize) + rw [toField_ofField] + +/-- Nonnegative rational scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_nnqsmul (q : ℚ≥0) (x : FastField F) : toField (q • x) = q • toField x := by + change toField (ofField (q • toField x)) = q • toField x + rw [toField_ofField] + +/-- Rational scalar multiplication is preserved by `toField`. -/ +@[simp] +theorem toField_qsmul (q : ℚ) (x : FastField F) : toField (q • x) = q • toField x := by + change toField (ofField (q • toField x)) = q • toField x + rw [toField_ofField] + +/-- Field instance transferred from the canonical field through `toField`. -/ +instance (priority := low) instField : _root_.Field (FastField F) := + toField_injective.field toField + toField_zero + toField_one + toField_add + toField_mul + toField_neg + toField_sub + toField_inv + toField_div + toField_nsmul + toField_zsmul + toField_nnqsmul + toField_qsmul + toField_npow + toField_zpow + toField_natCast + toField_intCast + toField_nnratCast + toField_ratCast + +/-- Commutative-ring instance inherited from the transferred field structure. -/ +instance (priority := low) instCommRing : CommRing (FastField F) := by + infer_instance + +/-- A fast 32-bit-word field is non-binary. -/ +instance (priority := low) instNonBinaryField : NonBinaryField (FastField F) where + char_neq_2 := by + change ((2 : Nat) : FastField F) ≠ 0 + intro h + exact P.two_ne_zero_in_field (by + calc + (2 : ZMod P.fieldSize) = ((2 : Nat) : ZMod P.fieldSize) := by norm_cast + _ = toField ((2 : Nat) : FastField F) := (toField_natCast 2).symm + _ = toField (0 : FastField F) := congrArg toField h + _ = 0 := toField_zero) + +end + +end Native32 +end Montgomery diff --git a/CompPoly/Fields/README.md b/CompPoly/Fields/README.md index ef884b31..f7718c2a 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** | `UInt32 × UInt64`, radix `R = 2^32` word-level Montgomery bridge over the generic core. | +| **Montgomery/Native32Field.lean** | Shared 32-bit-word fast-field implementation over the word bridge: the `Mont32Field` per-field data class, the `FastField` carrier, every field operation, the algebraic instances, and the `toField`/`ofField` correctness bridge — written once and instantiated by both BabyBear and KoalaBear. | | **Secp256k1.lean** | Base and scalar fields for the Secp256k1 curve (used in Bitcoin/Ethereum). | ## Binary-field modules 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..02b25071 --- /dev/null +++ b/tests/CompPolyTests/Fields/BabyBear/Fast.lean @@ -0,0 +1,41 @@ +/- +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 raw (0 : Field) = 0 +#guard raw (1 : Field) = rModModulus +#guard toCanonicalUInt32 (ofNat 37) = (37 : UInt32) +#guard toNat (ofNat BabyBear.fieldSize) = 0 +#guard toNat (ofNat (BabyBear.fieldSize + 37)) = 37 +#guard toNat ((ofNat (BabyBear.fieldSize - 1)) + (2 : Field)) = 1 +#guard toNat ((ofNat (BabyBear.fieldSize - 1)) + (ofNat (BabyBear.fieldSize - 1))) = + BabyBear.fieldSize - 2 +#guard toNat ((9 : Field) - (5 : Field)) = 4 +#guard toNat ((5 : Field) - (9 : Field)) = BabyBear.fieldSize - 4 +#guard toNat (-(0 : Field)) = 0 +#guard toNat (-(1 : Field)) = BabyBear.fieldSize - 1 +#guard toNat ((ofNat (BabyBear.fieldSize - 1)) * (ofNat (BabyBear.fieldSize - 1))) = 1 +#guard toNat (square (12345 : Field)) = 152399025 +#guard toNat ((37 : Field) ^ 0) = 1 +#guard toNat ((37 : Field) ^ 1) = 37 +#guard toField ((123456789 : Field) ^ 17) = ((123456789 : BabyBear.Field) ^ 17) +#guard toField ((123456789 : Field) ^ 255) = ((123456789 : BabyBear.Field) ^ 255) +#guard toNat ((0 : Field)⁻¹) = 0 +#guard toNat ((37 : Field)⁻¹ * (37 : Field)) = 1 +#guard toNat ((37 : Field) / (37 : Field)) = 1 +#guard toField ((37 : Field)⁻¹) = ((37 : BabyBear.Field)⁻¹) +#guard toField ((37 : Field) ^ (-3 : Int)) = ((37 : BabyBear.Field) ^ (-3 : Int)) + +end BabyBear.Fast