@[inline, extern lean_hex_word_mod_add]

def Hex.addModWord (m a b : UInt64) : UInt64

Full-range modular addition of two residues below m.

Equations

• Hex.addModWord m a b = if ((a.addCarry b false).snd || decide (m ≤ (a.addCarry b false).fst)) = true then ((a.addCarry b false).fst.subBorrow m false).fst else (a.addCarry b false).fst

@[inline, extern lean_hex_word_mod_sub]

def Hex.subModWord (m a b : UInt64) : UInt64

Full-range modular subtraction of two residues below m.

Equations

• Hex.subModWord m a b = if (a.subBorrow b false).snd = true then ((a.subBorrow b false).fst.addCarry m false).fst else (a.subBorrow b false).fst

theorem Hex.toNat_addModWord (m a b : UInt64) (hm : m.toNat ≤ UInt64.word) (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) : (addModWord m a b).toNat = (a.toNat + b.toNat) % m.toNat

addModWord computes the modular sum.

theorem Hex.addModWord_lt (m a b : UInt64) (hm : 0 < m.toNat) (hmw : m.toNat ≤ UInt64.word) (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) : (addModWord m a b).toNat < m.toNat

addModWord stays below m.

theorem Hex.toNat_subModWord (m a b : UInt64) (hm : m.toNat ≤ UInt64.word) (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) : (subModWord m a b).toNat = (a.toNat + (m.toNat - b.toNat)) % m.toNat

subModWord computes the modular difference.

theorem Hex.subModWord_lt (m a b : UInt64) (hm : 0 < m.toNat) (hmw : m.toNat ≤ UInt64.word) (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) : (subModWord m a b).toNat < m.toNat

structure Hex.WordMod {m : UInt64} (ctx : MontCtx m) : Type

Residues modulo an odd m < 2^64, stored in Montgomery form. val is the Montgomery representative; the represented residue is ctx.fromMont val.

The packed native polynomial kernels rely on proof erasure leaving val as the sole runtime constructor field. Any new data-bearing field requires a matching FFI update and native cross-check.

• val : UInt64

  Montgomery-form representative.

• isLt : self.val < m

  The representative is reduced.

theorem Hex.WordMod.ext {m : UInt64} {ctx : MontCtx m} {a b : WordMod ctx} (h : a.val = b.val) : a = b

theorem Hex.WordMod.ext_iff {m : UInt64} {ctx : MontCtx m} {a b : WordMod ctx} : a = b ↔ a.val = b.val

@[instance_reducible]

instance Hex.WordMod.instDecidableEq {m : UInt64} {ctx : MontCtx m} : DecidableEq (WordMod ctx)

Equations

• a.instDecidableEq b = if h : a.val = b.val then isTrue ⋯ else isFalse ⋯

@[inline]

