		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-lsh

Symbolic version of 4vec-lsh.

Signature
(a4vec-lsh amt x mask) → res
Arguments: amt — Guard (a4vec-p amt).; x — Guard (a4vec-p x).; mask — Guard (4vmask-p mask).
Returns: res — Type (a4vec-p res).

Definitions and Theorems

Function: a4vec-lsh

(defun a4vec-lsh (amt x mask)
 (declare (xargs :guard (and (a4vec-p amt)
                             (a4vec-p x)
                             (4vmask-p mask))))
 (let ((__function__ 'a4vec-lsh))
  (declare (ignorable __function__))
  (b* (((a4vec amt))
       ((a4vec x))
       (mask (4vmask-fix mask)))
   (a4vec-ite
    (a2vec-p amt)
    (b*
     ((shamt amt.upper)
      (sign (aig-sign-s shamt))
      ((mv upper-left lower-left)
       (b* (((when (eq sign t)) (mv nil nil))
            (lsh-amt (if (sparseint-< mask 0)
                         shamt
                       (aig-logcollapse-ns
                            (integer-length (sparseint-length mask))
                            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)
         (mv (aig-right-shift-ss 1 x.upper shamt)
             (aig-right-shift-ss 1 x.lower shamt))))
      (upper (aig-ite-bss-fn sign upper-right upper-left))
      (lower (aig-ite-bss-fn sign lower-right lower-left)))
     (a4vec upper lower))
    (a4vec-x)))))

Theorem: a4vec-p-of-a4vec-lsh

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

Theorem: a4vec-lsh-correct

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

Theorem: a4vec-lsh-of-a4vec-fix-amt

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

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

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

Theorem: a4vec-lsh-of-a4vec-fix-x

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

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

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

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

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

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

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