(gpr-sbb-spec-2 dst src input-rflags) → (mv * * *)
Function:
(defun gpr-sbb-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)) (input-cf (the (unsigned-byte 1) (rflagsbits->cf input-rflags))) (signed-raw-result (the (signed-byte 18) (- (the (signed-byte 16) (n16-to-i16 dst)) (the (signed-byte 17) (+ (the (signed-byte 16) (n16-to-i16 src)) input-cf))))) (result (the (unsigned-byte 16) (n-size 16 signed-raw-result))) (cf (the (unsigned-byte 1) (bool->bit (< dst (the (unsigned-byte 17) (+ input-cf src)))))) (pf (the (unsigned-byte 1) (pf-spec16 result))) (af (the (unsigned-byte 1) (sbb-af-spec16 dst src input-cf))) (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-sbb-spec-2 (unsigned-byte-p 16 (mv-nth 0 (gpr-sbb-spec-2 dst src cf))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 0 (gpr-sbb-spec-2 dst src cf))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 0 (gpr-sbb-spec-2 dst src cf))) (< (mv-nth 0 (gpr-sbb-spec-2 dst src cf)) 65536)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-1-gpr-sbb-spec-2 (unsigned-byte-p 32 (mv-nth 1 (gpr-sbb-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (gpr-sbb-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-sbb-spec-2 dst src input-rflags))) (< (mv-nth 1 (gpr-sbb-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-sbb-spec-2 (unsigned-byte-p 32 (mv-nth 2 (gpr-sbb-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (gpr-sbb-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-sbb-spec-2 dst src input-rflags))) (< (mv-nth 2 (gpr-sbb-spec-2 dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))