		Search-engine friendly clone of the ACL2 documentation.

Svmask-for-signx

Mask-for-generic-signx

Signature
(mask-for-generic-signx outer-mask) → arg-mask
Arguments: outer-mask — Guard (4vmask-p outer-mask).
Returns: arg-mask — Type (4vmask-p arg-mask).

Definitions and Theorems

Function: mask-for-generic-signx$inline

(defun mask-for-generic-signx$inline (outer-mask)
  (declare (xargs :guard (4vmask-p outer-mask)))
  (let ((__function__ 'mask-for-generic-signx))
    (declare (ignorable __function__))
    (b* ((mask (4vmask-fix outer-mask)))
      (if (sparseint-< mask 0)
          -1
        (let* ((mask-upper-bound (+ 1 (sparseint-length mask))))
          (sparseint-concatenate mask-upper-bound -1 0))))))

Theorem: 4vmask-p-of-mask-for-generic-signx

(defthm 4vmask-p-of-mask-for-generic-signx
  (b* ((arg-mask (mask-for-generic-signx$inline outer-mask)))
    (4vmask-p arg-mask))
  :rule-classes :type-prescription)

Theorem: mask-for-generic-signx$inline-of-4vmask-fix-outer-mask

(defthm mask-for-generic-signx$inline-of-4vmask-fix-outer-mask
  (equal (mask-for-generic-signx$inline (4vmask-fix outer-mask))
         (mask-for-generic-signx$inline outer-mask)))

Theorem: mask-for-generic-signx$inline-4vmask-equiv-congruence-on-outer-mask

(defthm
 mask-for-generic-signx$inline-4vmask-equiv-congruence-on-outer-mask
 (implies (4vmask-equiv outer-mask outer-mask-equiv)
          (equal (mask-for-generic-signx$inline outer-mask)
                 (mask-for-generic-signx$inline outer-mask-equiv)))
 :rule-classes :congruence)

Theorem: mask-for-generic-signx-correct-for-signx

(defthm mask-for-generic-signx-correct-for-signx
 (equal
  (4vec-mask mask
             (4vec-sign-ext n
                            (4vec-mask (mask-for-generic-signx mask)
                                       x)))
  (4vec-mask mask (4vec-sign-ext n x))))

Theorem: mask-for-generic-signx-specialized-for-signx

(defthm mask-for-generic-signx-specialized-for-signx
  (implies (and (equal (4vec-mask (mask-for-generic-signx mask)
                                  val1)
                       (4vec-mask (mask-for-generic-signx mask)
                                  val2))
                (syntaxp (term-order val2 val1)))
           (equal (4vec-mask mask (4vec-sign-ext n val2))
                  (4vec-mask mask (4vec-sign-ext n val1)))))

Theorem: mask-for-generic-signx-correct-for-concat-x

(defthm mask-for-generic-signx-correct-for-concat-x
 (equal
    (4vec-mask mask
               (4vec-concat n
                            (4vec-mask (mask-for-generic-signx mask)
                                       x)
                            y))
    (4vec-mask mask (4vec-concat n x y))))

Theorem: mask-for-generic-signx-correct-for-concat-y

(defthm mask-for-generic-signx-correct-for-concat-y
 (equal
    (4vec-mask mask
               (4vec-concat n x
                            (4vec-mask (mask-for-generic-signx mask)
                                       y)))
    (4vec-mask mask (4vec-concat n x y))))

Theorem: mask-for-generic-signx-specialized-for-concat-x

(defthm mask-for-generic-signx-specialized-for-concat-x
  (implies (and (equal (4vec-mask (mask-for-generic-signx mask)
                                  xval1)
                       (4vec-mask (mask-for-generic-signx mask)
                                  xval2))
                (syntaxp (term-order xval2 xval1)))
           (equal (4vec-mask mask (4vec-concat n xval1 yval))
                  (4vec-mask mask (4vec-concat n xval2 yval)))))

Theorem: mask-for-generic-signx-specialized-for-concat-y

(defthm mask-for-generic-signx-specialized-for-concat-y
  (implies (and (equal (4vec-mask (mask-for-generic-signx mask)
                                  yval1)
                       (4vec-mask (mask-for-generic-signx mask)
                                  yval2))
                (syntaxp (term-order yval2 yval1)))
           (equal (4vec-mask mask (4vec-concat n xval yval1))
                  (4vec-mask mask (4vec-concat n xval yval2)))))