• 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

Concatenation

Concatenation

Definitions and Theorems

Function: binary-cat

(defun binary-cat (x m y n)
  (declare (xargs :guard (and (integerp x)
                              (integerp y)
                              (natp m)
                              (natp n))))
  (if (and (natp m) (natp n))
      (+ (* (expt 2 n) (bits x (1- m) 0))
         (bits y (1- n) 0))
    0))

Function: formal-+

(defun formal-+ (x y)
  (declare (xargs :guard t))
  (if (and (acl2-numberp x) (acl2-numberp y))
      (+ x y)
    (list '+ x y)))

Function: cat-size

(defun cat-size (x)
  (declare (xargs :guard (and (true-listp x)
                              (evenp (length x)))))
  (if (endp (cddr x))
      (cadr x)
    (formal-+ (cadr x)
              (cat-size (cddr x)))))

Macro: cat

(defmacro cat (&rest x)
 (declare (xargs :guard (and x (true-listp x)
                             (evenp (length x)))))
 (cond
   ((endp (cddr x))
    (cons 'bits
          (cons (car x)
                (cons (formal-+ -1 (cadr x)) '(0)))))
   ((endp (cddddr x)) (cons 'binary-cat x))
   (t (cons 'binary-cat
            (cons (car x)
                  (cons (cadr x)
                        (cons (cons 'cat (cddr x))
                              (cons (cat-size (cddr x)) 'nil))))))))

Theorem: cat-nonnegative-integer-type

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

Theorem: cat-bvecp

(defthm cat-bvecp
  (implies (and (<= (+ m n) k)
                (case-split (integerp k)))
           (bvecp (cat x m y n) k)))

Theorem: cat-with-n-0

(defthm cat-with-n-0
  (equal (binary-cat x m y 0)
         (bits x (1- m) 0)))

Theorem: cat-with-m-0

(defthm cat-with-m-0
  (equal (binary-cat x 0 y n)
         (bits y (1- n) 0)))

Theorem: cat-0

(defthm cat-0
  (implies (and (case-split (bvecp y n))
                (case-split (integerp n))
                (case-split (integerp m))
                (case-split (<= 0 m)))
           (equal (cat 0 m y n) y)))

Theorem: cat-bits-1

(defthm cat-bits-1
  (equal (cat (bits x (1- m) 0) m y n)
         (cat x m y n)))

Theorem: cat-bits-2

(defthm cat-bits-2
  (equal (cat x m (bits y (1- n) 0) n)
         (cat x m y n)))

Theorem: cat-bits-3

(defthm cat-bits-3
  (implies (and (integerp i)
                (integerp m)
                (>= i (1- m)))
           (equal (cat (bits x i 0) m y n)
                  (cat x m y n))))

Theorem: cat-bits-4

(defthm cat-bits-4
  (implies (and (integerp i)
                (integerp n)
                (>= i (1- n)))
           (equal (cat x m (bits y i 0) n)
                  (cat x m y n))))

Theorem: cat-associative

(defthm cat-associative
  (implies (and (case-split (<= (+ m n) p))
                (case-split (<= 0 m))
                (case-split (<= 0 n))
                (case-split (<= 0 q))
                (case-split (integerp m))
                (case-split (integerp n))
                (case-split (integerp p))
                (case-split (integerp q)))
           (equal (cat (cat x m y n) p z q)
                  (cat x m (cat y n z q) (+ n q)))))

Theorem: cat-equal-constant

(defthm cat-equal-constant
  (implies (and (syntaxp (and (quotep k) (quotep m) (quotep n)))
                (case-split (bvecp y n))
                (case-split (bvecp x m))
                (case-split (< k (expt 2 (+ m n))))
                (case-split (integerp k))
                (case-split (<= 0 k))
                (case-split (integerp m))
                (case-split (<= 0 m))
                (case-split (integerp n))
                (case-split (<= 0 n)))
           (equal (equal k (cat x m y n))
                  (and (equal y (bits k (1- n) 0))
                       (equal x (bits k (+ -1 m n) n))))))

Theorem: cat-equal-rewrite

(defthm cat-equal-rewrite
  (implies (and (case-split (bvecp x1 m))
                (case-split (bvecp y1 n))
                (case-split (bvecp x2 m))
                (case-split (bvecp y2 n))
                (case-split (integerp n))
                (case-split (<= 0 n))
                (case-split (integerp m))
                (case-split (<= 0 m)))
           (equal (equal (cat x1 m y1 n) (cat x2 m y2 n))
                  (and (equal x1 x2) (equal y1 y2)))))

Theorem: cat-bits-bits

(defthm cat-bits-bits
  (implies (and (equal j (1+ k))
                (equal n (+ 1 (- l) k))
                (case-split (<= (+ 1 (- j) i) m))
                (case-split (<= j i))
                (case-split (<= l k))
                (case-split (integerp i))
                (case-split (integerp k))
                (case-split (integerp l))
                (case-split (integerp m)))
           (equal (cat (bits x i j) m (bits x k l) n)
                  (bits x i l))))

Theorem: cat-bitn-bits

(defthm cat-bitn-bits
  (implies (and (equal j (1+ k))
                (equal n (+ 1 (- l) k))
                (case-split (<= 1 m))
                (case-split (<= l k))
                (case-split (integerp j))
                (case-split (integerp k))
                (case-split (integerp l))
                (case-split (integerp m)))
           (equal (cat (bitn x j) m (bits x k l) n)
                  (bits x j l))))

Theorem: cat-bits-bitn

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

Theorem: cat-bitn-bitn

(defthm cat-bitn-bitn
  (implies (and (equal i (1+ j))
                (case-split (integerp i))
                (case-split (integerp j)))
           (equal (cat (bitn x i) 1 (bitn x j) 1)
                  (bits x i j))))

Theorem: bits-cat

(defthm bits-cat
  (implies (and (case-split (natp n))
                (case-split (natp m))
                (case-split (natp i))
                (case-split (natp j)))
           (equal (bits (cat x m y n) i j)
                  (if (< i n)
                      (bits y i j)
                    (if (>= j n)
                        (bits x (if (< i (+ m n)) (- i n) (1- m))
                              (- j n))
                      (cat (bits x (if (< i (+ m n)) (- i n) (1- m))
                                 0)
                           (1+ (- i n))
                           (bits y (1- n) j)
                           (- n j)))))))

Theorem: bits-cat-constants

(defthm bits-cat-constants
  (implies (and (syntaxp (quotep n))
                (syntaxp (quotep m))
                (syntaxp (quotep i))
                (syntaxp (quotep j))
                (natp n)
                (natp m)
                (natp i)
                (natp j))
           (equal (bits (cat x m y n) i j)
                  (if (< i n)
                      (bits y i j)
                    (if (>= j n)
                        (bits x (if (< i (+ m n)) (- i n) (1- m))
                              (- j n))
                      (cat (bits x (if (< i (+ m n)) (- i n) (1- m))
                                 0)
                           (1+ (- i n))
                           (bits y (1- n) j)
                           (- n j)))))))

Theorem: bitn-cat

(defthm bitn-cat
  (implies (and (case-split (natp n))
                (case-split (natp m))
                (case-split (natp i)))
           (equal (bitn (cat x m y n) i)
                  (if (< i n)
                      (bitn y i)
                    (if (< i (+ m n))
                        (bitn x (- i n))
                      0)))))

Theorem: bitn-cat-constants

(defthm bitn-cat-constants
  (implies (and (syntaxp (quotep n))
                (syntaxp (quotep m))
                (syntaxp (quotep i))
                (natp n)
                (natp m)
                (natp i))
           (equal (bitn (cat x m y n) i)
                  (if (< i n)
                      (bitn y i)
                    (if (< i (+ m n))
                        (bitn x (- i n))
                      0)))))

Function: mulcat

(defun mulcat (l n x)
  (declare (xargs :guard (and (natp l) (natp n) (natp x))))
  (if (and (integerp n) (> n 0))
      (cat (mulcat l (1- n) x)
           (* l (1- n))
           x l)
    0))

Theorem: mulcat-nonnegative-integer-type

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

Theorem: mulcat-bits

(defthm mulcat-bits
  (implies (and (integerp l) (integerp x))
           (equal (mulcat l n (bits x (1- l) 0))
                  (mulcat l n x))))

Theorem: mulcat-bvecp

(defthm mulcat-bvecp
  (implies (and (>= p (* l n))
                (case-split (integerp p))
                (case-split (natp l)))
           (bvecp (mulcat l n x) p)))

Theorem: mulcat-1

(defthm mulcat-1
  (implies (natp l)
           (equal (mulcat l 1 x)
                  (bits x (1- l) 0))))

Theorem: mulcat-0

(defthm mulcat-0
  (equal (mulcat l n 0) 0))

Theorem: mulcat-n-1

(defthm mulcat-n-1
  (implies (case-split (<= 0 n))
           (equal (mulcat 1 n 1) (1- (expt 2 n)))))

Theorem: bitn-mulcat-1

(defthm bitn-mulcat-1
  (implies (and (< m n)
                (case-split (bvecp x 1))
                (case-split (natp m))
                (case-split (integerp n)))
           (equal (bitn (mulcat 1 n x) m) x)))