		Search-engine friendly clone of the ACL2 documentation.

Rflag-specifications

General-pf-spec-fn

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

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

Parity flag Set if the least-significant byte of the result contains an even number of 1 bits; cleared otherwise.

Definitions and Theorems

Function: general-pf-spec-fn$inline

(defun general-pf-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
  (bool->bit (not (logbitp 0 (logcount (loghead 8 result)))))
  :exec
  (if
   (eql
    (logand
      1
      (the (integer 0 8)
           (bitcount8
                (the (unsigned-byte 8)
                     (logand 255
                             (if (eql result-nbits 64)
                                 result
                               (the (unsigned-byte 32) result)))))))
    0)
   1
   0)))

Theorem: n01p-general-pf-spec-fn

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