		Search-engine friendly clone of the ACL2 documentation.

Gpr-arith/logic-spec-8

Gpr-adcx/adox-spec-8

Signature
(gpr-adcx/adox-spec-8 adcx dst src input-rflags) → (mv * * *)
Arguments: adcx — Guard (booleanp adcx).

Definitions and Theorems

Function: gpr-adcx/adox-spec-8$inline

(defun gpr-adcx/adox-spec-8$inline (adcx dst src input-rflags)
 (declare (type (unsigned-byte 64) dst)
          (type (unsigned-byte 64) src)
          (type (unsigned-byte 32) input-rflags))
 (declare (xargs :guard (booleanp adcx)))
 (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))
   (input-cf (the (unsigned-byte 1)
                  (if adcx (rflagsbits->cf input-rflags)
                    (rflagsbits->of input-rflags))))
   (raw-result (the (unsigned-byte 65)
                    (+ (the (unsigned-byte 64) dst)
                       (the (unsigned-byte 64) src)
                       (the (unsigned-byte 1) input-cf))))
   (result (the (unsigned-byte 64)
                (n-size 64 raw-result)))
   (cf (the (unsigned-byte 1)
            (cf-spec64 raw-result)))
   (output-rflags
        (if adcx (mbe :logic (change-rflagsbits input-rflags :cf cf)
                      :exec (the (unsigned-byte 32)
                                 (!rflagsbits->cf cf input-rflags)))
          (mbe :logic (change-rflagsbits input-rflags :of cf)
               :exec (the (unsigned-byte 32)
                          (!rflagsbits->of cf 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-adcx/adox-spec-8

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

Theorem: mv-nth-1-gpr-adcx/adox-spec-8

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

Theorem: mv-nth-2-gpr-adcx/adox-spec-8

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