		Search-engine friendly clone of the ACL2 documentation.

Shrx-spec

Shrx-spec-64

Signature
(shrx-spec-64 src cnt) → *

Definitions and Theorems

Function: shrx-spec-64

(defun shrx-spec-64 (src cnt)
  (declare (type (unsigned-byte 64) src)
           (type (unsigned-byte 6) cnt))
  (let ((__function__ 'shrx-spec-64))
    (declare (ignorable __function__))
    (b* ((src (mbe :logic (n-size 64 src) :exec src))
         (cnt (mbe :logic (n-size 6 cnt) :exec cnt))
         (neg-cnt (the (signed-byte 65) (- cnt)))
         (raw-result (the (unsigned-byte 64)
                          (ash (the (unsigned-byte 64) src)
                               (the (signed-byte 65) neg-cnt))))
         (result (the (unsigned-byte 64)
                      (n-size 64 raw-result))))
      result)))

Theorem: n64-shrx-spec-64

(defthm n64-shrx-spec-64
 (unsigned-byte-p 64 (shrx-spec-64 src cnt))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (shrx-spec-64 src cnt))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (shrx-spec-64 src cnt))
                   (< (shrx-spec-64 src cnt)
                      18446744073709551616))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))