Honeycomb

15. 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 Honeycomb -- 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! 🐙)

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.

The block-float layer adds one more accumulation shape: a scaled sum. A multi-block dot with shared exponents folds each block to an integer dot d_b and accumulates d_b * 2 ^ t_b, where t_b is the per-block shift the compiler derives from the exponents (blockFpDot applies it as a left shift at the block boundary). The running sum lives in a full-width register, so the no-overflow obligation is the same magnitude argument with one extra factor: each term is bounded by D * 2 ^ T when the block dots are bounded by D and the shifts by T. This is the formal anchor for the compiler's per-layer output-exponent choice (E0): calibration bounds the runtime exponent range, which bounds T, and the side condition below is what the compiler must check when it emits shift words.

def scaledSum : List (Int × Nat) -> Int | [] => 0 | p :: l => p.1 * 2 ^ p.2 + scaledSum l theorem scaledTerm_natAbs_le (d : Int) (t : Nat) (D T : Nat) (hd : d.natAbs ≤ D) (ht : t ≤ T) : (d * 2 ^ t).natAbs ≤ D * 2 ^ T := d:Intt:NatD:NatT:Nathd:d.natAbs ≤ Dht:t ≤ T⊢ (d * 2 ^ t).natAbs ≤ D * 2 ^ T d:Intt:NatD:NatT:Nathd:d.natAbs ≤ Dht:t ≤ T⊢ d.natAbs * (2 ^ t).natAbs ≤ D * 2 ^ T d:Intt:NatD:NatT:Nathd:d.natAbs ≤ Dht:t ≤ Th2:(2 ^ t).natAbs = 2 ^ t⊢ d.natAbs * (2 ^ t).natAbs ≤ D * 2 ^ T d:Intt:NatD:NatT:Nathd:d.natAbs ≤ Dht:t ≤ Th2:(2 ^ t).natAbs = 2 ^ t⊢ d.natAbs * 2 ^ t ≤ D * 2 ^ T exact Nat.mul_le_mul hd (Nat.pow_le_pow_right (d:Intt:NatD:NatT:Nathd:d.natAbs ≤ Dht:t ≤ Th2:(2 ^ t).natAbs = 2 ^ t⊢ 2 > 0 All goals completed! 🐙) ht) theorem scaledSum_natAbs_le (l : List (Int × Nat)) (D T : Nat) (hd : forall p, p ∈ l -> p.1.natAbs ≤ D) (ht : forall p, p ∈ l -> p.2 ≤ T) : (scaledSum l).natAbs ≤ l.length * (D * 2 ^ T) := l:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ T⊢ (scaledSum l).natAbs ≤ l.length * (D * 2 ^ T) induction l with D:NatT:Nathd:∀ (p : Int × Nat), p ∈ [] → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ [] → p.snd ≤ T⊢ (scaledSum []).natAbs ≤ [].length * (D * 2 ^ T) All goals completed! 🐙 D:NatT:Natp:Int × Natl:List (Int × Nat)ih:(∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ D) → (∀ (p : Int × Nat), p ∈ l → p.snd ≤ T) → (scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)hd:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.fst.natAbs ≤ Dht:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.snd ≤ T⊢ (scaledSum (p :: l)).natAbs ≤ (p :: l).length * (D * 2 ^ T) D:NatT:Natp:Int × Natl:List (Int × Nat)ih:(∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ D) → (∀ (p : Int × Nat), p ∈ l → p.snd ≤ T) → (scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)hd:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.fst.natAbs ≤ Dht:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.snd ≤ Thterm:(p.fst * 2 ^ p.snd).natAbs ≤ D * 2 ^ T⊢ (scaledSum (p :: l)).natAbs ≤ (p :: l).length * (D * 2 ^ T) D:NatT:Natp:Int × Natl:List (Int × Nat)ih:(∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ D) → (∀ (p : Int × Nat), p ∈ l → p.snd ≤ T) → (scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)hd:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.fst.natAbs ≤ Dht:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.snd ≤ Thterm:(p.fst * 2 ^ p.snd).natAbs ≤ D * 2 ^ Threst:(scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)⊢ (scaledSum (p :: l)).natAbs ≤ (p :: l).length * (D * 2 ^ T) D:NatT:Natp:Int × Natl:List (Int × Nat)ih:(∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ D) → (∀ (p : Int × Nat), p ∈ l → p.snd ≤ T) → (scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)hd:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.fst.natAbs ≤ Dht:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.snd ≤ Thterm:(p.fst * 2 ^ p.snd).natAbs ≤ D * 2 ^ Threst:(scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)htri:(scaledSum (p :: l)).natAbs ≤ (p.fst * 2 ^ p.snd).natAbs + (scaledSum l).natAbs⊢ (scaledSum (p :: l)).natAbs ≤ (p :: l).length * (D * 2 ^ T) D:NatT:Natp:Int × Natl:List (Int × Nat)ih:(∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ D) → (∀ (p : Int × Nat), p ∈ l → p.snd ≤ T) → (scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)hd:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.fst.natAbs ≤ Dht:∀ (p_1 : Int × Nat), p_1 ∈ p :: l → p_1.snd ≤ Thterm:(p.fst * 2 ^ p.snd).natAbs ≤ D * 2 ^ Threst:(scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)htri:(scaledSum (p :: l)).natAbs ≤ (p.fst * 2 ^ p.snd).natAbs + (scaledSum l).natAbshlen:(p :: l).length * (D * 2 ^ T) = D * 2 ^ T + l.length * (D * 2 ^ T)⊢ (scaledSum (p :: l)).natAbs ≤ (p :: l).length * (D * 2 ^ T) All goals completed! 🐙

