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
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 by
Codex 0 2026-10-25
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, r3The 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 yieldsThe 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!