Access the |X86ISA|::|PKS| field of a cr4bits bit structure.
Function:
(defun cr4bits->pks$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 24 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 2) (ash (the (unsigned-byte 26) x) -24))))))
Theorem:
(defthm bitp-of-cr4bits->pks (b* ((pks (cr4bits->pks$inline x))) (bitp pks)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pks$inline-of-cr4bits-fix-x (equal (cr4bits->pks$inline (cr4bits-fix x)) (cr4bits->pks$inline x)))
Theorem:
(defthm cr4bits->pks$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pks$inline x) (cr4bits->pks$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pks-of-cr4bits (equal (cr4bits->pks (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 pks)))
Theorem:
(defthm cr4bits->pks-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) 16777216) 0)) (equal (cr4bits->pks x) (cr4bits->pks y))))