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