The output result isn't influenced by this patch, as shown by
following mathematical proof.
For convenience, let's mark '2^64' as '@', mark 'ADDC(A, B)' as 'A ⊕ B', then:
A ⊕ B = (A + B >= @) ? A + B - @ + 1 : A + B
What this patch did is transforming "sum ⊕ A ⊕ B ⊕ C ⊕ D" to "sum ⊕ (A
⊕ B) ⊕ (C ⊕ D)",
so what we are trying to prove is:
sum ⊕ A ⊕ B ⊕ C ⊕ D = sum ⊕ (A ⊕ B)
Let's first prove "sum ⊕ A ⊕ B" = "sum ⊕ (A ⊕ B)". There are 2 add ops
within 2 '⊕' here. According whether these add ops overflow, there are
4 cases:
Case 1: Only the first add op overflows.
Case 2: Only the second add op overflows.
Case 3: Both add ops overflow.
Case 4: Neither add ops overflow.
## In Case 1, we have
(1) sum + A >= @
=> sum ⊕ A = sum + A - @ + 1
(2) sum + A - @ + 1 + B < @
=> sum ⊕ A ⊕ B = sum + A + B - @ + 1
If A + B >= @:
=> A ⊕ B = A + B - @ + 1
=> sum + (A ⊕ B) = sum + A + B - @ + 1 < @ (see (2))
=> sum ⊕ (A ⊕ B) = sum + A + B - @ + 1 = sum ⊕ A ⊕ B
If A + B < @:
=> A ⊕ B = A + B
(3) => sum + (A ⊕ B) = sum + A + B
sum + A + B >= @ + B >= @ (adds B to both sides of (1))
=> sum + (A ⊕ B) >= @ (see (3))
=> sum ⊕ (A ⊕ B) = sum + A + B - @ + 1 = sum ⊕ A ⊕ B
## In Case 2, we have
(1) sum + A < @
=> sum ⊕ A = sum + A
(2) sum + A + B >= @
=> sum ⊕ A ⊕ B = sum + A + B - @ + 1
If A + B >= @:
=> A ⊕ B = A + B - @ + 1
(3) => sum + (A ⊕ B) = sum + A + B - @ + 1
sum + A + B - @ + 1 < @ + B - @ + 1 (adds 'B - @ + 1' to both
sides of (1))
=> sum + A + B - @ + 1 < B + 1 <= @
=> sum + A + B - @ + 1 < @
=> sum + (A ⊕ B) < @ (see (3))
=> sum ⊕ (A ⊕ B) = sum + A + B - @ + 1 = sum ⊕ A ⊕ B
If A + B < @:
=> A ⊕ B = A + B
=> sum + (A ⊕ B) = sum + A + B >= @ (see (2))
=> sum ⊕ (A ⊕ B) = sum + A + B - @ + 1 = sum ⊕ A ⊕ B
## In Case 3, we have
(1) sum + A >= @
=> sum ⊕ A = sum + A - @ + 1
(2) sum + A - @ + 1 + B >= @
=> sum ⊕ A ⊕ B = sum + A + B - 2@ + 2
(3) A + B >= 2@ - 1 - sum (transformed from (2))
1 + sum <= @ ( sum is in range [0, @) )
=> @ + 1 + sum <= 2@ ( adds @ to both sides)
=> @ <= 2@ - 1 - sum <= A + B (combining with (3))
=> A + B >= @ (cleaning up)
=> A ⊕ B = A + B - @ + 1
=> sum + (A ⊕ B) = sum + A + B - @ + 1 >= @ (see (2))
=> sum ⊕ (A ⊕ B) = sum + A + B - 2@ + 2 = sum ⊕ A ⊕ B
## In Case 4, we have
(1) sum + A < @
=> sum ⊕ A = sum + A
(2) sum + A + B < @
=> sum ⊕ A ⊕ B = sum + A + B
A + B < @ - sum (subtracts 'sum' from both sides of (2))
=> A + B < @
=> A ⊕ B = A + B
=> sum + (A ⊕ B) = sum + A + B < @ (see (2))
=> sum ⊕ (A ⊕ B) = sum + A + B = sum ⊕ A ⊕ B
Conclusion: sum ⊕ A ⊕ B = sum ⊕ (A ⊕ B)
Let U = sum ⊕ A ⊕ B (or sum ⊕ (A ⊕ B)), then
sum ⊕ A ⊕ B ⊕ C ⊕ D = U ⊕ C ⊕ D = U ⊕ (C ⊕ D) (use the conclusion)
so we have:
sum ⊕ A ⊕ B ⊕ C ⊕ D = sum ⊕ (A ⊕ B) ⊕ (C ⊕ D)
