		Search-engine friendly clone of the ACL2 documentation.

Shrx-spec

Shrx-spec-32

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

Definitions and Theorems

Function: shrx-spec-32

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

Theorem: n32-shrx-spec-32

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