		Search-engine friendly clone of the ACL2 documentation.

Shlx-spec

Shlx-spec-32

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

Definitions and Theorems

Function: shlx-spec-32

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

Theorem: n32-shlx-spec-32

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