Fast 32-bit Montgomery Fields

The bounded carrier, conversions, arithmetic, and field instances built on Native32 reduction.

class Montgomery.Native32.Mont32Field (modulus : ℕ) : Type

Per-field data for a fast 32-bit Montgomery field.

• prime : Nat.Prime modulus

  modulus is prime.

• modulus32 : UInt32

  modulus as a 32-bit word.

• modulus64 : UInt64

  modulus as a 64-bit word.

• rModModulus : UInt32

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

• r2ModModulus : UInt64

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

• montgomeryNegInv : UInt32

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

• modulus32_toNat : (modulus32 modulus).toNat = modulus
• modulus64_toNat : (modulus64 modulus).toNat = modulus
• two_lt_modulus : 2 < modulus
• modulus_lt_two_pow_31 : modulus < 2 ^ 31
• rModModulus_toNat : (rModModulus modulus).toNat = 2 ^ 32 % modulus
• r2ModModulus_toNat : (r2ModModulus modulus).toNat = (2 ^ 32) ^ 2 % modulus
• montgomeryNegInv_mul_modulus_mod_two_pow_32 : (montgomeryNegInv modulus).toNat * modulus % 2 ^ 32 = 2 ^ 32 - 1

@[implicit_reducible]

def Montgomery.Native32.FastField (modulus : ℕ) [Mont32Field modulus] : Type

The fast carrier for a prime modulus: a native word below modulus, interpreted as a Montgomery residue. At runtime this erases to UInt32.

@[instance_reducible]

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

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

@[simp]

theorem Montgomery.Native32.Mont32Field.modulus_pos {modulus : ℕ} [P : Mont32Field modulus] : 0 < modulus

@[simp]

theorem Montgomery.Native32.Mont32Field.modulus32_pos {modulus : ℕ} [P : Mont32Field modulus] : 0 < (modulus32 modulus).toNat

@[simp]

theorem Montgomery.Native32.Mont32Field.modulus64_pos {modulus : ℕ} [P : Mont32Field modulus] : 0 < (modulus64 modulus).toNat

@[simp]

theorem Montgomery.Native32.Mont32Field.modulus32_lt_two_pow_31 {modulus : ℕ} [P : Mont32Field modulus] : (modulus32 modulus).toNat < 2 ^ 31

@[simp]

theorem Montgomery.Native32.Mont32Field.modulus64_lt_two_pow_31 {modulus : ℕ} [P : Mont32Field modulus] : (modulus64 modulus).toNat < 2 ^ 31

@[simp]

theorem Montgomery.Native32.Mont32Field.modulus_lt_two_pow_32 {modulus : ℕ} [P : Mont32Field modulus] : modulus < 2 ^ 32

theorem Montgomery.Native32.Mont32Field.modulus_sq_lt_two_pow_64 {modulus : ℕ} [P : Mont32Field modulus] : modulus ^ 2 < 2 ^ 64

theorem Montgomery.Native32.Mont32Field.two_ne_zero {modulus : ℕ} [P : Mont32Field modulus] : 2 ≠ 0

theorem Montgomery.Native32.Mont32Field.two_pow_32_ne_zero {modulus : ℕ} [P : Mont32Field modulus] : ↑(2 ^ 32) ≠ 0

theorem Montgomery.Native32.Mont32Field.r2ModModulus_lt_modulus {modulus : ℕ} [P : Mont32Field modulus] : (2 ^ 32) ^ 2 % modulus < modulus

instance Montgomery.Native32.instNeZeroNat_compPoly {modulus : ℕ} [P : Mont32Field modulus] : NeZero modulus

Implementation

@[inline]

def Montgomery.Native32.reduce {modulus : ℕ} [P : Mont32Field modulus] (x : UInt64) (h : x.toNat < modulus * 2 ^ 32) : FastField modulus

Montgomery reduction for inputs known to be below p * 2^32.

Conversions

@[inline]

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

Build a fast element from a canonical natural representative.

@[inline]

def Montgomery.Native32.FastField.ofNat (modulus : ℕ) [P : Mont32Field modulus] (n : ℕ) : FastField modulus

Convert a natural number into fast Montgomery representation.

@[inline]

def Montgomery.Native32.FastField.ofUInt32 (modulus : ℕ) [P : Mont32Field modulus] (x : UInt32) : FastField modulus

Convert a 32-bit word into fast Montgomery representation.

@[inline]

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

Convert from the canonical ZMod field into fast Montgomery form.

@[inline]

def Montgomery.Native32.FastField.ofInt (modulus : ℕ) [P : Mont32Field modulus] (n : ℤ) : FastField modulus

Convert an integer into fast Montgomery representation.

@[inline]

def Montgomery.Native32.FastField.toUInt32 {modulus : ℕ} [P : Mont32Field modulus] (x : FastField modulus) : UInt32

Convert a fast element to its canonical native-word representative.

@[inline]

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

Convert a fast element to its canonical natural representative.

@[inline]

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

Convert a fast element to the canonical ZMod field.

Field operations

