def Hex.delayedDot {p : Nat} [ZMod64.Bounds p] {m : Nat} (ctx : BarrettCtx p) (u v : Vector (ZMod64 p) m) : ZMod64 p

Delayed-reduction Barrett dot product. Accumulates each one-word residue product u[i] * v[i] into the two-word accumulator and reduces modulo p only every barrettWindow terms (foldReduce), then reduces the final partial window. The window is fixed and independent of the length m, so this is correct for every inner dimension.

Equations

• Hex.delayedDot ctx u v = Hex.ZMod64.ofNat p (ctx.toUInt64Ctx.foldReduce (List.map (fun (i : Fin m) => u[i].toUInt64 * v[i].toUInt64) (List.finRange m))).toNat

@[irreducible]

def Hex.delayedDotLoop {p : Nat} [ZMod64.Bounds p] {m : Nat} (ctx : BarrettCtx p) (u v : Vector (ZMod64 p) m) : Nat → UInt64 → UInt64 → Nat → UInt64

Allocation-free scalar loop backing delayedDotImpl. The two-word accumulator (lo, hi) and the window counter are threaded as scalar arguments rather than a boxed (UInt64 × UInt64 × Nat) tuple, so the compiled loop keeps lo/hi in machine words with no per-term heap traffic. Each one-word product u[i] * v[i] is added with an inline carry (the wraparound compare lo + q < lo), avoiding the UInt64.addCarry extern call, and the two-word value is flushed through accReduce at every barrettWindow terms and once more at the end. The per-step state transition matches BarrettCtx.accStep (accStep_eq_inline), so the loop computes exactly foldReduce (delayedDotLoop_eq_foldl). (The repeated product subterm is written out rather than let-bound so the equations rewrite cleanly in the proofs below; the compiler's CSE emits it once.)

Equations

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

@[irreducible]

def Hex.delayedDotRun {p : Nat} [ZMod64.Bounds p] {m : Nat} (ctx : BarrettCtx p) (u v : Vector (ZMod64 p) m) : Nat → UInt64 → UInt64 → UInt64

Count-free fast path of delayedDotLoop, usable when the whole dot product fits in a single window (m < barrettWindow). This includes the ordinary square Strassen leaves; the generic base-kernel signature also admits larger inner dimensions that use the windowed loop. When this path applies, the accumulator never flushes mid-run, so the window counter and its per-term check disappear from the inner loop entirely. The carry is written as an unconditional add of an if-valued bit so the C compiler can lower it to a flag-based setb/cmov rather than a data-dependent branch.

Equations

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

def Hex.delayedDotImpl {p : Nat} [ZMod64.Bounds p] {m : Nat} (ctx : BarrettCtx p) (u v : Vector (ZMod64 p) m) : ZMod64 p

Allocation-free implementation of delayedDot: selection once per dot product on whether the length fits in a single window, then run a scalar loop that never materializes the List.finRange m product-word list nor a boxed accumulator tuple (delayedDotRun without the window counter when m < barrettWindow, the windowed delayedDotLoop otherwise). Swapped in for compiled code by the @[csimp] below; delayedDot stays the list-based reference form for proofs, mirroring Vector.dotProduct/dotProductImpl.

Equations

• Hex.delayedDotImpl ctx u v = if m < BarrettCtx.barrettWindow then Hex.ZMod64.ofNat p (Hex.delayedDotRun ctx u v 0 0 0).toNat else Hex.ZMod64.ofNat p (Hex.delayedDotLoop ctx u v 0 0 0 0).toNat

@[csimp]

theorem Hex.delayedDot_eq_impl : @delayedDot = @delayedDotImpl

The reference delayed dot product agrees with the windowed implementation, registered @[csimp] so compiled code runs delayedDotImpl while proofs keep reasoning about delayedDot.

theorem Hex.delayedDot_eq_dotProduct {p : Nat} [ZMod64.Bounds p] {m : Nat} (ctx : BarrettCtx p) (u v : Vector (ZMod64 p) m) : delayedDot ctx u v = u.dotProduct v

Correctness of the delayed dot product. The periodically-reduced dot product equals the naive Vector.dotProduct on ZMod64 p: reduction modulo p is a ring homomorphism, so reducing periodically has the same residue as reducing at every step.

def Hex.barrettBaseMul {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) {n m k : Nat} (M : Matrix (ZMod64 p) n m) (N : Matrix (ZMod64 p) m k) : Matrix (ZMod64 p) n k

Delayed-reduction base kernel, selecting on the runtime inner dimension: the delayed dot product is the fast path once the dot-product length is nontrivial (2 ≤ m), and it falls back to the naive mulImpl on the trivial residual shapes. Mirroring mulImpl, the fast path transposes N once, materializes the transposed rows once, and materializes each row of M once per output row. Every dot product then runs over two contiguous rows with no per-entry row copy. Both branches equal the reference mul, so the config built from this is Valid.

Equations

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

theorem Hex.barrettBaseMul_eq_mul {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) {n m k : Nat} (M : Matrix (ZMod64 p) n m) (N : Matrix (ZMod64 p) m k) : barrettBaseMul ctx M N = M.mul N

The delayed-reduction base kernel agrees with the reference mul on every input and shape.

def Hex.strassenBarrett {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) : Matrix.StrassenConfig (ZMod64 p)

The shipped performance demonstration config: the delayed-reduction Barrett base kernel over the prime field ZMod64 p, taking the Hex.BarrettCtx. Measurably faster than strassenDefault at every measured square and rectangular shape (see the measured outcome in the module docstring and the committed comparison in reports/figures/). Its cutoff is pinned at 128, the delayed kernel's own measured crossover: the delayed dot product has a lower per-term cost but a per-dot-product reduction constant, so it profits from longer base-case dot products than the default kernel does (the default cutoff is measured separately and may move).

Equations

• Hex.strassenBarrett ctx = { cutoff := 128, baseMul := fun {_n _m _k : Nat} (M : Hex.Matrix (Hex.ZMod64 p) _n _m) (N : Hex.Matrix (Hex.ZMod64 p) _m _k) => Hex.barrettBaseMul ctx M N }

theorem Hex.strassenBarrett_valid {p : Nat} [ZMod64.Bounds p] (ctx : BarrettCtx p) : (strassenBarrett ctx).Valid

The delayed config is Valid: its base kernel equals mul, so mulStrassen (strassenBarrett ctx) still computes the reference product.

def Hex.strassenDemo {p : Nat} [ZMod64.Bounds p] : Matrix.StrassenConfig (ZMod64 p)

A trivial alternate config that plugs the naive mulImpl base kernel into a non-default StrassenConfig (with a distinct cutoff): the minimal example of the pluggable-base-kernel path, with a verified-Valid config supplied by the caller and no performance claim attached. The performance example is strassenBarrett above.

Equations

• Hex.strassenDemo = { cutoff := 48, baseMul := fun {n m k : Nat} => Hex.Matrix.mulImpl }

theorem Hex.strassenDemo_valid {p : Nat} [ZMod64.Bounds p] : strassenDemo.Valid

The trivial alternate config is Valid: its naive base kernel equals mul by mul_eq_mulImpl.