(div-spec-16 dst src) → (mv * * *)
Function:
(defun div-spec-16 (dst src) (declare (type (unsigned-byte 32) dst) (type (unsigned-byte 16) src)) (declare (xargs :guard (not (equal src 0)))) (let ((__function__ 'div-spec-16)) (declare (ignorable __function__)) (b* ((dst (mbe :logic (n-size 32 dst) :exec dst)) (src (mbe :logic (n-size 16 src) :exec src)) (quotient (the (unsigned-byte 32) (floor dst src))) (remainder (the (unsigned-byte 16) (mod dst src))) (overflow? (< 65535 quotient)) ((when overflow?) (mv (list (cons 'quotient quotient) (cons 'remainder remainder)) 0 0))) (mv overflow? quotient remainder))))
Theorem:
(defthm n16-mv-nth-1-div-spec-16 (implies (not (mv-nth 0 (div-spec-16 dst src))) (unsigned-byte-p 16 (mv-nth 1 (div-spec-16 dst src)))) :rule-classes (:rewrite (:type-prescription :corollary (implies (not (mv-nth 0 (div-spec-16 dst src))) (natp (mv-nth 1 (div-spec-16 dst src)))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (implies (not (mv-nth 0 (div-spec-16 dst src))) (and (<= 0 (mv-nth 1 (div-spec-16 dst src))) (< (mv-nth 1 (div-spec-16 dst src)) 65536))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-2-div-spec-16 (implies (and (unsigned-byte-p 16 src) (< 0 src)) (unsigned-byte-p 16 (mv-nth 2 (div-spec-16 dst src)))) :rule-classes (:rewrite (:type-prescription :corollary (implies (and (unsigned-byte-p 16 src) (< 0 src)) (natp (mv-nth 2 (div-spec-16 dst src)))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (implies (and (unsigned-byte-p 16 src) (< 0 src)) (and (<= 0 (mv-nth 2 (div-spec-16 dst src))) (< (mv-nth 2 (div-spec-16 dst src)) 65536))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))