Access the |X86ISA|::|VMXE| field of a cr4bits bit structure.
Function:
(defun cr4bits->vmxe$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 13 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 13) (ash (the (unsigned-byte 26) x) -13))))))
Theorem:
(defthm bitp-of-cr4bits->vmxe (b* ((vmxe (cr4bits->vmxe$inline x))) (bitp vmxe)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->vmxe$inline-of-cr4bits-fix-x (equal (cr4bits->vmxe$inline (cr4bits-fix x)) (cr4bits->vmxe$inline x)))
Theorem:
(defthm cr4bits->vmxe$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->vmxe$inline x) (cr4bits->vmxe$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->vmxe-of-cr4bits (equal (cr4bits->vmxe (cr4bits vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr)) (bfix vmxe)))
Theorem:
(defthm cr4bits->vmxe-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x cr4bits-equiv-under-mask) (cr4bits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 8192) 0)) (equal (cr4bits->vmxe x) (cr4bits->vmxe y))))