Correctness of multiplication with overflow detection

Question

The following C++ template detects overflows from multiplying two unsigned integers.

template<typename UInt> UInt safe_multiply(UInt a, UInt b) {
    UInt x = a * b; // x := ab mod n, for n := 2^#bits > 0
    if (a != 0 && x / a != b)
        cerr << "Overflow for " << a << " * " << b << "." << endl;
    return x;
}

Can you give a proof that this algorithm detects every potential overflow, regardless of how many bits UInt uses?

The case

cannot result in overflows, so we can consider
.

It seems that the correctness proof boils down to leading

to a contradiction, since x / a actually means .

When assuming

, this leads to the straightforward consequence

thus

which contradicts n > 0.

So it remains to show

or there must be another way.

If the last equation is true, WolframAlpha fails to confirm that (also with exponents).
However, it asserts that the original assumptions have no integer solutions, so the algorithms seems to be correct indeed.
But it doesn't provide an explanation. So why is it correct?

I am looking for the smallest possible explanation that is still mathematically profound, ideally that it fits in a single-line comment. Maybe I am missing something trivial, or the problem is not as easy as it looks.

On a side note, I used Codecogs Equation Editor for the LaTeX markup images, which apparently looks bad in dark mode, so consider switching to light mode or, if you know, please tell me how to use different images depending on the client settings. It is just \bg{white} vs. \bg{black} as part of the image URLs.

Answer 1

To be clear, I'll use the multiplication and division symbols (*, /) mathematically.

Also, for convenience let's name the set N = {0, 1, ..., n - 1}.

Let's clear up what unsigned multiplication is:
Unsigned multiplication for some magnitude, n, is a modular n operation on unsigned-n inputs (inputs that are in N) that results in an unsigned-n output (ie. also in N).
In other words, the result of unsigned multiplication, x, is x = a*b (mod n), and, additionally, we know that x,a,b are in N.
It's important to be able to expand many modular formulas like so: x = a*b - k*n, where k is an integer - but in our case x,a,b are in N so this implies that k is in N.

Now, let's mathematically say what we're trying to prove:
Given positive integers, a,n, and non-negative integers x,b, where x,a,b are in N, and x = a*b (mod n), then a*b >= n (overflow) implies floor(x/a) != b.

Proof:

If overflow (a*b >= n) then x >= n - k*n = (1 - k)*n (for k in N),
As x < n then (1 - k)*n < n, so k > 0.
This means x <= a*b - n.

So, floor(x/a) <= floor([a*b - n]/a) = floor(a*b/a - n/a) = b - floor(n/a) <= b - 1,
Abbreviated: floor(x/a) <= b - 1
Therefore floor(x/a) != b

Answer 2

The multiplication gives either the mathematically correct result, or it is off by some multiple of 2^64. Since you check for a=0, the division always gives the correct result for its input. But in the case of overflow, the input is off by 2^64 or more, so the test will fail as you hoped.

The last bit is that unsigned operations don’t have undefined behaviour except for division by zero, so your code is fine.