def MontCtx.r2Loop (p : UInt64) : Nat → UInt64 → UInt64

Compute R^2 mod p by repeated doubling in native-word arithmetic.

Equations

• MontCtx.r2Loop p 0 x✝ = x✝
• MontCtx.r2Loop p n.succ x✝ = MontCtx.r2Loop p n (MontCtx.doubleMod✝ p x✝)

def MontCtx.r2OfModulus (p : UInt64) : UInt64

The R^2 mod p constant used to enter Montgomery form.

Equations

• MontCtx.r2OfModulus p = if p ≤ 1 then 0 else have rModP := MontCtx.r2Loop p 64 1; UInt64.ofNat (rModP.toNat * rModP.toNat % p.toNat)

theorem MontCtx.toNat_r2OfModulus (p : UInt64) (hp_pos : 0 < p.toNat) : (r2OfModulus p).toNat = UInt64.word * UInt64.word % p.toNat

The executable r2OfModulus computes R^2 mod p for positive moduli.

def MontCtx.mk (p : UInt64) (hp : p % 2 = 1) : MontCtx p

Build the executable Montgomery context for an odd UInt64 modulus.

Equations

• MontCtx.mk p hp = { p_odd := hp, p' := montInv p, p'_eq := ⋯, r2 := MontCtx.r2OfModulus p, r2_eq := ⋯ }

@[simp]

theorem MontCtx.mk_p_odd (p : UInt64) (hp : p % 2 = 1) : ⋯ = hp

The oddness witness stored by MontCtx.mk.

@[simp]

theorem MontCtx.mk_p' (p : UInt64) (hp : p % 2 = 1) : (mk p hp).p' = montInv p

The Montgomery inverse word stored by MontCtx.mk.

@[simp]

theorem MontCtx.mk_p'_eq (p : UInt64) (hp : p % 2 = 1) : (mk p hp).p'.toNat * p.toNat % UInt64.word = UInt64.word - 1

The inverse-word correctness fact specialized to MontCtx.mk.

@[simp]

theorem MontCtx.mk_r2 (p : UInt64) (hp : p % 2 = 1) : (mk p hp).r2 = r2OfModulus p

The R^2 mod p word stored by MontCtx.mk.

@[simp]

theorem MontCtx.mk_r2_eq (p : UInt64) (hp : p % 2 = 1) : (mk p hp).r2.toNat = UInt64.word * UInt64.word % p.toNat

The R^2 mod p correctness fact specialized to MontCtx.mk.

@[simp]

theorem MontCtx.p_odd_nat {p : UInt64} (ctx : MontCtx p) : p.toNat % 2 = 1

View the odd-modulus assumption as a Nat-level parity fact.

@[simp]

theorem MontCtx.p_pos {p : UInt64} (ctx : MontCtx p) : 0 < p.toNat

An odd UInt64 modulus is positive at the Nat level.

@[simp]

theorem MontCtx.p_lt_R {p : UInt64} (_ctx : MontCtx p) : p.toNat < UInt64.word

Every UInt64 modulus is below the Montgomery radix R = 2^64.

@[simp]

theorem MontCtx.mk_p_odd_nat (p : UInt64) (hp : p % 2 = 1) : p.toNat % 2 = 1

The Nat-level oddness fact specialized to MontCtx.mk.

@[simp]

theorem MontCtx.mk_p_pos (p : UInt64) (hp : p % 2 = 1) : 0 < p.toNat

Positivity of a modulus equipped with MontCtx.mk.

@[simp]

theorem MontCtx.mk_p_lt_R (p : UInt64) (hp : p % 2 = 1) : p.toNat < UInt64.word

The radix bound for a modulus equipped with MontCtx.mk.

@[extern lean_hex_mont_to]

def MontCtx.toMont {p : UInt64} (ctx : MontCtx p) (a : UInt64) : UInt64

Convert a standard residue into Montgomery form.

Equations

• ctx.toMont a = match a.mulFull ctx.r2 with | (hi, lo) => montgomeryReduce ctx hi lo

