		Search-engine friendly clone of the ACL2 documentation.

Floating-point-comparison-specifications

Sse-cmp

Signature
(sse-cmp 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-cmp

(defun sse-cmp (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-cmp))
  (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 (equal (mxcsrbits->daz mxcsr) 1))
       ((mv kind1 exp1 frac1)
        (sse-daz kind1 exp1 frac1 daz))
       ((mv kind2 exp2 frac2)
        (sse-daz kind2 exp2 frac2 daz))
       ((mv special-ok result invalid)
        (sse-cmp-special kind1 sign1 kind2
                         sign2 exp-width frac-width operation))
       (mxcsr (if invalid (!mxcsrbits->ie 1 mxcsr)
                mxcsr))
       (im (equal (mxcsrbits->im mxcsr) 1))
       ((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 (equal (mxcsrbits->dm mxcsr) 1))
       ((when (and de (not dm)))
        (mv 'denormal-operand-exception-is-not-masked
            0 mxcsr)))
   (if special-ok (mv nil result 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))
      (cmp-result (case operation
                    (0 (= rat1 rat2))
                    (1 (< rat1 rat2))
                    (2 (<= rat1 rat2))
                    (3 nil)
                    (4 (not (= rat1 rat2)))
                    (5 (not (< rat1 rat2)))
                    (6 (not (<= rat1 rat2)))
                    (7 t)
                    (otherwise nil)))
      (result
           (if (or (int= operation 8)
                   (int= operation 9))
               (cond ((> rat1 rat2) 0)
                     ((< rat1 rat2) 1)
                     (t 4))
             (if cmp-result (1- (ash 1 (+ 1 exp-width frac-width)))
               0))))
     (mv nil result mxcsr))))))

Theorem: integerp-result-sse-cmp

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

Theorem: n32p-mxcsr-sse-cmp

(defthm n32p-mxcsr-sse-cmp
 (unsigned-byte-p
      32
      (mv-nth 2
              (sse-cmp operation
                       op1 op2 mxcsr exp-width frac-width)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (natp (mv-nth 2
                    (sse-cmp 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-cmp operation
                             op1 op2 mxcsr exp-width frac-width)))
        (< (mv-nth 2
                   (sse-cmp operation
                            op1 op2 mxcsr exp-width frac-width))
           4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))