• 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

Signed Integer Formats

Signed Integer Formats

Definitions and Theorems

Function: ui

(defun ui (r)
  (declare (xargs :guard t))
  r)

Function: si

(defun si (r n)
  (declare (xargs :guard (and (integerp r) (natp n))))
  (if (= (bitn r (1- n)) 1)
      (- r (expt 2 n))
    r))

Theorem: int-si

(defthm int-si
  (implies (and (integerp r) (natp n))
           (integerp (si r n)))
  :rule-classes (:type-prescription :rewrite))

Theorem: si-bits

(defthm si-bits
  (implies (and (integerp x)
                (natp n)
                (< x (expt 2 (1- n)))
                (>= x (- (expt 2 (1- n)))))
           (= (si (bits x (1- n) 0) n) x))
  :rule-classes nil)

Theorem: bits-si

(defthm bits-si
  (implies (and (integerp n) (< i n))
           (equal (bits (si r n) i j)
                  (bits r i j))))

Theorem: si-shift

(defthm si-shift
  (implies (and (natp n) (natp k) (bvecp r n))
           (equal (si (* (expt 2 k) r) (+ k n))
                  (* (expt 2 k) (si r n)))))

Function: sextend

(defun sextend (m n r)
  (declare (xargs :guard (and (natp m) (natp n) (integerp r))))
  (bits (si r n) (1- m) 0))

Theorem: si-sextend

(defthm si-sextend
  (implies (and (natp n)
                (natp m)
                (<= n m)
                (bvecp r n))
           (equal (si (sextend m n r) m)
                  (si r n))))

Theorem: si-approx

(defthm si-approx
  (implies (and (not (zp n))
                (integerp x)
                (integerp y)
                (< (abs (si (mod x (expt 2 n)) n))
                   (- (expt 2 (1- n)) (abs (- x y)))))
           (equal (- (si (mod x (expt 2 n)) n)
                     (si (mod y (expt 2 n)) n))
                  (- x y))))

Theorem: si-to-fl-mod

(defthm si-to-fl-mod
  (implies (and (rationalp x)
                (integerp m)
                (integerp n)
                (< m n))
           (equal (si x n)
                  (+ (* (expt 2 m)
                        (si (fl (/ x (expt 2 m))) (- n m)))
                     (mod x (expt 2 m))))))

Function: uf

(defun uf (r n m)
  (declare (xargs :guard (and (natp r) (natp n) (natp m))))
  (* (expt 2 (- m n)) (ui r)))

Function: sf

(defun sf (r n m)
  (declare (xargs :guard (and (integerp r) (natp n) (natp m))))
  (* (expt 2 (- m n)) (si r n)))

Theorem: bits-uf

(defthm bits-uf
  (let ((x (uf r n m)) (f (- n m)))
    (implies (and (natp n)
                  (natp m)
                  (<= m n)
                  (bvecp r n)
                  (natp i)
                  (natp j)
                  (<= j i))
             (equal (bits r i j)
                    (* (expt 2 (- f j))
                       (- (chop x (- f j))
                          (chop x (- f (1+ i)))))))))

Theorem: bits-sf

(defthm bits-sf
  (let ((x (sf r n m)) (f (- n m)))
    (implies (and (natp n)
                  (natp m)
                  (<= m n)
                  (bvecp r n)
                  (natp i)
                  (natp j)
                  (<= j i)
                  (< i n))
             (equal (bits r i j)
                    (* (expt 2 (- f j))
                       (- (chop x (- f j))
                          (chop x (- f (1+ i)))))))))

Theorem: chop-uf

(defthm chop-uf
  (let ((x (uf r n m)) (f (- n m)))
    (implies (and (natp n)
                  (natp m)
                  (<= m n)
                  (bvecp r n)
                  (integerp k)
                  (<= (- f n) k)
                  (< k f))
             (iff (= (chop x k) x)
                  (= (bits r (1- (- f k)) 0) 0))))
  :rule-classes nil)

Theorem: chop-sf

(defthm chop-sf
  (let ((x (sf r n m)) (f (- n m)))
    (implies (and (natp n)
                  (natp m)
                  (<= m n)
                  (bvecp r n)
                  (integerp k)
                  (<= (- f n) k)
                  (< k f))
             (iff (= (chop x k) x)
                  (= (bits r (1- (- f k)) 0) 0))))
  :rule-classes nil)

Theorem: sf-val

(defthm sf-val
  (implies (and (natp n)
                (natp m)
                (<= m n)
                (bvecp r n)
                (integerp y)
                (= (mod y (expt 2 n)) r)
                (<= (- (expt 2 (1- n))) y)
                (< y (expt 2 (1- n))))
           (equal (sf r n m)
                  (* (expt 2 (- m n)) y))))