def Montgomery.Native32.zero (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus

The zero fast element.

def Montgomery.Native32.one (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus

The one fast element.

@[inline]

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

Fast modular addition in Montgomery form.

@[inline]

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

Fast modular negation in Montgomery form.

@[inline]

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

Fast modular subtraction in Montgomery form.

@[inline]

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

Fast modular multiplication in Montgomery form.

@[inline]

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

Fast squaring.

@[specialize #[]]

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

Exponentiation over the fast representation using repeated squaring.

@[inline]

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

Inversion in Montgomery form via Fermat's little theorem (x⁻¹ = x^(p-2)), by binary exponentiation (pow).

@[inline]

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

Division through inversion and fast multiplication.

@[instance_reducible]

instance Montgomery.Native32.instZeroFastField {modulus : ℕ} [P : Mont32Field modulus] : Zero (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instOneFastField {modulus : ℕ} [P : Mont32Field modulus] : One (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instAddFastField {modulus : ℕ} [P : Mont32Field modulus] : Add (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instNegFastField {modulus : ℕ} [P : Mont32Field modulus] : Neg (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instSubFastField {modulus : ℕ} [P : Mont32Field modulus] : Sub (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instMulFastField {modulus : ℕ} [P : Mont32Field modulus] : Mul (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instInvFastField {modulus : ℕ} [P : Mont32Field modulus] : Inv (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instDivFastField {modulus : ℕ} [P : Mont32Field modulus] : Div (FastField modulus)

theorem Montgomery.Native32.zero_def {modulus : ℕ} [P : Mont32Field modulus] : 0 = zero modulus

theorem Montgomery.Native32.one_def {modulus : ℕ} [P : Mont32Field modulus] : 1 = one modulus

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

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

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

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

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

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

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

@[instance_reducible]

instance Montgomery.Native32.instNatCastFastField {modulus : ℕ} [P : Mont32Field modulus] : NatCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instIntCastFastField {modulus : ℕ} [P : Mont32Field modulus] : IntCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instSMulNatFastField {modulus : ℕ} [P : Mont32Field modulus] : SMul ℕ (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instSMulIntFastField {modulus : ℕ} [P : Mont32Field modulus] : SMul ℤ (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instPowFastFieldNat {modulus : ℕ} [P : Mont32Field modulus] : Pow (FastField modulus) ℕ

@[instance_reducible]

instance Montgomery.Native32.instPowFastFieldInt {modulus : ℕ} [P : Mont32Field modulus] : Pow (FastField modulus) ℤ

@[instance_reducible]

instance Montgomery.Native32.instNNRatCastFastField {modulus : ℕ} [P : Mont32Field modulus] : NNRatCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instRatCastFastField {modulus : ℕ} [P : Mont32Field modulus] : RatCast (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instSMulNNRatFastField {modulus : ℕ} [P : Mont32Field modulus] : SMul ℚ≥0 (FastField modulus)

@[instance_reducible]

instance Montgomery.Native32.instSMulRatFastField {modulus : ℕ} [P : Mont32Field modulus] : SMul ℚ (FastField modulus)

Correctness

Reduction and conversions

@[simp]

theorem Montgomery.Native32.FastField.val_toNat_lt {modulus : ℕ} [P : Mont32Field modulus] (x : FastField modulus) : (↑x).toNat < modulus

theorem Montgomery.Native32.toNat_lt_modulus {modulus : ℕ} [P : Mont32Field modulus] {x : FastField modulus} : x.toNat < modulus

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

The canonical-field interpretation distinguishes fast values.

Field operations

@[simp]

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

toField maps fast zero to canonical zero.

@[simp]

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

toField maps fast one to canonical one.

@[simp]

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

Fast addition agrees with addition in the canonical field.

@[simp]

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

Fast subtraction agrees with subtraction in the canonical field.

@[simp]

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

Fast negation agrees with negation in the canonical field.

@[simp]

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

@[simp]

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

Fast squaring agrees with multiplication by itself in the canonical field.

@[simp]

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

Fast natural-power computation agrees with powers in the canonical field.

@[simp]

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

Fast inversion agrees with inversion in the canonical field.

@[simp]

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

Fast division agrees with division in the canonical field.

@[simp]

theorem Montgomery.Native32.toField_natCast {modulus : ℕ} [P : Mont32Field modulus] (n : ℕ) : (↑n).toField = ↑n

Natural casts into fast form agree with natural casts into the canonical field.

@[simp]

theorem Montgomery.Native32.toField_intCast {modulus : ℕ} [P : Mont32Field modulus] (n : ℤ) : (↑n).toField = ↑n

Integer casts into fast form agree with integer casts into the canonical field.

@[simp]

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

Natural scalar multiplication is preserved by toField.

@[simp]

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

Integer scalar multiplication is preserved by toField.

@[simp]

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

Natural powers through the Pow instance are preserved by toField.

@[simp]

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

Integer powers through the Pow instance are preserved by toField.

@[simp]

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

Nonnegative rational casts into fast form agree with canonical-field casts.

@[simp]

theorem Montgomery.Native32.toField_ratCast {modulus : ℕ} [P : Mont32Field modulus] (q : ℚ) : (↑q).toField = ↑q

Rational casts into fast form agree with canonical-field casts.

@[simp]

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

Nonnegative rational scalar multiplication is preserved by toField.

@[simp]

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

Rational scalar multiplication is preserved by toField.

Algebraic structure

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

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Field instance transferred from the canonical field through toField.

@[instance_reducible]

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

A fast 32-bit-word field is non-binary.