• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
      • Rtl
        • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
        • Implementation of Elementary Operations
        • Register-Transfer Logic
          • Bit Vectors
            • Bit Slices
            • Concatenation
            • Bit Extraction
            • Signed Integer Formats
            • Recognizing Bit Vectors
          • Logical Operations
          • Basic Arithmetic Functions
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Bit Vectors

Bit Slices

Bit Slices

Definitions and Theorems

Function: bits

(defun bits (x i j)
  (declare (xargs :guard (and (integerp x)
                              (integerp i)
                              (integerp j))))
  (mbe :logic
       (if (or (not (integerp i))
               (not (integerp j)))
           0
         (fl (/ (mod x (expt 2 (1+ i))) (expt 2 j))))
       :exec
       (if (< i j)
           0
         (logand (ash x (- j))
                 (1- (ash 1 (1+ (- i j))))))))

Theorem: bits-nonnegative-integerp-type

(defthm bits-nonnegative-integerp-type
  (and (<= 0 (bits x i j))
       (integerp (bits x i j)))
  :rule-classes (:type-prescription))

Theorem: bits-bvecp

(defthm bits-bvecp
  (implies (and (<= (+ 1 i (- j)) k)
                (case-split (integerp k)))
           (bvecp (bits x i j) k)))

Theorem: bits-bvecp-simple

(defthm bits-bvecp-simple
  (implies (equal k (+ 1 i (* -1 j)))
           (bvecp (bits x i j) k)))

Theorem: bits-bounds

(defthm bits-bounds
  (implies (and (integerp i) (integerp j))
           (and (natp (bits x i j))
                (< (bits x i j) (expt 2 (1+ (- i j))))))
  :rule-classes nil)

Theorem: bits-upper-bound

(defthm bits-upper-bound
  (implies (and (integerp i) (integerp j))
           (< (bits x i j) (expt 2 (1+ (- i j)))))
  :rule-classes :linear)

Theorem: mod-bits-equal

(defthm mod-bits-equal
  (implies (= (mod x (expt 2 (1+ i)))
              (mod y (expt 2 (1+ i))))
           (= (bits x i j) (bits y i j)))
  :rule-classes nil)

Theorem: mod-bits-equal-cor

(defthm mod-bits-equal-cor
  (implies (and (integerp x)
                (integerp n)
                (integerp i)
                (integerp j)
                (< i n))
           (equal (bits (mod x (expt 2 n)) i j)
                  (bits x i j))))

Theorem: bits-mod

(defthm bits-mod
  (implies (and (case-split (integerp x))
                (case-split (integerp i)))
           (equal (bits x i 0)
                  (mod x (expt 2 (1+ i))))))

Theorem: bits-diff-equal

(defthm bits-diff-equal
  (implies (and (natp n)
                (integerp x)
                (integerp y)
                (< (abs (- x y)) (expt 2 n)))
           (iff (= x y)
                (= (bits (- x y) (1- n) 0) 0)))
  :rule-classes nil)

Theorem: bits-tail

(defthm bits-tail
  (implies (and (bvecp x (1+ i))
                (case-split (acl2-numberp i)))
           (equal (bits x i 0) x)))

Theorem: bits-tail-gen

(defthm bits-tail-gen
  (implies (and (integerp x)
                (natp i)
                (< x (expt 2 i))
                (>= x (- (expt 2 (+ 1 i)))))
           (equal (bits x i 0)
                  (if (>= x 0)
                      x
                    (+ x (expt 2 (+ 1 i)))))))

Theorem: neg-bits-1

(defthm neg-bits-1
  (implies (and (integerp x)
                (natp i)
                (natp j)
                (< x 0)
                (>= x (- (expt 2 j)))
                (>= i j))
           (equal (bits x i j)
                  (1- (expt 2 (1+ (- i j)))))))

Theorem: bits-top-ones

(defthm bits-top-ones
  (implies (and (natp i)
                (natp j)
                (>= i j)
                (natp x)
                (< x (expt 2 (1+ i)))
                (>= x (- (expt 2 (1+ i)) (expt 2 j))))
           (equal (bits x i j)
                  (1- (expt 2 (- (1+ i) j))))))

Theorem: bits-bits-sum

(defthm bits-bits-sum
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j)
                (integerp k)
                (>= j 0)
                (>= k i))
           (equal (bits (+ (bits x k 0) y) i j)
                  (bits (+ x y) i j))))

Theorem: bits-bits-sum-alt

(defthm bits-bits-sum-alt
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j)
                (integerp k)
                (>= j 0)
                (>= k i))
           (equal (bits (+ x (bits y k 0)) i j)
                  (bits (+ x y) i j))))

Theorem: bits-bits-diff

(defthm bits-bits-diff
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j)
                (integerp k)
                (>= j 0)
                (>= k i))
           (equal (bits (+ x (- (bits y k 0))) i j)
                  (bits (- x y) i j))))

Theorem: bits-bits-prod

(defthm bits-bits-prod
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j)
                (integerp k)
                (>= j 0)
                (>= k i))
           (equal (bits (* x (bits y k 0)) i j)
                  (bits (* x y) i j))))

Theorem: bits-fl-diff

(defthm bits-fl-diff
  (implies (and (integerp x)
                (integerp i)
                (integerp j)
                (>= i j))
           (equal (bits x (1- i) j)
                  (- (fl (/ x (expt 2 j)))
                     (* (expt 2 (- i j))
                        (fl (/ x (expt 2 i)))))))
  :rule-classes nil)

