		Search-engine friendly clone of the ACL2 documentation.

Div-spec

Div-spec-64

Signature
(div-spec-64 dst src) → (mv * * *)

Definitions and Theorems

Function: div-spec-64

(defun div-spec-64 (dst src)
  (declare (type (unsigned-byte 128) dst)
           (type (unsigned-byte 64) src))
  (declare (xargs :guard (not (equal src 0))))
  (let ((__function__ 'div-spec-64))
    (declare (ignorable __function__))
    (b* ((dst (mbe :logic (n-size 128 dst) :exec dst))
         (src (mbe :logic (n-size 64 src) :exec src))
         (quotient (the (unsigned-byte 128)
                        (floor dst src)))
         (remainder (the (unsigned-byte 64) (mod dst src)))
         (overflow? (< 18446744073709551615 quotient))
         ((when overflow?)
          (mv (list (cons 'quotient quotient)
                    (cons 'remainder remainder))
              0 0)))
      (mv overflow? quotient remainder))))

Theorem: n64-mv-nth-1-div-spec-64

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

Theorem: mv-nth-2-div-spec-64

(defthm mv-nth-2-div-spec-64
 (implies (and (unsigned-byte-p 64 src) (< 0 src))
          (unsigned-byte-p 64 (mv-nth 2 (div-spec-64 dst src))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (and (unsigned-byte-p 64 src) (< 0 src))
                          (natp (mv-nth 2 (div-spec-64 dst src))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (implies (and (unsigned-byte-p 64 src) (< 0 src))
                       (and (<= 0 (mv-nth 2 (div-spec-64 dst src)))
                            (< (mv-nth 2 (div-spec-64 dst src))
                               18446744073709551616)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))