		Search-engine friendly clone of the ACL2 documentation.

Floating-point-arithmetic-specifications

Sse-max/min

Signature
(sse-max/min operation op1 op2 mxcsr exp-width frac-width) → (mv * * *)
Arguments: op1 — Guard (natp op1).; op2 — Guard (natp op2).; exp-width — Guard (posp exp-width).; frac-width — Guard (posp frac-width).

Definitions and Theorems

Function: sse-max/min

(defun sse-max/min (operation op1 op2 mxcsr exp-width frac-width)
 (declare (type (integer 0 38) operation)
          (type (unsigned-byte 32) mxcsr))
 (declare (xargs :guard (and (natp op1)
                             (natp op2)
                             (posp exp-width)
                             (posp frac-width))))
 (let ((__function__ 'sse-max/min))
  (declare (ignorable __function__))
  (b* ((mxcsr (mbe :logic (loghead 32 mxcsr)
                   :exec mxcsr))
       ((mv kind1 sign1 exp1 implicit1 frac1)
        (fp-decode op1 exp-width frac-width))
       ((mv kind2 sign2 exp2 implicit2 frac2)
        (fp-decode op2 exp-width frac-width))
       (daz (logbitp 6 mxcsr))
       ((mv kind1 exp1 frac1)
        (sse-daz kind1 exp1 frac1 daz))
       ((mv kind2 exp2 frac2)
        (sse-daz kind2 exp2 frac2 daz))
       ((mv special-ok sign exp & frac invalid)
        (sse-max/min-special kind1 sign1 exp1 implicit1 frac1 kind2
                             sign2 exp2 implicit2 frac2 operation))
       (mxcsr (if invalid (!mxcsrbits->ie 1 mxcsr)
                mxcsr))
       (im (logbitp 7 mxcsr))
       ((when (and invalid (not im)))
        (mv 'invalid-operand-exception-is-not-masked
            0 mxcsr))
       (de (denormal-exception kind1 kind2))
       (mxcsr (if de (!mxcsrbits->de 1 mxcsr) mxcsr))
       (dm (logbitp 8 mxcsr))
       ((when (and de (not dm)))
        (mv 'denormal-operand-exception-is-not-masked
            0 mxcsr)))
   (if special-ok
       (mv nil
           (fp-encode-integer sign exp frac exp-width frac-width)
           mxcsr)
    (b*
     ((bias
       (nfix
        (ec-call (rtl::bias (list nil (1+ frac-width) exp-width)))))
      (rat1 (fp-to-rat sign1
                       exp1 frac1 bias exp-width frac-width))
      (rat2 (fp-to-rat sign2
                       exp2 frac2 bias exp-width frac-width))
      (rat (case operation
             (34 (if (> rat1 rat2) rat1 rat2))
             (36 (if (< rat1 rat2) rat1 rat2))
             (otherwise 0)))
      (sign (sse-max/min-sign rat rat1 sign1 sign2))
      (fp-result (rat-to-fp rat sign
                            nil nil nil 0 exp-width frac-width)))
     (mv nil fp-result mxcsr))))))

Theorem: integerp-result-sse-max/min

(defthm integerp-result-sse-max/min
  (integerp
       (mv-nth 1
               (sse-max/min operation
                            op1 op2 mxcsr exp-width frac-width)))
  :rule-classes :type-prescription)

Theorem: n32p-mxcsr-sse-max/min

(defthm n32p-mxcsr-sse-max/min
 (unsigned-byte-p
      32
      (mv-nth 2
              (sse-max/min operation
                           op1 op2 mxcsr exp-width frac-width)))
 :rule-classes
 (:rewrite
  (:type-prescription
    :corollary
    (natp (mv-nth 2
                  (sse-max/min operation
                               op1 op2 mxcsr exp-width frac-width)))
    :hints
    (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
      (<= 0
          (mv-nth 2
                  (sse-max/min operation
                               op1 op2 mxcsr exp-width frac-width)))
      (< (mv-nth 2
                 (sse-max/min operation
                              op1 op2 mxcsr exp-width frac-width))
         4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))