(gpr-and-spec-2 dst src input-rflags) → (mv * * *)
Function:
(defun gpr-and-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)) ((the (unsigned-byte 16) result) (mbe :logic (part-select (logand dst src) :low 0 :width 16) :exec (logand dst src))) (cf 0) (pf (the (unsigned-byte 1) (pf-spec16 result))) (zf (the (unsigned-byte 1) (zf-spec result))) (sf (the (unsigned-byte 1) (sf-spec16 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 n16-mv-nth-0-gpr-and-spec-2 (unsigned-byte-p 16 (mv-nth 0 (gpr-and-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 0 (gpr-and-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-and-spec-2 dst src input-rflags))) (< (mv-nth 0 (gpr-and-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-and-spec-2 (unsigned-byte-p 32 (mv-nth 1 (gpr-and-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (gpr-and-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-and-spec-2 dst src input-rflags))) (< (mv-nth 1 (gpr-and-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-and-spec-2 (unsigned-byte-p 32 (mv-nth 2 (gpr-and-spec-2 dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (gpr-and-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-and-spec-2 dst src input-rflags))) (< (mv-nth 2 (gpr-and-spec-2 dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))