A 32-bit load or store: like the 64-bit form, but the imm12 offset is
scaled by 4 rather than 8, and the offset must be a multiple of 4. RM
handles are NvU32, so placing one into a parameter struct needs this width:
a 64-bit store would carry the neighbouring field along with it.
706def aarch64ScaledMemoryWord32 =
707 (lambda unrestricted base2 : Nat .
708 (lambda unrestricted base3 : Nat .
709 (lambda unrestricted register : (family AArch64Register) .
710 (lambda unrestricted address : (family AArch64Register) .
711 (lambda unrestricted offset : Nat .
712 (nat-eliminate
713 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
714 (constructor AArch64EncodeResult AArch64MisalignedOffset offset)
715 (lambda unrestricted predecessor : Nat .
716 (lambda unrestricted induction : (family AArch64EncodeResult) .
717 (aarch64EncodeBounded
718 offset
719 aarch64Scaled32OffsetLimit
720 (aarch64ByteWord
721 (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address))
722 (naturalAdd
723 (aarch64RnByte1 address)
724 (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Four)))
725 (naturalAdd
726 base2
727 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Four)))
728 base3))))
729 (naturalIsZero (naturalModuloUnchecked offset aarch64Four))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.