		Search-engine friendly clone of the ACL2 documentation.

Bitops/rotate

Rotate-left-1

Rotate a bit-vector by a single place to the left.

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

Definitions and Theorems

Function: rotate-left-1

(defun rotate-left-1 (x width)
       (declare (xargs :guard (and (integerp x) (posp width))))
       (let ((__function__ 'rotate-left-1))
            (declare (ignorable __function__))
            (b* (((when (mbe :logic (zp width) :exec nil))
                  0)
                 (msb (logbit (- width 1) x))
                 (chop (loghead (- width 1) x)))
                (logcons msb chop))))

Theorem: natp-of-rotate-left-1

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

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

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

Theorem: nat-equiv-implies-equal-rotate-left-1-2

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

Theorem: logbitp-of-rotate-left-1-split

(defthm logbitp-of-rotate-left-1-split
        (equal (logbitp n (rotate-left-1 x width))
               (b* ((n (nfix n)) (width (nfix width)))
                   (cond ((>= n width) nil)
                         ((equal n 0) (logbitp (+ -1 width) x))
                         (t (logbitp (+ -1 n) x))))))

Theorem: unsigned-byte-p-of-rotate-left-1

(defthm unsigned-byte-p-of-rotate-left-1
        (implies (natp width)
                 (unsigned-byte-p width (rotate-left-1 x width))))