		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-override

Implements svex-argmasks for OVERRIDE.

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

We are considering a (override stronger weaker) expression and we know that we only care about the bits mentioned in mask. We want to figure out which bits of stronger and weaker we care about. As a starting point, since override operates in a bit-by-bit fashion, we certainly don't care about any bits that are don't cares in our outer mask.

It doesn't seem like we can do any better than mask for stronger, since the output bit always depends on the stronger bit.

However, we definitely don't care about the value of weaker when the corresponding bit of stronger has a good Boolean value. So, we remove any such bits from the mask for weaker.

Definitions and Theorems

Function: svmask-for-override

(defun svmask-for-override (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-override))
    (declare (ignorable __function__))
    (b* (((svex-nths stronger weaker) args)
         (mask (4vmask-fix mask)))
      (b* (((s4vec sval) (svex-s4xeval stronger))
           (strong-nonbool (sparseint-bitxor sval.upper sval.lower))
           (weak-mask (sparseint-bitand mask strong-nonbool)))
        (list mask weak-mask)))))

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-override-correct

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