		Search-engine friendly clone of the ACL2 documentation.

Div-spec

Div-spec-32

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

Definitions and Theorems

Function: div-spec-32

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

Theorem: n32-mv-nth-1-div-spec-32

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

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

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