Documentation

CompPoly.Fields.Montgomery.Native32

Native 32-bit Montgomery Reduction #

Raw word operations for Montgomery reduction with radix 2 ^ 32.

source
@[inline]
def Montgomery.Native32.reduceRaw (p32 : UInt32) (p64 : UInt64) (negInv : UInt32) (x : UInt64) :
UInt32

Montgomery reduction.

Instances For
    source
    def Montgomery.Native32.reduceQuotient (negInv : UInt32) (p x : UInt64) :
    UInt32

    The native pre-subtraction quotient in 32-bit Montgomery reduction.

    Instances For
      source
      def Montgomery.Native32.conditionalSubtract (p32 u : UInt32) :
      UInt32

      Conditional subtraction of the modulus in 32-bit Montgomery reduction.

      Instances For
        source
        theorem Montgomery.Native32.reduceRaw_eq_conditionalSubtract {p32 negInv : UInt32} {p64 x : UInt64} :
        reduceRaw p32 p64 negInv x = conditionalSubtract p32 (reduceQuotient negInv p64 x)
        source
        theorem Montgomery.Native32.reduceQuotient_toNat {negInv : UInt32} {p64 x : UInt64} (hp_pos : 0 < p64.toNat) (hbound : p64.toNat < 2 ^ 31) (h : x.toNat < p64.toNat * 2 ^ 32) :
        (reduceQuotient negInv p64 x).toNat = reduceNatQuotient (2 ^ 32) p64.toNat negInv.toNat x.toNat

        The native quotient agrees with the Nat-level Montgomery quotient.

        source
        theorem Montgomery.Native32.conditionalSubtract_toNat {p32 u : UInt32} :
        (conditionalSubtract p32 u).toNat = if u.toNat < p32.toNat then u.toNat else u.toNat - p32.toNat
        source
        theorem Montgomery.Native32.reduceRaw_toNat {modulus : ℕ} {p32 negInv : UInt32} {p64 x : UInt64} (hp32 : p32.toNat = modulus) (hp64 : p64.toNat = modulus) (hp_pos : 0 < modulus) (hp_bound : modulus < 2 ^ 31) (h : x.toNat < modulus * 2 ^ 32) :
        (reduceRaw p32 p64 negInv x).toNat = reduceNat (2 ^ 32) modulus negInv.toNat x.toNat

        Native Montgomery reduction agrees with the natural-number specification.

        source
        theorem Montgomery.Native32.conditionalSubtract_lt {p32 u : UInt32} (h : u.toNat < 2 * p32.toNat) :
        (conditionalSubtract p32 u).toNat < p32.toNat
        source
        theorem Montgomery.Native32.conditionalSubtract_cast {p32 u : UInt32} :
        ↑(conditionalSubtract p32 u).toNat = ↑u.toNat
        source
        theorem Montgomery.Native32.reduceRaw_lt {p32 negInv : UInt32} {p64 x : UInt64} (hp : p32.toNat = p64.toNat) (hp_pos : 0 < p64.toNat) (hp_bound : p64.toNat < 2 ^ 31) (h : x.toNat < p64.toNat * 2 ^ 32) :
        (reduceRaw p32 p64 negInv x).toNat < p32.toNat
        source
        theorem Montgomery.Native32.reduceRaw_cast {modulus : ℕ} {p32 negInv : UInt32} {p64 x : UInt64} [Fact (Nat.Prime modulus)] (hp32 : p32.toNat = modulus) (hp64 : p64.toNat = modulus) (hp_pos : 0 < modulus) (hp_bound : modulus < 2 ^ 31) (hnegInv : negInv.toNat * modulus % 2 ^ 32 = 2 ^ 32 - 1) (hRne : ↑(2 ^ 32) ≠ 0) (h : x.toNat < modulus * 2 ^ 32) :
        ↑(reduceRaw p32 p64 negInv x).toNat = ↑x.toNat * (↑(2 ^ 32))⁻¹