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 / b

A logical right shift by $k$ moves $a_{i+k}$ into position $i$ and fills the high positions with zero. Its unsigned interpretation isMeanwhile the original unsigned interpretation decomposes asBy integer division, $q=\lfloor a/2^k\rfloor$, exactly the unsigned quotient. Thus the source instruction puts the required quotient into r1. This is a proof from binary representation, rather than an assumption that every kind of right shift implements every kind of division. The displayed bit argument applies to $0\le k\le n$, with endpoint operations implemented as a copy or zero where appropriate.