		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-sign-ext

Symbolic version of 4vec-sign-ext.

Signature
(a4vec-sign-ext n x mask) → res
Arguments: n — Guard (a4vec-p n).; x — Guard (a4vec-p x).; mask — Guard (4vmask-p mask).
Returns: res — Type (a4vec-p res).

We essentially just extract the sign bit, sign extend it, and then use a4vec-concat to carry out the concatenation, since it already provides special optimization to avoid problems due to large masks.

Definitions and Theorems

Function: a4vec-sign-ext

(defun a4vec-sign-ext (n x mask)
 (declare (xargs :guard (and (a4vec-p n)
                             (a4vec-p x)
                             (4vmask-p mask))))
 (let ((__function__ 'a4vec-sign-ext))
  (declare (ignorable __function__))
  (b* (((a4vec n) n) ((a4vec x) x))
   (a4vec-ite
    (aig-and (a2vec-p n)
             (aig-nor (aig-sign-s n.upper)
                      (aig-=-ss n.upper (aig-sterm nil))))
    (b*
     ((signpos (aig-+-ss nil (aig-sterm t) n.upper))
      (high-bits
           (a4vec (aig-sterm (aig-logbitp-n2v 1 signpos x.upper))
                  (aig-sterm (aig-logbitp-n2v 1 signpos x.lower)))))
     (a4vec-concat n x high-bits mask))
    (a4vec-x)))))

Theorem: a4vec-p-of-a4vec-sign-ext

(defthm a4vec-p-of-a4vec-sign-ext
  (b* ((res (a4vec-sign-ext n x mask)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-sign-ext-correct

(defthm a4vec-sign-ext-correct
  (4vec-mask-equiv (a4vec-eval (a4vec-sign-ext n x mask)
                               env)
                   (4vec-sign-ext (a4vec-eval n env)
                                  (a4vec-eval x env))
                   mask))

Theorem: a4vec-sign-ext-of-a4vec-fix-n

(defthm a4vec-sign-ext-of-a4vec-fix-n
  (equal (a4vec-sign-ext (a4vec-fix n) x mask)
         (a4vec-sign-ext n x mask)))

Theorem: a4vec-sign-ext-a4vec-equiv-congruence-on-n

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

Theorem: a4vec-sign-ext-of-a4vec-fix-x

(defthm a4vec-sign-ext-of-a4vec-fix-x
  (equal (a4vec-sign-ext n (a4vec-fix x) mask)
         (a4vec-sign-ext n x mask)))

Theorem: a4vec-sign-ext-a4vec-equiv-congruence-on-x

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

Theorem: a4vec-sign-ext-of-4vmask-fix-mask

(defthm a4vec-sign-ext-of-4vmask-fix-mask
  (equal (a4vec-sign-ext n x (4vmask-fix mask))
         (a4vec-sign-ext n x mask)))

Theorem: a4vec-sign-ext-4vmask-equiv-congruence-on-mask

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