• 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

Truncation

Truncation

Definitions and Theorems

Function: rtz

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

Theorem: rtz-rewrite

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

Theorem: rtz-integer-type-prescription

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

Theorem: rtz-neg-bits

(defthm rtz-neg-bits
  (implies (and (integerp n) (<= n 0))
           (equal (rtz x n) 0)))

Theorem: sgn-rtz

(defthm sgn-rtz
  (implies (and (< 0 n) (rationalp x) (integerp n))
           (equal (sgn (rtz x n)) (sgn x))))

Theorem: rtz-positive

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

Theorem: rtz-negative

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

Theorem: rtz-0

(defthm rtz-0 (equal (rtz 0 n) 0))

Theorem: abs-rtz

(defthm abs-rtz
  (equal (abs (rtz x n))
         (* (fl (* (expt 2 (1- n)) (sig x)))
            (expt 2 (- (1+ (expo x)) n)))))

Theorem: rtz-minus

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

Theorem: rtz-shift

(defthm rtz-shift
  (implies (integerp n)
           (equal (rtz (* x (expt 2 k)) n)
                  (* (rtz x n) (expt 2 k)))))

Theorem: rtz-upper-bound

(defthm rtz-upper-bound
  (implies (and (rationalp x) (integerp n))
           (<= (abs (rtz x n)) (abs x)))
  :rule-classes :linear)

Theorem: rtz-upper-pos

(defthm rtz-upper-pos
  (implies (and (<= 0 x)
                (rationalp x)
                (integerp n))
           (<= (rtz x n) x))
  :rule-classes :linear)

Theorem: expo-rtz

(defthm expo-rtz
  (implies (and (< 0 n) (rationalp x) (integerp n))
           (equal (expo (rtz x n)) (expo x))))

Theorem: rtz-lower-bound

(defthm rtz-lower-bound
  (implies (and (rationalp x) (integerp n))
           (> (abs (rtz x n))
              (- (abs x)
                 (expt 2 (- (1+ (expo x)) n)))))
  :rule-classes :linear)

Theorem: rtz-diff

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

Theorem: rtz-exactp-a

(defthm rtz-exactp-a
  (exactp (rtz x n) n))

Theorem: rtz-exactp-b

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

Theorem: rtz-exactp-c

(defthm rtz-exactp-c
  (implies (and (exactp a n)
                (<= a x)
                (rationalp x)
                (integerp n)
                (rationalp a))
           (<= a (rtz x n)))
  :rule-classes nil)

Theorem: rtz-squeeze

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

Theorem: rtz-monotone

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

Theorem: rtz-midpoint

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

Theorem: rtz-rtz

(defthm rtz-rtz
  (implies (and (>= n m) (integerp n) (integerp m))
           (equal (rtz (rtz x n) m) (rtz x m))))

Theorem: plus-rtz

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

Theorem: minus-rtz

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

Theorem: bits-rtz

(defthm bits-rtz
  (implies (and (= n (1+ (expo x)))
                (>= x 0)
                (integerp k)
                (> k 0))
           (equal (rtz x k)
                  (* (expt 2 (- n k))
                     (bits x (1- n) (- n k))))))

Theorem: bits-rtz-bits

(defthm bits-rtz-bits
  (implies (and (rationalp x)
                (>= x 0)
                (integerp k)
                (integerp i)
                (integerp j)
                (> k 0)
                (>= (expo x) i)
                (>= j (- (1+ (expo x)) k)))
           (equal (bits (rtz x k) i j)
                  (bits x i j))))

Theorem: rtz-split

(defthm rtz-split
  (implies (and (= n (1+ (expo x)))
                (>= x 0)
                (integerp m)
                (> m k)
                (integerp k)
                (> k 0))
           (equal (rtz x m)
                  (+ (rtz x k)
                     (* (expt 2 (- n m))
                        (bits x (1- (- n k)) (- n m)))))))

Theorem: rtz-logand

(defthm rtz-logand
  (implies (and (>= x (expt 2 (1- n)))
                (< x (expt 2 n))
                (integerp x)
                (integerp m)
                (>= m n)
                (integerp n)
                (> n k)
                (integerp k)
                (> k 0))
           (equal (rtz x k)
                  (logand x (- (expt 2 m) (expt 2 (- n k)))))))