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

Unbiased Rounding

Unbiased Rounding

Definitions and Theorems

Function: re

(defun re (x)
  (declare (xargs :guard (real/rationalp x)))
  (- x (fl x)))

Function: rne

(defun rne (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (let ((z (fl (* (expt 2 (1- n)) (sig x))))
        (f (re (* (expt 2 (1- n)) (sig x)))))
    (if (< f 1/2)
        (rtz x n)
      (if (> f 1/2)
          (raz x n)
        (if (evenp z) (rtz x n) (raz x n))))))

Theorem: rne-choice

(defthm rne-choice
  (or (= (rne x n) (rtz x n))
      (= (rne x n) (raz x n)))
  :rule-classes nil)

Theorem: sgn-rne

(defthm sgn-rne
  (implies (and (rationalp x) (integerp n) (> n 0))
           (equal (sgn (rne x n)) (sgn x))))

Theorem: rne-positive

(defthm rne-positive
  (implies (and (< 0 x)
                (< 0 n)
                (rationalp x)
                (integerp n))
           (< 0 (rne x n)))
  :rule-classes (:type-prescription :linear))

Theorem: rne-negative

(defthm rne-negative
  (implies (and (< x 0)
                (< 0 n)
                (rationalp x)
                (integerp n))
           (< (rne x n) 0))
  :rule-classes (:type-prescription :linear))

Theorem: rne-0

(defthm rne-0 (equal (rne 0 n) 0))

Theorem: rne-exactp-a

(defthm rne-exactp-a
  (implies (< 0 n) (exactp (rne x n) n)))

Theorem: rne-exactp-b

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

Theorem: rne-exactp-c

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

Theorem: rne-exactp-d

(defthm rne-exactp-d
  (implies (and (rationalp x)
                (integerp n)
                (> n 0)
                (rationalp a)
                (exactp a n)
                (<= a x))
           (<= a (rne x n)))
  :rule-classes nil)

Theorem: expo-rne

(defthm expo-rne
  (implies (and (rationalp x)
                (> n 0)
                (integerp n)
                (not (= (abs (rne x n))
                        (expt 2 (1+ (expo x))))))
           (equal (expo (rne x n)) (expo x))))

Theorem: rne<=raz

(defthm rne<=raz
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0))
           (<= (rne x n) (raz x n)))
  :rule-classes nil)

Theorem: rne>=rtz

(defthm rne>=rtz
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0))
           (>= (rne x n) (rtz x n)))
  :rule-classes nil)

Theorem: rne-shift

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

Theorem: rne-minus

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

Theorem: rne-rtz

(defthm rne-rtz
  (implies (and (< (abs (- x (rtz x n)))
                   (abs (- (raz x n) x)))
                (rationalp x)
                (integerp n))
           (equal (rne x n) (rtz x n))))

Theorem: rne-raz

(defthm rne-raz
  (implies (and (> (abs (- x (rtz x n)))
                   (abs (- (raz x n) x)))
                (rationalp x)
                (integerp n))
           (equal (rne x n) (raz x n))))

Theorem: rne-down

(defthm rne-down
  (implies (and (rationalp x)
                (rationalp a)
                (>= x a)
                (> a 0)
                (not (zp n))
                (exactp a n)
                (< x (+ a (expt 2 (- (expo a) n)))))
           (equal (rne x n) a)))

Theorem: rne-up

(defthm rne-up
  (implies (and (rationalp x)
                (rationalp a)
                (> a 0)
                (not (zp n))
                (exactp a n)
                (< x (fp+ a n))
                (> x (+ a (expt 2 (- (expo a) n)))))
           (equal (rne x n) (fp+ a n))))

Theorem: rne-up-2

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

Theorem: rne-nearest

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

Theorem: rne-diff

(defthm rne-diff
  (implies (and (integerp n) (> n 0) (rationalp x))
           (<= (abs (- x (rne x n)))
               (expt 2 (- (expo x) n))))
  :rule-classes nil)

Theorem: rne-diff-cor

(defthm rne-diff-cor
  (implies (and (integerp n) (> n 0) (rationalp x))
           (<= (abs (- x (rne x n)))
               (* (abs x) (expt 2 (- n)))))
  :rule-classes nil)

Theorem: rne-force

(defthm rne-force
  (implies (and (integerp n)
                (> n 0)
                (rationalp x)
                (not (= x 0))
                (rationalp y)
                (exactp y n)
                (< (abs (- x y))
                   (expt 2 (- (expo x) n))))
           (= y (rne x n)))
  :rule-classes nil)

Theorem: rne-monotone

(defthm rne-monotone
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y)
                (integerp n)
                (> n 0))
           (<= (rne x n) (rne y n)))
  :rule-classes nil)

Function: rne-witness

