Access the |X86ISA|::|OSXMMEXCPT| field of a cr4bits bit structure.
Function:
(defun cr4bits->osxmmexcpt$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 10 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 12) (ash (the (unsigned-byte 22) x) -10))))))
Theorem:
(defthm bitp-of-cr4bits->osxmmexcpt (b* ((osxmmexcpt (cr4bits->osxmmexcpt$inline x))) (bitp osxmmexcpt)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->osxmmexcpt$inline-of-cr4bits-fix-x (equal (cr4bits->osxmmexcpt$inline (cr4bits-fix x)) (cr4bits->osxmmexcpt$inline x)))
Theorem:
(defthm cr4bits->osxmmexcpt$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->osxmmexcpt$inline x) (cr4bits->osxmmexcpt$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->osxmmexcpt-of-cr4bits (equal (cr4bits->osxmmexcpt (cr4bits vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)) (bfix osxmmexcpt)))
Theorem:
(defthm cr4bits->osxmmexcpt-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) 1024) 0)) (equal (cr4bits->osxmmexcpt x) (cr4bits->osxmmexcpt y))))