• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • 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
  • Software-verification
  • Math
  • Testing-utilities

• Rounding

Odd Rounding

Odd Rounding

Definitions and Theorems

Function: rto

(defun rto (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (if (exactp x (1- n))
      x
    (+ (rtz x (1- n))
       (* (sgn x)
          (expt 2 (1+ (- (expo x) n)))))))

Theorem: sgn-rto

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

Theorem: rto-positive

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

Theorem: rto-negative

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

Theorem: rto-0

(defthm rto-0 (equal (rto 0 n) 0))

Theorem: rto-minus

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

Theorem: rto-shift

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

Function: err-rto

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

Function: sum-err-rto

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

Theorem: rto-unbiased

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

Theorem: expo-rto

(defthm expo-rto
  (implies (and (rationalp x) (integerp n) (> n 0))
           (equal (expo (rto x n)) (expo x))))

Theorem: rto-exactp-a

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

Theorem: rto-exactp-b

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

Theorem: rto-monotone

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

Theorem: rto-exactp-c

(defthm rto-exactp-c
  (implies (and (rationalp x)
                (integerp m)
                (integerp n)
                (> n m)
                (> m 0))
           (iff (exactp (rto x n) m)
                (exactp x m))))

Theorem: rtz-rto

(defthm rtz-rto
  (implies (and (rationalp x)
                (integerp m)
                (> m 0)
                (integerp n)
                (> n m))
           (equal (rtz (rto x n) m) (rtz x m))))

Theorem: raz-rto

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

Theorem: rne-rto

(defthm rne-rto
  (implies (and (rationalp x)
                (integerp m)
                (> m 0)
                (integerp n)
                (> n (1+ m)))
           (equal (rne (rto x n) m) (rne x m))))

Theorem: rna-rto

(defthm rna-rto
  (implies (and (rationalp x)
                (integerp m)
                (> m 0)
                (integerp n)
                (> n (1+ m)))
           (equal (rna (rto x n) m) (rna x m))))

Theorem: rto-rto

(defthm rto-rto
  (implies (and (rationalp x)
                (integerp m)
                (> m 1)
                (integerp n)
                (>= n m))
           (equal (rto (rto x n) m) (rto x m))))

Theorem: rto-plus

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