• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
          • Bitops/merge
          • Bitops-compatibility
          • Bitops-books
          • Logbitp-reasoning
          • Bitops/signed-byte-p
          • Fast-part-select
          • Bitops/integer-length
          • Bitops/extra-defs
          • Install-bit
          • Trailing-0-count
          • Bitops/defaults
          • Logbitp-mismatch
          • Trailing-1-count
          • Bitops/rotate
          • Bitops/equal-by-logbitp
          • Bitops/ash-bounds
          • Bitops/fast-logrev
          • Limited-shifts
          • Bitops/part-select
          • Bitops/parity
          • Bitops/saturate
          • Bitops/part-install
          • Bitops/logbitp-bounds
          • Bitops/ihsext-basics
          • Bitops/fast-rotate
            • Fast-rotate
              • Rotate-left-9
                • Rotate-left-8
                • Rotate-left-65
                • Rotate-left-64
                • Rotate-left-33
                • Rotate-left-32
                • Rotate-left-17
                • Rotate-left-16
                • Rotate-right-65
                • Rotate-right-64
                • Rotate-right-33
                • Rotate-right-32
                • Rotate-right-17
                • Rotate-right-16
                • Rotate-right-9
                • Rotate-right-8
            • Bitops/fast-logext
            • Bitops/ihs-extensions
          • Bv
          • Ihs
          • Rtl
        • Algebra
      • Testing-utilities
    • Fast-rotate

    Rotate-left-9

    Signature
    (rotate-left-9 x places) → *
    Arguments
    x — The bit vector to be rotated left.
    places — The number of places to rotate left.

    Definitions and Theorems

    Function: rotate-left-9$inline

    (defun rotate-left-9$inline (x places)
     (declare (type (unsigned-byte 9) x)
              (type (unsigned-byte 9) places))
     (let ((__function__ 'rotate-left-9))
      (declare (ignorable __function__))
      (mbe
       :logic (rotate-left x 9 places)
       :exec
       (let* ((x (mbe :logic (loghead 9 x) :exec x))
              (places (mbe :logic (lnfix places)
                           :exec places))
              (places (mbe :logic (mod places 9)
                           :exec
                           (if (< places 9)
                               (the (integer 0 8) places)
                             (the (integer 0 8) (rem places 9)))))
              (low-num (the (integer 0 9) (- 9 places)))
              (mask (the (unsigned-byte 9)
                         (1- (the (unsigned-byte 10)
                                  (ash 1 low-num)))))
              (xl (the (unsigned-byte 9) (logand x mask)))
              (xh (the (unsigned-byte 9)
                       (logand x
                               (the (signed-byte 10) (lognot mask)))))
              (xh-shift (the (unsigned-byte 9)
                             (ash xh (the (integer -9 0) (- low-num)))))
              (xl-shift (the (unsigned-byte 9)
                             (ash (the (unsigned-byte 9) xl)
                                  (the (integer 0 9) places))))
              (ans (the (unsigned-byte 9)
                        (logior xl-shift xh-shift))))
         ans))))