7.4. Barrett reduction🔗

Barrett reduction computes T mod p for a small modulus p using a single precomputed reciprocal, replacing the hardware division with one multiply-and-shift and at most one corrective subtraction. The Nat-level routine states the arithmetic abstractly over the radix barrettRadix. The reciprocal is pinv = floor(R / p).

def

barrettRadix : Nat
barrettRadix : Nat

The single-word radix used by the UInt64 Barrett reduction.

def

barrettReduceNat (p pinv T : Nat) : Nat
barrettReduceNat (p pinv T : Nat) : Nat

Barrett reduction at the Nat level.

Given T = a * b with T < 2^64 and pinv = floor(R / p), approximate the quotient using one multiply-and-shift step and correct the remainder by at most one subtraction.

The reciprocal approximates the true quotient from below, never overshooting by more than one. These two bounds make the single corrective subtraction sufficient.

theorem

barrettQuotient_le_div {p pinv T : Nat} (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p) : T * pinv / barrettRadix ≤ T / p
barrettQuotient_le_div {p pinv T : Nat}
  (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p) :
  T * pinv / barrettRadix ≤ T / p

The Barrett quotient computed from floor(R / p) never exceeds the exact quotient. This is the no-underflow fact needed when forming T - q * p.

theorem

div_le_barrettQuotient_add_one {p pinv T : Nat} (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p) (hT : T < barrettRadix) :
  T / p ≤ T * pinv / barrettRadix + 1
div_le_barrettQuotient_add_one
  {p pinv T : Nat} (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p)
  (hT : T < barrettRadix) :
  T / p ≤ T * pinv / barrettRadix + 1

The Barrett quotient computed from floor(R / p) is at most one below the exact quotient while T fits in one radix word.

With those bounds, the reducer is proved to compute the residue exactly and to land in the canonical interval [0, p).

theorem

barrettReduceNat_eq_mod {p pinv T : Nat} (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p) (hT : T < barrettRadix) :
  barrettReduceNat p pinv T = T % p
barrettReduceNat_eq_mod {p pinv T : Nat}
  (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p)
  (hT : T < barrettRadix) :
  barrettReduceNat p pinv T = T % p

With pinv = floor(R / p) and T < R, Nat-level Barrett reduction returns the same value as % p.

theorem

barrettReduceNat_lt {p pinv T : Nat} (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p) (hT : T < barrettRadix) :
  barrettReduceNat p pinv T < p
barrettReduceNat_lt {p pinv T : Nat}
  (hp : 1 < p)
  (hpinv : pinv = barrettRadix / p)
  (hT : T < barrettRadix) :
  barrettReduceNat p pinv T < p

Nat-level Barrett reduction always returns a canonical residue.

The executable side packages the modulus and its reciprocal in a BarrettCtx built by BarrettCtx.mk, which checks the small-modulus side conditions once so they need not be re-proved at each call.

structure

BarrettCtx (p : UInt64) : Type
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.

Constructor

BarrettCtx.mkCtx

Fields

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
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.

def

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

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

The machine-word reducer is proved to agree with the Nat model and to return a canonical residue.

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
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
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.