Janus

13. Kernel Overflow Bounds🔗

The kernel chapter states the exact-execution obligation as kernelPrefixFits: every prefix sum that can enter the accumulator must fit the signed accumulator width. That obligation is left abstract there because it depends on the operands. This chapter discharges it from concrete magnitude bounds, so a quantized block-float kernel with bounded weights and streamed operands satisfies the no-overflow condition automatically, without reasoning about the individual products.

The argument is a magnitude bound. Each operand has a bounded absolute value, so each product is bounded by the product of the bounds, a prefix of n products is bounded by n times that, and adding a bounded initial accumulator keeps the whole running value inside the signed range whenever the arithmetic bound is below 2 ^ (accBits - 1).

namespace Janus -- A signed value fits its width if its magnitude is below the signed bound. The -- magnitude is carried as an `Int`-cast `natAbs`, which `omega` understands. theorem signedFits_of_natAbs_lt (bits : Nat) (x : Int) (h : (x.natAbs : Int) < 2 ^ (bits - 1)) : signedFits bits x := bits:Natx:Inth:↑x.natAbs < 2 ^ (bits - 1)⊢ signedFits bits x bits:Natx:Inth:↑x.natAbs < 2 ^ (bits - 1)⊢ -2 ^ (bits - 1) ≤ x ∧ x < 2 ^ (bits - 1) All goals completed! 🐙 theorem prod_natAbs_le (x y : Int) (Wn An : Nat) (hx : x.natAbs ≤ Wn) (hy : y.natAbs ≤ An) : (x * y).natAbs ≤ Wn * An := x:Inty:IntWn:NatAn:Nathx:x.natAbs ≤ Wnhy:y.natAbs ≤ An⊢ (x * y).natAbs ≤ Wn * An x:Inty:IntWn:NatAn:Nathx:x.natAbs ≤ Wnhy:y.natAbs ≤ An⊢ x.natAbs * y.natAbs ≤ Wn * An All goals completed! 🐙

The dot-product prefix is bounded by its length times the per-product bound. The proof shifts the two pointers as it peels one product off the front, so the bound holds for every starting offset.

theorem fsumFrom_natAbs_le (w a : Nat -> Int) (Wn An : Nat) (hw : forall i, (w i).natAbs ≤ Wn) (ha : forall i, (a i).natAbs ≤ An) : forall (wp sp k : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An) := w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ An⊢ ∀ (wp sp k : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An) w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Anwp:Natsp:Natk:Nat⊢ (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An) induction k generalizing wp sp with w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Anwp:Natsp:Nat⊢ (fsumFrom w a wp sp 0).natAbs ≤ 0 * (Wn * An) All goals completed! 🐙 w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Ank:Natih:∀ (wp sp : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An)wp:Natsp:Nat⊢ (fsumFrom w a wp sp (k + 1)).natAbs ≤ (k + 1) * (Wn * An) w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Ank:Natih:∀ (wp sp : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An)wp:Natsp:Nathstep:fsumFrom w a wp sp (k + 1) = w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k⊢ (fsumFrom w a wp sp (k + 1)).natAbs ≤ (k + 1) * (Wn * An) w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Ank:Natih:∀ (wp sp : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An)wp:Natsp:Nathstep:fsumFrom w a wp sp (k + 1) = w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) kh2:(w wp * a sp).natAbs ≤ Wn * An⊢ (fsumFrom w a wp sp (k + 1)).natAbs ≤ (k + 1) * (Wn * An) w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Ank:Natih:∀ (wp sp : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An)wp:Natsp:Nathstep:fsumFrom w a wp sp (k + 1) = w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) kh2:(w wp * a sp).natAbs ≤ Wn * Anh3:(fsumFrom w a (wp + 1) (sp + 1) k).natAbs ≤ k * (Wn * An)⊢ (fsumFrom w a wp sp (k + 1)).natAbs ≤ (k + 1) * (Wn * An) w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Ank:Natih:∀ (wp sp : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An)wp:Natsp:Nathstep:fsumFrom w a wp sp (k + 1) = w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) kh2:(w wp * a sp).natAbs ≤ Wn * Anh3:(fsumFrom w a (wp + 1) (sp + 1) k).natAbs ≤ k * (Wn * An)htri:(fsumFrom w a wp sp (k + 1)).natAbs ≤ (w wp * a sp).natAbs + (fsumFrom w a (wp + 1) (sp + 1) k).natAbs⊢ (fsumFrom w a wp sp (k + 1)).natAbs ≤ (k + 1) * (Wn * An) w:Nat → Inta:Nat → IntWn:NatAn:Nathw:∀ (i : Nat), (w i).natAbs ≤ Wnha:∀ (i : Nat), (a i).natAbs ≤ Ank:Natih:∀ (wp sp : Nat), (fsumFrom w a wp sp k).natAbs ≤ k * (Wn * An)wp:Natsp:Nathstep:fsumFrom w a wp sp (k + 1) = w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) kh2:(w wp * a sp).natAbs ≤ Wn * Anh3:(fsumFrom w a (wp + 1) (sp + 1) k).natAbs ≤ k * (Wn * An)htri:(fsumFrom w a wp sp (k + 1)).natAbs ≤ (w wp * a sp).natAbs + (fsumFrom w a (wp + 1) (sp + 1) k).natAbshsm:(k + 1) * (Wn * An) = Wn * An + k * (Wn * An)⊢ (fsumFrom w a wp sp (k + 1)).natAbs ≤ (k + 1) * (Wn * An) All goals completed! 🐙

