		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-partinst

Implements svex-argmasks for PARTINST.

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

Definitions and Theorems

Function: svmask-for-partinst

(defun svmask-for-partinst (mask args)
 (declare (xargs :guard (and (4vmask-p mask)
                             (svexlist-p args))))
 (let ((__function__ 'svmask-for-partinst))
  (declare (ignorable __function__))
  (b* (((svex-nths lsb width in val) args)
       (mask (4vmask-fix mask)))
   (b*
    (((when (4vmask-empty mask))
      (list 0 0 0 0))
     (lsbval (svex-s4xeval lsb))
     (widthval (svex-s4xeval width))
     ((unless (s4vec-2vec-p widthval))
      (list -1 -1 mask -1))
     (widthval (s4vec->upper widthval))
     ((when (sparseint-< widthval 0))
      (list 0 -1 0 0))
     ((unless (s4vec-2vec-p lsbval))
      (list -1 -1 mask
            (sparseint-concatenate (sparseint-val widthval)
                                   -1 0)))
     (lsbval (s4vec->upper lsbval))
     ((unless (sparseint-< lsbval 0))
      (b*
       ((lsbval (sparseint-val lsbval))
        (widthval (sparseint-val widthval))
        (inmask
           (sparseint-concatenate
                lsbval mask
                (sparseint-concatenate
                     widthval 0
                     (sparseint-ash mask (- (+ lsbval widthval))))))
        (valmask
           (sparseint-concatenate widthval
                                  (sparseint-rightshift lsbval mask)
                                  0)))
       (list -1 -1 inmask valmask)))
     ((when (sparseint-< (sparseint-unary-minus lsbval)
                         widthval))
      (b*
       ((width+lsb (sparseint-val (sparseint-plus widthval lsbval)))
        (inmask (sparseint-concatenate
                     width+lsb 0
                     (sparseint-rightshift width+lsb mask)))
        (valmask (sparseint-concatenate
                      (sparseint-val (sparseint-unary-minus lsbval))
                      0
                      (sparseint-concatenate width+lsb mask 0))))
       (list -1 -1 inmask valmask))))
    (list -1 -1 mask 0)))))

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-partinst-correct

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