Add documentation note about signed overflow direction

[nickkuk]

In #151989 (comment) I noticed that signed overflow direction can be determined by returned wrapped value. It is not very obvious (especially, assuming additional carry: bool summand), but it is important if we want to add new leading (signed) limb to big integer in this case.

Examples for small summands x, y: i8 with result extension:

x	y	overflow	result as (u8, i8)
-1	-128	true	(127, -1)
0	-1	false	(255, -1)
2	2	false	(4, 0)
127	1	true	(128, 0)

Here is general proof.

1. Set $s=2^{N-1}$ and let's say iN::carrying_add(x, y, c) returns (result, true) then

$$ \mathrm{result}=\begin{cases} x + y + c + 2s,& x + y + c \le -s-1,\\ x+y+c-2s,& x+y+c\ge s. \end{cases} $$

First case is overflowing below iN::MIN and we have

$$ \mathrm{result}\ge -s-s+0+2s =0;\qquad \mathrm{result}=x + y + c + 2s\le -s-1+2s = s - 1, $$

so we obtain $[0; s-1]$ which is exactly range of non-negative iN.

Second case is overflowing above iN::MAX and

$$ \mathrm{result}=x+y+c-2s\ge s-2s =-s;\qquad \mathrm{result}\le s-1 + s-1+1-2s = -1, $$

that is, $[-s,-1]$ which is exactly range of negative iN.

2. Now suppose that iN::borrowing_sub(x,y,b) returns (result, true) then

$$ \mathrm{result}=\begin{cases} x - y - b + 2s,& x - y - b \le -s-1,\\ x - y - b - 2s,& x - y - b\ge s. \end{cases} $$

First case is overflowing below iN::MIN and we have

$$ \mathrm{result}\ge -s-(s-1)-1+2s =0;\qquad \mathrm{result}=x - y - b + 2s\le -s-1+2s = s - 1. $$

Second case is overflowing above iN::MAX and

$$ \mathrm{result}=x-y-b-2s\ge s-2s =-s;\qquad \mathrm{result}\le s-1 - (-s) - 0 - 2s = -1. $$

[rustbot]

r? @scottmcm

rustbot has assigned @scottmcm.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[jhpratt]

Neat! I've never thought of that, but it actually may be useful for some code of my own.

@bors r+ rollup

[rust-bors]

📌 Commit 689e8c2 has been approved by jhpratt

It is now in the queue for this repository.