		Search-engine friendly clone of the ACL2 documentation.

Idiv-spec

Idiv-spec-16

Signature
(idiv-spec-16 dst src) → (mv * * *)

Definitions and Theorems

Function: idiv-spec-16

(defun idiv-spec-16 (dst src)
  (declare (type (unsigned-byte 32) dst)
           (type (unsigned-byte 16) src))
  (declare (xargs :guard (not (equal src 0))))
  (let ((__function__ 'idiv-spec-16))
    (declare (ignorable __function__))
    (b* ((dst-int (the (signed-byte 32) (ntoi 32 dst)))
         (src-int (the (signed-byte 16) (ntoi 16 src)))
         (quotient-int (the (signed-byte 33)
                            (truncate dst-int src-int)))
         (remainder-int (the (signed-byte 16)
                             (rem dst-int src-int)))
         (overflow? (or (< (the (signed-byte 33) quotient-int)
                           -32768)
                        (< 32767
                           (the (signed-byte 33) quotient-int))))
         ((when overflow?)
          (mv (list (cons 'quotient-int quotient-int)
                    (cons 'remainder-int remainder-int))
              0 0))
         (quotient (the (unsigned-byte 16)
                        (n-size 16 quotient-int)))
         (remainder (the (unsigned-byte 16)
                         (n-size 16 remainder-int))))
      (mv overflow? quotient remainder))))

Theorem: n16-mv-nth-1-idiv-spec-16

(defthm n16-mv-nth-1-idiv-spec-16
 (implies (not (mv-nth 0 (idiv-spec-16 dst src)))
          (unsigned-byte-p 16 (mv-nth 1 (idiv-spec-16 dst src))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (not (mv-nth 0 (idiv-spec-16 dst src)))
                          (natp (mv-nth 1 (idiv-spec-16 dst src))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (implies (not (mv-nth 0 (idiv-spec-16 dst src)))
                       (and (<= 0 (mv-nth 1 (idiv-spec-16 dst src)))
                            (< (mv-nth 1 (idiv-spec-16 dst src))
                               65536)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: mv-nth-2-idiv-spec-16

(defthm mv-nth-2-idiv-spec-16
 (implies (and (unsigned-byte-p 16 src) (< 0 src))
          (unsigned-byte-p 16 (mv-nth 2 (idiv-spec-16 dst src))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (and (unsigned-byte-p 16 src) (< 0 src))
                          (natp (mv-nth 2 (idiv-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 (idiv-spec-16 dst src)))
                            (< (mv-nth 2 (idiv-spec-16 dst src))
                               65536)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))