theorem BarrettCtx.toNat_barrettReduce_mod {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) : (barrettReduce ctx T).toNat = T.toNat % p.toNat

barrettReduce computes T % p for every input word, not only for inputs below p^2. The single-word reducer only needs T < 2^64, which holds for every UInt64; the p^2 bound in toNat_barrettReduce_eq_mod is stronger than necessary. This is the reduction the wide accumulator flushes through.

theorem BarrettCtx.barrettReduce_lt_mod {p : UInt64} (ctx : BarrettCtx p) (T : UInt64) : barrettReduce ctx T < p

The full-range reducer returns a canonical residue for every input word.

def BarrettCtx.accVal (lo hi : UInt64) : Nat

The value carried by a two-word accumulator (lo, hi) in radix 2^64.

Equations

• BarrettCtx.accVal lo hi = lo.toNat + hi.toNat * UInt64.word

def BarrettCtx.accAddWord (lo hi q : UInt64) : UInt64 × UInt64

Add a single product word q into the two-word accumulator (lo, hi), propagating the carry into the high word.

Equations

• BarrettCtx.accAddWord lo hi q = match lo.addCarry q false with | (lo', c) => (lo', if c = true then hi + 1 else hi)

theorem BarrettCtx.accVal_accAddWord (lo hi q : UInt64) (hhi : hi.toNat + 1 < UInt64.word) : accVal (accAddWord lo hi q).fst (accAddWord lo hi q).snd = accVal lo hi + q.toNat

Adding a product word to the accumulator increases its value by exactly the product, provided the high word does not overflow (hi.toNat + 1 < 2^64).

theorem BarrettCtx.accAddWord_eq_inline (lo hi q : UInt64) : accAddWord lo hi q = (lo + q, hi + if lo + q < lo then 1 else 0)

accAddWord in inline-carry form: the wrapped word add, with the carry read off the wraparound compare (lo + q < lo) and added to the high word as a bit. This is the shape the delayed-reduction kernel's scalar loop computes per term (no addCarry extern call); the equality identifies that loop's step with accStep below.

def BarrettCtx.accReduce {p : UInt64} (ctx : BarrettCtx p) (cR lo hi : UInt64) : UInt64

Reduce the two-word accumulator (lo, hi) modulo p, using the precomputed constant cR = 2^64 % p. The scheme reduces each half, folds the high half in through cR, and reduces once more: (lo + hi * 2^64) % p = ((hi % p) * (2^64 % p) + lo % p) % p.

Equations

• ctx.accReduce cR lo hi = barrettReduce ctx (barrettReduce ctx (barrettReduce ctx hi * cR) + barrettReduce ctx lo)

theorem BarrettCtx.toNat_accReduce {p : UInt64} (ctx : BarrettCtx p) (cR lo hi : UInt64) (hcR : cR.toNat = UInt64.word % p.toNat) : (ctx.accReduce cR lo hi).toNat = accVal lo hi % p.toNat

accReduce computes (lo + hi * 2^64) % p, the residue of the full two-word accumulator value.

theorem BarrettCtx.accReduce_lt {p : UInt64} (ctx : BarrettCtx p) (cR lo hi : UInt64) (hcR : cR.toNat = UInt64.word % p.toNat) : ctx.accReduce cR lo hi < p

accReduce returns a canonical residue below p.

def BarrettCtx.radixResidue {p : UInt64} (_ctx : BarrettCtx p) : UInt64

The radix residue 2^64 % p, stored as a context-level constant so callers of accReduce/foldReduce need not carry the word and its correctness proof. Computed entirely in machine words: 0 - p wraps to 2^64 - p ≡ 2^64 (mod p), so one word-level reduction yields 2^64 % p with no 128-bit literal and no bignum Nat reduction of the radix (the former Nat-level computation cost a bignum mod on every call, which the delayed-reduction kernel pays once per dot product).

Equations

• _ctx.radixResidue = (0 - p) % p

theorem BarrettCtx.toNat_radixResidue {p : UInt64} (ctx : BarrettCtx p) : ctx.radixResidue.toNat = UInt64.word % p.toNat

radixResidue stores exactly 2^64 % p, the hcR side condition every accReduce/foldReduce lemma needs.

@[irreducible]

def BarrettCtx.barrettWindow : Nat

