		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-part-install

Signature
(a4vec-part-install lsb width in val mask) → partsel
Arguments: lsb — LSB of the range to write -- may be negative.
Guard (a4vec-p lsb).; width — Width of the range to write.
Guard (a4vec-p width).; in — input in which the range gets written.
Guard (a4vec-p in).; val — value to write to the range.
Guard (a4vec-p val).; mask — Guard (4vmask-p mask).
Returns: partsel — Type (a4vec-p partsel).

Definitions and Theorems

Function: a4vec-part-install

(defun a4vec-part-install (lsb width in val mask)
 (declare (xargs :guard (and (a4vec-p lsb)
                             (a4vec-p width)
                             (a4vec-p in)
                             (a4vec-p val)
                             (4vmask-p mask))))
 (let ((__function__ 'a4vec-part-install))
  (declare (ignorable __function__))
  (b* (((a4vec width))
       ((a4vec lsb))
       ((a4vec in))
       ((a4vec val))
       (mask (4vmask-fix mask))
       ((when (sparseint-equal mask 0))
        (a4vec-x)))
   (a4vec-ite
    (aig-and (a2vec-p lsb)
             (aig-and (a2vec-p width)
                      (aig-not (aig-sign-s width.upper))))
    (b*
     (((unless (sparseint-< 0 mask))
       (and
        (not (and (a4vec-constantp width)
                  (a4vec-constantp lsb)))
        (cw
         "Warning: bitblasting variable part install under unbounded mask~%"))
       (a4vec-ite
        (aig-sign-s lsb.upper)
        (a4vec-rsh
         (let ((minus-lsb (aig-unary-minus-s lsb.upper)))
           (a4vec minus-lsb minus-lsb))
         (a4vec-concat
              width val
              (a4vec-rsh
                   (let ((sum (aig-+-ss nil lsb.upper width.upper)))
                     (a4vec sum sum))
                   in -1)
              -1)
         mask)
        (a4vec-concat
         lsb in
         (a4vec-concat
              width val
              (a4vec-rsh
                   (let ((sum (aig-+-ss nil lsb.upper width.upper)))
                     (a4vec sum sum))
                   in -1)
              -1)
         mask)))
      (maskwidth (+ 1 (sparseint-length mask)))
      (lsbs.upper
        (aig-head-of-concat lsb.upper in.upper val.upper maskwidth))
      (lsbs.lower
        (aig-head-of-concat lsb.upper in.lower val.lower maskwidth))
      (overlap-idx (aig-+-ss nil lsb.upper width.upper))
      (overlap.upper
           (aig-overlap-width-ss overlap-idx
                                 lsbs.upper in.upper maskwidth))
      (overlap.lower
           (aig-overlap-width-ss overlap-idx
                                 lsbs.lower in.lower maskwidth)))
     (a4vec overlap.upper overlap.lower))
    (a4vec-x)))))

Theorem: a4vec-p-of-a4vec-part-install

(defthm a4vec-p-of-a4vec-part-install
  (b* ((partsel (a4vec-part-install lsb width in val mask)))
    (a4vec-p partsel))
  :rule-classes :rewrite)

Theorem: a4vec-part-install-correct

(defthm a4vec-part-install-correct
  (4vec-mask-equiv
       (a4vec-eval (a4vec-part-install lsb width in val mask)
                   env)
       (4vec-part-install (a4vec-eval lsb env)
                          (a4vec-eval width env)
                          (a4vec-eval in env)
                          (a4vec-eval val env))
       mask))

Theorem: a4vec-part-install-of-a4vec-fix-lsb

(defthm a4vec-part-install-of-a4vec-fix-lsb
  (equal (a4vec-part-install (a4vec-fix lsb)
                             width in val mask)
         (a4vec-part-install lsb width in val mask)))

Theorem: a4vec-part-install-a4vec-equiv-congruence-on-lsb

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

Theorem: a4vec-part-install-of-a4vec-fix-width

(defthm a4vec-part-install-of-a4vec-fix-width
  (equal (a4vec-part-install lsb (a4vec-fix width)
                             in val mask)
         (a4vec-part-install lsb width in val mask)))

Theorem: a4vec-part-install-a4vec-equiv-congruence-on-width

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

Theorem: a4vec-part-install-of-a4vec-fix-in

(defthm a4vec-part-install-of-a4vec-fix-in
  (equal (a4vec-part-install lsb width (a4vec-fix in)
                             val mask)
         (a4vec-part-install lsb width in val mask)))

Theorem: a4vec-part-install-a4vec-equiv-congruence-on-in

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

Theorem: a4vec-part-install-of-a4vec-fix-val

(defthm a4vec-part-install-of-a4vec-fix-val
  (equal (a4vec-part-install lsb width in (a4vec-fix val)
                             mask)
         (a4vec-part-install lsb width in val mask)))

Theorem: a4vec-part-install-a4vec-equiv-congruence-on-val

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

Theorem: a4vec-part-install-of-4vmask-fix-mask

(defthm a4vec-part-install-of-4vmask-fix-mask
  (equal (a4vec-part-install lsb width in val (4vmask-fix mask))
         (a4vec-part-install lsb width in val mask)))

Theorem: a4vec-part-install-4vmask-equiv-congruence-on-mask

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

Subtopics

Aig-overlap-width-ss: Symbolic function that replaces pos lower bits of y with bits of x.