structure BarrettCtx (p : UInt64) : Type

Context for Barrett reduction modulo p, specialized to the small-modulus regime p < 2^32 where products of residues still fit in one UInt64.

• mkCtx :: (
• p_gt : p.toNat > 1

  The modulus is at least 2.

• p_lt : p.toNat < 2 ^ 32

  The small-modulus bound p < 2^32, so products of residues fit in one word.

• pinv : UInt64

  The precomputed reciprocal word ⌊R / p⌋.

• pinv_eq : self.pinv = UInt64.ofNat (barrettRadix / p.toNat)

  The reciprocal field is exactly ⌊R / p⌋.

• )

def BarrettCtx.mk (p : UInt64) (hp : p.toNat > 1) (hlt : p.toNat < 2 ^ 32) : BarrettCtx p

Build the executable Barrett context for a small UInt64 modulus.

Equations

• BarrettCtx.mk p hp hlt = { p_gt := hp, p_lt := hlt, pinv := UInt64.ofNat (barrettRadix / p.toNat), pinv_eq := ⋯ }

def barrettReduce {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) : UInt64

Executable Barrett reduction on a single machine word, using the reciprocal stored in ctx.

Equations

• barrettReduce ctx T = if T - T.mulHi ctx.pinv * p ≥ p then T - T.mulHi ctx.pinv * p - p else T - T.mulHi ctx.pinv * p

@[simp]

theorem BarrettCtx.toNat_pinv {p : UInt64} (ctx : BarrettCtx p) : ctx.pinv.toNat = barrettRadix / p.toNat

The reciprocal stored in a Barrett context is the Nat-level floor(barrettRadix / p), not just propositionally equal as a UInt64.

theorem toNat_barrettReduce {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) (hT : T.toNat < p.toNat * p.toNat) : (barrettReduce ctx T).toNat = barrettReduceNat p.toNat ctx.pinv.toNat T.toNat

The executable Barrett reduction agrees with the Nat-level reduction when the input word is in the small-product range guaranteed by the context hypotheses.

@[simp]

theorem toNat_barrettReduce_eq_mod {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) (hT : T.toNat < p.toNat * p.toNat) : (barrettReduce ctx T).toNat = T.toNat % p.toNat

The executable Barrett reducer returns the ordinary Nat remainder for every input in the small-product range guaranteed by the context.

theorem barrettReduce_lt {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) (hT : T.toNat < p.toNat * p.toNat) : barrettReduce ctx T < p

The executable Barrett reducer returns a canonical residue.

@[simp]

theorem barrettReduce_eq_self_of_lt {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) (hT : T < p) : barrettReduce ctx T = T

Barrett reduction fixes inputs that are already canonical residues.

theorem barrettReduce_eq {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) (hT : T.toNat < p.toNat * p.toNat) : barrettReduce ctx T = UInt64.ofNat (T.toNat % p.toNat)

The executable Barrett reducer agrees with reducing the input word and re-encoding the canonical residue as a UInt64.