(defun rne-witness (x y n)
  (if (= (expo x) (expo y))
      (/ (+ (rne x n) (rne y n)) 2)
    (expt 2 (expo y))))

Theorem: rne-rne-lemma

(defthm rne-rne-lemma
  (implies (and (rationalp x)
                (rationalp y)
                (< 0 x)
                (< x y)
                (integerp n)
                (> n 0)
                (not (= (rne x n) (rne y n))))
           (and (<= x (rne-witness x y n))
                (<= (rne-witness x y n) y)
                (exactp (rne-witness x y n) (1+ n))))
  :rule-classes nil)

Theorem: rne-rne

(defthm rne-rne
  (implies (and (rationalp x)
                (rationalp y)
                (rationalp a)
                (integerp n)
                (integerp k)
                (> k 0)
                (>= n k)
                (< 0 a)
                (< a x)
                (< 0 y)
                (< y (fp+ a (1+ n)))
                (exactp a (1+ n)))
           (<= (rne y k) (rne x k)))
  :rule-classes nil)

Theorem: rne-boundary

(defthm rne-boundary
  (implies (and (rationalp x)
                (rationalp y)
                (rationalp a)
                (< 0 x)
                (< x a)
                (< a y)
                (integerp n)
                (> n 0)
                (exactp a (1+ n))
                (not (exactp a n)))
           (< (rne x n) (rne y n)))
  :rule-classes nil)

Theorem: rne-midpoint

(defthm rne-midpoint
  (implies (and (rationalp x)
                (integerp n)
                (> n 1)
                (exactp x (1+ n))
                (not (exactp x n)))
           (exactp (rne x n) (1- n)))
  :rule-classes nil)

Function: xfp

(defun xfp (k m x0)
  (+ x0 (* (expt 2 (- (1+ (expo x0)) m)) k)))

Function: err-rne

(defun err-rne (k m n x0)
  (- (rne (xfp k m x0) n) (xfp k m x0)))

Function: sum-err-rne

(defun sum-err-rne (i j m n x0)
  (if (and (natp i) (natp j) (<= i j))
      (+ (sum-err-rne i (1- j) m n x0)
         (err-rne j m n x0))
    0))

Theorem: rne-unbiased

(defthm rne-unbiased
  (implies (and (natp m)
                (natp n)
                (< 1 n)
                (< n m)
                (rationalp x0)
                (> x0 0)
                (exactp x0 (1- n)))
           (equal (sum-err-rne 0 (1- (expt 2 (- (1+ m) n)))
                               m n x0)
                  0)))

Function: rna

(defun rna (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (if (< (re (* (expt 2 (1- n)) (sig x))) 1/2)
      (rtz x n)
    (raz x n)))

Theorem: rna-choice

(defthm rna-choice
  (or (= (rna x n) (rtz x n))
      (= (rna x n) (raz x n)))
  :rule-classes nil)

Theorem: sgn-rna

(defthm sgn-rna
  (implies (and (rationalp x) (integerp n) (> n 0))
           (equal (sgn (rna x n)) (sgn x))))

Theorem: rna-positive

(defthm rna-positive
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0))
           (> (rna x n) 0))
  :rule-classes :linear)

Theorem: rna-negative

(defthm rna-negative
  (implies (and (< x 0)
                (rationalp x)
                (integerp n)
                (> n 0))
           (< (rna x n) 0))
  :rule-classes :linear)

Theorem: rna-0

(defthm rna-0 (equal (rna 0 n) 0))

Theorem: rna-exactp-a

(defthm rna-exactp-a
  (implies (> n 0) (exactp (rna x n) n)))

Theorem: rna-exactp-b

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

Theorem: rna-exactp-c

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

Theorem: rna-exactp-d

(defthm rna-exactp-d
  (implies (and (rationalp x)
                (integerp n)
                (> n 0)
                (rationalp a)
                (exactp a n)
                (<= a x))
           (<= a (rna x n)))
  :rule-classes nil)

Theorem: expo-rna

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

Theorem: rna<=raz

(defthm rna<=raz
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0))
           (<= (rna x n) (raz x n)))
  :rule-classes nil)

Theorem: rna>=rtz

(defthm rna>=rtz
  (implies (and (rationalp x)
                (> x 0)
                (integerp n)
                (> n 0))
           (>= (rna x n) (rtz x n)))
  :rule-classes nil)

Theorem: rna-shift

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

Theorem: rna-minus

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

Theorem: rna-rtz

(defthm rna-rtz
  (implies (and (rationalp x)
                (integerp n)
                (< (abs (- x (rtz x n)))
                   (abs (- (raz x n) x))))
           (equal (rna x n) (rtz x n))))

Theorem: rna-raz

(defthm rna-raz
  (implies (and (rationalp x)
                (integerp n)
                (> (abs (- x (rtz x n)))
                   (abs (- (raz x n) x))))
           (equal (rna x n) (raz x n))))

