Access the |X86ISA|::|BASE-ADDR| field of a hidden-segment-registerbits bit structure.
(hidden-segment-registerbits->base-addr x) → base-addr
Function:
(defun hidden-segment-registerbits->base-addr$inline (x) (declare (xargs :guard (hidden-segment-registerbits-p x))) (mbe :logic (let ((x (hidden-segment-registerbits-fix x))) (part-select x :low 0 :width 64)) :exec (the (unsigned-byte 64) (logand (the (unsigned-byte 64) 18446744073709551615) (the (unsigned-byte 112) x)))))
Theorem:
(defthm 64bits-p-of-hidden-segment-registerbits->base-addr (b* ((base-addr (hidden-segment-registerbits->base-addr$inline x))) (64bits-p base-addr)) :rule-classes :rewrite)
Theorem:
(defthm hidden-segment-registerbits->base-addr$inline-of-hidden-segment-registerbits-fix-x (equal (hidden-segment-registerbits->base-addr$inline (hidden-segment-registerbits-fix x)) (hidden-segment-registerbits->base-addr$inline 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 x) (hidden-segment-registerbits->base-addr$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm hidden-segment-registerbits->base-addr-of-hidden-segment-registerbits (equal (hidden-segment-registerbits->base-addr (hidden-segment-registerbits base-addr limit attr)) (64bits-fix base-addr)))
Theorem:
(defthm hidden-segment-registerbits->base-addr-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x hidden-segment-registerbits-equiv-under-mask) (hidden-segment-registerbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 18446744073709551615) 0)) (equal (hidden-segment-registerbits->base-addr x) (hidden-segment-registerbits->base-addr y))))