		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-bitsel

Implements svex-argmasks for BITSEL.

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

For n. If we care about ANY bit of (bitsel n x), then we care about all of n. But if we don't care about any bit of (bitsel n x), then N is completely irrelevant.

For x. The result of (4vec-bit-extract n x) is only one bit wide. If we can statically determine that n is a non-negative constant, then we can tell exactly which bit of x we care about and just care about that one bit.

Otherwise, if n is statically determined to be a negative constant, then the bitsel expression is going to return X anyway no matter what x is, so we don't care about x at all.

Otherwise, n might refer to anything, so we care about all of x unless the whole expression is completely irrelevant.

Definitions and Theorems

Function: svmask-for-bitsel

(defun svmask-for-bitsel (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-bitsel))
    (declare (ignorable __function__))
    (b* (((svex-nths n x) args)
         (mask (4vmask-fix mask)))
      (b* ((nval (svex-s4xeval n))
           (nmask (4vmask-all-or-none mask))
           ((unless (s4vec-2vec-p nval))
            (list nmask nmask))
           (nv (s4vec->upper nval))
           ((when (sparseint-< nv 0))
            (list nmask 0)))
        (list nmask
              (sparseint-concatenate
                   (sparseint-val nv)
                   0
                   (int-to-sparseint (sparseint-bit 0 mask))))))))

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-bitsel-correct

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