		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-sign-ext

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

Signature
(4vec-sign-ext n x) → x-ext
Arguments: n — Guard (4vec-p n).; x — Guard (4vec-p x).
Returns: x-ext — Type (4vec-p x-ext).

When n is a positive natural, we keep the least significant n bits of x and then sign-extend them to infinity, i.e., bit n-1 gets replicated out to infinity.

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

Definitions and Theorems

Function: 4vec-sign-ext

(defun 4vec-sign-ext (n x)
  (declare (xargs :guard (and (4vec-p n) (4vec-p x))))
  (let ((__function__ '4vec-sign-ext))
    (declare (ignorable __function__))
    (if (and (2vec-p n) (< 0 (2vec->val n)))
        (if-2vec-p (x)
                   (2vec (fast-logext (2vec->val n)
                                      (2vec->val x)))
                   (b* (((4vec x)) (nval (2vec->val n)))
                     (4vec (fast-logext nval x.upper)
                           (fast-logext nval x.lower))))
      (4vec-x))))

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

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

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

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

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

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

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

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

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

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