		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-bitxor

Implements svex-argmasks for BITXOR.

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

We are considering a (bitxor x y) expression and we know that we only care about the bits mentioned in mask. We want to figure out which bits of X and Y we care about. As a starting point, since bitwise XOR operates in a bit-by-bit fashion, we certainly don't care about any bits that are don't cares in our outer mask. We can only do slightly better than this.

Consider any two bits, Xi and Yi. Even if we know that Xi is 0 or 1, that doesn't help us to avoid needing to evaluate Yi. On the other hand, if we can statically determine that Xi is definitely X or Z, then we don't need to care about the corresponding bit of Yi.

We typically do these kinds of static determinations using svex-xeval. This can tell us when Xi is definitely Z, but not when it is definitely X. So for now we only try to improve the mask in cases where Xi is definitely Z, and we don't yet try to take advantage of knowing that Xi is definitely X. Some day we might want to consider whether we could easily modify svex-xeval to identify definite X values as well.

At any rate, this is largely similar to svmask-for-bitand; we can symmetrically ignore any bits in X where the corresponding bits of Y are Zs, and vice versa, except that we again have to watch out for the case where both X and Y share some Z bit and, in that case, we have to keep one or the other.

Definitions and Theorems

Function: svmask-for-bitxor

(defun svmask-for-bitxor (mask args)
 (declare (xargs :guard (and (4vmask-p mask)
                             (svexlist-p args))))
 (let ((__function__ 'svmask-for-bitxor))
  (declare (ignorable __function__))
  (b* (((svex-nths x y) args)
       (mask (4vmask-fix mask)))
    (b*
     (((s4vec xval) (svex-s4xeval x))
      ((s4vec yval) (svex-s4xeval y))
      (x-z (sparseint-bitandc1 xval.upper xval.lower))
      (y-z (sparseint-bitandc1 yval.upper yval.lower))
      (shared-zs (sparseint-bitand x-z (sparseint-bitand y-z mask)))
      (xm-nonz (sparseint-bitandc2 mask x-z))
      (ym-nonz (sparseint-bitandc2 mask y-z))
      ((when (sparseint-equal 0 shared-zs))
       (list ym-nonz xm-nonz))
      (y-x (sparseint-bitandc2 yval.upper yval.lower))
      (ym-x (sparseint-test-bitand mask y-x))
      ((unless ym-x)
       (list ym-nonz
             (sparseint-bitor xm-nonz shared-zs))))
     (list (sparseint-bitor ym-nonz shared-zs)
           xm-nonz)))))

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

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

Theorem: svmask-for-bitxor-of-4vmask-fix-mask

(defthm svmask-for-bitxor-of-4vmask-fix-mask
  (equal (svmask-for-bitxor (4vmask-fix mask)
                            args)
         (svmask-for-bitxor mask args)))

Theorem: svmask-for-bitxor-4vmask-equiv-congruence-on-mask

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

Theorem: svmask-for-bitxor-of-svexlist-fix-args

(defthm svmask-for-bitxor-of-svexlist-fix-args
  (equal (svmask-for-bitxor mask (svexlist-fix args))
         (svmask-for-bitxor mask args)))

Theorem: svmask-for-bitxor-svexlist-equiv-congruence-on-args

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

Theorem: svmask-for-bitxor-correct

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