		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-uand

Implements svex-argmasks for UAND.

Signature
(svmask-for-uand mask args) → argmasks
Arguments: mask — Care mask for the full expression.
Guard (4vmask-p mask).; args — Arguments to this UAND operator.
Guard (svexlist-p args).
Returns: argmasks — The new care masks inferred for the args.
Type (4vmasklist-p argmasks).

We are considering a (uand x) expression and we know that we only care about the bits mentioned in mask. We know that 4vec-reduction-and will need to consider all of the bits of x. Since it follows the boolean-convention, we also know that it is either going to return all 1s, all 0s, or all Xes.

Accordingly, it seems that if we care about any bit of the result, we need to care about all of the bits of the argument. On the other hand, if we don't care about any bits of the result, then we don't need to care about any bit of the argument.

Definitions and Theorems

Function: svmask-for-uand$inline

(defun svmask-for-uand$inline (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-uand))
    (declare (ignorable __function__))
    (b* (((svex-nths x) args)
         (mask (4vmask-fix mask)))
      (list (4vmask-all-or-none mask)))))

Theorem: 4vmasklist-p-of-svmask-for-uand

(defthm 4vmasklist-p-of-svmask-for-uand
  (b* ((argmasks (svmask-for-uand$inline mask args)))
    (4vmasklist-p argmasks))
  :rule-classes :rewrite)

Theorem: svmask-for-uand$inline-of-4vmask-fix-mask

(defthm svmask-for-uand$inline-of-4vmask-fix-mask
  (equal (svmask-for-uand$inline (4vmask-fix mask)
                                 args)
         (svmask-for-uand$inline mask args)))

Theorem: svmask-for-uand$inline-4vmask-equiv-congruence-on-mask

(defthm svmask-for-uand$inline-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (svmask-for-uand$inline mask args)
                  (svmask-for-uand$inline mask-equiv args)))
  :rule-classes :congruence)

Theorem: svmask-for-uand$inline-of-svexlist-fix-args

(defthm svmask-for-uand$inline-of-svexlist-fix-args
  (equal (svmask-for-uand$inline mask (svexlist-fix args))
         (svmask-for-uand$inline mask args)))

Theorem: svmask-for-uand$inline-svexlist-equiv-congruence-on-args

(defthm svmask-for-uand$inline-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svmask-for-uand$inline mask args)
                  (svmask-for-uand$inline mask args-equiv)))
  :rule-classes :congruence)

Theorem: svmask-for-uand-correct

(defthm svmask-for-uand-correct
 (implies
    (and (equal (4veclist-mask (svmask-for-uand mask args)
                               (svexlist-eval args env))
                (4veclist-mask (svmask-for-uand mask args)
                               args1))
         (syntaxp (not (equal args1
                              (cons 'svexlist-eval
                                    (cons args (cons env 'nil)))))))
    (equal (4vec-mask mask (svex-apply 'uand args1))
           (4vec-mask mask
                      (svex-apply 'uand
                                  (svexlist-eval args env))))))