Number of one-word products accumulated between reductions. Any value below 2^64 keeps the two-word accumulator's high word from overflowing (the add grows it by at most one per step). The 2^12 window keeps the periodic path operationally testable while amortizing each reduction across 4096 products; the committed window sweep compares it with shorter and effectively single-flush alternatives.

Equations

• BarrettCtx.barrettWindow = 2 ^ 12

theorem BarrettCtx.barrettWindow_pos : 0 < barrettWindow

theorem BarrettCtx.barrettWindow_lt_word : barrettWindow < UInt64.word

def BarrettCtx.accStep {p : UInt64} (ctx : BarrettCtx p) : UInt64 × UInt64 × Nat → UInt64 → UInt64 × UInt64 × Nat

One delayed-reduction step: add the product word q into the accumulator (lo, hi), and when the window count reaches barrettWindow flush the two-word value through accReduce back to a single reduced word, resetting the count.

Deliberately not @[expose]: leaving the body opaque to the kernel keeps reductions of foldl accStep … from unfolding the accReduce/barrettReduce machinery (which mentions the 2^64 radix) during defeq checks; all reasoning goes through accFold_spec, never kernel reduction of accStep.

Equations

• One or more equations did not get rendered due to their size.

theorem BarrettCtx.accStep_eq_inline {p : UInt64} (ctx : BarrettCtx p) (lo hi : UInt64) (count : Nat) (q : UInt64) : ctx.accStep (lo, hi, count) q = if count + 1 = barrettWindow then (ctx.accReduce ctx.radixResidue (lo + q) (hi + if lo + q < lo then 1 else 0), 0, 0) else (lo + q, hi + if lo + q < lo then 1 else 0, count + 1)

accStep in inline-carry scalar form: the state transition the delayed- reduction kernel's scalar loops compute per term. This is the exported equation for identifying an unfolded scalar loop with the (deliberately opaque) accStep fold step.

def BarrettCtx.wordsSum (ws : List UInt64) : Nat

Sum of the Nat values of a list of accumulator product words.

Equations

• BarrettCtx.wordsSum ws = List.foldr (fun (w : UInt64) (a : Nat) => w.toNat + a) 0 ws

@[simp]

theorem BarrettCtx.wordsSum_nil : wordsSum [] = 0

@[simp]

theorem BarrettCtx.wordsSum_cons (q : UInt64) (ws : List UInt64) : wordsSum (q :: ws) = q.toNat + wordsSum ws

theorem BarrettCtx.accFold_spec {p : UInt64} (ctx : BarrettCtx p) (ws : List UInt64) (lo hi : UInt64) (count : Nat) : hi.toNat ≤ count → count < barrettWindow → (List.foldl ctx.accStep (lo, hi, count) ws).snd.fst.toNat ≤ (List.foldl ctx.accStep (lo, hi, count) ws).snd.snd ∧ (List.foldl ctx.accStep (lo, hi, count) ws).snd.snd < barrettWindow ∧ accVal (List.foldl ctx.accStep (lo, hi, count) ws).fst (List.foldl ctx.accStep (lo, hi, count) ws).snd.fst % p.toNat = (accVal lo hi + wordsSum ws) % p.toNat

Per-window no-overflow invariant for the delayed-reduction fold. From any in-window start state (hi ≤ count < barrettWindow), folding accStep over a list of product words keeps the state in-window (hi ≤ count < barrettWindow, so the next add cannot overflow the high word) and preserves the residue: the accumulator's value modulo p equals the starting value plus the sum of the added words modulo p.

def BarrettCtx.foldReduce {p : UInt64} (ctx : BarrettCtx p) (ws : List UInt64) : UInt64

Reduce a list of product words modulo p with periodic reduction: fold accStep from an empty accumulator and flush the final partial window.

Equations

• ctx.foldReduce ws = ctx.accReduce ctx.radixResidue (List.foldl ctx.accStep (0, 0, 0) ws).fst (List.foldl ctx.accStep (0, 0, 0) ws).snd.fst

theorem BarrettCtx.toNat_foldReduce {p : UInt64} (ctx : BarrettCtx p) (ws : List UInt64) : (ctx.foldReduce ws).toNat = wordsSum ws % p.toNat

foldReduce computes (Σ words) % p: the delayed-reduction fold is exact for a run of any length, matching the residue of the fully-accumulated sum.