Fast eight-limb Montgomery fields

The bounded carrier, conversions, arithmetic, and field instances built on the raw eight-limb Montgomery operations of Montgomery/Native64x8. This is the multi-limb analogue of Montgomery/Native32Field, for prime moduli below 2 ^ 255.

A carrier element stores the Montgomery residue x * 2 ^ 256 mod q as eight 32-bit limbs; toField divides that residue by 2 ^ 256 again and lands in ZMod modulus. All arithmetic is transported along toField, which is a ring isomorphism onto ZMod modulus.

Main results

• FastField — the carrier, { x : Limbs8 // x.Bounded ∧ x.toNat < modulus }
• toField_add, toField_mul, … — @[simp] equivalences with the canonical field
• Mont64x8Field — the per-field constants class
• ringEquiv, instField — the ring isomorphism and the transferred Field instance

Per-field constants

class Montgomery.Native64x8.Mont64x8Field (modulus : ℕ) : Type

Per-field data for a fast eight-limb Montgomery field with radix R = 2 ^ 256. All side conditions are concrete numeral facts, discharged by decide at instantiation.

• prime : Nat.Prime modulus

  modulus is prime.

• modulusLimbs : Limbs8

  The modulus in eight 32-bit limbs.

• rModModulus : Limbs8

  2 ^ 256 mod modulus, the Montgomery representation of one.

• r2ModModulus : Limbs8

  (2 ^ 256) ^ 2 mod modulus, used to enter Montgomery form.

• montgomeryNegInv : UInt64

  -modulus⁻¹ mod 2 ^ 32, used by Montgomery reduction.

• modulusLimbs_bounded : (modulusLimbs modulus).Bounded
• modulusLimbs_toNat : (modulusLimbs modulus).toNat = modulus
• two_lt_modulus : 2 < modulus
• two_mul_modulus_lt : 2 * modulus < 2 ^ 256
• rModModulus_bounded : (rModModulus modulus).Bounded
• rModModulus_toNat : (rModModulus modulus).toNat = 2 ^ 256 % modulus
• r2ModModulus_bounded : (r2ModModulus modulus).Bounded
• r2ModModulus_toNat : (r2ModModulus modulus).toNat = (2 ^ 256) ^ 2 % modulus
• montgomeryNegInv_lt : (montgomeryNegInv modulus).toNat < 2 ^ 32
• montgomeryNegInv_mul_modulus_mod_two_pow_32 : (montgomeryNegInv modulus).toNat * modulus % 2 ^ 32 = 2 ^ 32 - 1

Modulus facts

instance Montgomery.Native64x8.Mont64x8Field.instFactPrime {modulus : ℕ} [P : Mont64x8Field modulus] : Fact (Nat.Prime modulus)

theorem Montgomery.Native64x8.Mont64x8Field.modulus_pos {modulus : ℕ} [P : Mont64x8Field modulus] : 0 < modulus

theorem Montgomery.Native64x8.Mont64x8Field.modulus_lt {modulus : ℕ} [P : Mont64x8Field modulus] : modulus < 2 ^ 256

theorem Montgomery.Native64x8.Mont64x8Field.q_toNat {modulus : ℕ} [P : Mont64x8Field modulus] : (modulusLimbs modulus).toNat = modulus

theorem Montgomery.Native64x8.Mont64x8Field.two_mul_q_lt {modulus : ℕ} [P : Mont64x8Field modulus] : 2 * (modulusLimbs modulus).toNat < 2 ^ 256

theorem Montgomery.Native64x8.Mont64x8Field.negInv_mul_q {modulus : ℕ} [P : Mont64x8Field modulus] : (montgomeryNegInv modulus).toNat * (modulusLimbs modulus).toNat % 2 ^ 32 = 2 ^ 32 - 1

instance Montgomery.Native64x8.Mont64x8Field.instNeZeroNat {modulus : ℕ} [P : Mont64x8Field modulus] : NeZero modulus

theorem Montgomery.Native64x8.Mont64x8Field.two_ne_zero {modulus : ℕ} [P : Mont64x8Field modulus] : 2 ≠ 0

theorem Montgomery.Native64x8.Mont64x8Field.r_ne_zero {modulus : ℕ} [P : Mont64x8Field modulus] : ↑(2 ^ 256) ≠ 0

The carrier

@[implicit_reducible]

def Montgomery.Native64x8.FastField (modulus : ℕ) [Mont64x8Field modulus] : Type

The fast carrier for a prime modulus: eight 32-bit limbs holding a value below modulus, interpreted as a Montgomery residue. At runtime this erases to Limbs8.

@[instance_reducible]

instance Montgomery.Native64x8.instDecidableEqFastField {modulus : ℕ} [P : Mont64x8Field modulus] : DecidableEq (FastField modulus)

theorem Montgomery.Native64x8.FastField.val_bounded {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : (↑x).Bounded

theorem Montgomery.Native64x8.FastField.val_lt {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : (↑x).toNat < (Mont64x8Field.modulusLimbs modulus).toNat

Arithmetic

def Montgomery.Native64x8.FastField.zero (modulus : ℕ) [P : Mont64x8Field modulus] : FastField modulus

The zero element.

def Montgomery.Native64x8.FastField.one (modulus : ℕ) [P : Mont64x8Field modulus] : FastField modulus

The one element, the Montgomery residue 2 ^ 256 mod modulus.

@[inline]

def Montgomery.Native64x8.FastField.add {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : FastField modulus

Fast modular addition in Montgomery form.

@[inline]

def Montgomery.Native64x8.FastField.sub {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : FastField modulus

Fast modular subtraction in Montgomery form.

@[inline]

def Montgomery.Native64x8.FastField.neg {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : FastField modulus

Fast modular negation in Montgomery form.

@[inline]

def Montgomery.Native64x8.FastField.mul {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : FastField modulus

Fast Montgomery multiplication.

@[inline]

def Montgomery.Native64x8.FastField.square {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : FastField modulus

Fast squaring.

@[specialize #[]]

def Montgomery.Native64x8.FastField.pow {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) (n : ℕ) : FastField modulus

Exponentiation by repeated squaring.

@[inline]

def Montgomery.Native64x8.FastField.inv {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : FastField modulus

Inversion by Fermat's little theorem, x⁻¹ = x ^ (modulus - 2).

@[inline]

def Montgomery.Native64x8.FastField.div {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : FastField modulus

Division through inversion.

Conversions

@[inline]

def Montgomery.Native64x8.FastField.toLimbs8 {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : Limbs8

The canonical limb representative of a fast element: one Montgomery reduction.

@[inline]

def Montgomery.Native64x8.FastField.toNat {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : ℕ

The canonical natural representative of a fast element.

@[inline]

def Montgomery.Native64x8.FastField.toField {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : ZMod modulus

The canonical ZMod value of a fast element.

@[inline]

def Montgomery.Native64x8.FastField.ofCanonicalNat {modulus : ℕ} [P : Mont64x8Field modulus] (n : ℕ) (h : n < modulus) : FastField modulus

Build a fast element from a canonical natural representative.

@[inline]

def Montgomery.Native64x8.FastField.ofNat (modulus : ℕ) [P : Mont64x8Field modulus] (n : ℕ) : FastField modulus

Convert a natural number into fast Montgomery form.

@[inline]

def Montgomery.Native64x8.FastField.ofField {modulus : ℕ} [P : Mont64x8Field modulus] (x : ZMod modulus) : FastField modulus

Convert from the canonical field into fast Montgomery form.

@[inline]

def Montgomery.Native64x8.FastField.ofInt (modulus : ℕ) [P : Mont64x8Field modulus] (n : ℤ) : FastField modulus

Convert an integer into fast Montgomery form.

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instZero {modulus : ℕ} [P : Mont64x8Field modulus] : Zero (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instOne {modulus : ℕ} [P : Mont64x8Field modulus] : One (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instAdd {modulus : ℕ} [P : Mont64x8Field modulus] : Add (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instNeg {modulus : ℕ} [P : Mont64x8Field modulus] : Neg (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instSub {modulus : ℕ} [P : Mont64x8Field modulus] : Sub (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instMul {modulus : ℕ} [P : Mont64x8Field modulus] : Mul (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instInv {modulus : ℕ} [P : Mont64x8Field modulus] : Inv (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instDiv {modulus : ℕ} [P : Mont64x8Field modulus] : Div (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instNatCast {modulus : ℕ} [P : Mont64x8Field modulus] : NatCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instIntCast {modulus : ℕ} [P : Mont64x8Field modulus] : IntCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instPowNat {modulus : ℕ} [P : Mont64x8Field modulus] : Pow (FastField modulus) ℕ

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instSMulNat {modulus : ℕ} [P : Mont64x8Field modulus] : SMul ℕ (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instSMulInt {modulus : ℕ} [P : Mont64x8Field modulus] : SMul ℤ (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instPowInt {modulus : ℕ} [P : Mont64x8Field modulus] : Pow (FastField modulus) ℤ

theorem Montgomery.Native64x8.FastField.zero_def {modulus : ℕ} [P : Mont64x8Field modulus] : 0 = zero modulus

theorem Montgomery.Native64x8.FastField.one_def {modulus : ℕ} [P : Mont64x8Field modulus] : 1 = one modulus

theorem Montgomery.Native64x8.FastField.add_def {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : x + y = x.add y

theorem Montgomery.Native64x8.FastField.neg_def {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : -x = x.neg

theorem Montgomery.Native64x8.FastField.sub_def {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : x - y = x.sub y

theorem Montgomery.Native64x8.FastField.mul_def {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : x * y = x.mul y

theorem Montgomery.Native64x8.FastField.inv_def {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : x⁻¹ = x.inv

theorem Montgomery.Native64x8.FastField.div_def {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : x / y = x * y⁻¹

theorem Montgomery.Native64x8.FastField.square_def {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : x.square = x * x

Correctness

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instNNRatCast {modulus : ℕ} [P : Mont64x8Field modulus] : NNRatCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instRatCast {modulus : ℕ} [P : Mont64x8Field modulus] : RatCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instSMulNNRat {modulus : ℕ} [P : Mont64x8Field modulus] : SMul ℚ≥0 (FastField modulus)

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instSMulRat {modulus : ℕ} [P : Mont64x8Field modulus] : SMul ℚ (FastField modulus)

theorem Montgomery.Native64x8.FastField.toNat_lt {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : x.toNat < modulus

@[simp]

theorem Montgomery.Native64x8.FastField.toField_ofCanonicalNat {modulus : ℕ} [P : Mont64x8Field modulus] {n : ℕ} (h : n < modulus) : (ofCanonicalNat n h).toField = ↑n

@[simp]

theorem Montgomery.Native64x8.FastField.toNat_ofCanonicalNat {modulus : ℕ} [P : Mont64x8Field modulus] {n : ℕ} (h : n < modulus) : (ofCanonicalNat n h).toNat = n

@[simp]

theorem Montgomery.Native64x8.FastField.toField_ofField {modulus : ℕ} [P : Mont64x8Field modulus] (x : ZMod modulus) : (ofField x).toField = x

Converting from the canonical field to fast form and back is the identity.

@[simp]

theorem Montgomery.Native64x8.FastField.ofField_toField {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : ofField x.toField = x

Converting from fast form to the canonical field and back is the identity.

theorem Montgomery.Native64x8.FastField.toField_injective {modulus : ℕ} [P : Mont64x8Field modulus] : Function.Injective toField

The canonical-field interpretation distinguishes fast values.

Field operations

@[simp]

theorem Montgomery.Native64x8.FastField.toField_zero {modulus : ℕ} [P : Mont64x8Field modulus] : toField 0 = 0

@[simp]

theorem Montgomery.Native64x8.FastField.toField_one {modulus : ℕ} [P : Mont64x8Field modulus] : toField 1 = 1

@[simp]

theorem Montgomery.Native64x8.FastField.toField_add {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : (x + y).toField = x.toField + y.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_sub {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : (x - y).toField = x.toField - y.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_neg {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : (-x).toField = -x.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_mul {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : (x * y).toField = x.toField * y.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_square {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : x.square.toField = x.toField * x.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_pow {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) (n : ℕ) : (x.pow n).toField = x.toField ^ n

@[simp]

theorem Montgomery.Native64x8.FastField.toField_inv {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) : x⁻¹.toField = x.toField⁻¹

@[simp]

theorem Montgomery.Native64x8.FastField.toField_div {modulus : ℕ} [P : Mont64x8Field modulus] (x y : FastField modulus) : (x / y).toField = x.toField / y.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_natCast {modulus : ℕ} [P : Mont64x8Field modulus] (n : ℕ) : (↑n).toField = ↑n

@[simp]

theorem Montgomery.Native64x8.FastField.toField_intCast {modulus : ℕ} [P : Mont64x8Field modulus] (n : ℤ) : (↑n).toField = ↑n

@[simp]

theorem Montgomery.Native64x8.FastField.toField_nsmul {modulus : ℕ} [P : Mont64x8Field modulus] (n : ℕ) (x : FastField modulus) : (n • x).toField = n • x.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_zsmul {modulus : ℕ} [P : Mont64x8Field modulus] (n : ℤ) (x : FastField modulus) : (n • x).toField = n • x.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_npow {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) (n : ℕ) : (x ^ n).toField = x.toField ^ n

@[simp]

theorem Montgomery.Native64x8.FastField.toField_zpow {modulus : ℕ} [P : Mont64x8Field modulus] (x : FastField modulus) (n : ℤ) : (x ^ n).toField = x.toField ^ n

@[simp]

theorem Montgomery.Native64x8.FastField.toField_nnratCast {modulus : ℕ} [P : Mont64x8Field modulus] (q : ℚ≥0) : (↑q).toField = ↑q

@[simp]

theorem Montgomery.Native64x8.FastField.toField_ratCast {modulus : ℕ} [P : Mont64x8Field modulus] (q : ℚ) : (↑q).toField = ↑q

@[simp]

theorem Montgomery.Native64x8.FastField.toField_nnqsmul {modulus : ℕ} [P : Mont64x8Field modulus] (q : ℚ≥0) (x : FastField modulus) : (q • x).toField = q • x.toField

@[simp]

theorem Montgomery.Native64x8.FastField.toField_qsmul {modulus : ℕ} [P : Mont64x8Field modulus] (q : ℚ) (x : FastField modulus) : (q • x).toField = q • x.toField

Algebraic structure

def Montgomery.Native64x8.FastField.ringEquiv (modulus : ℕ) [P : Mont64x8Field modulus] : FastField modulus ≃+* ZMod modulus

Ring equivalence between the fast Montgomery representation and the canonical field.

@[simp]

theorem Montgomery.Native64x8.FastField.ringEquiv_apply {modulus : ℕ} [P : Mont64x8Field modulus] {x : FastField modulus} : (ringEquiv modulus) x = x.toField

@[simp]

theorem Montgomery.Native64x8.FastField.ringEquiv_symm_apply {modulus : ℕ} [P : Mont64x8Field modulus] {x : ZMod modulus} : (ringEquiv modulus).symm x = ofField x

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instField {modulus : ℕ} [P : Mont64x8Field modulus] : Field (FastField modulus)

Field instance transferred from the canonical field through toField.

@[instance_reducible]

instance Montgomery.Native64x8.FastField.instNonBinaryField {modulus : ℕ} [P : Mont64x8Field modulus] : NonBinaryField (FastField modulus)

A fast eight-limb field is non-binary.