Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 1 / c / Solution

Let r1:r0 hold the first operand, high limb first, and r3:r2 the second. In assembly language the addition can be written:

adds r0, r0, r2
adcs r1, r1, r3

The first instruction produces the low result and its arithmetic carry; the second immediately consumes that arithmetic carry while adding the high limbs. No intervening flag-setting instruction is permitted.

For a proof, put $M=2^{32}$ and denote the input limbs by $X_1,X_0,Y_1,Y_0$. If the low addition gives $Z_0$ and arithmetic carry $c$, then $X_0+Y_0=Z_0+Mc$. The high addition gives $Z_1$ and final arithmetic carry $d$, so $X_1+Y_1+c=Z_1+Md$. Multiplying the second identity by $M$ and combining yieldsThe processor register pair is the correct result modulo $2^{64}$, and the final arithmetic carry records overflow beyond that unsigned width. If the mathematical sum fits in 64 bits, no reduction changes it.