@[extern lean_hex_mont_from]

def MontCtx.fromMont {p : UInt64} (ctx : MontCtx p) (a : UInt64) : UInt64

Convert a Montgomery residue back to the standard representation.

Equations

• ctx.fromMont a = montgomeryReduce ctx 0 a

@[extern lean_hex_mont_mul]

def MontCtx.mulMont {p : UInt64} (ctx : MontCtx p) (a b : UInt64) : UInt64

Multiply two Montgomery residues, staying inside the Montgomery domain.

Equations

• ctx.mulMont a b = match a.mulFull b with | (hi, lo) => montgomeryReduce ctx hi lo

theorem MontCtx.cancel_word_mod_of_lt {p : UInt64} (ctx : MontCtx p) {x y : Nat} (hx : x < p.toNat) (hy : y < p.toNat) (h : x * UInt64.word % p.toNat = y * UInt64.word % p.toNat) : x = y

Multiplication by word is injective on residues modulo p: since p is odd it is coprime to word = 2 ^ 64, so two reduced values x, y < p with x * word ≡ y * word (mod p) are equal. This is what lets the representative-mod-word characterisation pin down a unique mulMont value.

Public because any word-modular residue layer built on this context (for example a Montgomery-form residue ring) needs the same cancellation to prove that its additive operations preserve the represented value.

theorem MontCtx.fromMont_lt {p : UInt64} (ctx : MontCtx p) (a : UInt64) (ha : a < p) : ctx.fromMont a < p

Converting a reduced Montgomery residue back to standard form is canonical.

theorem MontCtx.fromMont_repr {p : UInt64} (ctx : MontCtx p) (a : UInt64) (ha : a < p) : (ctx.fromMont a).toNat * UInt64.word % p.toNat = a.toNat

fromMont removes one Montgomery radix factor from a reduced Montgomery residue.

@[simp]

theorem MontCtx.toNat_toMont {p : UInt64} (ctx : MontCtx p) (a : UInt64) (ha : a < p) : (ctx.toMont a).toNat = a.toNat * UInt64.word % p.toNat

The Nat value of toMont is multiplication by the Montgomery radix.

theorem MontCtx.toMont_lt {p : UInt64} (ctx : MontCtx p) (a : UInt64) (ha : a < p) : ctx.toMont a < p

Montgomery conversion returns a canonical residue.

theorem MontCtx.mulMont_lt {p : UInt64} (ctx : MontCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) : ctx.mulMont a b < p

Montgomery multiplication returns a canonical residue.

theorem MontCtx.mulMont_repr {p : UInt64} (ctx : MontCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) : (ctx.fromMont (ctx.mulMont a b)).toNat = (ctx.fromMont a).toNat * (ctx.fromMont b).toNat % p.toNat

Montgomery multiplication preserves the represented residue product.

@[simp]

theorem MontCtx.fromMont_toMont {p : UInt64} (ctx : MontCtx p) (a : UInt64) (ha : a < p) : ctx.fromMont (ctx.toMont a) = a

Converting into Montgomery form and back is the identity on reduced inputs.

@[simp]

theorem MontCtx.toNat_mulMont {p : UInt64} (ctx : MontCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) : (ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont b))).toNat = a.toNat * b.toNat % p.toNat

Montgomery multiplication computes modular multiplication after conversion.

theorem MontCtx.mulMont_eq {p : UInt64} (ctx : MontCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) : ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont b)) = UInt64.ofNat (a.toNat * b.toNat % p.toNat)

User-facing equality form of Montgomery multiplication.

@[simp]

theorem MontCtx.fromMont_mulMont_toMont_zero_left {p : UInt64} (ctx : MontCtx p) (a : UInt64) (ha : a < p) : ctx.fromMont (ctx.mulMont (ctx.toMont 0) (ctx.toMont a)) = 0

Multiplying by zero on the left in Montgomery form converts back to zero.

@[simp]

