• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
        • Floating-Point Arithmetic
          • Rounding
          • Floating-Point Formats
          • Floating-Point Numbers
            • Exactness
            • Floating-Point Decomposition
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Floating-Point Numbers

Exactness

Exactness

Definitions and Theorems

Function: exactp

(defun exactp (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (integerp (* (sig x) (expt 2 (1- n)))))

Theorem: exactp2

(defthm exactp2
  (implies (and (rationalp x) (integerp n))
           (equal (exactp x n)
                  (integerp (* x (expt 2 (- (1- n) (expo x))))))))

Theorem: exactp-sig

(defthm exactp-sig
  (equal (exactp (sig x) n) (exactp x n)))

Theorem: minus-exactp

(defthm minus-exactp
  (equal (exactp (- x) n) (exactp x n)))

Theorem: exactp-abs

(defthm exactp-abs
  (equal (exactp (abs x) n) (exactp x n)))

Theorem: exactp-shift

(defthm exactp-shift
  (implies (and (rationalp x)
                (integerp k)
                (integerp n))
           (equal (exactp (* (expt 2 k) x) n)
                  (exactp x n))))

Theorem: exactp-<=

(defthm exactp-<=
  (implies (and (exactp x m)
                (<= m n)
                (rationalp x)
                (integerp n)
                (integerp m))
           (exactp x n)))

Theorem: exactp-2**n

(defthm exactp-2**n
  (implies (and (case-split (integerp m))
                (case-split (> m 0)))
           (exactp (expt 2 n) m)))

Theorem: bvecp-exactp

(defthm bvecp-exactp
  (implies (bvecp x n) (exactp x n)))

Theorem: exactp-prod

(defthm exactp-prod
  (implies (and (rationalp x)
                (rationalp y)
                (integerp m)
                (integerp n)
                (exactp x m)
                (exactp y n))
           (exactp (* x y) (+ m n)))
  :rule-classes nil)

Theorem: exactp-x2

(defthm exactp-x2
  (implies (and (rationalp x)
                (integerp n)
                (exactp (* x x) (* 2 n)))
           (exactp x n))
  :rule-classes nil)

Theorem: exactp-factors

(defthm exactp-factors
  (implies (and (rationalp x)
                (rationalp y)
                (integerp k)
                (integerp n)
                (not (zerop x))
                (not (zerop y))
                (exactp x k)
                (exactp y k)
                (exactp (* x y) n))
           (exactp x n))
  :rule-classes nil)

Theorem: exact-bits-1

(defthm exact-bits-1
  (implies (and (equal (expo x) (1- n))
                (rationalp x)
                (integerp k))
           (equal (integerp (/ x (expt 2 k)))
                  (exactp x (- n k))))
  :rule-classes nil)

Theorem: exact-bits-2

(defthm exact-bits-2
  (implies (and (equal (expo x) (1- n))
                (rationalp x)
                (<= 0 x)
                (integerp k))
           (equal (integerp (/ x (expt 2 k)))
                  (equal (bits x (1- n) k)
                         (/ x (expt 2 k)))))
  :rule-classes nil)

Theorem: exact-bits-3

(defthm exact-bits-3
  (implies (integerp x)
           (equal (integerp (/ x (expt 2 k)))
                  (equal (bits x (1- k) 0) 0)))
  :rule-classes nil)

Theorem: exact-k+1

(defthm exact-k+1
  (implies (and (natp n)
                (natp x)
                (= (expo x) (1- n))
                (natp k)
                (< k (1- n))
                (exactp x (- n k)))
           (iff (exactp x (1- (- n k)))
                (= (bitn x k) 0)))
  :rule-classes nil)

Theorem: exactp-diff

(defthm exactp-diff
  (implies (and (rationalp x)
                (rationalp y)
                (integerp k)
                (integerp n)
                (> n 0)
                (> n k)
                (exactp x n)
                (exactp y n)
                (<= (+ k (expo (- x y))) (expo x))
                (<= (+ k (expo (- x y))) (expo y)))
           (exactp (- x y) (- n k)))
  :rule-classes nil)

Theorem: exactp-diff-cor

(defthm exactp-diff-cor
  (implies (and (rationalp x)
                (rationalp y)
                (integerp n)
                (> n 0)
                (exactp x n)
                (exactp y n)
                (<= (abs (- x y)) (abs x))
                (<= (abs (- x y)) (abs y)))
           (exactp (- x y) n))
  :rule-classes nil)

Function: fp+

(defun fp+ (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (+ x (expt 2 (- (1+ (expo x)) n))))

Theorem: fp+-positive

(defthm fp+-positive
  (implies (<= 0 x) (< 0 (fp+ x n)))
  :rule-classes :type-prescription)

Theorem: fp+1

(defthm fp+1
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0)
                (exactp x n))
           (exactp (fp+ x n) n))
  :rule-classes nil)

Theorem: fp+2

(defthm fp+2
  (implies (and (rationalp x)
                (> x 0)
                (rationalp y)
                (> y x)
                (integerp n)
                (> n 0)
                (exactp x n)
                (exactp y n))
           (>= y (fp+ x n)))
  :rule-classes nil)

Theorem: fp+expo

(defthm fp+expo
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0)
                (exactp x n)
                (not (= (expo (fp+ x n)) (expo x))))
           (equal (fp+ x n)
                  (expt 2 (1+ (expo x)))))
  :rule-classes nil)

Theorem: expo-diff-min

(defthm expo-diff-min
  (implies (and (rationalp x)
                (rationalp y)
                (integerp n)
                (> n 0)
                (exactp x n)
                (exactp y n)
                (not (= y x)))
           (>= (expo (- y x))
               (- (1+ (min (expo x) (expo y))) n)))
  :rule-classes nil)

Function: fp-

(defun fp- (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (if (= x (expt 2 (expo x)))
      (- x (expt 2 (- (expo x) n)))
    (- x (expt 2 (- (1+ (expo x)) n)))))

Theorem: fp--non-negative

(defthm fp--non-negative
  (implies (and (rationalp x)
                (integerp n)
                (> n 0)
                (> x 0))
           (and (rationalp (fp- x n))
                (< 0 (fp- x n))))
  :rule-classes :type-prescription)

Theorem: exactp-fp-

(defthm exactp-fp-
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0)
                (exactp x n))
           (exactp (fp- x n) n)))

Theorem: fp+-

(defthm fp+-
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0)
                (exactp x n))
           (equal (fp+ (fp- x n) n) x)))

Theorem: fp-+

(defthm fp-+
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0)
                (exactp x n))
           (equal (fp- (fp+ x n) n) x)))

Theorem: fp-2

(defthm fp-2
  (implies (and (rationalp x)
                (rationalp y)
                (> y 0)
                (> x y)
                (integerp n)
                (> n 0)
                (exactp x n)
                (exactp y n))
           (<= y (fp- x n)))
  :rule-classes nil)

Theorem: expo-fp-

(defthm expo-fp-
  (implies (and (rationalp x)
                (> x 0)
                (not (= x (expt 2 (expo x))))
                (integerp n)
                (> n 0)
                (exactp x n))
           (equal (expo (fp- x n)) (expo x))))