• 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-right-8

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

    Definitions and Theorems

    Function: rotate-right-8$inline

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