• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
• Integer-length

Bitops/integer-length

Basic theorems about integer-length.

Definitions and Theorems

Theorem: integer-length-type-prescription-strong

(defthm integer-length-type-prescription-strong
        (implies (and (integerp n) (< 0 n))
                 (and (integerp (integer-length n))
                      (< 0 (integer-length n))))
        :rule-classes :type-prescription)

Theorem: integer-length-type-prescription-strong-negative

(defthm integer-length-type-prescription-strong-negative
        (implies (and (integerp n) (< n -1))
                 (and (integerp (integer-length n))
                      (< 0 (integer-length n))))
        :rule-classes :type-prescription)

Theorem: integer-length-expt-upper-bound-n

(defthm integer-length-expt-upper-bound-n
        (implies (integerp n)
                 (< n (expt 2 (integer-length n))))
        :rule-classes :linear)

Theorem: integer-length-expt-upper-bound-n-1

(defthm integer-length-expt-upper-bound-n-1
        (implies (integerp n)
                 (<= n (expt 2 (integer-length (1- n)))))
        :rule-classes :linear)

Theorem: integer-length-monotonic

(defthm integer-length-monotonic
        (implies (and (<= i j) (natp i) (natp j))
                 (<= (integer-length i)
                     (integer-length j)))
        :rule-classes :linear)

Theorem: integer-length-less

(defthm integer-length-less
        (implies (natp n)
                 (<= (integer-length n) n))
        :rule-classes :linear)

Theorem: (integer-length (expt 2 n))

(defthm |(integer-length (expt 2 n))|
        (implies (natp n)
                 (equal (integer-length (expt 2 n))
                        (+ 1 n))))

Theorem: (integer-length (1- (expt 2 n)))

(defthm |(integer-length (1- (expt 2 n)))|
        (implies (natp n)
                 (equal (integer-length (+ -1 (expt 2 n)))
                        n)))

Theorem: (integer-length (floor n 2))

(defthm |(integer-length (floor n 2))|
        (implies (natp n)
                 (equal (integer-length (floor n 2))
                        (if (zp n)
                            0 (- (integer-length n) 1)))))

Theorem: 2^{(integer-length n) - 1} <= n

(defthm |2^{(integer-length n) - 1} <= n|
        (implies (posp n)
                 (<= (expt 2 (1- (integer-length n))) n))
        :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-of-logcdr-strong

(defthm integer-length-of-logcdr-strong
        (implies (posp (integer-length a))
                 (< (integer-length (logcdr a))
                    (integer-length a)))
        :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-of-logcdr-weak

(defthm integer-length-of-logcdr-weak
        (<= (integer-length (logcdr a))
            (integer-length a))
        :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-bounded-by-expt

(defthm
 integer-length-bounded-by-expt
 (implies (and (< a (expt 2 n)) (natp a) (natp n))
          (< (integer-length a) (+ 1 n)))
 :rule-classes
 ((:rewrite
     :corollary
     (implies (and (syntaxp (or (not (quotep n)) (< (cadr n) 1000)))
                   (< a (expt 2 n))
                   (natp a)
                   (natp n))
              (< (integer-length a) (+ 1 n))))
  (:linear)))

Theorem: (integer-length (mod a (expt 2 n)))

(defthm |(integer-length (mod a (expt 2 n)))|
        (implies (and (natp a) (natp n))
                 (< (integer-length (mod a (expt 2 n)))
                    (+ 1 n)))
        :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-expt-lower-bound

(defthm integer-length-expt-lower-bound
        (implies (posp n)
                 (<= (expt 2 (+ -1 (integer-length n)))
                     n))
        :rule-classes :linear)

Theorem: integer-length-when-less-than-exp

(defthm integer-length-when-less-than-exp
        (implies (and (< x (expt 2 y)) (natp x) (natp y))
                 (<= (integer-length x) y))
        :rule-classes :linear)

Theorem: integer-length-when-greater-than-exp

(defthm integer-length-when-greater-than-exp
        (implies (and (<= (expt 2 y) x)
                      (natp x)
                      (integerp y))
                 (< y (integer-length x)))
        :rule-classes :linear)

Theorem: integer-length-unique

(defthm integer-length-unique
        (implies (and (<= (expt 2 (1- y)) x)
                      (< x (expt 2 y))
                      (posp x)
                      (posp y))
                 (equal (integer-length x) y)))