A scaled 64-bit load or store: the offset must be a multiple of eight.
677def aarch64ScaledMemoryWord =
678 (lambda unrestricted base2 : Nat .
679 (lambda unrestricted base3 : Nat .
680 (lambda unrestricted register : (family AArch64Register) .
681 (lambda unrestricted address : (family AArch64Register) .
682 (lambda unrestricted offset : Nat .
683 (nat-eliminate
684 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
685 (constructor AArch64EncodeResult AArch64MisalignedOffset offset)
686 (lambda unrestricted predecessor : Nat .
687 (lambda unrestricted induction : (family AArch64EncodeResult) .
688 (aarch64EncodeBounded
689 offset
690 aarch64ScaledOffsetLimit
691 (aarch64ByteWord
692 (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address))
693 (naturalAdd
694 (aarch64RnByte1 address)
695 (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Eight)))
696 (naturalAdd
697 base2
698 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Eight)))
699 base3))))
700 (naturalIsZero (naturalModuloUnchecked offset aarch64Eight))))))))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.