		Search-engine friendly clone of the ACL2 documentation.

Rflag-specifications

General-sf-spec-fn

Signature
(general-sf-spec-fn result-nbits result) → *

General SF Specification (Source: Intel Manuals, Vol. 1, Section 3.4.3.1):

Sign flag Set equal to the most-significant bit of the result, which is the sign bit of a signed integer. (0 indicates a positive value and 1 indicates a negative value.)

Definitions and Theorems

Function: general-sf-spec-fn$inline

(defun general-sf-spec-fn$inline (result-nbits result)
  (declare (type (member 8 16 32 64) result-nbits)
           (type (integer 0 *) result))
  (declare (xargs :guard (unsigned-byte-p result-nbits result)))
  (mbe :logic (part-select result
                           :low (1- result-nbits)
                           :width 1)
       :exec (the (unsigned-byte 1)
                  (ash (if (eql result-nbits 64)
                           result
                         (the (unsigned-byte 50) result))
                       (the (integer -63 0)
                            (- (the (integer 0 63)
                                    (1- (the (integer 0 64)
                                             result-nbits)))))))))

Theorem: n01p-general-sf-spec-fn

(defthm n01p-general-sf-spec-fn
 (unsigned-byte-p 1
                  (general-sf-spec-fn result-nbits result))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary (bitp (general-sf-spec-fn result-nbits result))
     :hints
     (("Goal"
           :in-theory
           '(unsigned-byte-p integer-range-p natp bitp (:e expt)))))
  (:linear
   :corollary (and (<= 0
                       (general-sf-spec-fn result-nbits result))
                   (< (general-sf-spec-fn result-nbits result)
                      2))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))