theorem MontCtx.fromMont_mulMont_toMont_zero_right {p : UInt64} (ctx : MontCtx p) (a : UInt64) (ha : a < p) : ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont 0)) = 0

Multiplying by zero on the right in Montgomery form converts back to zero.

def HexArith.bitLength (n : Nat) : Nat

Number of binary digits in a natural number.

Equations

• HexArith.bitLength n = if n = 0 then 0 else n.log2 + 1

theorem HexArith.lt_two_pow_bitLength (n : Nat) : n < 2 ^ bitLength n

Every binary digit of a natural lies below its declared bit length.

def HexArith.powMont {p : UInt64} (ctx : MontCtx p) (base : UInt64) (n : Nat) : UInt64

Exponentiate a Montgomery-form base by repeated squaring.

Equations

• HexArith.powMont ctx base n = HexArith.powMontBitsGo✝ ctx n (HexArith.bitLength n) 0 (ctx.toMont (UInt64.ofNat (1 % p.toNat))) base

def HexArith.powModWordOdd (a n : Nat) (p : UInt64) (hp : p % 2 = 1) : Nat

Word-sized odd-modulus modular exponentiation via Montgomery arithmetic.

Equations

• HexArith.powModWordOdd a n p hp = ((MontCtx.mk p hp).fromMont (HexArith.powMont (MontCtx.mk p hp) ((MontCtx.mk p hp).toMont (UInt64.ofNat (a % p.toNat))) n)).toNat

def HexArith.powModNatGo (n p : Nat) : Nat → Nat → Nat → Nat → Nat

Tail-recursive Nat fallback for modular exponentiation.

Equations

• HexArith.powModNatGo n p 0 x✝² x✝¹ x✝ = x✝¹
• HexArith.powModNatGo n p remaining.succ x✝² x✝¹ x✝ = HexArith.powModNatGo n p remaining (x✝² + 1) (if n.testBit x✝² = true then x✝¹ * x✝ % p else x✝¹) (x✝ * x✝ % p)

def HexArith.powModBits (a n p : Nat) : Nat

Compiled Nat fallback, reducing after every multiplication.

Equations

• HexArith.powModBits a n p = if p = 0 then 0 else HexArith.powModNatGo n p (HexArith.bitLength n) 0 (1 % p) (a % p)

@[simp]

theorem HexArith.powModBits_modulus_zero (a n : Nat) : powModBits a n 0 = 0

powModBits modulo zero returns zero, matching powMod.

theorem HexArith.powModBits_eq (a n p : Nat) (hp : 0 < p) : powModBits a n p = a ^ n % p

powModBits_eq: for a positive modulus, powModBits a n p computes a ^ n % p.

def HexArith.powMod (a n p : Nat) : Nat

Modular exponentiation by repeated squaring, using Montgomery arithmetic for odd UInt64 moduli and a direct Nat fallback otherwise.

This is the runtime twin of powModNat, the kernel-facing specification; powModNat_eq_powMod is the @[csimp] equality relating them.

Equations

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

theorem HexArith.powMod_eq (a n p : Nat) (hp : p > 0) : powMod a n p = a ^ n % p

powMod agrees with ordinary modular exponentiation.

@[simp]

theorem HexArith.powMod_modulus_zero (a n : Nat) : powMod a n 0 = 0

Modular exponentiation modulo zero returns zero.

noncomputable def HexArith.powModNat.go (m : Nat) : Nat → Nat → Nat → Nat → Nat

Kernel reduction loop for powModNat, with an accumulator and decreasing fuel. go m fuel b e acc computes (b ^ e * acc) % m when e < fuel. Nat.rec avoids well-founded recursion, and Bool.rec avoids Decidable unfolding. Adapted from Bhavik Mehta's powModK in PrimeCert; see the license notices above.

Equations

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

noncomputable def HexArith.powModNat.window (b m k : Nat) : Nat → Nat → Nat

Fixed-window loop: window b m k fuel e computes b ^ e % m when 2 ≤ k and e < fuel. The small powers use the kernel's Nat.pow reduction.

Equations

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

