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