structure Hex.BarrettCtx (p : Nat) [ZMod64.Bounds p] : Type

Barrett reduction context specialized to a Hex.ZMod64 modulus.

The stored UInt64 modulus must agree with the Nat-indexed Hex.ZMod64 modulus; the underlying HexArith context then provides the small-modulus fast path.

• modulus : UInt64

  The executable machine-word modulus used by the underlying context.

• modulus_eq : self.modulus.toNat = p

  The stored word modulus agrees with the Nat-indexed ZMod64 modulus.

• toUInt64Ctx : _root_.BarrettCtx self.modulus

  The underlying UInt64 Barrett context from HexArith.

structure Hex.MontCtx (p : Nat) [ZMod64.Bounds p] : Type

Montgomery reduction context specialized to a ZMod64 modulus.

As with Hex.BarrettCtx, the executable context stores the machine-word modulus used by the underlying HexArith Montgomery code.

• modulus : UInt64

  The executable machine-word modulus used by the underlying context.

• modulus_eq : self.modulus.toNat = p

  The stored word modulus agrees with the Nat-indexed ZMod64 modulus.

• toUInt64Ctx : _root_.MontCtx self.modulus

  The underlying UInt64 Montgomery context from HexArith.

structure Hex.MontResidue (p : Nat) [ZMod64.Bounds p] : Type

Temporary Montgomery-form residue for hot loops.

This is intentionally distinct from Hex.ZMod64: values are still reduced into [0, p), but they represent residues in Montgomery form rather than the canonical standard representative.

• val : UInt64

  Backing word for the Montgomery-form representative.

• isLt : self.val.toNat < p

  The backing word remains reduced modulo p.

def Hex.MontResidue.toUInt64 {p : Nat} [ZMod64.Bounds p] (a : MontResidue p) : UInt64

View a Montgomery-form residue as its backing machine word.

Equations

• a.toUInt64 = a.val

def Hex.MontResidue.toNat {p : Nat} [ZMod64.Bounds p] (a : MontResidue p) : Nat

View a Montgomery-form residue as its reduced Nat representative.

Equations

• a.toNat = a.val.toNat

@[instance_reducible]

instance Hex.MontResidue.instCoeOutUInt64 {p : Nat} [ZMod64.Bounds p] : CoeOut (MontResidue p) UInt64

Equations

• Hex.MontResidue.instCoeOutUInt64 = { coe := Hex.MontResidue.toUInt64 }

@[instance_reducible]

instance Hex.MontResidue.instCoeOutNat {p : Nat} [ZMod64.Bounds p] : CoeOut (MontResidue p) Nat

Equations

• Hex.MontResidue.instCoeOutNat = { coe := Hex.MontResidue.toNat }

@[simp]

theorem Hex.MontResidue.toUInt64_eq_val {p : Nat} [ZMod64.Bounds p] (a : MontResidue p) : a.toUInt64 = a.val

The UInt64 view of a Montgomery residue is its backing word.

@[simp]

theorem Hex.MontResidue.toNat_eq_val {p : Nat} [ZMod64.Bounds p] (a : MontResidue p) : a.toNat = a.val.toNat

The Nat view of a Montgomery residue is the Nat value of its backing word.

@[simp]

theorem Hex.MontResidue.toNat_lt {p : Nat} [ZMod64.Bounds p] (a : MontResidue p) : a.toNat < p

The Nat view of a Montgomery residue is reduced modulo its indexed modulus.

theorem Hex.MontResidue.ext {p : Nat} [ZMod64.Bounds p] {a b : MontResidue p} (h : a.val = b.val) : a = b

Montgomery residues are equal when their backing words are equal.

theorem Hex.MontResidue.ext_iff {p : Nat} [ZMod64.Bounds p] {a b : MontResidue p} : a = b ↔ a.val = b.val

theorem Hex.MontResidue.ext_toNat {p : Nat} [ZMod64.Bounds p] {a b : MontResidue p} (h : a.toNat = b.toNat) : a = b

Extensionality for Montgomery residues via their canonical Nat representatives.

theorem Hex.MontResidue.eq_iff_toNat_eq {p : Nat} [ZMod64.Bounds p] (a b : MontResidue p) : a = b ↔ a.toNat = b.toNat

Two Montgomery residues are equal exactly when their canonical representatives agree.

def Hex.BarrettCtx.ofModulus {p : Nat} [ZMod64.Bounds p] (hp : 1 < p) (hlt : p < 2 ^ 32) : BarrettCtx p

Build a Barrett hot-loop context from the indexed small modulus.

Equations

• Hex.BarrettCtx.ofModulus hp hlt = { modulus := UInt64.ofNat p, modulus_eq := ⋯, toUInt64Ctx := BarrettCtx.mk (UInt64.ofNat p) ⋯ ⋯ }

@[simp]

theorem Hex.BarrettCtx.ofModulus_modulus {p : Nat} [ZMod64.Bounds p] (hp : 1 < p) (hlt : p < 2 ^ 32) : (ofModulus hp hlt).modulus = UInt64.ofNat p

