		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-rsh

Symbolic version of 4vec-rsh.

Signature
(a4vec-rsh amt x mask) → res
Arguments: amt — Right-shift amount.
Guard (a4vec-p amt).; x — Vector to shift.
Guard (a4vec-p x).; mask — Care mask for the result.
Guard (4vmask-p mask).
Returns: res — Type (a4vec-p res).

As a special consideration, we use the care mask to try to avoid creating enormous vectors when given a huge shift amount.

Definitions and Theorems

Function: a4vec-rsh

(defun a4vec-rsh (amt x mask)
 (declare (xargs :guard (and (a4vec-p amt)
                             (a4vec-p x)
                             (4vmask-p mask))))
 (let ((__function__ 'a4vec-rsh))
  (declare (ignorable __function__))
  (b* (((a4vec amt))
       ((a4vec x))
       (mask (4vmask-fix mask)))
   (a4vec-ite
    (a2vec-p amt)
    (b*
     ((shamt (aig-unary-minus-s amt.upper))
      ((when (sparseint-equal 0 mask))
       (a4vec-x))
      ((when (sparseint-< 0 mask))
       (b* ((maskwidth (+ 1 (sparseint-length mask)))
            (upper (aig-head-of-concat shamt (aig-sterm nil)
                                       x.upper maskwidth))
            (lower (aig-head-of-concat shamt (aig-sterm nil)
                                       x.lower maskwidth)))
         (a4vec upper lower)))
      (-
       (and
        (not (a4vec-constantp amt))
        (cw
         "Warning: bitblasting variable rightshift under unbounded mask~%")))
      (sign (aig-sign-s shamt))
      ((mv upper-left lower-left)
       (if (eq sign t)
           (mv nil nil)
         (b* ((lsh-amt (aig-force-sign-s nil shamt)))
           (mv (aig-ash-ss 1 x.upper lsh-amt)
               (aig-ash-ss 1 x.lower lsh-amt)))))
      ((mv upper-right lower-right)
       (if (not sign)
           (mv nil nil)
         (b* ((rsh-amt (aig-force-sign-s t shamt)))
           (mv (aig-right-shift-ss 1 x.upper rsh-amt)
               (aig-right-shift-ss 1 x.lower rsh-amt))))))
     (a4vec (aig-ite-bss-fn sign upper-right upper-left)
            (aig-ite-bss-fn sign lower-right lower-left)))
    (a4vec-x)))))

Theorem: a4vec-p-of-a4vec-rsh

(defthm a4vec-p-of-a4vec-rsh
  (b* ((res (a4vec-rsh amt x mask)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-rsh-correct

(defthm a4vec-rsh-correct
  (4vec-mask-equiv (a4vec-eval (a4vec-rsh amt x mask) env)
                   (4vec-rsh (a4vec-eval amt env)
                             (a4vec-eval x env))
                   mask))

Theorem: a4vec-rsh-of-a4vec-fix-amt

(defthm a4vec-rsh-of-a4vec-fix-amt
  (equal (a4vec-rsh (a4vec-fix amt) x mask)
         (a4vec-rsh amt x mask)))

Theorem: a4vec-rsh-a4vec-equiv-congruence-on-amt

(defthm a4vec-rsh-a4vec-equiv-congruence-on-amt
  (implies (a4vec-equiv amt amt-equiv)
           (equal (a4vec-rsh amt x mask)
                  (a4vec-rsh amt-equiv x mask)))
  :rule-classes :congruence)

Theorem: a4vec-rsh-of-a4vec-fix-x

(defthm a4vec-rsh-of-a4vec-fix-x
  (equal (a4vec-rsh amt (a4vec-fix x) mask)
         (a4vec-rsh amt x mask)))

Theorem: a4vec-rsh-a4vec-equiv-congruence-on-x

(defthm a4vec-rsh-a4vec-equiv-congruence-on-x
  (implies (a4vec-equiv x x-equiv)
           (equal (a4vec-rsh amt x mask)
                  (a4vec-rsh amt x-equiv mask)))
  :rule-classes :congruence)

Theorem: a4vec-rsh-of-4vmask-fix-mask

(defthm a4vec-rsh-of-4vmask-fix-mask
  (equal (a4vec-rsh amt x (4vmask-fix mask))
         (a4vec-rsh amt x mask)))

Theorem: a4vec-rsh-4vmask-equiv-congruence-on-mask

(defthm a4vec-rsh-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (a4vec-rsh amt x mask)
                  (a4vec-rsh amt x mask-equiv)))
  :rule-classes :congruence)

Subtopics

Aig-right-shift-ss