hex

8.5. Hot-loop operations🔗

Inner loops that multiply many residues under one fixed modulus can amortise the reduction by precomputing a context once. HexModArith wraps the two HexArith kernels for this. Both contexts store the machine-word modulus together with a proof that it agrees with the indexed p, so their results repackage as ordinary Hex.ZMod64 values.

Barrett reduction replaces the per-multiply division by a fixed-shift multiply. The context is built from the small modulus, and its multiplication agrees with the ordinary product.

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

Barrett reduction context specialized to a ZMod64 modulus.

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

Constructor

Hex.BarrettCtx.mk

Fields

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 : BarrettCtx self.modulus

The underlying UInt64 Barrett context from HexArith.

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

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

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

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

Montgomery multiplication works in a transformed domain. Values are first mapped to Montgomery form (a distinct type Hex.MontResidue, so the representation cannot be confused with a standard residue), then multiplied repeatedly without leaving the domain, and converted back once at the end.

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

Temporary Montgomery-form residue for hot loops.

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

Constructor

Hex.MontResidue.mk

Fields

val : UInt64

Backing word for the Montgomery-form representative.

isLt : self.val.toNat < p

The backing word remains reduced modulo p.

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

Montgomery reduction context specialized to a ZMod64 modulus.

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

Constructor

Hex.MontCtx.mk

Fields

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 : MontCtx self.modulus

The underlying UInt64 Montgomery context from HexArith.

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

Convert a standard residue into Montgomery form.

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

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

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

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

Entering Montgomery form, multiplying there, and leaving again computes exactly the ordinary product. This correctness statement licenses swapping the hot loop in for the default multiply.

🔗theorem
Hex.MontCtx.fromMont_mulMont_toMont {p : ℕ} [Hex.ZMod64.Bounds p]
  (ctx : Hex.MontCtx p) (a b : Hex.ZMod64 p) :
  ctx.fromMont (ctx.mulMont (ctx.toMont a) (ctx.toMont b)) = a * b
Hex.MontCtx.fromMont_mulMont_toMont
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (ctx : Hex.MontCtx p)
  (a b : Hex.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 ZMod64 multiplication.

8.5.1. Worked example: Barrett and Montgomery🔗

This block builds both contexts for the prime 7 and checks that each hot-loop product reproduces the ordinary residue product 3 · 5 ≡ 1. The Barrett smart constructor needs 1 < p and p < 2^32; the Montgomery one needs an odd modulus. Both side conditions are discharged by decide.

open Hex Hex.ZMod64 namespace HexModArithChapterHotLoop instance : Bounds 7 := ⟨⊢ 0 < 7 All goals completed! 🐙, ⊢ 7 ≤ UInt64.word All goals completed! 🐙⟩ def a : ZMod64 7 := ofNat 7 3 def b : ZMod64 7 := ofNat 7 5 -- Barrett context for the small prime 7. def bar : Hex.BarrettCtx 7 := Hex.BarrettCtx.ofModulus (p := 7) (⊢ 1 < 7 All goals completed! 🐙) (⊢ 7 < 2 ^ 32 All goals completed! 🐙) -- Montgomery context (7 is odd). def mon : Hex.MontCtx 7 := Hex.MontCtx.ofOddModulus (⊢ 7 < UInt64.word All goals completed! 🐙) (⊢ modulusWord 7 ⋯ % 2 = 1 All goals completed! 🐙) -- Barrett multiplication matches the ordinary product. #guard (bar.mulMod a b).toNat = (a * b).toNat -- A Montgomery round trip is the identity. #guard (mon.fromMont (mon.toMont a)).toNat = a.toNat -- Multiplying inside the Montgomery domain, then leaving, -- agrees with the ordinary product. #guard (mon.fromMont (mon.mulMont (mon.toMont a) (mon.toMont b))).toNat = (a * b).toNat end HexModArithChapterHotLoop