The smart constructor stores the indexed modulus as a machine word.

@[simp]

theorem Hex.BarrettCtx.ofModulus_modulus_eq {p : Nat} [ZMod64.Bounds p] (hp : 1 < p) (hlt : p < 2 ^ 32) : (ofModulus hp hlt).modulus.toNat = p

The smart constructor's stored word modulus agrees with the indexed modulus.

theorem Hex.BarrettCtx.ofModulus_toUInt64Ctx {p : Nat} [ZMod64.Bounds p] (hp : 1 < p) (hlt : p < 2 ^ 32) : (ofModulus hp hlt).toUInt64Ctx = _root_.BarrettCtx.mk (UInt64.ofNat p) ⋯ ⋯

The smart constructor delegates to the underlying UInt64 Barrett context.

@[simp]

theorem Hex.BarrettCtx.ofModulus_toUInt64Ctx_pinv {p : Nat} [ZMod64.Bounds p] (hp : 1 < p) (hlt : p < 2 ^ 32) : (ofModulus hp hlt).toUInt64Ctx.pinv = UInt64.ofNat (barrettRadix / p)

The smart constructor's underlying Barrett context stores the reciprocal for the indexed modulus.

def Hex.BarrettCtx.mulMod {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a b : ZMod64 p) : ZMod64 p

Multiply two standard residues using the Barrett context and repackage the result as a Hex.ZMod64.

Equations

• ctx.mulMod a b = Hex.ZMod64.ofNat p (ctx.toUInt64Ctx.mulMod a.toUInt64 b.toUInt64).toNat

@[simp]

theorem Hex.BarrettCtx.toNat_mulMod {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a b : ZMod64 p) : (ctx.mulMod a b).toNat = a.toNat * b.toNat % p

The Hex.ZMod64 Barrett wrapper computes the ordinary modular product on reduced representatives.

@[simp]

theorem Hex.BarrettCtx.mulMod_eq_mul {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a b : ZMod64 p) : ctx.mulMod a b = a * b

Barrett hot-loop multiplication agrees with the ordinary ZMod64 multiplication surface.

@[simp]

theorem Hex.BarrettCtx.mulMod_one_left {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a : ZMod64 p) : ctx.mulMod 1 a = a

Barrett hot-loop multiplication by one on the left returns the original standard residue.

@[simp]

theorem Hex.BarrettCtx.mulMod_zero_left {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a : ZMod64 p) : ctx.mulMod 0 a = 0

Barrett hot-loop multiplication by zero on the left returns zero.

@[simp]

theorem Hex.BarrettCtx.mulMod_one_right {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a : ZMod64 p) : ctx.mulMod a 1 = a

Barrett hot-loop multiplication by one on the right returns the original standard residue.

@[simp]

theorem Hex.BarrettCtx.mulMod_zero_right {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a : ZMod64 p) : ctx.mulMod a 0 = 0

Barrett hot-loop multiplication by zero on the right returns zero.

theorem Hex.BarrettCtx.mulMod_comm {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a b : ZMod64 p) : ctx.mulMod a b = ctx.mulMod b a

Barrett hot-loop multiplication is commutative on standard residues.

theorem Hex.BarrettCtx.mulMod_assoc {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) (a b c : ZMod64 p) : ctx.mulMod (ctx.mulMod a b) c = ctx.mulMod a (ctx.mulMod b c)

Barrett hot-loop multiplication is associative on standard residues.

def Hex.MontCtx.ofOddModulus {p : Nat} [ZMod64.Bounds p] (hp : p < UInt64.word) (hodd : ZMod64.modulusWord p hp % 2 = 1) : MontCtx p

Build a Montgomery hot-loop context from the indexed modulus and the word-level odd-modulus side condition required by the underlying HexArith context.

Equations

• Hex.MontCtx.ofOddModulus hp hodd = { modulus := Hex.ZMod64.modulusWord p hp, modulus_eq := ⋯, toUInt64Ctx := MontCtx.mk (Hex.ZMod64.modulusWord p hp) hodd }

@[simp]

theorem Hex.MontCtx.modulus_ofOddModulus {p : Nat} [ZMod64.Bounds p] (hp : p < UInt64.word) (hodd : ZMod64.modulusWord p hp % 2 = 1) : (ofOddModulus hp hodd).modulus = ZMod64.modulusWord p hp

The smart constructor stores the canonical machine-word modulus.

@[simp]

theorem Hex.MontCtx.modulus_toNat_ofOddModulus {p : Nat} [ZMod64.Bounds p] (hp : p < UInt64.word) (hodd : ZMod64.modulusWord p hp % 2 = 1) : (ofOddModulus hp hodd).modulus.toNat = p

The smart constructor's stored word modulus agrees with the indexed modulus.

@[simp]

