structure MontCtx (p : UInt64) : Type

Runtime Montgomery context for an odd UInt64 modulus.

The native Montgomery externs rely on proof erasure leaving p' and r2 as runtime constructor fields 0 and 1. Any change to the data-bearing fields must be mirrored in the C accessors and the native cross-checks.

• mkCtx :: (
• p_odd : p % 2 = 1

  The modulus is odd.

• p' : UInt64

  The Montgomery inverse word, satisfying p' · p ≡ -1 (mod R).

• p'_eq : self.p'.toNat * p.toNat % UInt64.word = UInt64.word - 1

  The inverse field satisfies p' · p ≡ R - 1 (mod R).

• r2 : UInt64

  The constant R² mod p, used to convert a residue into Montgomery form.

• r2_eq : self.r2.toNat = UInt64.word * UInt64.word % p.toNat

  The r2 field is exactly R² mod p.

• )

@[extern lean_hex_montgomery_reduce]

def montgomeryReduce {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64) : UInt64

Executable Montgomery reduction (classically REDC) from a two-word product (Thi, Tlo) encoded in base 2^64.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem montgomeryReduce_m_spec {p : UInt64} (ctx : MontCtx p) (_Thi Tlo : UInt64) : have m := Tlo * ctx.p'; m.toNat = Tlo.toNat * ctx.p'.toNat % UInt64.word

The low-word multiply computes the Montgomery correction factor m.

theorem montgomeryReduce_u_spec {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64) : have m := Tlo * ctx.p'; match m.mulFull p with | (mhi, mlo) => match Tlo.addCarry mlo false with | (fst, c1) => match Thi.addCarry mhi c1 with | (addHi, c2) => addHi.toNat + c2.toNat * UInt64.word = (Tlo.toNat + Thi.toNat * UInt64.word + m.toNat * p.toNat) / UInt64.word

The carry pair (c2, addHi) represents the exact quotient u, stated over the (mhi, mlo) pair returned by UInt64.mulFull m p rather than the split (UInt64.mulHi m p, m * p) view.

theorem montgomeryReduce_sub_spec {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64) (hT : Tlo.toNat + Thi.toNat * UInt64.word < p.toNat * UInt64.word) : (montgomeryReduce ctx Thi Tlo).toNat = montgomeryReduceNat p.toNat ctx.p'.toNat (Tlo.toNat + Thi.toNat * UInt64.word)

The final subtraction logic matches the Nat-level REDC normalization step.

theorem toNat_montgomeryReduce {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64) (hT : Tlo.toNat + Thi.toNat * UInt64.word < p.toNat * UInt64.word) : (montgomeryReduce ctx Thi Tlo).toNat = montgomeryReduceNat p.toNat ctx.p'.toNat (Tlo.toNat + Thi.toNat * UInt64.word)

The executable REDC routine agrees with the Nat-level specification.

theorem montgomeryReduce_lt {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64) (hT : Tlo.toNat + Thi.toNat * UInt64.word < p.toNat * UInt64.word) : montgomeryReduce ctx Thi Tlo < p

Executable REDC returns a canonical residue below the modulus.

theorem montgomeryReduce_mul_word_mod {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64) (hT : Tlo.toNat + Thi.toNat * UInt64.word < p.toNat * UInt64.word) : (montgomeryReduce ctx Thi Tlo).toNat * UInt64.word % p.toNat = (Tlo.toNat + Thi.toNat * UInt64.word) % p.toNat

Executable REDC represents division by the Montgomery radix modulo p.

This is the direct executable form of montgomeryReduceNat_eq_mod, avoiding an explicit unfolding through the Nat-level REDC definition for downstream callers.