		Search-engine friendly clone of the ACL2 documentation.

Gpr-arith/logic-spec-8

Gpr-xadd-spec-8

Signature
(gpr-xadd-spec-8 dst src input-rflags) → (mv * * *)

Definitions and Theorems

Function: gpr-xadd-spec-8$inline

(defun gpr-xadd-spec-8$inline (dst src input-rflags)
 (declare (type (unsigned-byte 64) dst)
          (type (unsigned-byte 64) src)
          (type (unsigned-byte 32) input-rflags))
 (b*
  ((dst (mbe :logic (n-size 64 dst) :exec dst))
   (src (mbe :logic (n-size 64 src) :exec src))
   (input-rflags (mbe :logic (n32 input-rflags)
                      :exec input-rflags))
   (raw-result (the (unsigned-byte 65)
                    (+ (the (unsigned-byte 64) dst)
                       (the (unsigned-byte 64) src))))
   (signed-raw-result
        (the (signed-byte 65)
             (+ (the (signed-byte 64) (n64-to-i64 dst))
                (the (signed-byte 64)
                     (n64-to-i64 src)))))
   (result (the (unsigned-byte 64)
                (n-size 64 raw-result)))
   (cf (the (unsigned-byte 1)
            (cf-spec64 raw-result)))
   (pf (the (unsigned-byte 1)
            (pf-spec64 result)))
   (af (the (unsigned-byte 1)
            (add-af-spec64 dst src)))
   (zf (the (unsigned-byte 1)
            (zf-spec result)))
   (sf (the (unsigned-byte 1)
            (sf-spec64 result)))
   (of (the (unsigned-byte 1)
            (of-spec64 signed-raw-result)))
   (output-rflags
    (mbe
     :logic (change-rflagsbits input-rflags
                               :cf cf
                               :pf pf
                               :af af
                               :zf zf
                               :sf sf
                               :of of)
     :exec
     (the
      (unsigned-byte 32)
      (!rflagsbits->cf
       cf
       (!rflagsbits->pf
        pf
        (!rflagsbits->af
         af
         (!rflagsbits->zf
          zf
          (!rflagsbits->sf sf
                           (!rflagsbits->of of input-rflags)))))))))
   (output-rflags (mbe :logic (n32 output-rflags)
                       :exec output-rflags))
   (undefined-flags 0))
  (mv result output-rflags undefined-flags)))

Theorem: n64-mv-nth-0-gpr-xadd-spec-8

(defthm n64-mv-nth-0-gpr-xadd-spec-8
 (unsigned-byte-p 64
                  (mv-nth 0
                          (gpr-xadd-spec-8 dst src input-rflags)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary (natp (mv-nth 0
                            (gpr-xadd-spec-8 dst src input-rflags)))
   :hints
   (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 0
                    (gpr-xadd-spec-8 dst src input-rflags)))
        (< (mv-nth 0
                   (gpr-xadd-spec-8 dst src input-rflags))
           18446744073709551616))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: mv-nth-1-gpr-xadd-spec-8

(defthm mv-nth-1-gpr-xadd-spec-8
 (unsigned-byte-p 32
                  (mv-nth 1
                          (gpr-xadd-spec-8 dst src input-rflags)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary (natp (mv-nth 1
                            (gpr-xadd-spec-8 dst src input-rflags)))
   :hints
   (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 1
                    (gpr-xadd-spec-8 dst src input-rflags)))
        (< (mv-nth 1
                   (gpr-xadd-spec-8 dst src input-rflags))
           4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: mv-nth-2-gpr-xadd-spec-8

(defthm mv-nth-2-gpr-xadd-spec-8
 (unsigned-byte-p 32
                  (mv-nth 2
                          (gpr-xadd-spec-8 dst src input-rflags)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary (natp (mv-nth 2
                            (gpr-xadd-spec-8 dst src input-rflags)))
   :hints
   (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 2
                    (gpr-xadd-spec-8 dst src input-rflags)))
        (< (mv-nth 2
                   (gpr-xadd-spec-8 dst src input-rflags))
           4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))