Update the |X86ISA|::|OFFSET15-0| field of a interrupt/trap-gate-descriptorbits bit structure.
(!interrupt/trap-gate-descriptorbits->offset15-0 offset15-0 x) → new-x
Function:
(defun !interrupt/trap-gate-descriptorbits->offset15-0$inline (offset15-0 x) (declare (xargs :guard (and (16bits-p offset15-0) (interrupt/trap-gate-descriptorbits-p x)))) (mbe :logic (b* ((offset15-0 (mbe :logic (16bits-fix offset15-0) :exec offset15-0)) (x (interrupt/trap-gate-descriptorbits-fix x))) (part-install offset15-0 x :width 16 :low 0)) :exec (the (unsigned-byte 128) (logior (the (unsigned-byte 128) (logand (the (unsigned-byte 128) x) (the (signed-byte 17) -65536))) (the (unsigned-byte 16) offset15-0)))))
Theorem:
(defthm interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->offset15-0 (b* ((new-x (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x))) (interrupt/trap-gate-descriptorbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset15-0$inline-of-16bits-fix-offset15-0 (equal (!interrupt/trap-gate-descriptorbits->offset15-0$inline (16bits-fix offset15-0) x) (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x)))
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset15-0$inline-16bits-equiv-congruence-on-offset15-0 (implies (16bits-equiv offset15-0 offset15-0-equiv) (equal (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x) (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset15-0$inline-of-interrupt/trap-gate-descriptorbits-fix-x (equal (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 (interrupt/trap-gate-descriptorbits-fix x)) (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x)))
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset15-0$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x (implies (interrupt/trap-gate-descriptorbits-equiv x x-equiv) (equal (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x) (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset15-0-is-interrupt/trap-gate-descriptorbits (equal (!interrupt/trap-gate-descriptorbits->offset15-0 offset15-0 x) (change-interrupt/trap-gate-descriptorbits x :offset15-0 offset15-0)))
Theorem:
(defthm interrupt/trap-gate-descriptorbits->offset15-0-of-!interrupt/trap-gate-descriptorbits->offset15-0 (b* ((?new-x (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x))) (equal (interrupt/trap-gate-descriptorbits->offset15-0 new-x) (16bits-fix offset15-0))))
Theorem:
(defthm !interrupt/trap-gate-descriptorbits->offset15-0-equiv-under-mask (b* ((?new-x (!interrupt/trap-gate-descriptorbits->offset15-0$inline offset15-0 x))) (interrupt/trap-gate-descriptorbits-equiv-under-mask new-x x -65536)))