		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-bitnot

Implements svex-argmasks for BITNOT.

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

Since bitwise negation just negates bits without moving them around or merging them together, it doesn't seem like there's any way to improve on the outer care mask here.

Definitions and Theorems

Function: svmask-for-bitnot$inline

(defun svmask-for-bitnot$inline (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-bitnot))
    (declare (ignorable __function__))
    (b* ((mask (4vmask-fix mask)))
      (list mask))))

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-bitnot-correct

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