		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

4vmask-all-or-none

Care mask for an argument that matters fully, unless we don't care about any bits at all.

Signature
(4vmask-all-or-none outer-mask) → arg-mask
Arguments: outer-mask — Care mask from the outer expression.
Guard (4vmask-p outer-mask).
Returns: arg-mask — Care mask for the argument.
Type (4vmask-p arg-mask).

In various SVEX functions, such as (bitsel index expr), the index expressions have a simple care-mask behavior:

If we care about any bit of the bitsel expression, then we care about all of the bits of index.
Otherwise, we don't care about this expression at all, so all of its arguments are completely irrelevant and there is no reason to care about the index at all.

Similar things happen in, e.g., reduction operators, arithmetic operators (due to globally caring about whether there are any X/Z bits), etc., so this function ends up being widely used in the the functions that implement svex-argmasks.

Definitions and Theorems

Function: 4vmask-all-or-none$inline

(defun 4vmask-all-or-none$inline (outer-mask)
  (declare (xargs :guard (4vmask-p outer-mask)))
  (let ((__function__ '4vmask-all-or-none))
    (declare (ignorable __function__))
    (if (4vmask-empty outer-mask) 0 -1)))

Theorem: 4vmask-p-of-4vmask-all-or-none

(defthm 4vmask-p-of-4vmask-all-or-none
  (b* ((arg-mask (4vmask-all-or-none$inline outer-mask)))
    (4vmask-p arg-mask))
  :rule-classes :rewrite)

Theorem: 4vmask-all-or-none$inline-of-4vmask-fix-outer-mask

(defthm 4vmask-all-or-none$inline-of-4vmask-fix-outer-mask
  (equal (4vmask-all-or-none$inline (4vmask-fix outer-mask))
         (4vmask-all-or-none$inline outer-mask)))

Theorem: 4vmask-all-or-none$inline-4vmask-equiv-congruence-on-outer-mask

(defthm
    4vmask-all-or-none$inline-4vmask-equiv-congruence-on-outer-mask
  (implies (4vmask-equiv outer-mask outer-mask-equiv)
           (equal (4vmask-all-or-none$inline outer-mask)
                  (4vmask-all-or-none$inline outer-mask-equiv)))
  :rule-classes :congruence)