• 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
          • Floating-Point Formats
            • Normal Encodings
            • Denormals and Zeroes
            • Classification of Formats
            • Rebiasing Exponents
            • Infinities and NaNs
          • Floating-Point Numbers
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Floating-Point Formats

Normal Encodings

Normal Encodings

Definitions and Theorems

Function: normp

(defun normp (x f)
  (declare (xargs :guard (encodingp x f)))
  (and (mbt (encodingp x f))
       (< 0 (expf x f))
       (< (expf x f) (1- (expt 2 (expw f))))
       (implies (explicitp f)
                (= (bitn x (1- (prec f))) 1))))

Function: unsupp

(defun unsupp (x f)
  (declare (xargs :guard (encodingp x f)))
  (and (mbt (encodingp x f))
       (explicitp f)
       (< 0 (expf x f))
       (= (bitn x (1- (prec f))) 0)))

Function: ndecode

(defun ndecode (x f)
  (declare (xargs :guard (encodingp x f)))
  (* (if (= (sgnf x f) 0) 1 -1)
     (expt 2 (- (expf x f) (bias f)))
     (1+ (* (manf x f)
            (expt 2 (- 1 (prec f)))))))

Theorem: sgn-ndecode

(defthm sgn-ndecode
  (implies (normp x f)
           (equal (sgn (ndecode x f))
                  (if (= (sgnf x f) 0) 1 -1))))

Theorem: expo-ndecode

(defthm expo-ndecode
  (implies (normp x f)
           (equal (expo (ndecode x f))
                  (- (expf x f) (bias f)))))

Theorem: sig-ndecode

(defthm sig-ndecode
  (implies (normp x f)
           (equal (sig (ndecode x f))
                  (+ 1
                     (/ (manf x f)
                        (expt 2 (1- (prec f))))))))

Function: nrepp

(defun nrepp (x f)
  (declare (xargs :guard t))
  (and (rationalp x)
       (formatp f)
       (not (= x 0))
       (< 0 (+ (expo x) (bias f)))
       (< (+ (expo x) (bias f))
          (1- (expt 2 (expw f))))
       (exactp x (prec f))))

Function: nencode

(defun nencode (x f)
  (declare (xargs :guard (and (rationalp x)
                              (formatp f)
                              (exactp x (prec f)))))
  (cat (if (= (sgn x) 1) 0 1)
       1 (+ (expo x) (bias f))
       (expw f)
       (* (sig x) (expt 2 (1- (prec f))))
       (sigw f)))

Theorem: nrepp-ndecode

(defthm nrepp-ndecode
  (implies (normp x f)
           (nrepp (ndecode x f) f)))

Theorem: nencode-ndecode

(defthm nencode-ndecode
  (implies (normp x f)
           (equal (nencode (ndecode x f) f) x)))

Theorem: normp-nencode

(defthm normp-nencode
  (implies (nrepp x f)
           (normp (nencode x f) f)))

Theorem: ndecode-nencode

(defthm ndecode-nencode
  (implies (nrepp x f)
           (equal (ndecode (nencode x f) f) x)))

Function: spn

(defun spn (f)
  (declare (xargs :guard (formatp f)))
  (expt 2 (- 1 (bias f))))

Theorem: positive-spn

(defthm positive-spn
  (> (spn f) 0)
  :rule-classes (:linear))

Theorem: expo-spn

(defthm expo-spn
  (implies (formatp f)
           (equal (expo (spn f)) (- 1 (bias f)))))

Theorem: nrepp-spn

(defthm nrepp-spn
  (implies (formatp f) (nrepp (spn f) f)))

Theorem: smallest-spn

(defthm smallest-spn
  (implies (nrepp x f)
           (>= (abs x) (spn f)))
  :rule-classes ((:rewrite :match-free :once)))

Function: lpn

(defun lpn (f)
  (declare (xargs :guard (formatp f)))
  (* (expt 2 (- (expt 2 (expw f)) (+ 2 (bias f))))
     (- 2 (expt 2 (- 1 (prec f))))))

Theorem: positive-lpn

(defthm positive-lpn
  (implies (formatp f) (> (lpn f) 0))
  :rule-classes (:linear))

Theorem: expo-lpn

(defthm expo-lpn
  (implies (formatp f)
           (equal (expo (lpn f))
                  (- (expt 2 (expw f)) (+ 2 (bias f))))))

Theorem: sig-lpn

(defthm sig-lpn
  (implies (formatp f)
           (equal (sig (lpn f))
                  (- 2 (expt 2 (- 1 (prec f)))))))

Theorem: nrepp-lpn

(defthm nrepp-lpn
  (implies (formatp f) (nrepp (lpn f) f)))

Theorem: largest-lpn

(defthm largest-lpn
  (implies (nrepp x f) (<= x (lpn f)))
  :rule-classes ((:rewrite :match-free :once)))