		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-offp

Implements svex-argmasks for OFFP.

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

Since offp affects each bit, without moving bits 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-offp$inline

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

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-offp-correct

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