		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-lsh

Left ``arithmetic'' shift of 4vecs.

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

In the usual case, amt is a 2vec, i.e., its bits are all good Boolean values. In this case:

If amt is non-negative, then we shift src to the left by amt-many places. The least significant bits become 0s.
If amt is negative, then we shift src to the right instead of to the left. This is an ``arithmetic'' shift, as described in 4vec-rsh. Note that this behavior differs from the (very strange) semantics of Verilog/SystemVerilog, where shift amounts are always treated as unsigned.

In cases where amt has any X or Z bits, the result is just all Xes.

Definitions and Theorems

Function: 4vec-lsh

(defun 4vec-lsh (amt src)
  (declare (xargs :guard (and (4vec-p amt) (4vec-p src))))
  (let ((__function__ '4vec-lsh))
    (declare (ignorable __function__))
    (if (2vec-p amt)
        (4vec-shift-core (2vec->val amt) src)
      (4vec-x))))

Theorem: 4vec-p-of-4vec-lsh

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

Theorem: 4vec-lsh-of-2vecx-fix-amt

(defthm 4vec-lsh-of-2vecx-fix-amt
  (equal (4vec-lsh (2vecx-fix amt) src)
         (4vec-lsh amt src)))

Theorem: 4vec-lsh-2vecx-equiv-congruence-on-amt

(defthm 4vec-lsh-2vecx-equiv-congruence-on-amt
  (implies (2vecx-equiv amt amt-equiv)
           (equal (4vec-lsh amt src)
                  (4vec-lsh amt-equiv src)))
  :rule-classes :congruence)

Theorem: 4vec-lsh-of-4vec-fix-src

(defthm 4vec-lsh-of-4vec-fix-src
  (equal (4vec-lsh amt (4vec-fix src))
         (4vec-lsh amt src)))

Theorem: 4vec-lsh-4vec-equiv-congruence-on-src

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