		Search-engine friendly clone of the ACL2 documentation.

Bitops/rotate

Rotate-right

Rotate a bit-vector some arbitrary number of places to the right.

Signature
(rotate-right x width places) → rotated
Arguments: x — The bit vector to be rotated right.
Guard (integerp x).; width — The width of x.
Guard (posp width).; places — The number of places to rotate right.
Guard (natp places).
Returns: rotated — Type (natp rotated).

Note that places can be larger than width. We automatically reduce the number of places modulo the width, which makes sense since rotating width-many times is the same as not rotating at all.

Definitions and Theorems

Function: rotate-right

(defun
     rotate-right (x width places)
     (declare (xargs :guard (and (integerp x)
                                 (posp width)
                                 (natp places))))
     (let ((__function__ 'rotate-right))
          (declare (ignorable __function__))
          (let* ((width (lnfix width))
                 (x (mbe :logic (loghead width x)
                         :exec (logand x (+ -1 (ash 1 width)))))
                 (places (lnfix places))
                 (places (mbe :logic (mod places width)
                              :exec (if (< places width)
                                        places (rem places width))))
                 (mask (1- (ash 1 places)))
                 (xl (logand x mask))
                 (xh-shift (ash x (- places)))
                 (high-num (- width places))
                 (xl-shift (ash xl high-num))
                 (ans (logior xl-shift xh-shift)))
                ans)))

Theorem: natp-of-rotate-right

(defthm acl2::natp-of-rotate-right
        (b* ((rotated (rotate-right x width places)))
            (natp rotated))
        :rule-classes :type-prescription)

Theorem: int-equiv-implies-equal-rotate-right-1

(defthm int-equiv-implies-equal-rotate-right-1
        (implies (int-equiv x x-equiv)
                 (equal (rotate-right x width places)
                        (rotate-right x-equiv width places)))
        :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-rotate-right-2

(defthm nat-equiv-implies-equal-rotate-right-2
        (implies (nat-equiv width width-equiv)
                 (equal (rotate-right x width places)
                        (rotate-right x width-equiv places)))
        :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-rotate-right-3

(defthm nat-equiv-implies-equal-rotate-right-3
        (implies (nat-equiv places places-equiv)
                 (equal (rotate-right x width places)
                        (rotate-right x width places-equiv)))
        :rule-classes (:congruence))

Theorem: logbitp-of-rotate-right-split

(defthm logbitp-of-rotate-right-split
        (let ((lhs (logbitp n (rotate-right x width places))))
             (equal lhs
                    (b* ((n (nfix n))
                         (width (nfix width))
                         (places (mod (nfix places) width)))
                        (cond ((>= n width) nil)
                              ((>= n (- width places))
                               (logbitp (+ n places (- width)) x))
                              (t (logbitp (+ n places) x)))))))

Theorem: rotate-right-zero-width

(defthm rotate-right-zero-width
        (equal (rotate-right x 0 places) 0))

Theorem: rotate-right-by-zero

(defthm rotate-right-by-zero
        (equal (rotate-right x width 0)
               (loghead width x)))

Theorem: rotate-right-by-width

(defthm rotate-right-by-width
        (equal (rotate-right x width width)
               (loghead width x)))

Theorem: unsigned-byte-p-of-rotate-right

(defthm
    unsigned-byte-p-of-rotate-right
    (implies (natp width)
             (unsigned-byte-p width (rotate-right x width places))))

Theorem: rotate-right-of-rotate-right

(defthm rotate-right-of-rotate-right
        (equal (rotate-right (rotate-right x width places1)
                             width places2)
               (rotate-right x width
                             (+ (nfix places1) (nfix places2)))))

Subtopics

Rotate-right**: Alternate, recursive definitions of rotate-right.