The main theorem discharges kernelPrefixFits from three magnitude bounds and one arithmetic side condition. Wn and An bound the weight and stream operands, Cn bounds the initial accumulator, and the side condition keeps the worst-case running value inside the signed accumulator range.

theorem kernelPrefixFits_of_bounds (cfg : Config) (s : KernelState) (n : Nat) (Wn An Cn : Nat) (hw : forall i, (s.weights i).natAbs ≤ Wn) (ha : forall i, (s.stream i).natAbs ≤ An) (hacc : s.acc.natAbs ≤ Cn) (hb : Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)) : kernelPrefixFits cfg s n := cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)⊢ kernelPrefixFits cfg s n cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)k:Nathk:k ≤ n⊢ signedFits cfg.accBits (s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k) cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)k:Nathk:k ≤ n⊢ ↑(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs < 2 ^ (cfg.accBits - 1) cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)k:Nathk:k ≤ nhsum:(fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ k * (Wn * An)⊢ ↑(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs < 2 ^ (cfg.accBits - 1) cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)k:Nathk:k ≤ nhsum:(fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ k * (Wn * An)htri:(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ s.acc.natAbs + (fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs⊢ ↑(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs < 2 ^ (cfg.accBits - 1) cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)k:Nathk:k ≤ nhsum:(fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ k * (Wn * An)htri:(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ s.acc.natAbs + (fsumFrom s.weights s.stream s.wptr s.sptr k).natAbshk':k * (Wn * An) ≤ n * (Wn * An)⊢ ↑(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs < 2 ^ (cfg.accBits - 1) cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)k:Nathk:k ≤ nhsum:(fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ k * (Wn * An)htri:(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ s.acc.natAbs + (fsumFrom s.weights s.stream s.wptr s.sptr k).natAbshk':k * (Wn * An) ≤ n * (Wn * An)hnat:(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ Cn + n * (Wn * An)⊢ ↑(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs < 2 ^ (cfg.accBits - 1) cfg:Configs:KernelStaten:NatWn:NatAn:NatCn:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ Wnha:∀ (i : Nat), (s.stream i).natAbs ≤ Anhacc:s.acc.natAbs ≤ Cnhb:Cn + n * (Wn * An) < 2 ^ (cfg.accBits - 1)k:Nathk:k ≤ nhsum:(fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ k * (Wn * An)htri:(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ s.acc.natAbs + (fsumFrom s.weights s.stream s.wptr s.sptr k).natAbshk':k * (Wn * An) ≤ n * (Wn * An)hnat:(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs ≤ Cn + n * (Wn * An)h1:(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs < 2 ^ (cfg.accBits - 1)⊢ ↑(s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k).natAbs < 2 ^ (cfg.accBits - 1) All goals completed! 🐙

The concrete corollary is the intended use: an int8-quantized block-float kernel. Weights and streamed operands are signed eight-bit values, so their magnitudes are at most 127; the accumulator starts cleared; and the default 64-bit accumulator absorbs any block up to 2 ^ 40 MACs with room to spare (2 ^ 40 * 127 * 127 is far below 2 ^ 63). Such a kernel discharges its no-overflow obligation with no further arithmetic reasoning.

theorem kernelPrefixFits_int8_block (s : KernelState) (n : Nat) (hw : forall i, (s.weights i).natAbs ≤ 127) (ha : forall i, (s.stream i).natAbs ≤ 127) (hacc : s.acc = 0) (hn : n ≤ 2 ^ 40) : kernelPrefixFits defaultConfig s n := s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40⊢ kernelPrefixFits defaultConfig s n s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40⊢ s.acc.natAbs ≤ 0s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40⊢ 0 + n * (127 * 127) < 2 ^ (defaultConfig.accBits - 1) s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40⊢ s.acc.natAbs ≤ 0 All goals completed! 🐙 s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40⊢ 0 + n * (127 * 127) < 2 ^ (defaultConfig.accBits - 1) s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40⊢ 0 + n * (127 * 127) < 2 ^ 63 s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40hmul:n * (127 * 127) ≤ 2 ^ 40 * (127 * 127)⊢ 0 + n * (127 * 127) < 2 ^ 63 s:KernelStaten:Nathw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0hn:n ≤ 2 ^ 40hmul:n * (127 * 127) ≤ 2 ^ 40 * (127 * 127)hlt:2 ^ 40 * (127 * 127) < 2 ^ 63⊢ 0 + n * (127 * 127) < 2 ^ 63 All goals completed! 🐙 -- A fully concrete smoke check: a 1024-length int8 block cannot overflow. theorem kernelPrefixFits_int8_1024 (s : KernelState) (hw : forall i, (s.weights i).natAbs ≤ 127) (ha : forall i, (s.stream i).natAbs ≤ 127) (hacc : s.acc = 0) : kernelPrefixFits defaultConfig s 1024 := kernelPrefixFits_int8_block s 1024 hw ha hacc (s:KernelStatehw:∀ (i : Nat), (s.weights i).natAbs ≤ 127ha:∀ (i : Nat), (s.stream i).natAbs ≤ 127hacc:s.acc = 0⊢ 1024 ≤ 2 ^ 40 All goals completed! 🐙) end Janus

Combined with kernel_accumulator_exact_when_prefixFits from the kernel chapter, this gives an end-to-end statement for quantized kernels: a bounded int8 block up to the stated length both computes the exact integer dot product and never wraps the fixed-width accumulator. The overflow obligation is no longer a proof the caller must supply; it follows from the block's quantization and length.