		Search-engine friendly clone of the ACL2 documentation.

Shlx-spec

Shlx-spec-64

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

Definitions and Theorems

Function: shlx-spec-64

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

Theorem: n64-shlx-spec-64

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