(sparseint$-binary-bitop-int-width op width offset x x.height y) → (mv binary-res height)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)