Function:
(defun sse-cvt-int-to-fp (op mxcsr exp-width frac-width) (declare (type (unsigned-byte 32) mxcsr)) (declare (xargs :guard (and (integerp op) (posp exp-width) (posp frac-width)))) (let ((__function__ 'sse-cvt-int-to-fp)) (declare (ignorable __function__)) (b* ((mxcsr (mbe :logic (loghead 32 mxcsr) :exec mxcsr)) (rc (mbe :logic (part-select mxcsr :low 13 :high (1+ 13)) :exec (logand 3 (ash mxcsr (- 13))))) (bias (nfix (ec-call (rtl::bias (list nil (1+ frac-width) exp-width))))) (int-to-rat (rat-round op rc bias exp-width frac-width)) (sign (cond ((> int-to-rat 0) 0) ((< int-to-rat 0) 1) (t (if (int= rc 1) 1 0)))) (pe (not (= op int-to-rat))) (mxcsr (if pe (!mxcsrbits->pe 1 mxcsr) mxcsr)) (pm (equal (mxcsrbits->pm mxcsr) 1)) ((when (and pe (not pm))) (mv 'precision-exception-is-not-masked 0 mxcsr)) (fp-result (rat-to-fp int-to-rat sign nil nil nil rc exp-width frac-width))) (mv nil fp-result mxcsr))))
Theorem:
(defthm integerp-result-sse-cvt-int-to-fp (integerp (mv-nth 1 (sse-cvt-int-to-fp op mxcsr exp-width frac-width))) :rule-classes :type-prescription)
Theorem:
(defthm n32p-mxcsr-sse-cvt-int-to-fp (unsigned-byte-p 32 (mv-nth 2 (sse-cvt-int-to-fp op mxcsr exp-width frac-width))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (sse-cvt-int-to-fp op mxcsr exp-width frac-width))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (sse-cvt-int-to-fp op mxcsr exp-width frac-width))) (< (mv-nth 2 (sse-cvt-int-to-fp op mxcsr exp-width frac-width)) 4294967296)) :hints (("Goal" :in-theory (e/d* (unsigned-byte-p) nil))))))