Solution

ID: 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 and denote the input limbs by . If the low addition gives and arithmetic carry , then . The high addition gives and final arithmetic carry , so . Multiplying the second identity by and combining yields
The processor register pair is the correct result modulo , and the final arithmetic carry records overflow beyond that unsigned width. If the mathematical sum fits in 64 bits, no reduction changes it.

New to topics? Read the docs here!