Update the |X86ISA|::|BASE15-0| field of a code-segment-descriptorbits bit structure.
(!code-segment-descriptorbits->base15-0 base15-0 x) → new-x
Function:
(defun !code-segment-descriptorbits->base15-0$inline (base15-0 x) (declare (xargs :guard (and (16bits-p base15-0) (code-segment-descriptorbits-p x)))) (mbe :logic (b* ((base15-0 (mbe :logic (16bits-fix base15-0) :exec base15-0)) (x (code-segment-descriptorbits-fix x))) (part-install base15-0 x :width 16 :low 16)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 33) -4294901761))) (the (unsigned-byte 32) (ash (the (unsigned-byte 16) base15-0) 16))))))
Theorem:
(defthm code-segment-descriptorbits-p-of-!code-segment-descriptorbits->base15-0 (b* ((new-x (!code-segment-descriptorbits->base15-0$inline base15-0 x))) (code-segment-descriptorbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !code-segment-descriptorbits->base15-0$inline-of-16bits-fix-base15-0 (equal (!code-segment-descriptorbits->base15-0$inline (16bits-fix base15-0) x) (!code-segment-descriptorbits->base15-0$inline base15-0 x)))
Theorem:
(defthm !code-segment-descriptorbits->base15-0$inline-16bits-equiv-congruence-on-base15-0 (implies (16bits-equiv base15-0 base15-0-equiv) (equal (!code-segment-descriptorbits->base15-0$inline base15-0 x) (!code-segment-descriptorbits->base15-0$inline base15-0-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !code-segment-descriptorbits->base15-0$inline-of-code-segment-descriptorbits-fix-x (equal (!code-segment-descriptorbits->base15-0$inline base15-0 (code-segment-descriptorbits-fix x)) (!code-segment-descriptorbits->base15-0$inline base15-0 x)))
Theorem:
(defthm !code-segment-descriptorbits->base15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x (implies (code-segment-descriptorbits-equiv x x-equiv) (equal (!code-segment-descriptorbits->base15-0$inline base15-0 x) (!code-segment-descriptorbits->base15-0$inline base15-0 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !code-segment-descriptorbits->base15-0-is-code-segment-descriptorbits (equal (!code-segment-descriptorbits->base15-0 base15-0 x) (change-code-segment-descriptorbits x :base15-0 base15-0)))
Theorem:
(defthm code-segment-descriptorbits->base15-0-of-!code-segment-descriptorbits->base15-0 (b* ((?new-x (!code-segment-descriptorbits->base15-0$inline base15-0 x))) (equal (code-segment-descriptorbits->base15-0 new-x) (16bits-fix base15-0))))
Theorem:
(defthm !code-segment-descriptorbits->base15-0-equiv-under-mask (b* ((?new-x (!code-segment-descriptorbits->base15-0$inline base15-0 x))) (code-segment-descriptorbits-equiv-under-mask new-x x -4294901761)))