• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • 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-offset

    Signature
    (sparseint$-binary-bitop-offset op x x.height y-offset y y.height) 
      → 
    (mv binary-res height)
    Arguments
    op — Guard (integerp op).
    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-offset

    (defun sparseint$-binary-bitop-offset
           (op x x.height y-offset y y.height)
     (declare (type (unsigned-byte 4) op))
     (declare (xargs :guard (and (integerp op)
                                 (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-offset))
      (declare (ignorable __function__))
      (b* ((x.height (mbe :logic (sparseint$-height x)
                          :exec x.height))
           (y.height (mbe :logic (sparseint$-height y)
                          :exec y.height))
           (y-offset (lnfix y-offset)))
       (sparseint$-case
         x
         :leaf
         (sparseint$-case
              y
              :leaf
              (mv (sparseint$-leaf
                       (binary-bitop op x.val (logtail y-offset y.val)))
                  0)
              :concat
              (sparseint$-binary-bitop-int (binary-bitop-swap op)
                                           y-offset y y.height x.val))
         :concat
         (sparseint$-case
              y :leaf
              (sparseint$-binary-bitop-int
                   op
                   0 x x.height (logtail y-offset y.val))
              :concat
              (b* ((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-offset
                         op x x.height (- y-offset y.width)
                         y.msbs y.msbs.height))
                   (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-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-offset
                         op 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-offset.binary-res

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

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

    (defthm return-type-of-sparseint$-binary-bitop-offset.height
      (b* (((mv ?binary-res ?height)
            (sparseint$-binary-bitop-offset
                 op 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-offset

    (defthm sparseint$-height-correctp-of-sparseint$-binary-bitop-offset
      (b* (((mv ?binary-res ?height)
            (sparseint$-binary-bitop-offset
                 op 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-offset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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