Prove accumulator bounds before shrinking operands

For affine operands, the mathematical integer accumulator sums products of qx minus zx and qw minus zw. The largest centered magnitude depends on both the stored range and the zero point. An unsigned eight-bit code can differ from its zero point by as much as 255; assuming the symmetric signed maximum 127 would understate that case. If weights have per-channel scales, the conversion back to real units also varies by output channel. Keep scale application separate from the integer magnitude proof.

A direct centered multiply and a kernel using expanded zero-point correction are algebraically equivalent over unbounded integers. Their intermediate requirements can differ because the expansion contains sums of raw codes and correction terms that later cancel. Check those terms and partial reductions in the implementation, not only the final centered sum. Bias expressed in accumulator units must be included too. A representable output after cancellation does not prove that an earlier narrow multiply or reduction was representable.

If centered operand magnitudes are bounded by A and B, the triangle inequality gives an accumulator magnitude no larger than KAB plus the absolute integer bias. Requiring that bound to fit the positive signed maximum gives a conservative condition that protects either sign. The negative endpoint has one extra representable magnitude, but using it requires a more specific sign analysis. A power-of-two bound equal to the positive range limit is an easy place to make a one-bit error.

The ONNX MatMulInteger version 10 contract returns an int32 result and permits overflow at the 32-bit accumulation level; exporting that operator is not a proof that arbitrary dimensions are safe. Hardware can also use internal instructions with their own intermediate behavior. Inspect the selected backend and adversarially test long reductions, extreme centered codes and large bias. If a bound fails, widen, split the reduction with a proven wider combination, constrain ranges or change the representation. Do not silently substitute saturation for exact accumulation.

A final requantizer typically rescales the wide accumulator, rounds and clips to a smaller output code range. That final saturation can be intentional and measurable. Overflow before it changes the accumulator itself, so clipping the corrupted value afterward does not recover the intended result. Keep counters or tests for the two failure modes separate. Test the complete conversion path, including multiplier approximation, shifts, tie rules and destination signedness; a correct accumulation proof alone does not prove bit-identical requantization.

In the modular lab, Reset and set both m=16 and a=7. Predict three Steps from zero as 7, 14 and 5, because the third addition wraps 21 modulo 16. A hypothetical saturating unsigned four-bit accumulator would instead give 7, 14 and 15. The instrument has neither signed dot products nor machine-specific overflow rules. Its explicit modulo arithmetic simply makes the loss of an intended mathematical sum visible; actual kernel bounds must be proved from their own centered operands and widths.