		Search-engine friendly clone of the ACL2 documentation.

Sarx-spec

Sarx-spec-64

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

Definitions and Theorems

Function: sarx-spec-64

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

Theorem: n64-sarx-spec-64

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