		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-concat

Implements svex-argmasks for CONCAT.

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

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

For n. If we care about ANY bit of (concat n x y), 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 and y. If n is statically known but is negative, then the result of 4vec-concat is just all Xes no matter what x and y are, so they don't matter at all.

If n is statically known and positive, then we can adjust mask as appropriate, taking the first n bits of it as the care mask for x, and taking the remaining bits of it as the care mask for y.

If we don't statically know n, then we may still be able to do something based on the outer mask. For instance, if mask is #b1000, then even if we don't know where the bits are coming from, we certainly know that we don't care about bits of x or y that are above bit 4, because no matter what index is used that's as many bits as we could take from either of them.

BOZO for now we don't exploit this and simply say that we depend on all of x. In the future, it would be good to integrate something like mask-for-generic-signx here.

Definitions and Theorems

Function: svmask-for-concat

(defun svmask-for-concat (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-concat))
    (declare (ignorable __function__))
    (b* (((svex-nths n x y) args)
         (mask (4vmask-fix mask)))
      (b* (((when (4vmask-empty mask))
            (list 0 0 0))
           (nval (svex-s4xeval n))
           ((unless (s4vec-2vec-p nval))
            (let ((argmask (mask-for-generic-signx mask)))
              (list -1 argmask argmask)))
           (n (s4vec->upper nval))
           ((when (sparseint-< n 0))
            (list -1 0 0)))
        (list -1
              (sparseint-concatenate (sparseint-val n)
                                     mask 0)
              (sparseint-rightshift (sparseint-val n)
                                    mask))))))

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-concat-correct

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