Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2023/digital-systems-linear-algebra-and-introduction-to-formal-proof/1/d/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Digital systems, linear algebra and introduction to formal proof 1 d Solution by
Codex 0 2026-10-25
Let , let , and let denote the least nonnegative residue. Here is a signed 32-bit two's complement value. The source instructions, annotated with their derived values, are:The first instruction is an arithmetic right shift, so it replicates the sign bit. The second is a logical right shift, turning the all-one word into . The paired shifts then extract the low ten bits, as in (c). Their effect is the residue of even if its two's complement interpretation is negative, because divides the word modulus . The adjusted value is representable for every input: positive inputs are unchanged, and negative inputs gain only .
rem1024:
asrs r3, r0, #31 // r3 = -s: all zero bits or all one bits
lsrs r3, r3, #22 // r3 = b = 1023*s
adds r0, r0, r3 // r0 = a+b
lsls r0, r0, #22 // r0 has word value (a+b)*2^22 modulo 2^32
lsrs r0, r0, #22 // r0 = u = (a+b) modulo 1024, in 0,...,1023
subs r0, r0, r3 // r0 = u-b
bx lr // return u-bFor , , so the return value is the usual nonnegative remainder . For , put as a mathematical integer, and write with . If , then and the return value is zero. If , thenThese are precisely the remainders for C integer division, whose quotient truncates towards zero. In every case the result has the dividend's sign or is zero, has magnitude below , and satisfies . The proof includes the smallest representable input: was used only in mathematical reasoning, not as an overflowing machine operation.[ref]
C11 committee draft N1570. section 6.5.5 paragraph 6, quotient truncation and the quotient–remainder identity
New to topics? Read the docs here!