def Hex.WordMod.toNat {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : Nat

Represented residue as a Nat in [0, m).

Equations

• a.toNat = (ctx.fromMont a.val).toNat

theorem Hex.WordMod.val_toNat_lt {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : a.val.toNat < m.toNat

theorem Hex.WordMod.m_le_word {m : UInt64} (ctx : MontCtx m) : m.toNat ≤ UInt64.word

theorem Hex.WordMod.toNat_lt {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : a.toNat < m.toNat

theorem Hex.WordMod.toNat_mul_word {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : a.toNat * UInt64.word % m.toNat = a.val.toNat

Multiplication by word recovers the Montgomery representative: the key input to the word-cancellation used by the additive specs.

@[inline]

def Hex.WordMod.ofNat {m : UInt64} {ctx : MontCtx m} (n : Nat) : WordMod ctx

Reduce a Nat into WordMod ctx.

Equations

• Hex.WordMod.ofNat n = { val := ctx.toMont (UInt64.ofNat (n % m.toNat)), isLt := ⋯ }

@[simp]

theorem Hex.WordMod.toNat_ofNat {m : UInt64} {ctx : MontCtx m} (n : Nat) : (ofNat n).toNat = n % m.toNat

@[instance_reducible]

instance Hex.WordMod.instZero {m : UInt64} {ctx : MontCtx m} : Zero (WordMod ctx)

Equations

• Hex.WordMod.instZero = { zero := Hex.WordMod.ofNat 0 }

@[instance_reducible]

instance Hex.WordMod.instOne {m : UInt64} {ctx : MontCtx m} : One (WordMod ctx)

Equations

• Hex.WordMod.instOne = { one := Hex.WordMod.ofNat 1 }

@[instance_reducible]

instance Hex.WordMod.instNatCast {m : UInt64} {ctx : MontCtx m} : NatCast (WordMod ctx)

Equations

• Hex.WordMod.instNatCast = { natCast := Hex.WordMod.ofNat }

@[inline]

def Hex.WordMod.div {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : WordMod ctx

Division, defined only where it is used: by the leading coefficient of a monic divisor, which is 1. Dividing by 1 is the identity (div_one); other divisors return 0 and are never exercised by monic divMod.

Equations

• a.div b = if b = 1 then a else 0

@[instance_reducible]

instance Hex.WordMod.instDiv {m : UInt64} {ctx : MontCtx m} : Div (WordMod ctx)

Equations

• Hex.WordMod.instDiv = { div := Hex.WordMod.div }

@[simp]

theorem Hex.WordMod.div_one {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : a / 1 = a

@[simp]

theorem Hex.WordMod.toNat_zero {m : UInt64} {ctx : MontCtx m} : toNat 0 = 0

@[simp]

theorem Hex.WordMod.toNat_one {m : UInt64} {ctx : MontCtx m} : toNat 1 = 1 % m.toNat

@[inline]

def Hex.WordMod.mul {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : WordMod ctx

Montgomery multiplication: one reduction.

Equations

• a.mul b = { val := ctx.mulMont a.val b.val, isLt := ⋯ }

@[instance_reducible]

instance Hex.WordMod.instMul {m : UInt64} {ctx : MontCtx m} : Mul (WordMod ctx)

Equations

• Hex.WordMod.instMul = { mul := Hex.WordMod.mul }

@[simp]

theorem Hex.WordMod.toNat_mul {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : (a * b).toNat = a.toNat * b.toNat % m.toNat

@[inline]

def Hex.WordMod.add {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : WordMod ctx

Full-range modular addition.

Equations

• a.add b = { val := Hex.addModWord m a.val b.val, isLt := ⋯ }

@[instance_reducible]

instance Hex.WordMod.instAdd {m : UInt64} {ctx : MontCtx m} : Add (WordMod ctx)

Equations

• Hex.WordMod.instAdd = { add := Hex.WordMod.add }

@[inline]

def Hex.WordMod.sub {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : WordMod ctx

Full-range modular subtraction.

Equations

• a.sub b = { val := Hex.subModWord m a.val b.val, isLt := ⋯ }

@[instance_reducible]

instance Hex.WordMod.instSub {m : UInt64} {ctx : MontCtx m} : Sub (WordMod ctx)

Equations

• Hex.WordMod.instSub = { sub := Hex.WordMod.sub }

@[inline]

def Hex.WordMod.neg {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : WordMod ctx

Modular negation, as subtraction from zero.

Equations

• a.neg = 0 - a

@[instance_reducible]

instance Hex.WordMod.instNeg {m : UInt64} {ctx : MontCtx m} : Neg (WordMod ctx)

Equations

• Hex.WordMod.instNeg = { neg := Hex.WordMod.neg }

def Hex.WordMod.pow {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : Nat → WordMod ctx

Iterated product, the natural-power operation.

Equations

• a.pow 0 = 1
• a.pow n.succ = a.pow n * a

@[instance_reducible]

instance Hex.WordMod.instPowNat {m : UInt64} {ctx : MontCtx m} : Pow (WordMod ctx) Nat

Equations

• Hex.WordMod.instPowNat = { pow := Hex.WordMod.pow }

@[instance_reducible]

instance Hex.WordMod.instOfNat {m : UInt64} {ctx : MontCtx m} (n : Nat) : OfNat (WordMod ctx) n

Equations

• Hex.WordMod.instOfNat n = { ofNat := Hex.WordMod.ofNat n }

@[instance_reducible]

instance Hex.WordMod.instSMulNat {m : UInt64} {ctx : MontCtx m} : SMul Nat (WordMod ctx)

Equations

• Hex.WordMod.instSMulNat = { smul := fun (n : Nat) (a : Hex.WordMod ctx) => ↑n * a }

@[instance_reducible]

instance Hex.WordMod.instIntCast {m : UInt64} {ctx : MontCtx m} : IntCast (WordMod ctx)

Equations

• Hex.WordMod.instIntCast = { intCast := fun (i : Int) => match i with | Int.ofNat n => ↑n | Int.negSucc n => -↑(n + 1) }

@[instance_reducible]

instance Hex.WordMod.instSMulInt {m : UInt64} {ctx : MontCtx m} : SMul Int (WordMod ctx)

Equations

• Hex.WordMod.instSMulInt = { smul := fun (i : Int) (a : Hex.WordMod ctx) => ↑i * a }

@[simp]

theorem Hex.WordMod.toNat_add {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : (a + b).toNat = (a.toNat + b.toNat) % m.toNat

@[simp]

theorem Hex.WordMod.toNat_sub {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : (a - b).toNat = (a.toNat + (m.toNat - b.toNat)) % m.toNat

@[simp]

theorem Hex.WordMod.toNat_neg {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) : (-a).toNat = (m.toNat - a.toNat) % m.toNat

@[simp]

theorem Hex.WordMod.toNat_pow {m : UInt64} {ctx : MontCtx m} (a : WordMod ctx) (n : Nat) : (a ^ n).toNat = a.toNat ^ n % m.toNat

@[simp]

theorem Hex.WordMod.toNat_nsmul {m : UInt64} {ctx : MontCtx m} (n : Nat) (a : WordMod ctx) : (n • a).toNat = n % m.toNat * a.toNat % m.toNat

@[simp]

theorem Hex.WordMod.toNat_neg_mul {m : UInt64} {ctx : MontCtx m} (a b : WordMod ctx) : (-a * b).toNat = (m.toNat - a.toNat * b.toNat % m.toNat) % m.toNat