Avoiding Hardware Aliasing: Verifying RISC Machine and Assembly Code for Encrypted Computing

´Hardware aliasing´ classically arises when a processor through failure or design has fewer bits than required to address each memory location uniquely, and also - nowadays - in the context of homomorphically encrypted computing. In such contexts, different physical locations may sporadically be accessed by the same address due to factors not directly under the control of the programmer but still deterministic in nature. We check RISC machine and assembly code to ensure that each memory address is calculated in exactly the same way at one write to and the next read from it, which allows programs to work correctly even in a hardware aliasing context.