Documentation

HexArith.Barrett.Context

source
@[simp]
theorem BarrettCtx.mk_p_gt (p : UInt64) (hp : p.toNat > 1) (hlt : p.toNat < 2 ^ 32) :
⋯ = hp

The small-modulus lower-bound proof stored by BarrettCtx.mk.

source
@[simp]
theorem BarrettCtx.mk_p_lt (p : UInt64) (hp : p.toNat > 1) (hlt : p.toNat < 2 ^ 32) :
⋯ = hlt

The small-modulus upper-bound proof stored by BarrettCtx.mk.

source
@[simp]
theorem BarrettCtx.mk_pinv (p : UInt64) (hp : p.toNat > 1) (hlt : p.toNat < 2 ^ 32) :
(mk p hp hlt).pinv = UInt64.ofNat (barrettRadix / p.toNat)

The reciprocal word stored by BarrettCtx.mk.

source
@[simp]
theorem BarrettCtx.mk_pinv_toNat (p : UInt64) (hp : p.toNat > 1) (hlt : p.toNat < 2 ^ 32) :
(mk p hp hlt).pinv.toNat = barrettRadix / p.toNat

The Nat value of the reciprocal word stored by BarrettCtx.mk.

source
def BarrettCtx.mulMod {p : UInt64} (ctx : BarrettCtx p) (a b : UInt64) :
UInt64

Multiply two residues modulo p using the Barrett reduction context. The caller-side condition a, b < p < 2^32 ensures the product fits in one UInt64.

Equations
Instances For
    source
    @[simp]
    theorem BarrettCtx.toNat_mulMod {p : UInt64} (ctx : BarrettCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) :
    (ctx.mulMod a b).toNat = a.toNat * b.toNat % p.toNat

    The Nat value of Barrett modular multiplication is the ordinary modular product.

    source
    theorem BarrettCtx.mulMod_lt {p : UInt64} (ctx : BarrettCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) :
    ctx.mulMod a b < p

    Barrett modular multiplication returns a residue strictly below the modulus.

    source
    theorem BarrettCtx.mulMod_eq {p : UInt64} (ctx : BarrettCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) :
    ctx.mulMod a b = UInt64.ofNat (a.toNat * b.toNat % p.toNat)

    Barrett modular multiplication agrees with reducing the Nat-level product and re-encoding it as a UInt64.

    source
    @[simp]
    theorem BarrettCtx.mulMod_eq_mul_of_mul_lt {p : UInt64} (ctx : BarrettCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) (hmul : a.toNat * b.toNat < p.toNat) :
    ctx.mulMod a b = a * b

    Barrett modular multiplication fixes products that are already canonical residues.

    source
    @[simp]
    theorem BarrettCtx.mulMod_zero_left {p : UInt64} (ctx : BarrettCtx p) (b : UInt64) (hb : b < p) :
    ctx.mulMod 0 b = 0

    Zero is a left absorbing element for Barrett modular multiplication.

    source
    @[simp]
    theorem BarrettCtx.mulMod_zero_right {p : UInt64} (ctx : BarrettCtx p) (a : UInt64) (ha : a < p) :
    ctx.mulMod a 0 = 0

    Zero is a right absorbing element for Barrett modular multiplication.

    source
    @[simp]
    theorem BarrettCtx.mulMod_one_left {p : UInt64} (ctx : BarrettCtx p) (a : UInt64) (ha : a < p) :
    ctx.mulMod 1 a = a

    One is a left identity for Barrett modular multiplication on reduced residues.

    source
    @[simp]
    theorem BarrettCtx.mulMod_one_right {p : UInt64} (ctx : BarrettCtx p) (a : UInt64) (ha : a < p) :
    ctx.mulMod a 1 = a

    One is a right identity for Barrett modular multiplication on reduced residues.

    source
    theorem BarrettCtx.mulMod_comm {p : UInt64} (ctx : BarrettCtx p) (a b : UInt64) (ha : a < p) (hb : b < p) :
    ctx.mulMod a b = ctx.mulMod b a

    Barrett modular multiplication is commutative on reduced residues.