		Search-engine friendly clone of the ACL2 documentation.

4vmask

4vec-mask

Reduce a constant 4vec using a 4vmask; any irrelevant bits become Xes.

Signature
(4vec-mask mask value) → masked-value
Arguments: mask — Mask of bits that we care about.
Guard (4vmask-p mask).; value — Original value to be masked.
Guard (4vec-p value).
Returns: masked-value — value with irrelevant bits replaced by Xes.
Type (4vec-p masked-value).

Definitions and Theorems

Function: 4vec-mask

(defun 4vec-mask (mask value)
  (declare (xargs :guard (and (4vmask-p mask) (4vec-p value))))
  (let ((__function__ '4vec-mask))
    (declare (ignorable __function__))
    (b* ((mask (sparseint-val (4vmask-fix mask)))
         ((4vec value) value))
      (4vec (logior (lognot mask) value.upper)
            (logand mask value.lower)))))

Theorem: 4vec-p-of-4vec-mask

(defthm 4vec-p-of-4vec-mask
  (b* ((masked-value (4vec-mask mask value)))
    (4vec-p masked-value))
  :rule-classes :rewrite)

Theorem: 4vec-mask-of-4vmask-fix-mask

(defthm 4vec-mask-of-4vmask-fix-mask
  (equal (4vec-mask (4vmask-fix mask) value)
         (4vec-mask mask value)))

Theorem: 4vec-mask-4vmask-equiv-congruence-on-mask

(defthm 4vec-mask-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (4vec-mask mask value)
                  (4vec-mask mask-equiv value)))
  :rule-classes :congruence)

Theorem: 4vec-mask-of-4vec-fix-value

(defthm 4vec-mask-of-4vec-fix-value
  (equal (4vec-mask mask (4vec-fix value))
         (4vec-mask mask value)))

Theorem: 4vec-mask-4vec-equiv-congruence-on-value

(defthm 4vec-mask-4vec-equiv-congruence-on-value
  (implies (4vec-equiv value value-equiv)
           (equal (4vec-mask mask value)
                  (4vec-mask mask value-equiv)))
  :rule-classes :congruence)

Theorem: 4vec-mask-idempotent

(defthm 4vec-mask-idempotent
  (equal (4vec-mask mask (4vec-mask mask value))
         (4vec-mask mask value)))

Theorem: 4vec-mask-minus-1

(defthm 4vec-mask-minus-1
  (equal (4vec-mask -1 value)
         (4vec-fix value)))

Theorem: 4vec-mask-zero

(defthm 4vec-mask-zero
  (equal (4vec-mask 0 value) (4vec-x)))