The fit statement follows, and — because a prefix of the list satisfies the same hypotheses with a shorter length — it covers every running value of the register accumulation, not just the final sum. That matches how blockFpDot actually accumulates: one add per block, each intermediate visible in r4.

theorem scaledSum_fits (bits : Nat) (l : List (Int × Nat)) (D T : Nat) (hd : forall p, p ∈ l -> p.1.natAbs ≤ D) (ht : forall p, p ∈ l -> p.2 ≤ T) (hb : l.length * (D * 2 ^ T) < 2 ^ (bits - 1)) : signedFits bits (scaledSum l) := bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)⊢ signedFits bits (scaledSum l) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)⊢ ↑(scaledSum l).natAbs < 2 ^ (bits - 1) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)h:(scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)⊢ ↑(scaledSum l).natAbs < 2 ^ (bits - 1) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)h:(scaledSum l).natAbs ≤ l.length * (D * 2 ^ T)this:(scaledSum l).natAbs < 2 ^ (bits - 1)⊢ ↑(scaledSum l).natAbs < 2 ^ (bits - 1) All goals completed! 🐙 theorem scaledSum_prefixFits (bits : Nat) (l : List (Int × Nat)) (D T : Nat) (hd : forall p, p ∈ l -> p.1.natAbs ≤ D) (ht : forall p, p ∈ l -> p.2 ≤ T) (hb : l.length * (D * 2 ^ T) < 2 ^ (bits - 1)) : forall k, signedFits bits (scaledSum (l.take k)) := bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)⊢ ∀ (k : Nat), signedFits bits (scaledSum (List.take k l)) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nat⊢ signedFits bits (scaledSum (List.take k l)) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nat⊢ ∀ (p : Int × Nat), p ∈ List.take k l → p.fst.natAbs ≤ Dbits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nat⊢ ∀ (p : Int × Nat), p ∈ List.take k l → p.snd ≤ Tbits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nat⊢ (List.take k l).length * (D * 2 ^ T) < 2 ^ (bits - 1) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nat⊢ ∀ (p : Int × Nat), p ∈ List.take k l → p.fst.natAbs ≤ D All goals completed! 🐙 bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nat⊢ ∀ (p : Int × Nat), p ∈ List.take k l → p.snd ≤ T All goals completed! 🐙 bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nat⊢ (List.take k l).length * (D * 2 ^ T) < 2 ^ (bits - 1) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nathlen:(List.take k l).length ≤ l.length⊢ (List.take k l).length * (D * 2 ^ T) < 2 ^ (bits - 1) bits:Natl:List (Int × Nat)D:NatT:Nathd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ Dht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ Thb:l.length * (D * 2 ^ T) < 2 ^ (bits - 1)k:Nathlen:(List.take k l).length ≤ l.lengthhmul:(List.take k l).length * (D * 2 ^ T) ≤ l.length * (D * 2 ^ T)⊢ (List.take k l).length * (D * 2 ^ T) < 2 ^ (bits - 1) All goals completed! 🐙

