Update the |X86ISA|::|SF| field of a rflagsbits bit structure.
(!rflagsbits->sf sf x) → new-x
Function:
(defun !rflagsbits->sf$inline (sf x) (declare (xargs :guard (and (bitp sf) (rflagsbits-p x)))) (mbe :logic (b* ((sf (mbe :logic (bfix sf) :exec sf)) (x (rflagsbits-fix x))) (part-install sf x :width 1 :low 7)) :exec (the (unsigned-byte 32) (logior (the (unsigned-byte 32) (logand (the (unsigned-byte 32) x) (the (signed-byte 9) -129))) (the (unsigned-byte 8) (ash (the (unsigned-byte 1) sf) 7))))))
Theorem:
(defthm rflagsbits-p-of-!rflagsbits->sf (b* ((new-x (!rflagsbits->sf$inline sf x))) (rflagsbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !rflagsbits->sf$inline-of-bfix-sf (equal (!rflagsbits->sf$inline (bfix sf) x) (!rflagsbits->sf$inline sf x)))
Theorem:
(defthm !rflagsbits->sf$inline-bit-equiv-congruence-on-sf (implies (bit-equiv sf sf-equiv) (equal (!rflagsbits->sf$inline sf x) (!rflagsbits->sf$inline sf-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !rflagsbits->sf$inline-of-rflagsbits-fix-x (equal (!rflagsbits->sf$inline sf (rflagsbits-fix x)) (!rflagsbits->sf$inline sf x)))
Theorem:
(defthm !rflagsbits->sf$inline-rflagsbits-equiv-congruence-on-x (implies (rflagsbits-equiv x x-equiv) (equal (!rflagsbits->sf$inline sf x) (!rflagsbits->sf$inline sf x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !rflagsbits->sf-is-rflagsbits (equal (!rflagsbits->sf sf x) (change-rflagsbits x :sf sf)))
Theorem:
(defthm rflagsbits->sf-of-!rflagsbits->sf (b* ((?new-x (!rflagsbits->sf$inline sf x))) (equal (rflagsbits->sf new-x) (bfix sf))))
Theorem:
(defthm !rflagsbits->sf-equiv-under-mask (b* ((?new-x (!rflagsbits->sf$inline sf x))) (rflagsbits-equiv-under-mask new-x x -129)))