Theorem: rna-down

(defthm rna-down
  (implies (and (rationalp x)
                (rationalp a)
                (>= x a)
                (> a 0)
                (not (zp n))
                (exactp a n)
                (< x (+ a (expt 2 (- (expo a) n)))))
           (equal (rna x n) a)))

Theorem: rna-up

(defthm rna-up
  (implies (and (rationalp x)
                (rationalp a)
                (> a 0)
                (not (zp n))
                (exactp a n)
                (< x (fp+ a n))
                (> x (+ a (expt 2 (- (expo a) n)))))
           (equal (rna x n) (fp+ a n))))

Theorem: rna-up-2

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

Theorem: rna-nearest

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

Theorem: rna-force

(defthm rna-force
  (implies (and (integerp n)
                (> n 0)
                (rationalp x)
                (not (= x 0))
                (rationalp y)
                (exactp y n)
                (< (abs (- x y))
                   (expt 2 (- (expo x) n))))
           (= y (rna x n)))
  :rule-classes nil)

Theorem: rna-diff

(defthm rna-diff
  (implies (and (integerp n) (> n 0) (rationalp x))
           (<= (abs (- x (rna x n)))
               (expt 2 (- (expo x) n))))
  :rule-classes nil)

Theorem: rna-monotone

(defthm rna-monotone
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y)
                (natp n))
           (<= (rna x n) (rna y n)))
  :rule-classes nil)

Function: rna-witness

(defun rna-witness (x y n)
  (if (= (expo x) (expo y))
      (/ (+ (rna x n) (rna y n)) 2)
    (expt 2 (expo y))))

Theorem: rna-rna-lemma

(defthm rna-rna-lemma
  (implies (and (rationalp x)
                (rationalp y)
                (< 0 x)
                (< x y)
                (integerp n)
                (> n 0)
                (not (= (rna x n) (rna y n))))
           (and (<= x (rna-witness x y n))
                (<= (rna-witness x y n) y)
                (exactp (rna-witness x y n) (1+ n))))
  :rule-classes nil)

Theorem: rna-rna

(defthm rna-rna
  (implies (and (rationalp x)
                (rationalp y)
                (rationalp a)
                (integerp n)
                (integerp k)
                (> k 0)
                (>= n k)
                (< 0 a)
                (< a x)
                (< 0 y)
                (< y (fp+ a (1+ n)))
                (exactp a (1+ n)))
           (<= (rna y k) (rna x k)))
  :rule-classes nil)

Theorem: rna-midpoint

(defthm rna-midpoint
  (implies (and (rationalp x)
                (integerp n)
                (exactp x (1+ n))
                (not (exactp x n)))
           (equal (rna x n) (raz x n))))

Theorem: rne-pow-2

(defthm rne-pow-2
  (implies (and (rationalp x)
                (> x 0)
                (not (zp n))
                (>= (+ x (expt 2 (- (expo x) n)))
                    (expt 2 (1+ (expo x)))))
           (= (rne x n) (expt 2 (1+ (expo x)))))
  :rule-classes nil)

Theorem: rtz-pow-2

(defthm rtz-pow-2
  (implies (and (rationalp x)
                (> x 0)
                (not (zp n))
                (>= (+ x (expt 2 (- (expo x) n)))
                    (expt 2 (1+ (expo x)))))
           (= (rtz (+ x (expt 2 (- (expo x) n))) n)
              (expt 2 (1+ (expo x)))))
  :rule-classes nil)

Theorem: rna-pow-2

(defthm rna-pow-2
  (implies (and (rationalp x)
                (> x 0)
                (not (zp n))
                (>= (+ x (expt 2 (- (expo x) n)))
                    (expt 2 (1+ (expo x)))))
           (= (rna x n) (expt 2 (1+ (expo x)))))
  :rule-classes nil)

Theorem: plus-rne

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

Theorem: plus-rna

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

Theorem: rne-impl

(defthm rne-impl
  (implies (and (rationalp x) (> x 0) (not (zp n)))
           (equal (rne x n)
                  (if (and (> n 1)
                           (exactp x (1+ n))
                           (not (exactp x n)))
                      (rtz (+ x (expt 2 (- (expo x) n)))
                           (1- n))
                    (rtz (+ x (expt 2 (- (expo x) n)))
                         n)))))

Theorem: rna-impl

(defthm rna-impl
  (implies (and (rationalp x) (> x 0) (not (zp n)))
           (equal (rna x n)
                  (rtz (+ x (expt 2 (- (expo x) n))) n))))

Theorem: rna-imp-cor

(defthm rna-imp-cor
  (implies (and (rationalp x)
                (integerp m)
                (integerp n)
                (> n m)
                (> m 0))
           (equal (rna (rtz x n) m) (rna x m))))