		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-part-install

Part install operation: replace width bits of in starting at lsb with the least-significant bits of val.

Signature
(4vec-part-install lsb width in val) → res
Arguments: lsb — Guard (4vec-p lsb).; width — Guard (4vec-p width).; in — Guard (4vec-p in).; val — Guard (4vec-p val).
Returns: res — Type (4vec-p res).

Definitions and Theorems

Function: 4vec-part-install

(defun 4vec-part-install (lsb width in val)
 (declare (xargs :guard (and (4vec-p lsb)
                             (4vec-p width)
                             (4vec-p in)
                             (4vec-p val))))
 (let ((__function__ '4vec-part-install))
  (declare (ignorable __function__))
  (if
   (and (2vec-p lsb)
        (2vec-p width)
        (<= 0 (2vec->val width)))
   (b*
    ((lsbval (2vec->val lsb))
     (widthval (2vec->val width))
     ((when (<= 0 lsbval))
      (4vec-concat lsb in
                   (4vec-concat width val
                                (4vec-rsh (2vec (+ lsbval widthval))
                                          in))))
     ((when (<= widthval (- lsbval)))
      (4vec-fix in)))
    (4vec-concat (2vec (+ widthval lsbval))
                 (4vec-rsh (2vec (- lsbval)) val)
                 (4vec-rsh (2vec (+ widthval lsbval))
                           in)))
   (4vec-x))))

Theorem: 4vec-p-of-4vec-part-install

(defthm 4vec-p-of-4vec-part-install
  (b* ((res (4vec-part-install lsb width in val)))
    (4vec-p res))
  :rule-classes :rewrite)

Theorem: 4vec-part-install-of-part-select

(defthm 4vec-part-install-of-part-select
  (implies
       (and (2vec-p lsb)
            (2vec-p width)
            (<= 0 (2vec->val width)))
       (equal (4vec-part-install lsb width
                                 in (4vec-part-select lsb width in))
              (4vec-fix in))))

Theorem: 4vec-part-select-of-install

(defthm 4vec-part-select-of-install
 (implies
  (and (2vec-p lsb)
       (2vec-p width)
       (<= 0 (2vec->val width)))
  (equal
   (4vec-part-select lsb width
                     (4vec-part-install lsb width in val))
   (if
    (< (2vec->val lsb) 0)
    (if
     (< (- (2vec->val lsb))
        (2vec->val width))
     (4vec-concat
         (2vec (- (2vec->val lsb)))
         (4vec-x)
         (4vec-zero-ext (2vec (+ (2vec->val width) (2vec->val lsb)))
                        (4vec-rsh (2vec (- (2vec->val lsb)))
                                  val)))
     (4vec-zero-ext width (4vec-x)))
    (4vec-zero-ext width val)))))

Theorem: 4vec-part-install-of-2vecx-fix-lsb

(defthm 4vec-part-install-of-2vecx-fix-lsb
  (equal (4vec-part-install (2vecx-fix lsb)
                            width in val)
         (4vec-part-install lsb width in val)))

Theorem: 4vec-part-install-2vecx-equiv-congruence-on-lsb

(defthm 4vec-part-install-2vecx-equiv-congruence-on-lsb
  (implies (2vecx-equiv lsb lsb-equiv)
           (equal (4vec-part-install lsb width in val)
                  (4vec-part-install lsb-equiv width in val)))
  :rule-classes :congruence)

Theorem: 4vec-part-install-of-2vecx-fix-width

(defthm 4vec-part-install-of-2vecx-fix-width
  (equal (4vec-part-install lsb (2vecx-fix width)
                            in val)
         (4vec-part-install lsb width in val)))

Theorem: 4vec-part-install-2vecx-equiv-congruence-on-width

(defthm 4vec-part-install-2vecx-equiv-congruence-on-width
  (implies (2vecx-equiv width width-equiv)
           (equal (4vec-part-install lsb width in val)
                  (4vec-part-install lsb width-equiv in val)))
  :rule-classes :congruence)

Theorem: 4vec-part-install-of-4vec-fix-in

(defthm 4vec-part-install-of-4vec-fix-in
  (equal (4vec-part-install lsb width (4vec-fix in)
                            val)
         (4vec-part-install lsb width in val)))

Theorem: 4vec-part-install-4vec-equiv-congruence-on-in

(defthm 4vec-part-install-4vec-equiv-congruence-on-in
  (implies (4vec-equiv in in-equiv)
           (equal (4vec-part-install lsb width in val)
                  (4vec-part-install lsb width in-equiv val)))
  :rule-classes :congruence)

Theorem: 4vec-part-install-of-4vec-fix-val

(defthm 4vec-part-install-of-4vec-fix-val
  (equal (4vec-part-install lsb width in (4vec-fix val))
         (4vec-part-install lsb width in val)))

Theorem: 4vec-part-install-4vec-equiv-congruence-on-val

(defthm 4vec-part-install-4vec-equiv-congruence-on-val
  (implies (4vec-equiv val val-equiv)
           (equal (4vec-part-install lsb width in val)
                  (4vec-part-install lsb width in val-equiv)))
  :rule-classes :congruence)