theorem Hex.MontCtx.toUInt64Ctx_ofOddModulus {p : Nat} [ZMod64.Bounds p] (hp : p < UInt64.word) (hodd : ZMod64.modulusWord p hp % 2 = 1) : (ofOddModulus hp hodd).toUInt64Ctx = _root_.MontCtx.mk (ZMod64.modulusWord p hp) hodd

The smart constructor delegates to the underlying UInt64 Montgomery context.

def Hex.MontCtx.toMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : MontResidue p

Convert a standard residue into Montgomery form.

Equations

• ctx.toMont a = { val := ctx.toUInt64Ctx.toMont a.toUInt64, isLt := ⋯ }

def Hex.MontCtx.mulMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a b : MontResidue p) : MontResidue p

Multiply two Montgomery-form residues, staying inside the Montgomery domain.

Equations

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

def Hex.MontCtx.fromMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : MontResidue p) : ZMod64 p

Convert a Montgomery-form loop temporary back to the standard Hex.ZMod64 representation.

Equations

• ctx.fromMont a = Hex.ZMod64.ofNat p (ctx.toUInt64Ctx.fromMont a.toUInt64).toNat

theorem Hex.MontCtx.toUInt64_toMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : (ctx.toMont a).toUInt64 = ctx.toUInt64Ctx.toMont a.toUInt64

toMont delegates to the underlying UInt64 Montgomery conversion.

theorem Hex.MontCtx.toUInt64_mulMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a b : MontResidue p) : (ctx.mulMont a b).toUInt64 = ctx.toUInt64Ctx.mulMont a.toUInt64 b.toUInt64

mulMont delegates to the underlying UInt64 Montgomery multiplication.

theorem Hex.MontCtx.toNat_fromMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : MontResidue p) : (ctx.fromMont a).toNat = (ctx.toUInt64Ctx.fromMont a.toUInt64).toNat

fromMont exposes the reduced Nat value computed by the underlying context.

@[simp]

theorem Hex.MontCtx.toNat_toMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : (ctx.toMont a).toNat = a.toNat * UInt64.word % p

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

theorem Hex.MontCtx.fromMont_repr {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : MontResidue p) : (ctx.fromMont a).toNat * UInt64.word % p = a.toNat

fromMont removes one Montgomery radix factor from a Montgomery-form loop temporary.

@[simp]

theorem Hex.MontCtx.fromMont_toMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : ctx.fromMont (ctx.toMont a) = a

Converting a standard residue into Montgomery form and back is the identity.

@[simp]

theorem Hex.MontCtx.toNat_mulMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a b : ZMod64 p) : (ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont b))).toNat = a.toNat * b.toNat % p

Multiplying two standard residues by entering Montgomery form, multiplying, and leaving Montgomery form computes the ordinary modular product.

@[simp]

theorem Hex.MontCtx.mulMont_repr {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a b : MontResidue p) : (ctx.fromMont (ctx.mulMont a b)).toNat = (ctx.fromMont a).toNat * (ctx.fromMont b).toNat % p

Montgomery multiplication preserves the represented standard-residue product when converted back out of Montgomery form.

@[simp]

theorem Hex.MontCtx.fromMont_mulMont_toMont {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a b : ZMod64 p) : ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont b)) = a * b

Multiplying two standard residues by entering Montgomery form, multiplying, and leaving Montgomery form agrees with ordinary Hex.ZMod64 multiplication.

@[simp]

theorem Hex.MontCtx.fromMont_mulMont_toMont_one_left {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : ctx.fromMont (ctx.mulMont (ctx.toMont 1) (ctx.toMont a)) = a

The Montgomery round trip for a wrapped product returns the original residue when the left standard input is one.

@[simp]

theorem Hex.MontCtx.fromMont_mulMont_toMont_zero_left {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : ctx.fromMont (ctx.mulMont (ctx.toMont 0) (ctx.toMont a)) = 0

The Montgomery round trip for a wrapped product returns zero when the left standard input is zero.

@[simp]

theorem Hex.MontCtx.fromMont_mulMont_toMont_one_right {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont 1)) = a

The Montgomery round trip for a wrapped product returns the original residue when the right standard input is one.

@[simp]

theorem Hex.MontCtx.fromMont_mulMont_toMont_zero_right {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a : ZMod64 p) : ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont 0)) = 0

The Montgomery round trip for a wrapped product returns zero when the right standard input is zero.

theorem Hex.MontCtx.fromMont_mulMont_toMont_comm {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a b : ZMod64 p) : ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont b)) = ctx.fromMont (ctx.mulMont (ctx.toMont b) (ctx.toMont a))

The Montgomery round trip for a wrapped product is commutative on standard residue inputs.

theorem Hex.MontCtx.fromMont_mulMont_toMont_assoc {p : Nat} [ZMod64.Bounds p] (ctx : MontCtx p) (a b c : ZMod64 p) : ctx.fromMont (ctx.mulMont (ctx.toMont (ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont b)))) (ctx.toMont c)) = ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont (ctx.fromMont (ctx.mulMont (ctx.toMont b) (ctx.toMont c)))))

The Montgomery round trip for wrapped products is associative on standard residue inputs.