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