• 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
        • Floating-Point Formats
        • Floating-Point Numbers
          • Exactness
          • Floating-Point Decomposition
      • Modeling Algorithms in C++ and ACL2
      • Bibliography
  • Software-verification
  • Math
  • Testing-utilities

• Floating-Point Numbers

Floating-Point Decomposition

Floating-Point Decomposition

Definitions and Theorems

Function: sgn

(defun sgn (x)
  (declare (xargs :guard t))
  (if (or (not (rationalp x)) (equal x 0))
      0
    (if (< x 0) -1 1)))

Function: expo

(defun expo (x)
  (declare (xargs :guard t))
  (mbe :logic
       (cond ((or (not (rationalp x)) (equal x 0)) 0)
             ((< x 0) (expo (- x)))
             ((< x 1) (1- (expo (* 2 x))))
             ((< x 2) 0)
             (t (1+ (expo (/ x 2)))))
       :exec
       (if (rationalp x)
           (let* ((n (abs (numerator x)))
                  (d (denominator x))
                  (ln (integer-length n))
                  (ld (integer-length d))
                  (l (- ln ld)))
             (if (>= ln ld)
                 (if (>= (ash n (- l)) d) l (1- l))
               (if (> ln 1)
                   (if (> n (ash d l)) l (1- l))
                 (- (integer-length (1- d))))))
         0)))

Function: sig

(defun sig (x)
  (declare (xargs :guard t))
  (if (rationalp x)
      (if (< x 0)
          (- (* x (expt 2 (- (expo x)))))
        (* x (expt 2 (- (expo x)))))
    0))

Theorem: expo-minus

(defthm expo-minus
  (implies (rationalp x)
           (equal (expo (- x)) (expo x))))

Theorem: sig-minus

(defthm sig-minus
  (implies (rationalp x)
           (equal (sig (- x)) (sig x))))

Theorem: expo-lower-bound

(defthm expo-lower-bound
  (implies (and (rationalp x) (not (equal x 0)))
           (<= (expt 2 (expo x)) (abs x)))
  :rule-classes :linear)

Theorem: expo-upper-bound

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

Theorem: expo-unique

(defthm expo-unique
  (implies (and (<= (expt 2 n) (abs x))
                (< (abs x) (expt 2 (1+ n)))
                (rationalp x)
                (integerp n))
           (equal n (expo x)))
  :rule-classes nil)

Theorem: fp-rep

(defthm fp-rep
  (implies (rationalp x)
           (equal x
                  (* (sgn x) (sig x) (expt 2 (expo x)))))
  :rule-classes nil)

Theorem: fp-abs

(defthm fp-abs
  (implies (rationalp x)
           (equal (abs x)
                  (* (sig x) (expt 2 (expo x)))))
  :rule-classes nil)

Theorem: expo>=

(defthm expo>=
  (implies (and (<= (expt 2 n) x)
                (rationalp x)
                (integerp n))
           (<= n (expo x)))
  :rule-classes :linear)

Theorem: expo<=

(defthm expo<=
  (implies (and (< x (* 2 (expt 2 n)))
                (< 0 x)
                (rationalp x)
                (integerp n))
           (<= (expo x) n))
  :rule-classes :linear)

Theorem: expo-2**n

(defthm expo-2**n
  (implies (integerp n)
           (equal (expo (expt 2 n)) n)))

Theorem: bitn-expo

(defthm bitn-expo
  (implies (not (zp x))
           (equal (bitn x (expo x)) 1)))

Theorem: expo-monotone

(defthm expo-monotone
  (implies (and (<= (abs x) (abs y))
                (case-split (rationalp x))
                (case-split (not (equal x 0)))
                (case-split (rationalp y)))
           (<= (expo x) (expo y)))
  :rule-classes :linear)

Theorem: bvecp-expo

(defthm bvecp-expo
  (implies (case-split (natp x))
           (bvecp x (1+ (expo x)))))

Theorem: mod-expo

(defthm mod-expo
  (implies (and (< 0 x) (rationalp x))
           (equal (mod x (expt 2 (expo x)))
                  (- x (expt 2 (expo x))))))

Theorem: sig-lower-bound

(defthm sig-lower-bound
  (implies (and (rationalp x) (not (equal x 0)))
           (<= 1 (sig x)))
  :rule-classes (:rewrite :linear))

Theorem: sig-upper-bound

(defthm sig-upper-bound
  (< (sig x) 2)
  :rule-classes (:rewrite :linear))

Theorem: expo-sig

(defthm expo-sig
  (implies (rationalp x)
           (equal (expo (sig x)) 0)))

Theorem: sig-self

(defthm sig-self
  (implies (and (rationalp x) (<= 1 x) (< x 2))
           (equal (sig x) x)))

Theorem: sig-sig

(defthm sig-sig
  (equal (sig (sig x)) (sig x)))

Theorem: fp-rep-unique

(defthm fp-rep-unique
  (implies (and (rationalp x)
                (rationalp m)
                (<= 1 m)
                (< m 2)
                (integerp e)
                (= (abs x) (* m (expt 2 e))))
           (and (= m (sig x)) (= e (expo x))))
  :rule-classes nil)

Theorem: sgn-shift

(defthm sgn-shift
  (equal (sgn (* x (expt 2 k))) (sgn x)))

Theorem: expo-shift

(defthm expo-shift
  (implies (and (rationalp x)
                (not (equal x 0))
                (integerp n))
           (equal (expo (* (expt 2 n) x))
                  (+ n (expo x)))))

Theorem: sig-shift

(defthm sig-shift
  (equal (sig (* (expt 2 n) x)) (sig x)))

Theorem: sgn-prod

(defthm sgn-prod
  (implies (and (case-split (rationalp x))
                (case-split (rationalp y)))
           (equal (sgn (* x y))
                  (* (sgn x) (sgn y)))))

Theorem: expo-prod

(defthm expo-prod
  (implies (and (rationalp x)
                (not (= x 0))
                (rationalp y)
                (not (= y 0)))
           (equal (expo (* x y))
                  (if (< (* (sig x) (sig y)) 2)
                      (+ (expo x) (expo y))
                    (+ 1 (expo x) (expo y))))))

Theorem: expo-prod-lower

(defthm expo-prod-lower
  (implies (and (rationalp x)
                (not (= x 0))
                (rationalp y)
                (not (= y 0)))
           (<= (+ (expo x) (expo y))
               (expo (* x y))))
  :rule-classes :linear)

Theorem: expo-prod-upper

(defthm expo-prod-upper
  (implies (and (rationalp x)
                (not (= x 0))
                (rationalp y)
                (not (= y 0)))
           (>= (+ (expo x) (expo y) 1)
               (expo (* x y))))
  :rule-classes :linear)

Theorem: sig-prod

(defthm sig-prod
  (implies (and (rationalp x)
                (not (= x 0))
                (rationalp y)
                (not (= y 0)))
           (equal (sig (* x y))
                  (if (< (* (sig x) (sig y)) 2)
                      (* (sig x) (sig y))
                    (* 1/2 (sig x) (sig y))))))

Theorem: expo-fl

(defthm expo-fl
  (implies (and (rationalp x) (>= x 1))
           (equal (expo (fl x)) (expo x))))

Theorem: expo-logior

(defthm expo-logior
  (implies (and (natp x)
                (natp y)
                (<= (expo x) (expo y)))
           (equal (expo (logior x y)) (expo y))))