• 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
        • Floating-Point Arithmetic
          • Rounding
            • Unbiased Rounding
            • IEEE Rounding
            • Denormal Rounding
            • Rounding Away from Zero
            • Truncation
            • Odd Rounding
          • Floating-Point Formats
          • Floating-Point Numbers
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Rounding

Rounding Away from Zero

Rounding Away from Zero

Definitions and Theorems

Function: raz

(defun raz (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (* (sgn x)
     (cg (* (expt 2 (1- n)) (sig x)))
     (expt 2 (- (1+ (expo x)) n))))

Theorem: raz-rewrite

(defthm raz-rewrite
  (implies (and (rationalp x) (integerp n) (> n 0))
           (equal (raz x n)
                  (* (sgn x)
                     (cg (* (expt 2 (- (1- n) (expo x)))
                            (abs x)))
                     (expt 2 (- (1+ (expo x)) n))))))

Theorem: abs-raz

(defthm abs-raz
  (implies (and (rationalp x) (integerp n))
           (equal (abs (raz x n))
                  (* (cg (* (expt 2 (1- n)) (sig x)))
                     (expt 2 (- (1+ (expo x)) n))))))

Theorem: raz-integer-type-prescription

(defthm raz-integer-type-prescription
  (implies (and (>= (expo x) n)
                (case-split (integerp n)))
           (integerp (raz x n)))
  :rule-classes :type-prescription)

Theorem: sgn-raz

(defthm sgn-raz
  (equal (sgn (raz x n)) (sgn x)))

Theorem: raz-positive

(defthm raz-positive
  (implies (and (< 0 x) (case-split (rationalp x)))
           (< 0 (raz x n)))
  :rule-classes (:rewrite :linear))

Theorem: raz-negative

(defthm raz-negative
  (implies (and (< x 0) (case-split (rationalp x)))
           (< (raz x n) 0))
  :rule-classes (:rewrite :linear))

Theorem: raz-0

(defthm raz-0 (equal (raz 0 n) 0))

Theorem: raz-minus

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

Theorem: raz-shift

(defthm raz-shift
  (implies (integerp n)
           (= (raz (* x (expt 2 k)) n)
              (* (raz x n) (expt 2 k))))
  :rule-classes nil)

Theorem: raz-neg-bits

(defthm raz-neg-bits
  (implies (and (<= n 0)
                (rationalp x)
                (integerp n))
           (equal (raz x n)
                  (* (sgn x)
                     (expt 2 (+ 1 (expo x) (- n)))))))

Theorem: raz-lower-bound

(defthm raz-lower-bound
  (implies (and (case-split (rationalp x))
                (case-split (integerp n)))
           (>= (abs (raz x n)) (abs x)))
  :rule-classes :linear)

Theorem: raz-lower-pos

(defthm raz-lower-pos
  (implies (and (>= x 0)
                (case-split (rationalp x))
                (case-split (integerp n)))
           (>= (raz x n) x))
  :rule-classes :linear)

Theorem: raz-upper-bound

(defthm raz-upper-bound
  (implies (and (rationalp x) (integerp n) (> n 0))
           (< (abs (raz x n))
              (+ (abs x)
                 (expt 2 (- (1+ (expo x)) n)))))
  :rule-classes :linear)

Theorem: raz-diff

(defthm raz-diff
  (implies (and (rationalp x) (integerp n) (> n 0))
           (< (abs (- (raz x n) x))
              (expt 2 (- (1+ (expo x)) n))))
  :rule-classes :linear)

Theorem: raz-expo-upper

(defthm raz-expo-upper
  (implies (and (rationalp x)
                (not (= x 0))
                (natp n))
           (<= (abs (raz x n))
               (expt 2 (1+ (expo x)))))
  :rule-classes nil)

Theorem: expo-raz-upper-bound

(defthm expo-raz-upper-bound
  (implies (and (rationalp x) (natp n))
           (<= (expo (raz x n)) (1+ (expo x))))
  :rule-classes :linear)

Theorem: expo-raz-lower-bound

(defthm expo-raz-lower-bound
  (implies (and (rationalp x) (natp n))
           (>= (expo (raz x n)) (expo x)))
  :rule-classes :linear)

Theorem: expo-raz

(defthm expo-raz
  (implies (and (rationalp x)
                (natp n)
                (not (= (abs (raz x n))
                        (expt 2 (1+ (expo x))))))
           (equal (expo (raz x n)) (expo x))))

Theorem: raz-exactp-a

(defthm raz-exactp-a
  (implies (case-split (< 0 n))
           (exactp (raz x n) n)))

Theorem: raz-exactp-b

(defthm raz-exactp-b
  (implies (and (rationalp x) (integerp n) (> n 0))
           (iff (exactp x n) (= x (raz x n)))))

Theorem: raz-exactp-c

(defthm raz-exactp-c
  (implies (and (exactp a n)
                (>= a x)
                (rationalp x)
                (integerp n)
                (> n 0)
                (rationalp a))
           (>= a (raz x n)))
  :rule-classes nil)

Theorem: raz-squeeze

(defthm raz-squeeze
  (implies (and (rationalp x)
                (rationalp a)
                (> x a)
                (> a 0)
                (not (zp n))
                (exactp a n)
                (<= x (fp+ a n)))
           (equal (raz x n) (fp+ a n))))

Theorem: raz-up

(defthm raz-up
  (implies (and (rationalp x)
                (integerp k)
                (not (zp n))
                (not (zp m))
                (< m n)
                (< (abs x) (expt 2 k))
                (= (abs (raz x n)) (expt 2 k)))
           (equal (abs (raz x m)) (expt 2 k))))

Theorem: raz-monotone

(defthm raz-monotone
  (implies (and (rationalp x)
                (rationalp y)
                (integerp n)
                (<= x y))
           (<= (raz x n) (raz y n)))
  :rule-classes :linear)

Theorem: rtz-raz

(defthm rtz-raz
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0)
                (not (exactp x n)))
           (equal (raz x n)
                  (+ (rtz x n)
                     (expt 2 (+ (expo x) 1 (- n)))))))

Theorem: raz-midpoint

(defthm raz-midpoint
  (implies (and (natp n)
                (rationalp x)
                (> x 0)
                (exactp x (1+ n))
                (not (exactp x n)))
           (equal (raz x n)
                  (+ x (expt 2 (- (expo x) n))))))

Theorem: raz-raz

(defthm raz-raz
  (implies (and (rationalp x)
                (>= x 0)
                (integerp n)
                (integerp m)
                (> m 0)
                (>= n m))
           (equal (raz (raz x n) m) (raz x m))))

Theorem: plus-raz

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

Theorem: minus-rtz-raz

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

Theorem: rtz-plus-minus

(defthm rtz-plus-minus
  (implies (and (rationalp x)
                (rationalp y)
                (not (= x 0))
                (not (= y 0))
                (not (= (+ x y) 0))
                (integerp k)
                (> k 0)
                (= k1 (+ k (- (expo x) (expo y))))
                (= k2 (+ k (expo (+ x y)) (- (expo y))))
                (exactp x k1)
                (> k2 0))
           (= (+ x (rtz y k))
              (if (= (sgn (+ x y)) (sgn y))
                  (rtz (+ x y) k2)
                (raz (+ x y) k2))))
  :rule-classes nil)

Theorem: raz-impl

(defthm raz-impl
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0)
                (integerp m)
                (>= m n)
                (exactp x m))
           (equal (raz x n)
                  (rtz (+ x (expt 2 (- (1+ (expo x)) n))
                          (- (expt 2 (- (1+ (expo x)) m))))
                       n))))