lsl by amount is ubfm with immr = (64 - amount) mod 64 and imms = 63 - amount.
940def aarch64ShiftLeftWord =
941 (lambda unrestricted destination : (family AArch64Register) .
942 (lambda unrestricted source : (family AArch64Register) .
943 (lambda unrestricted amount : Nat .
944 (aarch64EncodeBounded
945 amount
946 aarch64ShiftLimit
947 (app
948 (lambda unrestricted immr : Nat .
949 (app
950 (lambda unrestricted imms : Nat .
951 (aarch64ByteWord
952 (naturalAdd (aarch64LowFive destination) (aarch64RnByte0 source))
953 (naturalAdd (aarch64RnByte1 source) (aarch64Immediate12Byte1 imms))
954 (naturalAdd aarch64SixtyFour immr)
955 211))
956 (naturalSaturatingSubtract 63 amount)))
957 (naturalModuloUnchecked
958 (naturalSaturatingSubtract aarch64SixtyFour amount)
959 aarch64SixtyFour))))))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.