• 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 Extraction

Bit Extraction

Definitions and Theorems

Function: bitn

(defun bitn (x n)
  (declare (xargs :guard (and (integerp x) (integerp n))))
  (mbe :logic (bits x n n)
       :exec (if (evenp (ash x (- n))) 0 1)))

Theorem: bitn-nonnegative-integer

(defthm bitn-nonnegative-integer
  (and (integerp (bitn x n))
       (<= 0 (bitn x n)))
  :rule-classes (:type-prescription))

Theorem: bits-n-n-rewrite

(defthm bits-n-n-rewrite
  (equal (bits x n n) (bitn x n)))

Theorem: bitn-def

(defthm bitn-def
  (implies (case-split (integerp n))
           (equal (bitn x n)
                  (mod (fl (/ x (expt 2 n))) 2))))

Theorem: bitn-rec-0

(defthm bitn-rec-0
  (implies (integerp x)
           (equal (bitn x 0) (mod x 2))))

Theorem: bitn-rec-pos

(defthm bitn-rec-pos
  (implies (< 0 n)
           (equal (bitn x n)
                  (bitn (fl (/ x 2)) (1- n))))
  :rule-classes ((:definition :controller-alist ((bitn t t)))))

Theorem: bitn-0-1

(defthm bitn-0-1
  (or (equal (bitn x n) 0)
      (equal (bitn x n) 1))
  :rule-classes nil)

Theorem: bitn-bvecp

(defthm bitn-bvecp
  (implies (and (<= 1 k) (case-split (integerp k)))
           (bvecp (bitn x n) k)))

Theorem: bitn-bvecp-forward

(defthm bitn-bvecp-forward
  (bvecp (bitn x n) 1)
  :rule-classes ((:forward-chaining :trigger-terms ((bitn x n)))))

Theorem: bitn-neg

(defthm bitn-neg
  (implies (and (< n 0) (integerp x))
           (equal (bitn x n) 0)))

Theorem: bitn-0

(defthm bitn-0 (equal (bitn 0 k) 0))

Theorem: bitn-bvecp-1

(defthm bitn-bvecp-1
  (implies (bvecp x 1)
           (equal (bitn x 0) x)))

Theorem: bitn-bitn-0

(defthm bitn-bitn-0
  (equal (bitn (bitn x n) 0) (bitn x n)))

Theorem: bitn-mod

(defthm bitn-mod
  (implies (and (< k n) (integerp n) (integerp k))
           (equal (bitn (mod x (expt 2 n)) k)
                  (bitn x k))))

Theorem: bvecp-bitn-0

(defthm bvecp-bitn-0
  (implies (bvecp x n)
           (equal (bitn x n) 0)))

Theorem: neg-bitn-1

(defthm neg-bitn-1
  (implies (and (integerp x)
                (integerp n)
                (< x 0)
                (>= x (- (expt 2 n))))
           (equal (bitn x n) 1)))

Theorem: bitn-minus-1

(defthm bitn-minus-1
  (implies (natp i)
           (equal (bitn -1 i) 1)))

Theorem: neg-bitn-2

(defthm neg-bitn-2
  (implies (and (integerp x)
                (integerp n)
                (integerp k)
                (< k n)
                (< x (- (expt 2 k) (expt 2 n)))
                (>= x (- (expt 2 n))))
           (equal (bitn x k) 0)))

Theorem: neg-bitn-0

(defthm neg-bitn-0
  (implies (and (integerp x)
                (natp n)
                (< x (- (expt 2 n)))
                (>= x (- (expt 2 (1+ n)))))
           (equal (bitn x n) 0)))

Theorem: bitn-shift-up

(defthm bitn-shift-up
  (implies (and (integerp n) (integerp k))
           (equal (bitn (* x (expt 2 k)) (+ n k))
                  (bitn x n))))

Theorem: bitn-shift-down

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

Theorem: bitn-bits

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

Theorem: bitn-plus-bits

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

Theorem: bits-plus-bitn

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

Function: sumbits

(defun sumbits (x n)
  (declare (xargs :guard (and (integerp x) (natp n))))
  (if (zp n)
      0
    (+ (* (expt 2 (1- n)) (bitn x (1- n)))
       (sumbits x (1- n)))))

Theorem: sumbits-bits

(defthm sumbits-bits
  (implies (and (integerp x) (natp n) (> n 0))
           (equal (sumbits x n)
                  (bits x (1- n) 0))))

Theorem: sumbits-thm

(defthm sumbits-thm
  (implies (and (bvecp x n) (natp n) (> n 0))
           (equal (sumbits x n) x)))

Function: all-bits-p

(defun all-bits-p (b k)
  (declare (xargs :guard t))
  (if (posp k)
      (and (consp b)
           (all-bits-p (cdr b) (1- k))
           (or (equal (car b) 0)
               (equal (car b) 1)))
    (and (true-listp b) (equal k 0))))

Function: sum-b

(defun sum-b (b k)
  (declare (xargs :guard (all-bits-p b k)))
  (if (zp k)
      0
    (+ (* (expt 2 (1- k)) (nth (1- k) b))
       (sum-b b (1- k)))))

Theorem: sum-bitn

(defthm sum-bitn
  (implies (and (all-bits-p b n) (natp k) (< k n))
           (equal (bitn (sum-b b n) k) (nth k b))))

Function: bit-diff

(defun bit-diff (x y)
  (declare (xargs :guard t))
  (if (or (not (integerp x))
          (not (integerp y))
          (= x y))
      nil
    (if (= (bitn x 0) (bitn y 0))
        (1+ (bit-diff (fl (/ x 2)) (fl (/ y 2))))
      0)))

Theorem: bit-diff-diff

(defthm bit-diff-diff
  (implies (and (integerp x)
                (integerp y)
                (not (= x y)))
           (let ((n (bit-diff x y)))
             (and (natp n)
                  (not (= (bitn x n) (bitn y n))))))
  :rule-classes nil)

Theorem: bvecp-bitn-1

(defthm bvecp-bitn-1
  (implies (and (bvecp x (1+ n))
                (<= (expt 2 n) x)
                (natp n))
           (equal (bitn x n) 1)))

Theorem: bvecp-bitn-2

(defthm bvecp-bitn-2
  (implies (and (bvecp x n)
                (< k n)
                (<= (- (expt 2 n) (expt 2 k)) x)
                (integerp n)
                (integerp k))
           (equal (bitn x k) 1))
  :rule-classes ((:rewrite :match-free :all)))

Theorem: bitn-expt

(defthm bitn-expt
  (implies (case-split (integerp n))
           (equal (bitn (expt 2 n) n) 1)))

Theorem: bitn-expt-0

(defthm bitn-expt-0
  (implies (and (not (equal i n))
                (case-split (integerp i)))
           (equal (bitn (expt 2 i) n) 0)))

Theorem: bitn-plus-expt-1

(defthm bitn-plus-expt-1
  (implies (and (rationalp x) (integerp n))
           (not (equal (bitn (+ x (expt 2 n)) n)
                       (bitn x n))))
  :rule-classes nil)

Theorem: bitn-plus-mult

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

Theorem: bitn-plus-mult-rewrite

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