		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-binary-bitop-width

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

Definitions and Theorems

Function: sparseint$-binary-bitop-width

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: sparseint$-binary-bitop-width-of-sparseint$-fix-y

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

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

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

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

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

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

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