		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-binary-bittest-width

Signature
(sparseint$-binary-bittest-width op width x y-offset y) → test
Arguments: op — Guard (integerp op).; width — Guard (posp width).; x — Guard (sparseint$-p x).; y-offset — Guard (natp y-offset).; y — Guard (sparseint$-p y).
Returns: test — Type (booleanp test).

Definitions and Theorems

Function: sparseint$-binary-bittest-width

(defun sparseint$-binary-bittest-width (op width x y-offset y)
 (declare (type (unsigned-byte 4) op))
 (declare (xargs :guard (and (integerp op)
                             (posp width)
                             (sparseint$-p x)
                             (natp y-offset)
                             (sparseint$-p y))))
 (let ((__function__ 'sparseint$-binary-bittest-width))
  (declare (ignorable __function__))
  (b* ((width (lposfix width))
       (y-offset (lnfix y-offset)))
   (sparseint$-case
    x
    :leaf
    (sparseint$-case
     y
     :leaf
     (binary-bittest op (bignum-logext width x.val)
                     (bignum-logext width (logtail y-offset y.val)))
     :concat (sparseint$-binary-bittest-int-width
                  (binary-bitop-swap op)
                  width
                  y-offset y (bignum-logext width x.val)))
    :concat
    (sparseint$-case
     y :leaf
     (sparseint$-binary-bittest-int-width
          op width 0 x
          (bignum-logext width (logtail y-offset y.val)))
     :concat
     (b* (((when (<= width x.width))
           (sparseint$-binary-bittest-width
                op width x.lsbs y-offset y))
          ((when (<= y.width y-offset))
           (sparseint$-binary-bittest-width
                op width x (- y-offset y.width)
                y.msbs))
          (y-width1 (- y.width y-offset))
          ((when (<= width y-width1))
           (sparseint$-binary-bittest-width
                op width x y-offset y.lsbs)))
      (or
        (sparseint$-binary-bittest-width
             op x.width x.lsbs y-offset y)
        (sparseint$-binary-bittest-width op (- width x.width)
                                         x.msbs (+ x.width y-offset)
                                         y))))))))

Theorem: booleanp-of-sparseint$-binary-bittest-width

(defthm booleanp-of-sparseint$-binary-bittest-width
  (b*
    ((test (sparseint$-binary-bittest-width op width x y-offset y)))
    (booleanp test))
  :rule-classes :type-prescription)

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

(defthm sparseint$-val-of-sparseint$-binary-bittest-width
  (b*
   ((?test (sparseint$-binary-bittest-width op width x y-offset y)))
   (equal test
          (binary-bittest
               op (logext width (sparseint$-val x))
               (logext width
                       (logtail y-offset (sparseint$-val y)))))))

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

(defthm sparseint$-binary-bittest-width-of-ifix-op
  (equal (sparseint$-binary-bittest-width (ifix op)
                                          width x y-offset y)
         (sparseint$-binary-bittest-width op width x y-offset y)))

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

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

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

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

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

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

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

(defthm sparseint$-binary-bittest-width-of-sparseint$-fix-x
 (equal (sparseint$-binary-bittest-width op width (sparseint$-fix x)
                                         y-offset y)
        (sparseint$-binary-bittest-width op width x y-offset y)))

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

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

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

(defthm sparseint$-binary-bittest-width-of-nfix-y-offset
  (equal (sparseint$-binary-bittest-width op width x (nfix y-offset)
                                          y)
         (sparseint$-binary-bittest-width op width x y-offset y)))

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

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

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

(defthm sparseint$-binary-bittest-width-of-sparseint$-fix-y
  (equal (sparseint$-binary-bittest-width
              op width x y-offset (sparseint$-fix y))
         (sparseint$-binary-bittest-width op width x y-offset y)))

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

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