Theorem: bits-fl-diff-alt

(defthm bits-fl-diff-alt
  (implies (and (integerp x)
                (integerp i)
                (integerp j)
                (>= i (1- j)))
           (equal (bits x i j)
                  (- (fl (/ x (expt 2 j)))
                     (* (expt 2 (- (1+ i) j))
                        (fl (/ x (expt 2 (1+ i)))))))))

Theorem: bits-mod-fl

(defthm bits-mod-fl
  (implies (and (integerp i) (integerp j))
           (equal (bits x (1- i) j)
                  (mod (fl (/ x (expt 2 j)))
                       (expt 2 (- i j)))))
  :rule-classes nil)

Theorem: bits-neg-indices

(defthm bits-neg-indices
  (implies (and (< i 0) (integerp x))
           (equal (bits x i j) 0)))

Theorem: bits-reverse-indices

(defthm bits-reverse-indices
  (implies (< i j)
           (equal (bits x i j) 0)))

Theorem: bvecp-bits-0

(defthm bvecp-bits-0
  (implies (bvecp x j)
           (equal (bits x i j) 0)))

Theorem: bits-0

(defthm bits-0 (equal (bits 0 i j) 0))

Theorem: bits-shift-down-1

(defthm bits-shift-down-1
  (implies (and (<= 0 j)
                (integerp i)
                (integerp j)
                (integerp k))
           (equal (bits (fl (/ x (expt 2 k))) i j)
                  (bits x (+ i k) (+ j k)))))

Theorem: bits-shift-down-2

(defthm bits-shift-down-2
  (implies (and (integerp x) (natp i) (natp k))
           (equal (fl (/ (bits x (+ i k) 0) (expt 2 k)))
                  (bits (fl (/ x (expt 2 k))) i 0))))

Theorem: bits-shift-up-1

(defthm bits-shift-up-1
  (implies (and (integerp k)
                (integerp i)
                (integerp j))
           (equal (bits (* (expt 2 k) x) i j)
                  (bits x (- i k) (- j k)))))

Theorem: bits-shift-up-2

(defthm bits-shift-up-2
  (implies (and (integerp x) (natp k) (integerp i))
           (equal (* (expt 2 k) (bits x i 0))
                  (bits (* (expt 2 k) x) (+ i k) 0))))

Theorem: bits-plus-mult-1

(defthm bits-plus-mult-1
  (implies (and (bvecp x k)
                (<= k m)
                (integerp y)
                (case-split (integerp m))
                (case-split (integerp n))
                (case-split (integerp k)))
           (equal (bits (+ x (* y (expt 2 k))) n m)
                  (bits y (- n k) (- m k)))))

Theorem: bits-plus-mult-2

(defthm bits-plus-mult-2
  (implies (and (< n k) (integerp y) (integerp k))
           (equal (bits (+ x (* y (expt 2 k))) n m)
                  (bits x n m))))

Theorem: bits-plus-mult-2-rewrite

(defthm bits-plus-mult-2-rewrite
  (implies (and (syntaxp (quotep c))
                (equal (mod c (expt 2 (1+ n))) 0))
           (equal (bits (+ c x) n m)
                  (bits x n m))))

Theorem: bits-plus-bits

(defthm bits-plus-bits
  (implies (and (integerp m)
                (integerp p)
                (integerp n)
                (<= m p)
                (<= p n))
           (= (bits x n m)
              (+ (bits x (1- p) m)
                 (* (expt 2 (- p m)) (bits x n p)))))
  :rule-classes nil)

Theorem: bits-bits

(defthm bits-bits
  (implies (and (case-split (<= 0 l))
                (case-split (integerp i))
                (case-split (integerp j))
                (case-split (integerp k))
                (case-split (integerp l)))
           (equal (bits (bits x i j) k l)
                  (if (<= k (- i j))
                      (bits x (+ k j) (+ l j))
                    (bits x i (+ l j))))))

Theorem: bits-match

(defthm bits-match
  (implies (and (syntaxp (and (quotep i) (quotep j) (quotep k)))
                (equal (bits x i2 j2) k2)
                (syntaxp (and (quotep i2)
                              (quotep j2)
                              (quotep k2)))
                (<= j2 j)
                (<= j i)
                (<= i i2)
                (equal k (bits k2 (+ i (- j2)) (+ (- j2) j)))
                (<= 0 i)
                (<= 0 j)
                (<= 0 k)
                (<= 0 i2)
                (<= 0 j2)
                (<= 0 k2)
                (integerp i)
                (integerp j)
                (integerp k)
                (integerp i2)
                (integerp j2)
                (integerp k2))
           (equal (equal k (bits x i j)) t)))

Theorem: bits-dont-match

(defthm bits-dont-match
  (implies (and (syntaxp (and (quotep i) (quotep j) (quotep k)))
                (equal (bits x i2 j2) k2)
                (syntaxp (and (quotep i2)
                              (quotep j2)
                              (quotep k2)))
                (<= j2 j)
                (<= j i)
                (<= i i2)
                (not (equal k (bits k2 (+ i (- j2)) (+ (- j2) j))))
                (<= 0 i)
                (<= 0 j)
                (<= 0 k)
                (<= 0 i2)
                (<= 0 j2)
                (<= 0 k2)
                (integerp i)
                (integerp j)
                (integerp k)
                (integerp i2)
                (integerp j2)
                (integerp k2))
           (equal (equal k (bits x i j)) nil)))