• 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

IEEE Rounding

IEEE Rounding

Definitions and Theorems

Function: rup

(defun rup (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (if (>= x 0) (raz x n) (rtz x n)))

Function: rdn

(defun rdn (x n)
  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
  (if (>= x 0) (rtz x n) (raz x n)))

Theorem: rup-lower-bound

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

Theorem: rdn-upper-bound

(defthm rdn-upper-bound
  (implies (and (case-split (rationalp x))
                (case-split (integerp n)))
           (<= (rdn x n) x))
  :rule-classes :linear)

Function: ieee-rounding-mode-p

(defun ieee-rounding-mode-p (mode)
  (declare (xargs :guard t))
  (member mode '(rtz rup rdn rne)))

Function: common-mode-p

(defun common-mode-p (mode)
  (declare (xargs :guard t))
  (or (ieee-rounding-mode-p mode)
      (equal mode 'raz)
      (equal mode 'rna)))

Theorem: ieee-mode-is-common-mode

(defthm ieee-mode-is-common-mode
  (implies (ieee-rounding-mode-p mode)
           (common-mode-p mode)))

Function: rnd

(defun rnd (x mode n)
  (declare (xargs :guard (and (real/rationalp x)
                              (common-mode-p mode)
                              (integerp n))))
  (case mode
    (raz (raz x n))
    (rna (rna x n))
    (rtz (rtz x n))
    (rup (rup x n))
    (rdn (rdn x n))
    (rne (rne x n))
    (otherwise 0)))

Theorem: rationalp-rnd

(defthm rationalp-rnd
  (rationalp (rnd x mode n))
  :rule-classes (:type-prescription))

Theorem: rnd-choice

(defthm rnd-choice
  (implies (and (rationalp x)
                (integerp n)
                (common-mode-p mode))
           (or (= (rnd x mode n) (rtz x n))
               (= (rnd x mode n) (raz x n))))
  :rule-classes nil)

Theorem: sgn-rnd

(defthm sgn-rnd
  (implies (and (common-mode-p mode)
                (integerp n)
                (> n 0))
           (equal (sgn (rnd x mode n)) (sgn x))))

Theorem: rnd-positive

(defthm rnd-positive
  (implies (and (< 0 x)
                (rationalp x)
                (integerp n)
                (> n 0)
                (common-mode-p mode))
           (> (rnd x mode n) 0))
  :rule-classes (:type-prescription))

Theorem: rnd-negative

(defthm rnd-negative
  (implies (and (< x 0)
                (rationalp x)
                (integerp n)
                (> n 0)
                (common-mode-p mode))
           (< (rnd x mode n) 0))
  :rule-classes (:type-prescription))

Theorem: rnd-0

(defthm rnd-0 (equal (rnd 0 mode n) 0))

Theorem: rnd-non-pos

(defthm rnd-non-pos
  (implies (<= x 0) (<= (rnd x mode n) 0))
  :rule-classes (:rewrite :type-prescription :linear))

Theorem: rnd-non-neg

(defthm rnd-non-neg
  (implies (<= 0 x) (<= 0 (rnd x mode n)))
  :rule-classes (:rewrite :type-prescription :linear))

Function: flip-mode

(defun flip-mode (m)
  (declare (xargs :guard (common-mode-p m)))
  (case m (rup 'rdn) (rdn 'rup) (t m)))

Theorem: ieee-rounding-mode-p-flip-mode

(defthm ieee-rounding-mode-p-flip-mode
  (implies (ieee-rounding-mode-p m)
           (ieee-rounding-mode-p (flip-mode m))))

Theorem: common-mode-p-flip-mode

(defthm common-mode-p-flip-mode
  (implies (common-mode-p m)
           (common-mode-p (flip-mode m))))

Theorem: rnd-minus

(defthm rnd-minus
  (equal (rnd (- x) mode n)
         (- (rnd x (flip-mode mode) n))))

Theorem: rnd-exactp-a

(defthm rnd-exactp-a
  (implies (< 0 n)
           (exactp (rnd x mode n) n)))

Theorem: rnd-exactp-b

(defthm rnd-exactp-b
  (implies (and (rationalp x)
                (common-mode-p mode)
                (integerp n)
                (> n 0))
           (equal (exactp x n)
                  (equal x (rnd x mode n)))))

Theorem: rnd-exactp-c

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

Theorem: rnd-exactp-d

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

Theorem: rnd<=raz

(defthm rnd<=raz
  (implies (and (rationalp x)
                (>= x 0)
                (common-mode-p mode)
                (natp n))
           (<= (rnd x mode n) (raz x n)))
  :rule-classes nil)

Theorem: rnd>=rtz

(defthm rnd>=rtz
  (implies (and (rationalp x)
                (> x 0)
                (common-mode-p mode)
                (integerp n)
                (> n 0))
           (>= (rnd x mode n) (rtz x n)))
  :rule-classes nil)

Theorem: rnd<equal

(defthm rnd<equal
  (implies (and (rationalp x)
                (rationalp y)
                (natp n)
                (common-mode-p mode)
                (> n 0)
                (> x 0)
                (not (exactp x (1+ n)))
                (< (rtz x (1+ n)) y)
                (< y x))
           (= (rnd y mode n) (rnd x mode n)))
  :rule-classes nil)

Theorem: rnd>equal

(defthm rnd>equal
  (implies (and (rationalp x)
                (rationalp y)
                (natp n)
                (common-mode-p mode)
                (> n 0)
                (> x 0)
                (not (exactp x (1+ n)))
                (> (raz x (1+ n)) y)
                (> y x))
           (= (rnd y mode n) (rnd x mode n)))
  :rule-classes nil)

Theorem: rnd-near-equal

(defthm rnd-near-equal
  (implies (and (rationalp x)
                (rationalp y)
                (natp n)
                (common-mode-p mode)
                (> n 0)
                (> x 0)
                (not (exactp x (1+ n))))
           (let ((d (min (- x (rtz x (1+ n)))
                         (- (raz x (1+ n)) x))))
             (and (> d 0)
                  (implies (< (abs (- x y)) d)
                           (= (rnd y mode n) (rnd x mode n))))))
  :rule-classes nil)

Theorem: expo-rnd

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

Theorem: rnd-monotone

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

Theorem: rnd-shift

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

Theorem: plus-rnd

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

Theorem: rnd-rto

(defthm rnd-rto
  (implies (and (common-mode-p mode)
                (rationalp x)
                (integerp m)
                (> m 0)
                (integerp n)
                (>= n (+ m 2)))
           (equal (rnd (rto x n) mode m)
                  (rnd x mode m))))

Theorem: rnd-up

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

Function: rnd-const

(defun rnd-const (e mode n)
  (declare (xargs :guard (and (integerp e)
                              (common-mode-p mode)
                              (integerp n))))
  (case mode
    ((rne rna) (expt 2 (- e n)))
    ((rup raz) (1- (expt 2 (1+ (- e n)))))
    (otherwise 0)))

Theorem: rnd-const-lemma

(defthm rnd-const-lemma
  (implies (and (common-mode-p mode)
                (not (zp n))
                (not (zp x))
                (implies (or (= mode 'raz) (= mode 'rup))
                         (>= (expo x) (1- n))))
           (equal (rnd x mode n)
                  (if (and (eql mode 'rne)
                           (> n 1)
                           (exactp x (1+ n))
                           (not (exactp x n)))
                      (rtz (+ x (rnd-const (expo x) mode n))
                           (1- n))
                    (rtz (+ x (rnd-const (expo x) mode n))
                         n)))))

Function: roundup-pos

(defun roundup-pos (x e sticky mode n)
  (declare (xargs :guard (and (integerp x)
                              (integerp e)
                              (integerp sticky)
                              (common-mode-p mode)
                              (integerp n))))
  (case mode
    ((rup raz)
     (or (not (= (bits x (- e n) 0) 0))
         (= sticky 1)))
    (rna (= (bitn x (- e n)) 1))
    (rne (and (= (bitn x (- e n)) 1)
              (or (not (= (bits x (- e (1+ n)) 0) 0))
                  (= sticky 1)
                  (= (bitn x (- (1+ e) n)) 1))))
    (otherwise nil)))

Theorem: rnd-const-cor-a

(defthm rnd-const-cor-a
  (implies (and (common-mode-p mode)
                (posp n)
                (posp m)
                (> (expo m) n))
           (let* ((e (expo m))
                  (sum (+ m (rnd-const e mode n)))
                  (sh (bits sum (1+ e) (1+ (- e n))))
                  (sl (bits sum (- e n) 0)))
             (equal (rnd m mode n)
                    (if (and (= mode 'rne) (= sl 0))
                        (* (expt 2 (+ 2 (- e n))) (bits sh n 1))
                      (* (expt 2 (1+ (- e n))) sh))))))

Theorem: rnd-const-cor-b

(defthm rnd-const-cor-b
  (implies (and (common-mode-p mode)
                (posp n)
                (posp m)
                (> (expo m) n))
           (let* ((e (expo m))
                  (c (rnd-const e mode n))
                  (sum (+ m c))
                  (sl (bits sum (- e n) 0)))
             (iff (= m (rnd m mode n)) (= sl c)))))

Theorem: roundup-pos-thm-1

(defthm roundup-pos-thm-1
  (implies (and (rationalp z)
                (not (zp n))
                (<= (expt 2 n) z))
           (let ((x (fl z)))
             (iff (exactp z n)
                  (and (integerp z)
                       (= (bits x (- (expo x) n) 0) 0))))))

Theorem: roundup-pos-thm-2

(defthm roundup-pos-thm-2
  (implies (and (common-mode-p mode)
                (rationalp z)
                (not (zp n))
                (<= (expt 2 n) z))
           (let ((x (fl z))
                 (sticky (if (integerp z) 0 1)))
             (equal (rnd z mode n)
                    (if (roundup-pos x (expo x) sticky mode n)
                        (fp+ (rtz x n) n)
                      (rtz x n))))))

Theorem: roundup-pos-thm

(defthm roundup-pos-thm
  (implies (and (common-mode-p mode)
                (rationalp z)
                (not (zp n))
                (<= (expt 2 n) z))
           (let ((x (fl z))
                 (sticky (if (integerp z) 0 1)))
             (and (iff (exactp z n)
                       (and (integerp z)
                            (= (bits x (- (expo x) n) 0) 0)))
                  (equal (rnd z mode n)
                         (if (roundup-pos x (expo x) sticky mode n)
                             (fp+ (rtz x n) n)
                           (rtz x n)))))))

Function: roundup-neg

(defun roundup-neg (x e sticky mode n)
  (declare (xargs :guard (and (integerp x)
                              (integerp e)
                              (integerp sticky)
                              (common-mode-p mode)
                              (integerp n))))
  (case mode
    ((rdn raz) t)
    ((rup rtz)
     (and (= (bits x (- e n) 0) 0)
          (= sticky 0)))
    (rna (or (= (bitn x (- e n)) 0)
             (and (= (bits x (- e (1+ n)) 0) 0)
                  (= sticky 0))))
    (rne (or (= (bitn x (- e n)) 0)
             (and (= (bitn x (- (1+ e) n)) 0)
                  (= (bits x (- e (1+ n)) 0) 0)
                  (= sticky 0))))
    (otherwise nil)))

Theorem: roundup-neg-thm

(defthm roundup-neg-thm
  (implies (and (common-mode-p mode)
                (rationalp z)
                (not (zp n))
                (natp k)
                (< n k)
                (<= (- (expt 2 k)) z)
                (< z (- (expt 2 n))))
           (let* ((x (+ (fl z) (expt 2 k)))
                  (xc (1- (- (expt 2 k) x)))
                  (e (expo xc))
                  (sticky (if (integerp z) 0 1)))
             (and (implies (not (= (expo z) e))
                           (= z (- (expt 2 (1+ e)))))
                  (iff (exactp z n)
                       (and (integerp z)
                            (= (bits x (- (expo xc) n) 0) 0)))
                  (equal (abs (rnd z mode n))
                         (if (roundup-neg x (expo xc) sticky mode n)
                             (fp+ (rtz xc n) n)
                           (rtz xc n))))))
  :rule-classes nil)