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