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