(gpr-xadd-spec-2 dst src input-rflags) → (mv * * *)
Function:
(defun gpr-xadd-spec-2$inline (dst src input-rflags) (declare (type (unsigned-byte 16) dst) (type (unsigned-byte 16) src) (type (unsigned-byte 32) input-rflags)) (b* ((dst (mbe :logic (n-size 16 dst) :exec dst)) (src (mbe :logic (n-size 16 src) :exec src)) (input-rflags (mbe :logic (n32 input-rflags) :exec input-rflags)) (raw-result (the (unsigned-byte 17) (+ (the (unsigned-byte 16) dst) (the (unsigned-byte 16) src)))) (signed-raw-result (the (signed-byte 17) (+ (the (signed-byte 16) (n16-to-i16 dst)) (the (signed-byte 16) (n16-to-i16 src))))) (result (the (unsigned-byte 16) (n-size 16 raw-result))) (cf (the (unsigned-byte 1) (cf-spec16 raw-result))) (pf (the (unsigned-byte 1) (pf-spec16 result))) (af (the (unsigned-byte 1) (add-af-spec16 dst src))) (zf (the (unsigned-byte 1) (zf-spec result))) (sf (the (unsigned-byte 1) (sf-spec16 result))) (of (the (unsigned-byte 1) (of-spec16 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:
(defthm n16-mv-nth-0-gpr-xadd-spec-2 (unsigned-byte-p 16 (mv-nth 0 (gpr-xadd-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 0 (gpr-xadd-spec-2 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-2 dst src input-rflags))) (< (mv-nth 0 (gpr-xadd-spec-2 dst src input-rflags)) 65536)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-1-gpr-xadd-spec-2 (unsigned-byte-p 32 (mv-nth 1 (gpr-xadd-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (gpr-xadd-spec-2 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-2 dst src input-rflags))) (< (mv-nth 1 (gpr-xadd-spec-2 dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-2-gpr-xadd-spec-2 (unsigned-byte-p 32 (mv-nth 2 (gpr-xadd-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (gpr-xadd-spec-2 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-2 dst src input-rflags))) (< (mv-nth 2 (gpr-xadd-spec-2 dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))