adr: a 21-bit BYTE distance, its low two bits at bits 29-30 and the rest at bit 5.
910def aarch64AddressWord =
911 (lambda unrestricted destination : (family AArch64Register) .
912 (lambda unrestricted direction : (family AArch64Direction) .
913 (lambda unrestricted distance : Nat .
914 (nat-eliminate
915 (lambda unrestricted accepted : Nat . (family AArch64EncodeResult))
916 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance)
917 (lambda unrestricted predecessor : Nat .
918 (lambda unrestricted induction : (family AArch64EncodeResult) .
919 (app
920 (lambda unrestricted field : Nat .
921 (app
922 (lambda unrestricted high : Nat .
923 (aarch64ByteWord
924 (naturalAdd (aarch64LowFive destination) (aarch64FromBitFiveByte0 high))
925 (aarch64FromBitFiveByte1 high)
926 (aarch64FromBitFiveByte2 high)
927 (naturalAdd
928 16
929 (naturalMultiply
930 (naturalModuloUnchecked field aarch64Four)
931 aarch64ThirtyTwo))))
932 (naturalDivideUnchecked field aarch64Four)))
933 (aarch64SignedField direction distance aarch64Modulus21))))
934 (aarch64DistanceAccepted
935 direction
936 distance
937 (naturalDivideUnchecked aarch64Modulus21 aarch64Two))))))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.