		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-binary-bitop-int-width

Signature
(sparseint$-binary-bitop-int-width op width offset x x.height y) → (mv binary-res height)
Arguments: op — Guard (integerp op).; width — Guard (posp width).; offset — Guard (natp offset).; x — Guard (sparseint$-p x).; x.height — Guard (natp x.height).; y — Guard (integerp y).
Returns: binary-res — Type (sparseint$-p binary-res).; height — Type (equal height (sparseint$-height binary-res)).

Definitions and Theorems

Function: sparseint$-binary-bitop-int-width

(defun sparseint$-binary-bitop-int-width
       (op width offset x x.height y)
 (declare (type (unsigned-byte 4) op))
 (declare (xargs :guard (and (integerp op)
                             (posp width)
                             (natp offset)
                             (sparseint$-p x)
                             (natp x.height)
                             (integerp y))))
 (declare
      (xargs :guard (and (sparseint$-height-correctp x)
                         (equal x.height (sparseint$-height x)))))
 (let ((__function__ 'sparseint$-binary-bitop-int-width))
  (declare (ignorable __function__))
  (b*
   ((width (lposfix width))
    (offset (lnfix offset))
    (y (lifix y))
    (x.height (mbe :logic (sparseint$-height x)
                   :exec x.height))
    ((when (or (eql y 0) (eql y -1)))
     (b* ((cofactor (binary-bitop-cofactor2 op (- y))))
       (mbe :logic
            (b* (((mv shift shift-height)
                  (sparseint$-rightshift-rec offset x x.height))
                 ((mv ext ext-height)
                  (sparseint$-sign-ext width shift shift-height)))
              (sparseint$-unary-bitop cofactor ext ext-height))
            :exec
            (b* (((when (eql cofactor 0))
                  (mv (sparseint$-leaf 0) 0))
                 ((when (eql cofactor 3))
                  (mv (sparseint$-leaf -1) 0))
                 ((mv shift shift-height)
                  (sparseint$-rightshift-rec offset x x.height))
                 ((mv ext ext-height)
                  (sparseint$-sign-ext width shift shift-height)))
              (sparseint$-unary-bitop cofactor ext ext-height))))))
   (sparseint$-case
     x :leaf
     (mv (sparseint$-leaf
              (bignum-logext width
                             (binary-bitop op (logtail offset x.val)
                                           y)))
         0)
     :concat
     (b* ((x.msbs.height
               (mbe :logic (sparseint$-height x.msbs)
                    :exec (- x.height (if x.lsbs-taller 2 1))))
          ((when (<= x.width offset))
           (sparseint$-binary-bitop-int-width
                op width (- offset x.width)
                x.msbs x.msbs.height y))
          (width1 (- x.width offset))
          (x.lsbs.height
               (mbe :logic (sparseint$-height x.lsbs)
                    :exec (- x.height (if x.msbs-taller 2 1))))
          ((when (<= width width1))
           (sparseint$-binary-bitop-int-width
                op width offset x.lsbs x.lsbs.height y))
          ((mv lsbs-and lsbs-and-height)
           (sparseint$-binary-bitop-int-width
                op width1 offset x.lsbs
                x.lsbs.height (bignum-logext width1 y)))
          ((mv msbs-and msbs-and-height)
           (sparseint$-binary-bitop-int-width
                op (- width width1)
                0 x.msbs
                x.msbs.height (logtail width1 y))))
       (sparseint$-concatenate-rebalance
            width1 lsbs-and lsbs-and-height
            msbs-and msbs-and-height))))))

Theorem: sparseint$-p-of-sparseint$-binary-bitop-int-width.binary-res

(defthm sparseint$-p-of-sparseint$-binary-bitop-int-width.binary-res
  (b* (((mv ?binary-res ?height)
        (sparseint$-binary-bitop-int-width
             op width offset x x.height y)))
    (sparseint$-p binary-res))
  :rule-classes :rewrite)

Theorem: return-type-of-sparseint$-binary-bitop-int-width.height

(defthm return-type-of-sparseint$-binary-bitop-int-width.height
  (b* (((mv ?binary-res ?height)
        (sparseint$-binary-bitop-int-width
             op width offset x x.height y)))
    (equal height (sparseint$-height binary-res)))
  :rule-classes :rewrite)

Theorem: sparseint$-height-correctp-of-sparseint$-binary-bitop-int-width

(defthm
    sparseint$-height-correctp-of-sparseint$-binary-bitop-int-width
  (b* (((mv ?binary-res ?height)
        (sparseint$-binary-bitop-int-width
             op width offset x x.height y)))
    (implies (sparseint$-height-correctp x)
             (sparseint$-height-correctp binary-res))))

Theorem: sparseint$-val-of-sparseint$-binary-bitop-int-width

(defthm sparseint$-val-of-sparseint$-binary-bitop-int-width
 (b* (((mv ?binary-res ?height)
       (sparseint$-binary-bitop-int-width
            op width offset x x.height y)))
   (equal
        (sparseint$-val binary-res)
        (logext (pos-fix width)
                (binary-bitop op (logtail offset (sparseint$-val x))
                              y)))))

Theorem: sparseint$-binary-bitop-int-width-of-ifix-op

(defthm sparseint$-binary-bitop-int-width-of-ifix-op
 (equal
  (sparseint$-binary-bitop-int-width (ifix op)
                                     width offset x x.height y)
  (sparseint$-binary-bitop-int-width op width offset x x.height y)))

Theorem: sparseint$-binary-bitop-int-width-int-equiv-congruence-on-op

(defthm sparseint$-binary-bitop-int-width-int-equiv-congruence-on-op
 (implies
  (int-equiv op op-equiv)
  (equal
    (sparseint$-binary-bitop-int-width op width offset x x.height y)
    (sparseint$-binary-bitop-int-width
         op-equiv width offset x x.height y)))
 :rule-classes :congruence)

Theorem: sparseint$-binary-bitop-int-width-of-pos-fix-width

(defthm sparseint$-binary-bitop-int-width-of-pos-fix-width
 (equal
  (sparseint$-binary-bitop-int-width op (pos-fix width)
                                     offset x x.height y)
  (sparseint$-binary-bitop-int-width op width offset x x.height y)))

Theorem: sparseint$-binary-bitop-int-width-pos-equiv-congruence-on-width

(defthm
    sparseint$-binary-bitop-int-width-pos-equiv-congruence-on-width
 (implies
  (pos-equiv width width-equiv)
  (equal
    (sparseint$-binary-bitop-int-width op width offset x x.height y)
    (sparseint$-binary-bitop-int-width
         op width-equiv offset x x.height y)))
 :rule-classes :congruence)

Theorem: sparseint$-binary-bitop-int-width-of-nfix-offset

(defthm sparseint$-binary-bitop-int-width-of-nfix-offset
 (equal
  (sparseint$-binary-bitop-int-width op width (nfix offset)
                                     x x.height y)
  (sparseint$-binary-bitop-int-width op width offset x x.height y)))

Theorem: sparseint$-binary-bitop-int-width-nat-equiv-congruence-on-offset

(defthm
   sparseint$-binary-bitop-int-width-nat-equiv-congruence-on-offset
 (implies
  (nat-equiv offset offset-equiv)
  (equal
    (sparseint$-binary-bitop-int-width op width offset x x.height y)
    (sparseint$-binary-bitop-int-width
         op width offset-equiv x x.height y)))
 :rule-classes :congruence)

Theorem: sparseint$-binary-bitop-int-width-of-sparseint$-fix-x

(defthm sparseint$-binary-bitop-int-width-of-sparseint$-fix-x
 (equal
  (sparseint$-binary-bitop-int-width
       op width offset (sparseint$-fix x)
       x.height y)
  (sparseint$-binary-bitop-int-width op width offset x x.height y)))

Theorem: sparseint$-binary-bitop-int-width-sparseint$-equiv-congruence-on-x

(defthm
 sparseint$-binary-bitop-int-width-sparseint$-equiv-congruence-on-x
 (implies
  (sparseint$-equiv x x-equiv)
  (equal
    (sparseint$-binary-bitop-int-width op width offset x x.height y)
    (sparseint$-binary-bitop-int-width
         op width offset x-equiv x.height y)))
 :rule-classes :congruence)

Theorem: sparseint$-binary-bitop-int-width-of-nfix-x.height

(defthm sparseint$-binary-bitop-int-width-of-nfix-x.height
 (equal
  (sparseint$-binary-bitop-int-width
       op width offset x (nfix x.height)
       y)
  (sparseint$-binary-bitop-int-width op width offset x x.height y)))

Theorem: sparseint$-binary-bitop-int-width-nat-equiv-congruence-on-x.height

(defthm
 sparseint$-binary-bitop-int-width-nat-equiv-congruence-on-x.height
 (implies
  (nat-equiv x.height x.height-equiv)
  (equal
    (sparseint$-binary-bitop-int-width op width offset x x.height y)
    (sparseint$-binary-bitop-int-width
         op width offset x x.height-equiv y)))
 :rule-classes :congruence)

Theorem: sparseint$-binary-bitop-int-width-of-ifix-y

(defthm sparseint$-binary-bitop-int-width-of-ifix-y
 (equal
  (sparseint$-binary-bitop-int-width
       op width offset x x.height (ifix y))
  (sparseint$-binary-bitop-int-width op width offset x x.height y)))

Theorem: sparseint$-binary-bitop-int-width-int-equiv-congruence-on-y

(defthm sparseint$-binary-bitop-int-width-int-equiv-congruence-on-y
 (implies
  (int-equiv y y-equiv)
  (equal
    (sparseint$-binary-bitop-int-width op width offset x x.height y)
    (sparseint$-binary-bitop-int-width
         op width offset x x.height y-equiv)))
 :rule-classes :congruence)