Update the |X86ISA|::|ATTR| field of a hidden-segment-registerbits bit structure.
(!hidden-segment-registerbits->attr attr x) → new-x
Function:
(defun !hidden-segment-registerbits->attr$inline (attr x) (declare (xargs :guard (and (16bits-p attr) (hidden-segment-registerbits-p x)))) (mbe :logic (b* ((attr (mbe :logic (16bits-fix attr) :exec attr)) (x (hidden-segment-registerbits-fix x))) (part-install attr x :width 16 :low 96)) :exec (the (unsigned-byte 112) (logior (the (unsigned-byte 112) (logand (the (unsigned-byte 112) x) (the (signed-byte 113) -5192217630372313364192902785269761))) (the (unsigned-byte 112) (ash (the (unsigned-byte 16) attr) 96))))))
Theorem:
(defthm hidden-segment-registerbits-p-of-!hidden-segment-registerbits->attr (b* ((new-x (!hidden-segment-registerbits->attr$inline attr x))) (hidden-segment-registerbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !hidden-segment-registerbits->attr$inline-of-16bits-fix-attr (equal (!hidden-segment-registerbits->attr$inline (16bits-fix attr) x) (!hidden-segment-registerbits->attr$inline attr x)))
Theorem:
(defthm !hidden-segment-registerbits->attr$inline-16bits-equiv-congruence-on-attr (implies (16bits-equiv attr attr-equiv) (equal (!hidden-segment-registerbits->attr$inline attr x) (!hidden-segment-registerbits->attr$inline attr-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !hidden-segment-registerbits->attr$inline-of-hidden-segment-registerbits-fix-x (equal (!hidden-segment-registerbits->attr$inline attr (hidden-segment-registerbits-fix x)) (!hidden-segment-registerbits->attr$inline attr x)))
Theorem:
(defthm !hidden-segment-registerbits->attr$inline-hidden-segment-registerbits-equiv-congruence-on-x (implies (hidden-segment-registerbits-equiv x x-equiv) (equal (!hidden-segment-registerbits->attr$inline attr x) (!hidden-segment-registerbits->attr$inline attr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !hidden-segment-registerbits->attr-is-hidden-segment-registerbits (equal (!hidden-segment-registerbits->attr attr x) (change-hidden-segment-registerbits x :attr attr)))
Theorem:
(defthm hidden-segment-registerbits->attr-of-!hidden-segment-registerbits->attr (b* ((?new-x (!hidden-segment-registerbits->attr$inline attr x))) (equal (hidden-segment-registerbits->attr new-x) (16bits-fix attr))))
Theorem:
(defthm !hidden-segment-registerbits->attr-equiv-under-mask (b* ((?new-x (!hidden-segment-registerbits->attr$inline attr x))) (hidden-segment-registerbits-equiv-under-mask new-x x 79228162514264337593543950335)))