• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
        • Bitset-members
        • Bitset-insert
        • Bitset-delete
        • Bitset-intersectp
        • Bitset-intersect
        • Bitset-difference
        • Bitset-subsetp
        • Bitset-union
        • Bitset-memberp
        • Bitset-singleton
        • Bitset-list
        • Bitset-cardinality
        • Bitset-list*
        • Utilities
          • Bits-between
          • Bits-0-31
          • 60bits-0-59
          • Add-to-each
          • Bits-0-7
          • 60bits-0-7
          • 60bits-0-3
      • Sbitsets
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Utilities

Bits-between

(bits-between n m x) returns a proper, ordered set of all i in [n, m) such that (logbitp i x).

Signature

(bits-between n m x) → set-of-bits

Arguments

n — lower bound, inclusive.
    Guard (natp n).

m — upper bound, exclusive.
    Guard (natp m).

x — integer to extract bits from.
    Guard (integerp x).

This is a key function in the definition of bitset-members.

Definitions and Theorems

Function: bits-between

(defun bits-between (n m x)
  (declare (xargs :guard (and (natp n) (natp m) (integerp x))))
  (declare (xargs :guard (<= n m)))
  (let ((__function__ 'bits-between))
    (declare (ignorable __function__))
    (let* ((n (lnfix n)) (m (lnfix m)))
      (cond ((mbe :logic (zp (- m n)) :exec (= m n))
             nil)
            ((logbitp n x)
             (cons n (bits-between (+ n 1) m x)))
            (t (bits-between (+ n 1) m x))))))

Theorem: true-listp-of-bits-between

(defthm true-listp-of-bits-between
  (true-listp (bits-between n m x))
  :rule-classes :type-prescription)

Theorem: integer-listp-of-bits-between

(defthm integer-listp-of-bits-between
  (integer-listp (bits-between n m x)))

Theorem: nat-listp-of-bits-between

(defthm nat-listp-of-bits-between
  (nat-listp (bits-between n m x)))

Theorem: bits-between-when-not-integer

(defthm bits-between-when-not-integer
  (implies (not (integerp x))
           (equal (bits-between n m x) nil)))

Theorem: member-equal-of-bits-between

(defthm member-equal-of-bits-between
  (iff (member-equal a (bits-between n m x))
       (and (natp a)
            (<= (nfix n) a)
            (< a (nfix m))
            (logbitp a x))))

Theorem: no-duplicatesp-equal-of-bits-between

(defthm no-duplicatesp-equal-of-bits-between
  (no-duplicatesp-equal (bits-between n m x)))

Theorem: bits-between-of-increment-right-index

(defthm bits-between-of-increment-right-index
  (implies (and (force (natp n))
                (force (natp m))
                (force (<= n m)))
           (equal (bits-between n (+ 1 m) x)
                  (if (logbitp m x)
                      (append (bits-between n m x) (list m))
                    (bits-between n m x)))))

Theorem: merge-appended-bits-between

(defthm merge-appended-bits-between
  (implies (and (natp n)
                (natp m)
                (natp k)
                (<= n m)
                (<= m k))
           (equal (append (bits-between n m x)
                          (bits-between m k x))
                  (bits-between n k x))))

Theorem: bits-between-of-right-shift

(defthm bits-between-of-right-shift
 (implies (and (natp n)
               (natp m)
               (<= n m)
               (integerp k)
               (< k 0))
          (equal (bits-between n m (ash x k))
                 (add-to-each k (bits-between (- n k) (- m k) x)))))

Theorem: bits-between-of-mod-2^n

(defthm bits-between-of-mod-2^n
  (implies (and (integerp x) (natp k) (<= m k))
           (equal (bits-between n m (mod x (expt 2 k)))
                  (bits-between n m x))))

Theorem: bits-between-of-mod-2^32

(defthm bits-between-of-mod-2^32
  (implies (and (integerp x) (<= m 32))
           (equal (bits-between n m (mod x 4294967296))
                  (bits-between n m x))))

Theorem: bits-between-upper

(defthm bits-between-upper
 (implies
   (and (syntaxp (not (equal m
                             (cons 'integer-length (cons x 'nil)))))
        (natp n)
        (natp m)
        (natp x)
        (<= (integer-length x) m))
   (equal (bits-between n m x)
          (bits-between n (integer-length x) x))))

Theorem: setp-of-bits-between

(defthm setp-of-bits-between
  (setp (bits-between n m x)))

Theorem: in-of-bits-between

(defthm in-of-bits-between
  (equal (in a (bits-between n m x))
         (and (natp a)
              (<= (nfix n) a)
              (< a (nfix m))
              (logbitp a x))))