The int8 instance chains this to the per-block bound already proved: a block of n int8 lanes has d_b.natAbs ≤ n * (127 * 127) by fsumFrom_natAbs_le, so D is not a new obligation. The concrete corollary is a production shape: a Llama-8B MLP row is K = 14336, i.e. 448 blocks of 32, and with calibrated shifts up to T = 34 the 64-bit accumulator holds every prefix (448 * (32 * 127 * 127) * 2 ^ 34 < 2 ^ 63). The compiler's emission-time check is exactly this side condition with its own nb, n, and T.

theorem scaledSum_int8_fits (l : List (Int × Nat)) (n T : Nat) (hd : forall p, p ∈ l -> p.1.natAbs ≤ n * (127 * 127)) (ht : forall p, p ∈ l -> p.2 ≤ T) (hb : l.length * (n * (127 * 127) * 2 ^ T) < 2 ^ 63) : signedFits defaultConfig.accBits (scaledSum l) := scaledSum_fits defaultConfig.accBits l (n * (127 * 127)) T hd ht hb theorem scaledSum_llama_mlp_fits (l : List (Int × Nat)) (hlen : l.length ≤ 448) (hd : forall p, p ∈ l -> p.1.natAbs ≤ 32 * (127 * 127)) (ht : forall p, p ∈ l -> p.2 ≤ 34) : signedFits defaultConfig.accBits (scaledSum l) := l:List (Int × Nat)hlen:l.length ≤ 448hd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ 32 * (127 * 127)ht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ 34⊢ signedFits defaultConfig.accBits (scaledSum l) l:List (Int × Nat)hlen:l.length ≤ 448hd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ 32 * (127 * 127)ht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ 34⊢ l.length * (32 * (127 * 127) * 2 ^ 34) < 2 ^ 63 l:List (Int × Nat)hlen:l.length ≤ 448hd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ 32 * (127 * 127)ht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ 34hmul:l.length * (32 * (127 * 127) * 2 ^ 34) ≤ 448 * (32 * (127 * 127) * 2 ^ 34)⊢ l.length * (32 * (127 * 127) * 2 ^ 34) < 2 ^ 63 exact Nat.lt_of_le_of_lt hmul (l:List (Int × Nat)hlen:l.length ≤ 448hd:∀ (p : Int × Nat), p ∈ l → p.fst.natAbs ≤ 32 * (127 * 127)ht:∀ (p : Int × Nat), p ∈ l → p.snd ≤ 34hmul:l.length * (32 * (127 * 127) * 2 ^ 34) ≤ 448 * (32 * (127 * 127) * 2 ^ 34)⊢ 448 * (32 * (127 * 127) * 2 ^ 34) < 2 ^ 63 All goals completed! 🐙) end Honeycomb

A scaled sum whose block dots come from int8 blocks and whose shifts respect the calibrated ceiling therefore needs no per-model overflow reasoning: the length, block size, and shift bound are all the compiler knows at emission time, and the side condition is a single comparison it performs before writing the shift words.