(dp-sse-cvt-fp-to-int nbytes op mxcsr trunc) → (mv * * *)
Function:
(defun dp-sse-cvt-fp-to-int (nbytes op mxcsr trunc) (declare (type (integer 0 *) nbytes) (type (unsigned-byte 64) op) (type (unsigned-byte 32) mxcsr)) (declare (xargs :guard (booleanp trunc))) (let ((__function__ 'dp-sse-cvt-fp-to-int)) (declare (ignorable __function__)) (b* (((mv flg result mxcsr) (sse-cvt-fp-to-int nbytes op mxcsr trunc 11 52)) (result (trunc nbytes result))) (mv flg result mxcsr))))
Theorem:
(defthm bytesp-dp-sse-cvt-fp-to-int-1 (implies (and (natp nbytes) (member nbytes '(1 2 4 8 16))) (unsigned-byte-p (ash nbytes 3) (mv-nth 1 (dp-sse-cvt-fp-to-int nbytes op mxcsr trunc)))))
Theorem:
(defthm n32p-mxcsr-dp-sse-cvt-fp-to-int (unsigned-byte-p 32 (mv-nth 2 (dp-sse-cvt-fp-to-int nbytes op mxcsr trunc))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (dp-sse-cvt-fp-to-int nbytes op mxcsr trunc))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (dp-sse-cvt-fp-to-int nbytes op mxcsr trunc))) (< (mv-nth 2 (dp-sse-cvt-fp-to-int nbytes op mxcsr trunc)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))