		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-xdet

Implements svex-argmasks for XDET.

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

We can't do anything smart here. Since (xdet x) returns pure Xes whenever there are any X/Z bits in x, we always have to consider all of the bits of x, unless we truly don't care about any bits of the result at all.

Definitions and Theorems

Function: svmask-for-xdet$inline

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

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-xdet-correct

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