Correctness of multiplication with overflow detection-CodePudding

The following C template $a=0\lor b=0$

cannot result in overflows, so we can consider
$a,b,n\in\mathbb{N}_{>0}$ .

It seems that the correctness proof boils down to leading
$\left\lfloor\frac{ab \mod n}{a}\right\rfloor=b~\land~ab\ge n$

to a contradiction, since x / a actually means $\left\lfloor\frac{x}{a}\right\rfloor$ .

When assuming
$\left\lfloor\frac{x}{a}\right\rfloor=\frac{x}{a}$

, this leads to the straightforward consequence
$\left\lfloor\frac{x}{a}\right\rfloor=b\Leftrightarrow\frac{x}{a}=b\Leftrightarrow ab \mod n=ab$

thus
$ab\mod n=ab\ge n$

which contradicts n > 0.

So it remains to show
$\left\lfloor\frac{ab \mod n}{a}\right\rfloor=\frac{ab \mod n}{a}$

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.

CodePudding user response：

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

CodePudding user response：

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.