• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• Bitops
• Logbitp

Logbitp-mismatch

(logbitp-mismatch a b) finds the minimal bit-position for which a and b differ, or returns NIL if no such bit exists.

This is mainly useful for proving equal-by-logbitp, but it's also occasionally useful as a witness in other theorems.

Definitions and Theorems

Function: logbitp-mismatch

(defun logbitp-mismatch (a b)
       (declare (xargs :guard (and (integerp a) (integerp b))))
       (cond ((not (equal (logcar a) (logcar b))) 0)
             ((and (zp (integer-length a))
                   (zp (integer-length b)))
              nil)
             (t (let ((tail (logbitp-mismatch (logcdr a)
                                              (logcdr b))))
                     (and tail (+ 1 tail))))))

Theorem: logbitp-mismatch-under-iff

(defthm logbitp-mismatch-under-iff
        (iff (logbitp-mismatch a b)
             (not (equal (ifix a) (ifix b)))))

Theorem: logbitp-mismatch-correct

(defthm logbitp-mismatch-correct
        (implies (logbitp-mismatch a b)
                 (not (equal (logbitp (logbitp-mismatch a b) a)
                             (logbitp (logbitp-mismatch a b) b)))))

Theorem: logbitp-mismatch-upper-bound

(defthm logbitp-mismatch-upper-bound
        (implies (logbitp-mismatch a b)
                 (<= (logbitp-mismatch a b)
                     (max (integer-length a)
                          (integer-length b))))
        :rule-classes ((:rewrite) (:linear)))

Theorem: logbitp-mismatch-upper-bound-for-nonnegatives

(defthm
  logbitp-mismatch-upper-bound-for-nonnegatives
  (implies (and (not (and (integerp a) (< a 0)))
                (not (and (integerp b) (< b 0)))
                (logbitp-mismatch a b))
           (< (logbitp-mismatch a b)
              (max (integer-length a)
                   (integer-length b))))
  :rule-classes ((:rewrite)
                 (:linear :trigger-terms ((logbitp-mismatch a b)))))

Theorem: integerp-of-logbitp-mismatch

(defthm integerp-of-logbitp-mismatch
        (iff (integerp (logbitp-mismatch a b))
             (logbitp-mismatch a b)))