		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-zero-ext

Like loghead for 4vecs; the width is also a 4vec.

Signature
(4vec-zero-ext n x) → x-ext
Arguments: n — Position to truncate/zero-extend at.
Guard (4vec-p n).; x — The 4vec to truncate/zero-extend.
Guard (4vec-p x).
Returns: x-ext — Type (4vec-p x-ext).

When n is a natural number, we keep the least significant n bits of x and clear any bits above this to zero.

When n has any X or Z bits or is negative, the result is all X bits.

Definitions and Theorems

Function: 4vec-zero-ext

(defun 4vec-zero-ext (n x)
 (declare (xargs :guard (and (4vec-p n) (4vec-p x))))
 (let ((__function__ '4vec-zero-ext))
  (declare (ignorable __function__))
  (if
   (and (2vec-p n) (<= 0 (2vec->val n)))
   (if
    (mbe
        :logic nil
        :exec (and (>= (2vec->val n) (4vec-bit-limit))
                   (b* (((4vec x)))
                     (or (< x.upper 0) (< x.lower 0)))
                   (4vec-very-large-integer-warning (2vec->val n))))
    (4vec-x)
    (if-2vec-p (x)
               (2vec (loghead (2vec->val n) (2vec->val x)))
               (b* (((4vec x)) (nval (2vec->val n)))
                 (4vec (loghead nval x.upper)
                       (loghead nval x.lower)))))
   (4vec-x))))

Theorem: 4vec-p-of-4vec-zero-ext

(defthm 4vec-p-of-4vec-zero-ext
  (b* ((x-ext (4vec-zero-ext n x)))
    (4vec-p x-ext))
  :rule-classes :rewrite)

Theorem: 4vec-zero-ext-of-4vec-fix-n

(defthm 4vec-zero-ext-of-4vec-fix-n
  (equal (4vec-zero-ext (4vec-fix n) x)
         (4vec-zero-ext n x)))

Theorem: 4vec-zero-ext-4vec-equiv-congruence-on-n

(defthm 4vec-zero-ext-4vec-equiv-congruence-on-n
  (implies (4vec-equiv n n-equiv)
           (equal (4vec-zero-ext n x)
                  (4vec-zero-ext n-equiv x)))
  :rule-classes :congruence)

Theorem: 4vec-zero-ext-of-4vec-fix-x

(defthm 4vec-zero-ext-of-4vec-fix-x
  (equal (4vec-zero-ext n (4vec-fix x))
         (4vec-zero-ext n x)))

Theorem: 4vec-zero-ext-4vec-equiv-congruence-on-x

(defthm 4vec-zero-ext-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (4vec-zero-ext n x)
                  (4vec-zero-ext n x-equiv)))
  :rule-classes :congruence)