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

Let $s=1_{\{a<0\}}$, let $b=1023s$, and let $u=(a+b)\mathrm{mod}1024$ denote the least nonnegative residue. Here $a$ 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 $1023$. The paired shifts then extract the low ten bits, as in (c). Their effect is the residue of $a+b$ even if its two's complement interpretation is negative, because $1024$ divides the word modulus $2^{32}$. The adjusted value $a+b$ is representable for every input: positive inputs are unchanged, and negative inputs gain only $1023$.

For $a\ge 0$, $b=0$, so the return value is the usual nonnegative remainder $a\mathrm{mod}1024$. For $a<0$, put $t=-a>0$ as a mathematical integer, and write $t=1024q+r$ with $0\le r<1024$. If $r=0$, then $u=1023$ and the return value is zero. If $1\le r\le 1023$, 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 $1024$, and satisfies $a=1024q_C+r_C$. The proof includes the smallest representable input: $t=-a$ was used only in mathematical reasoning, not as an overflowing machine operation.^[ref]