Update the |X86ISA|::|ALL-ZEROES?| field of a call-gate-descriptorbits bit structure.
(!call-gate-descriptorbits->all-zeroes? all-zeroes? x) → new-x
Function:
(defun !call-gate-descriptorbits->all-zeroes?$inline (all-zeroes? x) (declare (xargs :guard (and (5bits-p all-zeroes?) (call-gate-descriptorbits-p x)))) (mbe :logic (b* ((all-zeroes? (mbe :logic (5bits-fix all-zeroes?) :exec all-zeroes?)) (x (call-gate-descriptorbits-fix x))) (part-install all-zeroes? 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-zeroes?) 104))))))
Theorem:
(defthm call-gate-descriptorbits-p-of-!call-gate-descriptorbits->all-zeroes? (b* ((new-x (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x))) (call-gate-descriptorbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !call-gate-descriptorbits->all-zeroes?$inline-of-5bits-fix-all-zeroes? (equal (!call-gate-descriptorbits->all-zeroes?$inline (5bits-fix all-zeroes?) x) (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x)))
Theorem:
(defthm !call-gate-descriptorbits->all-zeroes?$inline-5bits-equiv-congruence-on-all-zeroes? (implies (5bits-equiv all-zeroes? all-zeroes?-equiv) (equal (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x) (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes?-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptorbits->all-zeroes?$inline-of-call-gate-descriptorbits-fix-x (equal (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? (call-gate-descriptorbits-fix x)) (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x)))
Theorem:
(defthm !call-gate-descriptorbits->all-zeroes?$inline-call-gate-descriptorbits-equiv-congruence-on-x (implies (call-gate-descriptorbits-equiv x x-equiv) (equal (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x) (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptorbits->all-zeroes?-is-call-gate-descriptorbits (equal (!call-gate-descriptorbits->all-zeroes? all-zeroes? x) (change-call-gate-descriptorbits x :all-zeroes? all-zeroes?)))
Theorem:
(defthm call-gate-descriptorbits->all-zeroes?-of-!call-gate-descriptorbits->all-zeroes? (b* ((?new-x (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x))) (equal (call-gate-descriptorbits->all-zeroes? new-x) (5bits-fix all-zeroes?))))
Theorem:
(defthm !call-gate-descriptorbits->all-zeroes?-equiv-under-mask (b* ((?new-x (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x))) (call-gate-descriptorbits-equiv-under-mask new-x x -628754697713201783142364789866497)))