Update the |X86ISA|::|OFFSET63-32| field of a interrupt/trap-gate-descriptorbits bit structure.
(!interrupt/trap-gate-descriptorbits->offset63-32 offset63-32 x) → new-x
Function:
(defun !interrupt/trap-gate-descriptorbits->offset63-32$inline (offset63-32 x) (declare (xargs :guard (and (32bits-p offset63-32) (interrupt/trap-gate-descriptorbits-p x)))) (mbe :logic (b* ((offset63-32 (mbe :logic (32bits-fix offset63-32) :exec offset63-32)) (x (interrupt/trap-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 interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->offset63-32 (b* ((new-x (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x))) (interrupt/trap-gate-descriptorbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset63-32$inline-of-32bits-fix-offset63-32 (equal (!interrupt/trap-gate-descriptorbits->offset63-32$inline (32bits-fix offset63-32) x) (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x)))
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset63-32$inline-32bits-equiv-congruence-on-offset63-32 (implies (32bits-equiv offset63-32 offset63-32-equiv) (equal (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x) (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset63-32$inline-of-interrupt/trap-gate-descriptorbits-fix-x (equal (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 (interrupt/trap-gate-descriptorbits-fix x)) (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x)))
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset63-32$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x (implies (interrupt/trap-gate-descriptorbits-equiv x x-equiv) (equal (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x) (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset63-32-is-interrupt/trap-gate-descriptorbits (equal (!interrupt/trap-gate-descriptorbits->offset63-32 offset63-32 x) (change-interrupt/trap-gate-descriptorbits x :offset63-32 offset63-32)))
Theorem:
(defthm interrupt/trap-gate-descriptorbits->offset63-32-of-!interrupt/trap-gate-descriptorbits->offset63-32 (b* ((?new-x (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x))) (equal (interrupt/trap-gate-descriptorbits->offset63-32 new-x) (32bits-fix offset63-32))))
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset63-32-equiv-under-mask (b* ((?new-x (!interrupt/trap-gate-descriptorbits->offset63-32$inline offset63-32 x))) (interrupt/trap-gate-descriptorbits-equiv-under-mask new-x x -79228162495817593519834398721)))