def barrettRadix : Nat

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

Equations

• barrettRadix = UInt64.word

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

Equations

• barrettReduceNat p pinv T = if T - T * pinv / barrettRadix * p ≥ p then T - T * pinv / barrettRadix * p - p else T - T * pinv / barrettRadix * p

theorem 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

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

@[simp]

theorem 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

Nat-level Barrett reduction always returns a canonical residue.

@[simp]

theorem barrettReduceNat_eq_self_of_lt {p pinv T : Nat} (hp : 1 < p) (hpinv : pinv = barrettRadix / p) (hpRadix : p ≤ barrettRadix) (hT : T < p) : barrettReduceNat p pinv T = T

Nat-level Barrett reduction fixes inputs that are already canonical residues for a modulus fitting in one radix word.