(imul-spec-32 dst src) → (mv * * * *)
Function:
(defun imul-spec-32 (dst src) (declare (type (unsigned-byte 32) dst) (type (unsigned-byte 32) src)) (let ((__function__ 'imul-spec-32)) (declare (ignorable __function__)) (b* ((dst-int (the (signed-byte 32) (ntoi 32 dst))) (src-int (the (signed-byte 32) (ntoi 32 src))) (product-int (the (signed-byte 64) (* (the (signed-byte 32) dst-int) (the (signed-byte 32) src-int)))) (product (the (unsigned-byte 64) (n-size 64 product-int))) (product-high (mbe :logic (part-select product :low 32 :width 32) :exec (the (unsigned-byte 32) (ash (the (unsigned-byte 64) product) -32)))) (product-low (mbe :logic (part-select product :low 0 :width 32) :exec (the (unsigned-byte 32) (logand 4294967295 product)))) (product-low-int (the (signed-byte 32) (ntoi 32 product-low))) (cf-and-of (the (unsigned-byte 1) (bool->bit (not (equal (the (signed-byte 32) product-low-int) (the (signed-byte 64) product-int))))))) (mv product-high product-low product cf-and-of))))
Theorem:
(defthm n32-mv-nth-0-imul-spec-32 (unsigned-byte-p 32 (mv-nth 0 (imul-spec-32 dst src))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 0 (imul-spec-32 dst src))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 0 (imul-spec-32 dst src))) (< (mv-nth 0 (imul-spec-32 dst src)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-1-imul-spec-32 (unsigned-byte-p 32 (mv-nth 1 (imul-spec-32 dst src))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (imul-spec-32 dst src))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (imul-spec-32 dst src))) (< (mv-nth 1 (imul-spec-32 dst src)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-2-imul-spec-32 (unsigned-byte-p 64 (mv-nth 2 (imul-spec-32 dst src))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (imul-spec-32 dst src))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (imul-spec-32 dst src))) (< (mv-nth 2 (imul-spec-32 dst src)) 18446744073709551616)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-3-imul-spec-32 (unsigned-byte-p 1 (mv-nth 3 (imul-spec-32 dst src))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 3 (imul-spec-32 dst src))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 3 (imul-spec-32 dst src))) (< (mv-nth 3 (imul-spec-32 dst src)) 2)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))