• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
        • Sparseint-impl
          • Sparseint$-binary-bitop-width
          • Sparseint$-plus-width
          • Sparseint$-binary-bitop-offset
          • Sparseint$-binary-bitop-int-width
          • Sparseint$-plus-int-width
          • Sum-with-cin
          • Sparseint$-plus-offset
          • Sparseint$-binary-bitop-int
          • Sparseint$-finalize-concat
          • Sparseint$-plus-int
          • Sparseint$-binary-bittest-width
          • Sparseint$-binary-bittest-int-width
          • Sparseint$-trailing-0-count-width
          • Sparseint$-height
          • Int-to-sparseint$-rec
          • Carry-out
          • Sparseint$-compare-width
          • Sparseint$-binary-bittest-offset
          • Sparseint$-equal-width
          • Sparseint$-binary-bittest-int
          • Sparseint$-compare-int-width
          • Sparseint$-bitcount-width
          • Sparseint$-unary-bittest-width
          • Sparseint$-rightshift-rec
          • Sparseint$-equal-int-width
          • Sparseint$-trailing-0-count-rec
          • Sparseint$-unary-bitop
          • Sparseint$-concatenate
          • Sparseint$-length-width-rec
          • Sparseint$-sign-ext
          • Sparseint$-binary-bitop
          • Binary-bitop
          • Sparseint$-compare-offset
          • Sparseint$-unary-bittest-offset
          • Sparseint$-equal-offset
          • Sparseint$-truncate
          • Sparseint$-mergeable-leaves-p
          • Carry-out-bit
          • Sparseint$-truncate-height
          • Sparseint$-compare-int
          • Sparseint$-binary-bittest
          • Sparseint$-equal-int
          • Sparseint$-rightshift
          • Sparseint$-leaves-mergeable-p
          • Sparseint$-plus
          • Unary-bitop
          • Sparseint$-bitcount-rec
          • Within-1
          • Sparseint$
          • Binary-bitop-cofactor2
          • Binary-bitop-cofactor1
          • Sparseint$-compare
          • Sparseint$-unary-bittest
          • Sparseint$-height-correct-exec
          • Sparseint$-equal
          • Sparseint$-bitnot
          • Sparseint$-unary-minus
          • Sparseint$-bit
          • Int-to-sparseint$
          • Binary-bittest
          • Sparseint$-length-rec
          • Sparseint$-val
          • Binary-bitop-swap
          • Compare
          • Sparseint$-real-height
          • Sparseint$-height-correctp
          • Sparseint$-length
        • Sparseint-p
        • Sparseint-binary-bittest
        • Sparseint-concatenate
        • Sparseint-binary-bitop
        • Sparseint-bitite
        • Sparseint-fix
        • Sparseint$-binary-minus
        • Sparseint-trailing-1-count-from
        • Sparseint-trailing-0-count-from
        • Sparseint-equal
        • Sparseint-test-bitorc2
        • Sparseint-test-bitorc1
        • Sparseint-test-bitnand
        • Sparseint-test-bitandc2
        • Sparseint-test-bitandc1
        • Sparseint-test-bitand
        • Sparseint-rightshift
        • Sparseint-bitcount-from
        • Sparseint-test-bitxor
        • Sparseint-test-bitor
        • Sparseint-test-bitnor
        • Sparseint-test-biteqv
        • Sparseint-compare
        • Sparseint-binary-minus
        • Sparseint-sign-ext
        • Sparseint-plus
        • Sparseint-bitandc2
        • Sparseint-bitandc1
        • Sparseint-bitand
        • Sparseint$-leaf-bitlimit
        • Sparseint-bitxor
        • Sparseint-bitorc2
        • Sparseint-bitorc1
        • Sparseint-bitor
        • Sparseint-bitnor
        • Sparseint-bitnand
        • Sparseint-biteqv
        • Sparseint-ash
        • Sparseint-<
        • Sparseint-bit
        • Sparseint-trailing-1-count
        • Sparseint-trailing-0-count
        • Sparseint-unary-minus
        • Sparseint-length
        • Sparseint-bitnot
        • Sparseint-bitcount
        • Int-to-sparseint
        • Sparseint-val
      • Bitops
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Sparseint-impl

Sparseint$-binary-bitop-int

Signature

(sparseint$-binary-bitop-int op offset x x.height y) 
  → 
(mv binary-res height)

Arguments

op — Guard (integerp op).

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

(defun sparseint$-binary-bitop-int (op offset x x.height y)
 (declare (type (unsigned-byte 4) op))
 (declare (xargs :guard (and (integerp op)
                             (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))
  (declare (ignorable __function__))
  (b*
   ((y (lifix y))
    (offset (lnfix offset))
    (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)))
           (sparseint$-unary-bitop cofactor shift shift-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)))
           (sparseint$-unary-bitop cofactor shift shift-height))))))
   (sparseint$-case
        x :leaf
        (mv (sparseint$-leaf (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 op (- 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))))
             ((mv lsbs-and lsbs-and-height)
              (sparseint$-binary-bitop-int-width
                   op width1 offset x.lsbs
                   x.lsbs.height (bignum-logext width1 y)))
             (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-int
                   op 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.binary-res

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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