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