		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-shift-core

Signature
(4vec-shift-core amt src) → shift
Arguments: amt — Shift amount.
Guard (integerp amt).; src — Source operand.
Guard (4vec-p src).
Returns: shift — Type (4vec-p shift).

Definitions and Theorems

Function: 4vec-shift-core

(defun 4vec-shift-core (amt src)
  (declare (xargs :guard (and (integerp amt) (4vec-p src))))
  (let ((__function__ '4vec-shift-core))
    (declare (ignorable __function__))
    (b* ((amt (lifix amt)))
      (if (mbe :logic nil
               :exec (and (>= amt (4vec-bit-limit))
                          (b* (((4vec src)))
                            (not (and (eql src.upper 0)
                                      (eql src.lower 0))))
                          (4vec-very-large-integer-warning amt)))
          (4vec-x)
        (if-2vec-p (src)
                   (2vec (ash (2vec->val src) amt))
                   (b* (((4vec src)))
                     (4vec (ash src.upper amt)
                           (ash src.lower amt))))))))

Theorem: 4vec-p-of-4vec-shift-core

(defthm 4vec-p-of-4vec-shift-core
  (b* ((shift (4vec-shift-core amt src)))
    (4vec-p shift))
  :rule-classes :rewrite)

Theorem: 4vec-shift-core-of-ifix-amt

(defthm 4vec-shift-core-of-ifix-amt
  (equal (4vec-shift-core (ifix amt) src)
         (4vec-shift-core amt src)))

Theorem: 4vec-shift-core-int-equiv-congruence-on-amt

(defthm 4vec-shift-core-int-equiv-congruence-on-amt
  (implies (int-equiv amt amt-equiv)
           (equal (4vec-shift-core amt src)
                  (4vec-shift-core amt-equiv src)))
  :rule-classes :congruence)

Theorem: 4vec-shift-core-of-4vec-fix-src

(defthm 4vec-shift-core-of-4vec-fix-src
  (equal (4vec-shift-core amt (4vec-fix src))
         (4vec-shift-core amt src)))

Theorem: 4vec-shift-core-4vec-equiv-congruence-on-src

(defthm 4vec-shift-core-4vec-equiv-congruence-on-src
  (implies (4vec-equiv src src-equiv)
           (equal (4vec-shift-core amt src)
                  (4vec-shift-core amt src-equiv)))
  :rule-classes :congruence)