noncomputable def HexArith.powModNat (a n p : Nat) : Nat

Kernel-facing modular exponentiation. Six-bit windows through 2^64, four-bit windows through 2^512, three-bit windows through 2^1024, and two-bit windows through 2^2048 reduce kernel recursion. Above that, a reduced base below 2^64 uses two-bit windows through 2^4096, then one-bit windows; other inputs use the binary accumulator. Modulus zero returns zero. Compiled evaluation uses powMod, with their equality proved below.

Equations

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

@[simp]

theorem HexArith.powModNat_modulus_zero (a n : Nat) : powModNat a n 0 = 0

Modular exponentiation modulo zero returns zero.

theorem HexArith.powModNat_eq (a n p : Nat) (hp : 0 < p) : powModNat a n p = a ^ n % p

For a positive modulus, powModNat computes a ^ n % p.

theorem HexArith.powMod_eq_powModNat (a n p : Nat) : powMod a n p = powModNat a n p

The dispatching powMod and the Nat-level powModNat agree at every input, including modulus zero.

@[csimp]

theorem HexArith.powModNat_eq_powMod : powModNat = powMod

powModNat is the kernel-facing specification and powMod its runtime twin: compiled code evaluating powModNat dispatches through powMod, taking the Montgomery path for odd word-sized moduli.

@[simp]

theorem HexArith.powMod_zero_exp (a p : Nat) (hp : p > 0) : powMod a 0 p = 1 % p

Modular exponentiation with exponent zero returns the residue of 1.

@[simp]

theorem HexArith.powMod_one_exp (a p : Nat) (hp : p > 0) : powMod a 1 p = a % p

Modular exponentiation with exponent one returns the reduced base.

@[simp]

theorem HexArith.powMod_zero_base (n p : Nat) (hp : p > 0) : powMod 0 n p = 0 ^ n % p

Modular exponentiation with base zero returns the residue of 0 ^ n.

@[simp]

theorem HexArith.powMod_zero_base_of_pos_exp (n p : Nat) (hn : n > 0) (hp : p > 0) : powMod 0 n p = 0

A positive power of zero is zero modulo any positive modulus.

@[simp]

theorem HexArith.powMod_one_base (n p : Nat) (hp : p > 0) : powMod 1 n p = 1 % p

Modular exponentiation with base one returns the residue of 1.

@[simp]

theorem HexArith.powMod_modulus_one (a n : Nat) : powMod a n 1 = 0

Modular exponentiation modulo one returns zero.

theorem HexArith.powMod_succ (a n p : Nat) (hp : p > 0) : powMod a (n + 1) p = a * powMod a n p % p

Successor-exponent expansion for powMod: multiply by the base on the left and reduce.

@[simp]

theorem HexArith.powMod_mod_base (a n p : Nat) (hp : p > 0) : powMod (a % p) n p = powMod a n p

Reducing the base before modular exponentiation does not change powMod.

theorem HexArith.powMod_mul_base (a b n p : Nat) (hp : p > 0) : powMod (a * b) n p = powMod a n p * powMod b n p % p

Modular exponentiation is compatible with multiplying bases.

theorem HexArith.powMod_add_exp (a m n p : Nat) (hp : p > 0) : powMod a (m + n) p = powMod a m p * powMod a n p % p

Exponent-addition expansion for powMod: combine two exponentiation steps by multiplying their reduced results.

theorem HexArith.powMod_add_exp_left (a m n p : Nat) (hp : p > 0) : powMod a (m + n) p = powMod a n p * powMod a m p % p

Left-oriented companion of powMod_add_exp.

theorem HexArith.powMod_mul_exp (a m n p : Nat) (hp : p > 0) : powMod a (m * n) p = powMod (powMod a m p) n p

Exponent-multiplication composition for powMod: an exponent product is a two-stage modular exponentiation.

theorem HexArith.powMod_mul_exp_swap (a m n p : Nat) (hp : p > 0) : powMod a (m * n) p = powMod (powMod a n p) m p

Swap-oriented companion of powMod_mul_exp.