		Search-engine friendly clone of the ACL2 documentation.

Sarx-spec

Sarx-spec-32

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

Definitions and Theorems

Function: sarx-spec-32

(defun sarx-spec-32 (src cnt)
 (declare (type (unsigned-byte 32) src)
          (type (unsigned-byte 6) cnt))
 (let ((__function__ 'sarx-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
     (if
      (eql (mbe :logic (logbit 31 src)
                :exec (logand 1
                              (the (unsigned-byte 1)
                                   (ash (the (unsigned-byte 32) src)
                                        -31))))
           1)
      (loghead 32
               (ash (mbe :logic (logext 32 src)
                         :exec (fast-logext 32 src))
                    neg-cnt))
      (the (unsigned-byte 32)
           (ash (the (unsigned-byte 32) src)
                (the (signed-byte 33) neg-cnt)))))
    (result (mbe :logic (n-size 32 raw-result)
                 :exec raw-result)))
   result)))

Theorem: n32-sarx-spec-32

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