		Search-engine friendly clone of the ACL2 documentation.

Limited-shifts

Limshift-loghead-of-ash

Computes (loghead width (ash x shift-amt)).

Signature
(limshift-loghead-of-ash width x shift-amt) → shifted
Arguments: width — Guard (natp width).; x — Guard (integerp x).; shift-amt — Guard (integerp shift-amt).
Returns: shifted — Type (integerp shifted).

Definitions and Theorems

Function: limshift-loghead-of-ash

(defun limshift-loghead-of-ash (width x shift-amt)
  (declare (xargs :guard (and (natp width)
                              (integerp x)
                              (integerp shift-amt))))
  (let ((__function__ 'limshift-loghead-of-ash))
    (declare (ignorable __function__))
    (b* ((shift-amt (lifix shift-amt))
         (x (lifix x))
         (width (lnfix width))
         ((when (< shift-amt 0))
          (loghead width (logtail (- shift-amt) x)))
         (shift-amt-limited (logcollapse (integer-length width)
                                         shift-amt)))
      (loghead width (ash x shift-amt-limited)))))

Theorem: integerp-of-limshift-loghead-of-ash

(defthm integerp-of-limshift-loghead-of-ash
  (b* ((shifted (limshift-loghead-of-ash width x shift-amt)))
    (integerp shifted))
  :rule-classes :type-prescription)

Theorem: limshift-loghead-of-ash-correct

(defthm limshift-loghead-of-ash-correct
  (equal (limshift-loghead-of-ash width x shift-amt)
         (loghead width (ash x shift-amt))))