• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • 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
          • Rotate-right
          • Rotate-left
            • Rotate-left**
          • Rotate-right-1
          • Rotate-left-1
          • Rotate-right**
          • Rotate-left**
        • 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
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• Bitops/rotate

Rotate-left

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

Signature

(rotate-left x width places) → rotated

Arguments

x — The bit vector to be rotated left.
    Guard (integerp x).

width — The width of x.
    Guard (posp width).

places — The number of places to rotate left.
    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-left

(defun
 rotate-left (x width places)
 (declare (xargs :guard (and (integerp x)
                             (posp width)
                             (natp places))))
 (let
  ((__function__ 'rotate-left))
  (declare (ignorable __function__))
  (let*
   ((width (lnfix width))
    (places (lnfix places))
    (wmask (1- (ash 1 width)))
    (x (logand x wmask))
    (places (mbe :logic (mod places width)
                 :exec (if (< places width)
                           places (rem places width))))
    (places (acl2::gl-mbe
                 places
                 (logand places
                         (lognot (ash -1 (integer-length width))))))
    (low-num (- width places))
    (mask (1- (ash 1 low-num)))
    (xl (logand x mask))
    (xh (logand x (lognot mask)))
    (xh-shift (ash xh (- low-num)))
    (xl-shift (ash xl places))
    (ans (logior xl-shift xh-shift)))
   ans)))

Theorem: natp-of-rotate-left

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

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

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

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

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

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

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

Theorem: logbitp-of-rotate-left-split

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

Theorem: rotate-left-zero-width

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

Theorem: rotate-left-by-zero

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

Theorem: rotate-left-by-width

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

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

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

Theorem: rotate-left-of-rotate-left

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

Subtopics

Rotate-left**

Alternate, recursive definitions of rotate-left.