(gpr-xor-spec-1 dst src input-rflags) → (mv * * *)
Function:
(defun gpr-xor-spec-1$inline (dst src input-rflags) (declare (type (unsigned-byte 8) dst) (type (unsigned-byte 8) src) (type (unsigned-byte 32) input-rflags)) (b* ((dst (mbe :logic (n-size 8 dst) :exec dst)) (src (mbe :logic (n-size 8 src) :exec src)) (input-rflags (mbe :logic (n32 input-rflags) :exec input-rflags)) ((the (unsigned-byte 8) result) (mbe :logic (part-select (logxor dst src) :low 0 :width 8) :exec (logxor dst src))) (cf 0) (pf (the (unsigned-byte 1) (pf-spec8 result))) (zf (the (unsigned-byte 1) (zf-spec result))) (sf (the (unsigned-byte 1) (sf-spec8 result))) (of 0) (output-rflags (mbe :logic (change-rflagsbits input-rflags :cf cf :pf pf :zf zf :sf sf :of of) :exec (the (unsigned-byte 32) (!rflagsbits->cf cf (!rflagsbits->pf pf (!rflagsbits->zf zf (!rflagsbits->sf sf (!rflagsbits->of of input-rflags)))))))) (output-rflags (mbe :logic (n32 output-rflags) :exec output-rflags)) (undefined-flags (!rflagsbits->af 1 0))) (mv result output-rflags undefined-flags)))
Theorem:
(defthm n08-mv-nth-0-gpr-xor-spec-1 (unsigned-byte-p 8 (mv-nth 0 (gpr-xor-spec-1 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 0 (gpr-xor-spec-1 dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 0 (gpr-xor-spec-1 dst src input-rflags))) (< (mv-nth 0 (gpr-xor-spec-1 dst src input-rflags)) 256)) :hints (("Goal" :in-theory (e/d (unsigned-byte-p) (unsigned-byte-p-of-logxor)))))))
Theorem:
(defthm mv-nth-1-gpr-xor-spec-1 (unsigned-byte-p 32 (mv-nth 1 (gpr-xor-spec-1 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (gpr-xor-spec-1 dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (gpr-xor-spec-1 dst src input-rflags))) (< (mv-nth 1 (gpr-xor-spec-1 dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm mv-nth-2-gpr-xor-spec-1 (unsigned-byte-p 32 (mv-nth 2 (gpr-xor-spec-1 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (gpr-xor-spec-1 dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (gpr-xor-spec-1 dst src input-rflags))) (< (mv-nth 2 (gpr-xor-spec-1 dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))