Update the |X86ISA|::|OFFSET31-16| field of a call-gate-descriptorbits bit structure.
(!call-gate-descriptorbits->offset31-16 offset31-16 x) → new-x
Function:
(defun !call-gate-descriptorbits->offset31-16$inline (offset31-16 x) (declare (xargs :guard (and (16bits-p offset31-16) (call-gate-descriptorbits-p x)))) (mbe :logic (b* ((offset31-16 (mbe :logic (16bits-fix offset31-16) :exec offset31-16)) (x (call-gate-descriptorbits-fix x))) (part-install offset31-16 x :width 16 :low 48)) :exec (the (unsigned-byte 128) (logior (the (unsigned-byte 128) (logand (the (unsigned-byte 128) x) (the (signed-byte 65) -18446462598732840961))) (the (unsigned-byte 64) (ash (the (unsigned-byte 16) offset31-16) 48))))))
Theorem:
(defthm call-gate-descriptorbits-p-of-!call-gate-descriptorbits->offset31-16 (b* ((new-x (!call-gate-descriptorbits->offset31-16$inline offset31-16 x))) (call-gate-descriptorbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !call-gate-descriptorbits->offset31-16$inline-of-16bits-fix-offset31-16 (equal (!call-gate-descriptorbits->offset31-16$inline (16bits-fix offset31-16) x) (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)))
Theorem:
(defthm !call-gate-descriptorbits->offset31-16$inline-16bits-equiv-congruence-on-offset31-16 (implies (16bits-equiv offset31-16 offset31-16-equiv) (equal (!call-gate-descriptorbits->offset31-16$inline offset31-16 x) (!call-gate-descriptorbits->offset31-16$inline offset31-16-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptorbits->offset31-16$inline-of-call-gate-descriptorbits-fix-x (equal (!call-gate-descriptorbits->offset31-16$inline offset31-16 (call-gate-descriptorbits-fix x)) (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)))
Theorem:
(defthm !call-gate-descriptorbits->offset31-16$inline-call-gate-descriptorbits-equiv-congruence-on-x (implies (call-gate-descriptorbits-equiv x x-equiv) (equal (!call-gate-descriptorbits->offset31-16$inline offset31-16 x) (!call-gate-descriptorbits->offset31-16$inline offset31-16 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptorbits->offset31-16-is-call-gate-descriptorbits (equal (!call-gate-descriptorbits->offset31-16 offset31-16 x) (change-call-gate-descriptorbits x :offset31-16 offset31-16)))
Theorem:
(defthm call-gate-descriptorbits->offset31-16-of-!call-gate-descriptorbits->offset31-16 (b* ((?new-x (!call-gate-descriptorbits->offset31-16$inline offset31-16 x))) (equal (call-gate-descriptorbits->offset31-16 new-x) (16bits-fix offset31-16))))
Theorem:
(defthm !call-gate-descriptorbits->offset31-16-equiv-under-mask (b* ((?new-x (!call-gate-descriptorbits->offset31-16$inline offset31-16 x))) (call-gate-descriptorbits-equiv-under-mask new-x x -18446462598732840961)))