Update the |X86ISA|::|BASE-ADDR| field of a hidden-segment-registerbits bit structure.
(!hidden-segment-registerbits->base-addr base-addr x) → new-x
Function:
(defun !hidden-segment-registerbits->base-addr$inline (base-addr x) (declare (xargs :guard (and (64bits-p base-addr) (hidden-segment-registerbits-p x)))) (mbe :logic (b* ((base-addr (mbe :logic (64bits-fix base-addr) :exec base-addr)) (x (hidden-segment-registerbits-fix x))) (part-install base-addr x :width 64 :low 0)) :exec (the (unsigned-byte 112) (logior (the (unsigned-byte 112) (logand (the (unsigned-byte 112) x) (the (signed-byte 65) -18446744073709551616))) (the (unsigned-byte 64) base-addr)))))
Theorem:
(defthm hidden-segment-registerbits-p-of-!hidden-segment-registerbits->base-addr (b* ((new-x (!hidden-segment-registerbits->base-addr$inline base-addr x))) (hidden-segment-registerbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !hidden-segment-registerbits->base-addr$inline-of-64bits-fix-base-addr (equal (!hidden-segment-registerbits->base-addr$inline (64bits-fix base-addr) x) (!hidden-segment-registerbits->base-addr$inline base-addr x)))
Theorem:
(defthm !hidden-segment-registerbits->base-addr$inline-64bits-equiv-congruence-on-base-addr (implies (64bits-equiv base-addr base-addr-equiv) (equal (!hidden-segment-registerbits->base-addr$inline base-addr x) (!hidden-segment-registerbits->base-addr$inline base-addr-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !hidden-segment-registerbits->base-addr$inline-of-hidden-segment-registerbits-fix-x (equal (!hidden-segment-registerbits->base-addr$inline base-addr (hidden-segment-registerbits-fix x)) (!hidden-segment-registerbits->base-addr$inline base-addr x)))
Theorem:
(defthm !hidden-segment-registerbits->base-addr$inline-hidden-segment-registerbits-equiv-congruence-on-x (implies (hidden-segment-registerbits-equiv x x-equiv) (equal (!hidden-segment-registerbits->base-addr$inline base-addr x) (!hidden-segment-registerbits->base-addr$inline base-addr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !hidden-segment-registerbits->base-addr-is-hidden-segment-registerbits (equal (!hidden-segment-registerbits->base-addr base-addr x) (change-hidden-segment-registerbits x :base-addr base-addr)))
Theorem:
(defthm hidden-segment-registerbits->base-addr-of-!hidden-segment-registerbits->base-addr (b* ((?new-x (!hidden-segment-registerbits->base-addr$inline base-addr x))) (equal (hidden-segment-registerbits->base-addr new-x) (64bits-fix base-addr))))
Theorem:
(defthm !hidden-segment-registerbits->base-addr-equiv-under-mask (b* ((?new-x (!hidden-segment-registerbits->base-addr$inline base-addr x))) (hidden-segment-registerbits-equiv-under-mask new-x x -18446744073709551616)))