		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-rsh

Implements svex-argmasks for RSH.

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

We are considering a (rsh n x) expression and we know that we only care about the bits mentioned in mask. We need to figure out which bits of n and x we care about.

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

For x. If we statically know n, then we are just going to shift the bits of x right (or left, if n is negative) by that many places, so we just need to similarly shift the outer care mask.

If n is not statically known, and we care about any bits of the answer, then it seems like we need to care about all of x. After all, any bit of x might in principle get shifted into the bit position that we care about.

Definitions and Theorems

Function: svmask-for-rsh

(defun svmask-for-rsh (mask args)
 (declare (xargs :guard (and (4vmask-p mask)
                             (svexlist-p args))))
 (let ((__function__ 'svmask-for-rsh))
  (declare (ignorable __function__))
  (b* (((svex-nths n x) args)
       (mask (4vmask-fix mask)))
    (b*
      (((when (4vmask-empty mask)) (list 0 0))
       (nval (svex-s4xeval n))
       ((when (s4vec-2vec-p nval))
        (list -1
              (sparseint-ash mask
                             (sparseint-val (s4vec->upper nval))))))
      (list -1 -1)))))

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-rsh-correct

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