|
|
|---|
|
|
|
|---|
An 26-bit unsigned bitstruct type.
This is a bitstruct type introduced by defbitstruct, represented as a unsigned 26-bit integer.
Source: Intel Manual, Dec-23, Vol. 3A, Section 2.5
Function:
(defun cr4bits-p$inline (x) (declare (xargs :guard t)) (mbe :logic (unsigned-byte-p 26 x) :exec (and (natp x) (< x 67108864))))
Theorem:
(defthm cr4bits-p-when-unsigned-byte-p (implies (unsigned-byte-p 26 x) (cr4bits-p x)))
Theorem:
(defthm unsigned-byte-p-when-cr4bits-p (implies (cr4bits-p x) (unsigned-byte-p 26 x)))
Theorem:
(defthm cr4bits-p-compound-recognizer (implies (cr4bits-p x) (natp x)) :rule-classes :compound-recognizer)
Function:
(defun cr4bits-fix$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (loghead 26 x) :exec x))
Theorem:
(defthm cr4bits-p-of-cr4bits-fix (b* ((fty::fixed (cr4bits-fix$inline x))) (cr4bits-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits-fix-when-cr4bits-p (implies (cr4bits-p x) (equal (cr4bits-fix x) x)))
Function:
(defun cr4bits-equiv$inline (x y) (declare (xargs :guard (and (cr4bits-p x) (cr4bits-p y)))) (equal (cr4bits-fix x) (cr4bits-fix y)))
Theorem:
(defthm cr4bits-equiv-is-an-equivalence (and (booleanp (cr4bits-equiv x y)) (cr4bits-equiv x x) (implies (cr4bits-equiv x y) (cr4bits-equiv y x)) (implies (and (cr4bits-equiv x y) (cr4bits-equiv y z)) (cr4bits-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm cr4bits-equiv-implies-equal-cr4bits-fix-1 (implies (cr4bits-equiv x x-equiv) (equal (cr4bits-fix x) (cr4bits-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm cr4bits-fix-under-cr4bits-equiv (cr4bits-equiv (cr4bits-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Function:
(defun cr4bits$inline (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) (declare (xargs :guard (and (bitp vme) (bitp pvi) (bitp tsd) (bitp de) (bitp pse) (bitp pae) (bitp mce) (bitp pge) (bitp pce) (bitp osfxsr) (bitp osxmmexcpt) (bitp umip) (bitp la57) (bitp vmxe) (bitp smxe) (bitp res1) (bitp fsgsbase) (bitp pcide) (bitp osxsave) (bitp kl) (bitp smep) (bitp smap) (bitp pke) (bitp cet) (bitp pks) (bitp uintr)))) (b* ((vme (mbe :logic (bfix vme) :exec vme)) (pvi (mbe :logic (bfix pvi) :exec pvi)) (tsd (mbe :logic (bfix tsd) :exec tsd)) (de (mbe :logic (bfix de) :exec de)) (pse (mbe :logic (bfix pse) :exec pse)) (pae (mbe :logic (bfix pae) :exec pae)) (mce (mbe :logic (bfix mce) :exec mce)) (pge (mbe :logic (bfix pge) :exec pge)) (pce (mbe :logic (bfix pce) :exec pce)) (osfxsr (mbe :logic (bfix osfxsr) :exec osfxsr)) (osxmmexcpt (mbe :logic (bfix osxmmexcpt) :exec osxmmexcpt)) (umip (mbe :logic (bfix umip) :exec umip)) (la57 (mbe :logic (bfix la57) :exec la57)) (vmxe (mbe :logic (bfix vmxe) :exec vmxe)) (smxe (mbe :logic (bfix smxe) :exec smxe)) (res1 (mbe :logic (bfix res1) :exec res1)) (fsgsbase (mbe :logic (bfix fsgsbase) :exec fsgsbase)) (pcide (mbe :logic (bfix pcide) :exec pcide)) (osxsave (mbe :logic (bfix osxsave) :exec osxsave)) (kl (mbe :logic (bfix kl) :exec kl)) (smep (mbe :logic (bfix smep) :exec smep)) (smap (mbe :logic (bfix smap) :exec smap)) (pke (mbe :logic (bfix pke) :exec pke)) (cet (mbe :logic (bfix cet) :exec cet)) (pks (mbe :logic (bfix pks) :exec pks)) (uintr (mbe :logic (bfix uintr) :exec uintr))) (logapp 1 vme (logapp 1 pvi (logapp 1 tsd (logapp 1 de (logapp 1 pse (logapp 1 pae (logapp 1 mce (logapp 1 pge (logapp 1 pce (logapp 1 osfxsr (logapp 1 osxmmexcpt (logapp 1 umip (logapp 1 la57 (logapp 1 vmxe (logapp 1 smxe (logapp 1 res1 (logapp 1 fsgsbase (logapp 1 pcide (logapp 1 osxsave (logapp 1 kl (logapp 1 smep (logapp 1 smap (logapp 1 pke (logapp 1 cet (logapp 1 pks uintr)))))))))))))))))))))))))))
Theorem:
(defthm cr4bits-p-of-cr4bits (b* ((cr4bits (cr4bits$inline 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))) (cr4bits-p cr4bits)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits$inline-of-bfix-vme (equal (cr4bits$inline (bfix 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) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-vme (implies (bit-equiv vme vme-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme-equiv 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))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pvi (equal (cr4bits$inline vme (bfix 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) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pvi (implies (bit-equiv pvi pvi-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi-equiv tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-tsd (equal (cr4bits$inline vme pvi (bfix tsd) de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-tsd (implies (bit-equiv tsd tsd-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd-equiv de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-de (equal (cr4bits$inline vme pvi tsd (bfix de) pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-de (implies (bit-equiv de de-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de-equiv pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pse (equal (cr4bits$inline vme pvi tsd de (bfix pse) pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pse (implies (bit-equiv pse pse-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse-equiv pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pae (equal (cr4bits$inline vme pvi tsd de pse (bfix pae) mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pae (implies (bit-equiv pae pae-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae-equiv mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-mce (equal (cr4bits$inline vme pvi tsd de pse pae (bfix mce) pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-mce (implies (bit-equiv mce mce-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce-equiv pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pge (equal (cr4bits$inline vme pvi tsd de pse pae mce (bfix pge) pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pge (implies (bit-equiv pge pge-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge-equiv pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pce (equal (cr4bits$inline vme pvi tsd de pse pae mce pge (bfix pce) osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pce (implies (bit-equiv pce pce-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce-equiv osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-osfxsr (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce (bfix osfxsr) osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-osfxsr (implies (bit-equiv osfxsr osfxsr-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr-equiv osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-osxmmexcpt (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr (bfix osxmmexcpt) umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-osxmmexcpt (implies (bit-equiv osxmmexcpt osxmmexcpt-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt-equiv umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-umip (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt (bfix umip) la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-umip (implies (bit-equiv umip umip-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip-equiv la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-la57 (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip (bfix la57) vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-la57 (implies (bit-equiv la57 la57-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57-equiv vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-vmxe (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 (bfix vmxe) smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-vmxe (implies (bit-equiv vmxe vmxe-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe-equiv smxe res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-smxe (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe (bfix smxe) res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-smxe (implies (bit-equiv smxe smxe-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe-equiv res1 fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-res1 (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe (bfix res1) fsgsbase pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-res1 (implies (bit-equiv res1 res1-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1-equiv fsgsbase pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-fsgsbase (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 (bfix fsgsbase) pcide osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-fsgsbase (implies (bit-equiv fsgsbase fsgsbase-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase-equiv pcide osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pcide (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase (bfix pcide) osxsave kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pcide (implies (bit-equiv pcide pcide-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide-equiv osxsave kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-osxsave (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide (bfix osxsave) kl smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-osxsave (implies (bit-equiv osxsave osxsave-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave-equiv kl smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-kl (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave (bfix kl) smep smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-kl (implies (bit-equiv kl kl-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl-equiv smep smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-smep (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl (bfix smep) smap pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-smep (implies (bit-equiv smep smep-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep-equiv smap pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-smap (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep (bfix smap) pke cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-smap (implies (bit-equiv smap smap-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap-equiv pke cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pke (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap (bfix pke) cet pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pke (implies (bit-equiv pke pke-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke-equiv cet pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-cet (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke (bfix cet) pks uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-cet (implies (bit-equiv cet cet-equiv) (equal (cr4bits$inline 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) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet-equiv pks uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-pks (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave kl smep smap pke cet (bfix pks) uintr) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-pks (implies (bit-equiv pks pks-equiv) (equal (cr4bits$inline 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) (cr4bits$inline 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-equiv uintr))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-uintr (equal (cr4bits$inline 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 (bfix uintr)) (cr4bits$inline 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)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-uintr (implies (bit-equiv uintr uintr-equiv) (equal (cr4bits$inline 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) (cr4bits$inline 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-equiv))) :rule-classes :congruence)
Function:
(defun cr4bits-equiv-under-mask$inline (x x1 mask) (declare (xargs :guard (and (cr4bits-p x) (cr4bits-p x1) (integerp mask)))) (fty::int-equiv-under-mask (cr4bits-fix x) (cr4bits-fix x1) mask))
Function:
(defun cr4bits->vme$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 0 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 26) x)))))
Theorem:
(defthm bitp-of-cr4bits->vme (b* ((vme (cr4bits->vme$inline x))) (bitp vme)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->vme$inline-of-cr4bits-fix-x (equal (cr4bits->vme$inline (cr4bits-fix x)) (cr4bits->vme$inline x)))
Theorem:
(defthm cr4bits->vme$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->vme$inline x) (cr4bits->vme$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->vme-of-cr4bits (equal (cr4bits->vme (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 vme)))
Theorem:
(defthm cr4bits->vme-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) 1) 0)) (equal (cr4bits->vme x) (cr4bits->vme y))))
Function:
(defun cr4bits->pvi$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 1 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 25) (ash (the (unsigned-byte 26) x) -1))))))
Theorem:
(defthm bitp-of-cr4bits->pvi (b* ((pvi (cr4bits->pvi$inline x))) (bitp pvi)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pvi$inline-of-cr4bits-fix-x (equal (cr4bits->pvi$inline (cr4bits-fix x)) (cr4bits->pvi$inline x)))
Theorem:
(defthm cr4bits->pvi$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pvi$inline x) (cr4bits->pvi$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pvi-of-cr4bits (equal (cr4bits->pvi (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 pvi)))
Theorem:
(defthm cr4bits->pvi-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) 2) 0)) (equal (cr4bits->pvi x) (cr4bits->pvi y))))
Function:
(defun cr4bits->tsd$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 2 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 24) (ash (the (unsigned-byte 26) x) -2))))))
Theorem:
(defthm bitp-of-cr4bits->tsd (b* ((tsd (cr4bits->tsd$inline x))) (bitp tsd)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->tsd$inline-of-cr4bits-fix-x (equal (cr4bits->tsd$inline (cr4bits-fix x)) (cr4bits->tsd$inline x)))
Theorem:
(defthm cr4bits->tsd$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->tsd$inline x) (cr4bits->tsd$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->tsd-of-cr4bits (equal (cr4bits->tsd (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 tsd)))
Theorem:
(defthm cr4bits->tsd-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) 4) 0)) (equal (cr4bits->tsd x) (cr4bits->tsd y))))
Function:
(defun cr4bits->de$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 3 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 23) (ash (the (unsigned-byte 26) x) -3))))))
Theorem:
(defthm bitp-of-cr4bits->de (b* ((de (cr4bits->de$inline x))) (bitp de)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->de$inline-of-cr4bits-fix-x (equal (cr4bits->de$inline (cr4bits-fix x)) (cr4bits->de$inline x)))
Theorem:
(defthm cr4bits->de$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->de$inline x) (cr4bits->de$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->de-of-cr4bits (equal (cr4bits->de (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 de)))
Theorem:
(defthm cr4bits->de-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) 8) 0)) (equal (cr4bits->de x) (cr4bits->de y))))
Function:
(defun cr4bits->pse$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 4 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 22) (ash (the (unsigned-byte 26) x) -4))))))
Theorem:
(defthm bitp-of-cr4bits->pse (b* ((pse (cr4bits->pse$inline x))) (bitp pse)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pse$inline-of-cr4bits-fix-x (equal (cr4bits->pse$inline (cr4bits-fix x)) (cr4bits->pse$inline x)))
Theorem:
(defthm cr4bits->pse$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pse$inline x) (cr4bits->pse$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pse-of-cr4bits (equal (cr4bits->pse (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 pse)))
Theorem:
(defthm cr4bits->pse-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) 16) 0)) (equal (cr4bits->pse x) (cr4bits->pse y))))
Function:
(defun cr4bits->pae$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 5 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 21) (ash (the (unsigned-byte 26) x) -5))))))
Theorem:
(defthm bitp-of-cr4bits->pae (b* ((pae (cr4bits->pae$inline x))) (bitp pae)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pae$inline-of-cr4bits-fix-x (equal (cr4bits->pae$inline (cr4bits-fix x)) (cr4bits->pae$inline x)))
Theorem:
(defthm cr4bits->pae$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pae$inline x) (cr4bits->pae$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pae-of-cr4bits (equal (cr4bits->pae (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 pae)))
Theorem:
(defthm cr4bits->pae-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) 32) 0)) (equal (cr4bits->pae x) (cr4bits->pae y))))
Function:
(defun cr4bits->mce$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 6 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 20) (ash (the (unsigned-byte 26) x) -6))))))
Theorem:
(defthm bitp-of-cr4bits->mce (b* ((mce (cr4bits->mce$inline x))) (bitp mce)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->mce$inline-of-cr4bits-fix-x (equal (cr4bits->mce$inline (cr4bits-fix x)) (cr4bits->mce$inline x)))
Theorem:
(defthm cr4bits->mce$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->mce$inline x) (cr4bits->mce$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->mce-of-cr4bits (equal (cr4bits->mce (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 mce)))
Theorem:
(defthm cr4bits->mce-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) 64) 0)) (equal (cr4bits->mce x) (cr4bits->mce y))))
Function:
(defun cr4bits->pge$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 7 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 19) (ash (the (unsigned-byte 26) x) -7))))))
Theorem:
(defthm bitp-of-cr4bits->pge (b* ((pge (cr4bits->pge$inline x))) (bitp pge)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pge$inline-of-cr4bits-fix-x (equal (cr4bits->pge$inline (cr4bits-fix x)) (cr4bits->pge$inline x)))
Theorem:
(defthm cr4bits->pge$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pge$inline x) (cr4bits->pge$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pge-of-cr4bits (equal (cr4bits->pge (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 pge)))
Theorem:
(defthm cr4bits->pge-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) 128) 0)) (equal (cr4bits->pge x) (cr4bits->pge y))))
Function:
(defun cr4bits->pce$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 8 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 18) (ash (the (unsigned-byte 26) x) -8))))))
Theorem:
(defthm bitp-of-cr4bits->pce (b* ((pce (cr4bits->pce$inline x))) (bitp pce)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pce$inline-of-cr4bits-fix-x (equal (cr4bits->pce$inline (cr4bits-fix x)) (cr4bits->pce$inline x)))
Theorem:
(defthm cr4bits->pce$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pce$inline x) (cr4bits->pce$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pce-of-cr4bits (equal (cr4bits->pce (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 pce)))
Theorem:
(defthm cr4bits->pce-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) 256) 0)) (equal (cr4bits->pce x) (cr4bits->pce y))))
Function:
(defun cr4bits->osfxsr$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 9 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 17) (ash (the (unsigned-byte 26) x) -9))))))
Theorem:
(defthm bitp-of-cr4bits->osfxsr (b* ((osfxsr (cr4bits->osfxsr$inline x))) (bitp osfxsr)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->osfxsr$inline-of-cr4bits-fix-x (equal (cr4bits->osfxsr$inline (cr4bits-fix x)) (cr4bits->osfxsr$inline x)))
Theorem:
(defthm cr4bits->osfxsr$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->osfxsr$inline x) (cr4bits->osfxsr$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->osfxsr-of-cr4bits (equal (cr4bits->osfxsr (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 osfxsr)))
Theorem:
(defthm cr4bits->osfxsr-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) 512) 0)) (equal (cr4bits->osfxsr x) (cr4bits->osfxsr y))))
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 16) (ash (the (unsigned-byte 26) 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 kl smep smap pke cet pks uintr)) (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))))
Function:
(defun cr4bits->umip$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 11 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 15) (ash (the (unsigned-byte 26) x) -11))))))
Theorem:
(defthm bitp-of-cr4bits->umip (b* ((umip (cr4bits->umip$inline x))) (bitp umip)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->umip$inline-of-cr4bits-fix-x (equal (cr4bits->umip$inline (cr4bits-fix x)) (cr4bits->umip$inline x)))
Theorem:
(defthm cr4bits->umip$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->umip$inline x) (cr4bits->umip$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->umip-of-cr4bits (equal (cr4bits->umip (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 umip)))
Theorem:
(defthm cr4bits->umip-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) 2048) 0)) (equal (cr4bits->umip x) (cr4bits->umip y))))
Function:
(defun cr4bits->la57$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 12 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 14) (ash (the (unsigned-byte 26) x) -12))))))
Theorem:
(defthm bitp-of-cr4bits->la57 (b* ((la57 (cr4bits->la57$inline x))) (bitp la57)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->la57$inline-of-cr4bits-fix-x (equal (cr4bits->la57$inline (cr4bits-fix x)) (cr4bits->la57$inline x)))
Theorem:
(defthm cr4bits->la57$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->la57$inline x) (cr4bits->la57$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->la57-of-cr4bits (equal (cr4bits->la57 (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 la57)))
Theorem:
(defthm cr4bits->la57-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) 4096) 0)) (equal (cr4bits->la57 x) (cr4bits->la57 y))))
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))))
Function:
(defun cr4bits->smxe$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 14 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 12) (ash (the (unsigned-byte 26) x) -14))))))
Theorem:
(defthm bitp-of-cr4bits->smxe (b* ((smxe (cr4bits->smxe$inline x))) (bitp smxe)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->smxe$inline-of-cr4bits-fix-x (equal (cr4bits->smxe$inline (cr4bits-fix x)) (cr4bits->smxe$inline x)))
Theorem:
(defthm cr4bits->smxe$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->smxe$inline x) (cr4bits->smxe$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->smxe-of-cr4bits (equal (cr4bits->smxe (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 smxe)))
Theorem:
(defthm cr4bits->smxe-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) 16384) 0)) (equal (cr4bits->smxe x) (cr4bits->smxe y))))
Function:
(defun cr4bits->res1$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 15 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 11) (ash (the (unsigned-byte 26) x) -15))))))
Theorem:
(defthm bitp-of-cr4bits->res1 (b* ((res1 (cr4bits->res1$inline x))) (bitp res1)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->res1$inline-of-cr4bits-fix-x (equal (cr4bits->res1$inline (cr4bits-fix x)) (cr4bits->res1$inline x)))
Theorem:
(defthm cr4bits->res1$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->res1$inline x) (cr4bits->res1$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->res1-of-cr4bits (equal (cr4bits->res1 (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 res1)))
Theorem:
(defthm cr4bits->res1-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) 32768) 0)) (equal (cr4bits->res1 x) (cr4bits->res1 y))))
Function:
(defun cr4bits->fsgsbase$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 16 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 10) (ash (the (unsigned-byte 26) x) -16))))))
Theorem:
(defthm bitp-of-cr4bits->fsgsbase (b* ((fsgsbase (cr4bits->fsgsbase$inline x))) (bitp fsgsbase)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->fsgsbase$inline-of-cr4bits-fix-x (equal (cr4bits->fsgsbase$inline (cr4bits-fix x)) (cr4bits->fsgsbase$inline x)))
Theorem:
(defthm cr4bits->fsgsbase$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->fsgsbase$inline x) (cr4bits->fsgsbase$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->fsgsbase-of-cr4bits (equal (cr4bits->fsgsbase (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 fsgsbase)))
Theorem:
(defthm cr4bits->fsgsbase-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) 65536) 0)) (equal (cr4bits->fsgsbase x) (cr4bits->fsgsbase y))))
Function:
(defun cr4bits->pcide$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 17 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 9) (ash (the (unsigned-byte 26) x) -17))))))
Theorem:
(defthm bitp-of-cr4bits->pcide (b* ((pcide (cr4bits->pcide$inline x))) (bitp pcide)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pcide$inline-of-cr4bits-fix-x (equal (cr4bits->pcide$inline (cr4bits-fix x)) (cr4bits->pcide$inline x)))
Theorem:
(defthm cr4bits->pcide$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pcide$inline x) (cr4bits->pcide$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pcide-of-cr4bits (equal (cr4bits->pcide (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 pcide)))
Theorem:
(defthm cr4bits->pcide-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) 131072) 0)) (equal (cr4bits->pcide x) (cr4bits->pcide y))))
Function:
(defun cr4bits->osxsave$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 18 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 8) (ash (the (unsigned-byte 26) x) -18))))))
Theorem:
(defthm bitp-of-cr4bits->osxsave (b* ((osxsave (cr4bits->osxsave$inline x))) (bitp osxsave)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->osxsave$inline-of-cr4bits-fix-x (equal (cr4bits->osxsave$inline (cr4bits-fix x)) (cr4bits->osxsave$inline x)))
Theorem:
(defthm cr4bits->osxsave$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->osxsave$inline x) (cr4bits->osxsave$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->osxsave-of-cr4bits (equal (cr4bits->osxsave (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 osxsave)))
Theorem:
(defthm cr4bits->osxsave-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) 262144) 0)) (equal (cr4bits->osxsave x) (cr4bits->osxsave y))))
Function:
(defun cr4bits->kl$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 19 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 7) (ash (the (unsigned-byte 26) x) -19))))))
Theorem:
(defthm bitp-of-cr4bits->kl (b* ((kl (cr4bits->kl$inline x))) (bitp kl)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->kl$inline-of-cr4bits-fix-x (equal (cr4bits->kl$inline (cr4bits-fix x)) (cr4bits->kl$inline x)))
Theorem:
(defthm cr4bits->kl$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->kl$inline x) (cr4bits->kl$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->kl-of-cr4bits (equal (cr4bits->kl (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 kl)))
Theorem:
(defthm cr4bits->kl-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) 524288) 0)) (equal (cr4bits->kl x) (cr4bits->kl y))))
Function:
(defun cr4bits->smep$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 20 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 6) (ash (the (unsigned-byte 26) x) -20))))))
Theorem:
(defthm bitp-of-cr4bits->smep (b* ((smep (cr4bits->smep$inline x))) (bitp smep)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->smep$inline-of-cr4bits-fix-x (equal (cr4bits->smep$inline (cr4bits-fix x)) (cr4bits->smep$inline x)))
Theorem:
(defthm cr4bits->smep$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->smep$inline x) (cr4bits->smep$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->smep-of-cr4bits (equal (cr4bits->smep (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 smep)))
Theorem:
(defthm cr4bits->smep-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) 1048576) 0)) (equal (cr4bits->smep x) (cr4bits->smep y))))
Function:
(defun cr4bits->smap$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 21 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 5) (ash (the (unsigned-byte 26) x) -21))))))
Theorem:
(defthm bitp-of-cr4bits->smap (b* ((smap (cr4bits->smap$inline x))) (bitp smap)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->smap$inline-of-cr4bits-fix-x (equal (cr4bits->smap$inline (cr4bits-fix x)) (cr4bits->smap$inline x)))
Theorem:
(defthm cr4bits->smap$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->smap$inline x) (cr4bits->smap$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->smap-of-cr4bits (equal (cr4bits->smap (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 smap)))
Theorem:
(defthm cr4bits->smap-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) 2097152) 0)) (equal (cr4bits->smap x) (cr4bits->smap y))))
Function:
(defun cr4bits->pke$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 22 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 4) (ash (the (unsigned-byte 26) x) -22))))))
Theorem:
(defthm bitp-of-cr4bits->pke (b* ((pke (cr4bits->pke$inline x))) (bitp pke)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->pke$inline-of-cr4bits-fix-x (equal (cr4bits->pke$inline (cr4bits-fix x)) (cr4bits->pke$inline x)))
Theorem:
(defthm cr4bits->pke$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->pke$inline x) (cr4bits->pke$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->pke-of-cr4bits (equal (cr4bits->pke (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 pke)))
Theorem:
(defthm cr4bits->pke-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) 4194304) 0)) (equal (cr4bits->pke x) (cr4bits->pke y))))
Function:
(defun cr4bits->cet$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 23 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 3) (ash (the (unsigned-byte 26) x) -23))))))
Theorem:
(defthm bitp-of-cr4bits->cet (b* ((cet (cr4bits->cet$inline x))) (bitp cet)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->cet$inline-of-cr4bits-fix-x (equal (cr4bits->cet$inline (cr4bits-fix x)) (cr4bits->cet$inline x)))
Theorem:
(defthm cr4bits->cet$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->cet$inline x) (cr4bits->cet$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->cet-of-cr4bits (equal (cr4bits->cet (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 cet)))
Theorem:
(defthm cr4bits->cet-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) 8388608) 0)) (equal (cr4bits->cet x) (cr4bits->cet y))))
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))))
Function:
(defun cr4bits->uintr$inline (x) (declare (xargs :guard (cr4bits-p x))) (mbe :logic (let ((x (cr4bits-fix x))) (part-select x :low 25 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 1) (ash (the (unsigned-byte 26) x) -25))))))
Theorem:
(defthm bitp-of-cr4bits->uintr (b* ((uintr (cr4bits->uintr$inline x))) (bitp uintr)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->uintr$inline-of-cr4bits-fix-x (equal (cr4bits->uintr$inline (cr4bits-fix x)) (cr4bits->uintr$inline x)))
Theorem:
(defthm cr4bits->uintr$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->uintr$inline x) (cr4bits->uintr$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->uintr-of-cr4bits (equal (cr4bits->uintr (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 uintr)))
Theorem:
(defthm cr4bits->uintr-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) 33554432) 0)) (equal (cr4bits->uintr x) (cr4bits->uintr y))))
Theorem:
(defthm cr4bits-fix-in-terms-of-cr4bits (equal (cr4bits-fix x) (change-cr4bits x)))
Function:
(defun !cr4bits->vme$inline (vme x) (declare (xargs :guard (and (bitp vme) (cr4bits-p x)))) (mbe :logic (b* ((vme (mbe :logic (bfix vme) :exec vme)) (x (cr4bits-fix x))) (part-install vme x :width 1 :low 0)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 2) -2))) (the (unsigned-byte 1) vme)))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->vme (b* ((new-x (!cr4bits->vme$inline vme x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->vme$inline-of-bfix-vme (equal (!cr4bits->vme$inline (bfix vme) x) (!cr4bits->vme$inline vme x)))
Theorem:
(defthm !cr4bits->vme$inline-bit-equiv-congruence-on-vme (implies (bit-equiv vme vme-equiv) (equal (!cr4bits->vme$inline vme x) (!cr4bits->vme$inline vme-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->vme$inline-of-cr4bits-fix-x (equal (!cr4bits->vme$inline vme (cr4bits-fix x)) (!cr4bits->vme$inline vme x)))
Theorem:
(defthm !cr4bits->vme$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->vme$inline vme x) (!cr4bits->vme$inline vme x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->vme-is-cr4bits (equal (!cr4bits->vme vme x) (change-cr4bits x :vme vme)))
Theorem:
(defthm cr4bits->vme-of-!cr4bits->vme (b* ((?new-x (!cr4bits->vme$inline vme x))) (equal (cr4bits->vme new-x) (bfix vme))))
Theorem:
(defthm !cr4bits->vme-equiv-under-mask (b* ((?new-x (!cr4bits->vme$inline vme x))) (cr4bits-equiv-under-mask new-x x -2)))
Function:
(defun !cr4bits->pvi$inline (pvi x) (declare (xargs :guard (and (bitp pvi) (cr4bits-p x)))) (mbe :logic (b* ((pvi (mbe :logic (bfix pvi) :exec pvi)) (x (cr4bits-fix x))) (part-install pvi x :width 1 :low 1)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 3) -3))) (the (unsigned-byte 2) (ash (the (unsigned-byte 1) pvi) 1))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pvi (b* ((new-x (!cr4bits->pvi$inline pvi x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pvi$inline-of-bfix-pvi (equal (!cr4bits->pvi$inline (bfix pvi) x) (!cr4bits->pvi$inline pvi x)))
Theorem:
(defthm !cr4bits->pvi$inline-bit-equiv-congruence-on-pvi (implies (bit-equiv pvi pvi-equiv) (equal (!cr4bits->pvi$inline pvi x) (!cr4bits->pvi$inline pvi-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pvi$inline-of-cr4bits-fix-x (equal (!cr4bits->pvi$inline pvi (cr4bits-fix x)) (!cr4bits->pvi$inline pvi x)))
Theorem:
(defthm !cr4bits->pvi$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pvi$inline pvi x) (!cr4bits->pvi$inline pvi x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pvi-is-cr4bits (equal (!cr4bits->pvi pvi x) (change-cr4bits x :pvi pvi)))
Theorem:
(defthm cr4bits->pvi-of-!cr4bits->pvi (b* ((?new-x (!cr4bits->pvi$inline pvi x))) (equal (cr4bits->pvi new-x) (bfix pvi))))
Theorem:
(defthm !cr4bits->pvi-equiv-under-mask (b* ((?new-x (!cr4bits->pvi$inline pvi x))) (cr4bits-equiv-under-mask new-x x -3)))
Function:
(defun !cr4bits->tsd$inline (tsd x) (declare (xargs :guard (and (bitp tsd) (cr4bits-p x)))) (mbe :logic (b* ((tsd (mbe :logic (bfix tsd) :exec tsd)) (x (cr4bits-fix x))) (part-install tsd x :width 1 :low 2)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 4) -5))) (the (unsigned-byte 3) (ash (the (unsigned-byte 1) tsd) 2))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->tsd (b* ((new-x (!cr4bits->tsd$inline tsd x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->tsd$inline-of-bfix-tsd (equal (!cr4bits->tsd$inline (bfix tsd) x) (!cr4bits->tsd$inline tsd x)))
Theorem:
(defthm !cr4bits->tsd$inline-bit-equiv-congruence-on-tsd (implies (bit-equiv tsd tsd-equiv) (equal (!cr4bits->tsd$inline tsd x) (!cr4bits->tsd$inline tsd-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->tsd$inline-of-cr4bits-fix-x (equal (!cr4bits->tsd$inline tsd (cr4bits-fix x)) (!cr4bits->tsd$inline tsd x)))
Theorem:
(defthm !cr4bits->tsd$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->tsd$inline tsd x) (!cr4bits->tsd$inline tsd x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->tsd-is-cr4bits (equal (!cr4bits->tsd tsd x) (change-cr4bits x :tsd tsd)))
Theorem:
(defthm cr4bits->tsd-of-!cr4bits->tsd (b* ((?new-x (!cr4bits->tsd$inline tsd x))) (equal (cr4bits->tsd new-x) (bfix tsd))))
Theorem:
(defthm !cr4bits->tsd-equiv-under-mask (b* ((?new-x (!cr4bits->tsd$inline tsd x))) (cr4bits-equiv-under-mask new-x x -5)))
Function:
(defun !cr4bits->de$inline (de x) (declare (xargs :guard (and (bitp de) (cr4bits-p x)))) (mbe :logic (b* ((de (mbe :logic (bfix de) :exec de)) (x (cr4bits-fix x))) (part-install de x :width 1 :low 3)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 5) -9))) (the (unsigned-byte 4) (ash (the (unsigned-byte 1) de) 3))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->de (b* ((new-x (!cr4bits->de$inline de x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->de$inline-of-bfix-de (equal (!cr4bits->de$inline (bfix de) x) (!cr4bits->de$inline de x)))
Theorem:
(defthm !cr4bits->de$inline-bit-equiv-congruence-on-de (implies (bit-equiv de de-equiv) (equal (!cr4bits->de$inline de x) (!cr4bits->de$inline de-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->de$inline-of-cr4bits-fix-x (equal (!cr4bits->de$inline de (cr4bits-fix x)) (!cr4bits->de$inline de x)))
Theorem:
(defthm !cr4bits->de$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->de$inline de x) (!cr4bits->de$inline de x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->de-is-cr4bits (equal (!cr4bits->de de x) (change-cr4bits x :de de)))
Theorem:
(defthm cr4bits->de-of-!cr4bits->de (b* ((?new-x (!cr4bits->de$inline de x))) (equal (cr4bits->de new-x) (bfix de))))
Theorem:
(defthm !cr4bits->de-equiv-under-mask (b* ((?new-x (!cr4bits->de$inline de x))) (cr4bits-equiv-under-mask new-x x -9)))
Function:
(defun !cr4bits->pse$inline (pse x) (declare (xargs :guard (and (bitp pse) (cr4bits-p x)))) (mbe :logic (b* ((pse (mbe :logic (bfix pse) :exec pse)) (x (cr4bits-fix x))) (part-install pse x :width 1 :low 4)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 6) -17))) (the (unsigned-byte 5) (ash (the (unsigned-byte 1) pse) 4))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pse (b* ((new-x (!cr4bits->pse$inline pse x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pse$inline-of-bfix-pse (equal (!cr4bits->pse$inline (bfix pse) x) (!cr4bits->pse$inline pse x)))
Theorem:
(defthm !cr4bits->pse$inline-bit-equiv-congruence-on-pse (implies (bit-equiv pse pse-equiv) (equal (!cr4bits->pse$inline pse x) (!cr4bits->pse$inline pse-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pse$inline-of-cr4bits-fix-x (equal (!cr4bits->pse$inline pse (cr4bits-fix x)) (!cr4bits->pse$inline pse x)))
Theorem:
(defthm !cr4bits->pse$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pse$inline pse x) (!cr4bits->pse$inline pse x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pse-is-cr4bits (equal (!cr4bits->pse pse x) (change-cr4bits x :pse pse)))
Theorem:
(defthm cr4bits->pse-of-!cr4bits->pse (b* ((?new-x (!cr4bits->pse$inline pse x))) (equal (cr4bits->pse new-x) (bfix pse))))
Theorem:
(defthm !cr4bits->pse-equiv-under-mask (b* ((?new-x (!cr4bits->pse$inline pse x))) (cr4bits-equiv-under-mask new-x x -17)))
Function:
(defun !cr4bits->pae$inline (pae x) (declare (xargs :guard (and (bitp pae) (cr4bits-p x)))) (mbe :logic (b* ((pae (mbe :logic (bfix pae) :exec pae)) (x (cr4bits-fix x))) (part-install pae x :width 1 :low 5)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 7) -33))) (the (unsigned-byte 6) (ash (the (unsigned-byte 1) pae) 5))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pae (b* ((new-x (!cr4bits->pae$inline pae x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pae$inline-of-bfix-pae (equal (!cr4bits->pae$inline (bfix pae) x) (!cr4bits->pae$inline pae x)))
Theorem:
(defthm !cr4bits->pae$inline-bit-equiv-congruence-on-pae (implies (bit-equiv pae pae-equiv) (equal (!cr4bits->pae$inline pae x) (!cr4bits->pae$inline pae-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pae$inline-of-cr4bits-fix-x (equal (!cr4bits->pae$inline pae (cr4bits-fix x)) (!cr4bits->pae$inline pae x)))
Theorem:
(defthm !cr4bits->pae$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pae$inline pae x) (!cr4bits->pae$inline pae x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pae-is-cr4bits (equal (!cr4bits->pae pae x) (change-cr4bits x :pae pae)))
Theorem:
(defthm cr4bits->pae-of-!cr4bits->pae (b* ((?new-x (!cr4bits->pae$inline pae x))) (equal (cr4bits->pae new-x) (bfix pae))))
Theorem:
(defthm !cr4bits->pae-equiv-under-mask (b* ((?new-x (!cr4bits->pae$inline pae x))) (cr4bits-equiv-under-mask new-x x -33)))
Function:
(defun !cr4bits->mce$inline (mce x) (declare (xargs :guard (and (bitp mce) (cr4bits-p x)))) (mbe :logic (b* ((mce (mbe :logic (bfix mce) :exec mce)) (x (cr4bits-fix x))) (part-install mce x :width 1 :low 6)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 8) -65))) (the (unsigned-byte 7) (ash (the (unsigned-byte 1) mce) 6))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->mce (b* ((new-x (!cr4bits->mce$inline mce x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->mce$inline-of-bfix-mce (equal (!cr4bits->mce$inline (bfix mce) x) (!cr4bits->mce$inline mce x)))
Theorem:
(defthm !cr4bits->mce$inline-bit-equiv-congruence-on-mce (implies (bit-equiv mce mce-equiv) (equal (!cr4bits->mce$inline mce x) (!cr4bits->mce$inline mce-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->mce$inline-of-cr4bits-fix-x (equal (!cr4bits->mce$inline mce (cr4bits-fix x)) (!cr4bits->mce$inline mce x)))
Theorem:
(defthm !cr4bits->mce$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->mce$inline mce x) (!cr4bits->mce$inline mce x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->mce-is-cr4bits (equal (!cr4bits->mce mce x) (change-cr4bits x :mce mce)))
Theorem:
(defthm cr4bits->mce-of-!cr4bits->mce (b* ((?new-x (!cr4bits->mce$inline mce x))) (equal (cr4bits->mce new-x) (bfix mce))))
Theorem:
(defthm !cr4bits->mce-equiv-under-mask (b* ((?new-x (!cr4bits->mce$inline mce x))) (cr4bits-equiv-under-mask new-x x -65)))
Function:
(defun !cr4bits->pge$inline (pge x) (declare (xargs :guard (and (bitp pge) (cr4bits-p x)))) (mbe :logic (b* ((pge (mbe :logic (bfix pge) :exec pge)) (x (cr4bits-fix x))) (part-install pge x :width 1 :low 7)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 9) -129))) (the (unsigned-byte 8) (ash (the (unsigned-byte 1) pge) 7))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pge (b* ((new-x (!cr4bits->pge$inline pge x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pge$inline-of-bfix-pge (equal (!cr4bits->pge$inline (bfix pge) x) (!cr4bits->pge$inline pge x)))
Theorem:
(defthm !cr4bits->pge$inline-bit-equiv-congruence-on-pge (implies (bit-equiv pge pge-equiv) (equal (!cr4bits->pge$inline pge x) (!cr4bits->pge$inline pge-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pge$inline-of-cr4bits-fix-x (equal (!cr4bits->pge$inline pge (cr4bits-fix x)) (!cr4bits->pge$inline pge x)))
Theorem:
(defthm !cr4bits->pge$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pge$inline pge x) (!cr4bits->pge$inline pge x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pge-is-cr4bits (equal (!cr4bits->pge pge x) (change-cr4bits x :pge pge)))
Theorem:
(defthm cr4bits->pge-of-!cr4bits->pge (b* ((?new-x (!cr4bits->pge$inline pge x))) (equal (cr4bits->pge new-x) (bfix pge))))
Theorem:
(defthm !cr4bits->pge-equiv-under-mask (b* ((?new-x (!cr4bits->pge$inline pge x))) (cr4bits-equiv-under-mask new-x x -129)))
Function:
(defun !cr4bits->pce$inline (pce x) (declare (xargs :guard (and (bitp pce) (cr4bits-p x)))) (mbe :logic (b* ((pce (mbe :logic (bfix pce) :exec pce)) (x (cr4bits-fix x))) (part-install pce x :width 1 :low 8)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 10) -257))) (the (unsigned-byte 9) (ash (the (unsigned-byte 1) pce) 8))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pce (b* ((new-x (!cr4bits->pce$inline pce x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pce$inline-of-bfix-pce (equal (!cr4bits->pce$inline (bfix pce) x) (!cr4bits->pce$inline pce x)))
Theorem:
(defthm !cr4bits->pce$inline-bit-equiv-congruence-on-pce (implies (bit-equiv pce pce-equiv) (equal (!cr4bits->pce$inline pce x) (!cr4bits->pce$inline pce-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pce$inline-of-cr4bits-fix-x (equal (!cr4bits->pce$inline pce (cr4bits-fix x)) (!cr4bits->pce$inline pce x)))
Theorem:
(defthm !cr4bits->pce$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pce$inline pce x) (!cr4bits->pce$inline pce x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pce-is-cr4bits (equal (!cr4bits->pce pce x) (change-cr4bits x :pce pce)))
Theorem:
(defthm cr4bits->pce-of-!cr4bits->pce (b* ((?new-x (!cr4bits->pce$inline pce x))) (equal (cr4bits->pce new-x) (bfix pce))))
Theorem:
(defthm !cr4bits->pce-equiv-under-mask (b* ((?new-x (!cr4bits->pce$inline pce x))) (cr4bits-equiv-under-mask new-x x -257)))
Function:
(defun !cr4bits->osfxsr$inline (osfxsr x) (declare (xargs :guard (and (bitp osfxsr) (cr4bits-p x)))) (mbe :logic (b* ((osfxsr (mbe :logic (bfix osfxsr) :exec osfxsr)) (x (cr4bits-fix x))) (part-install osfxsr x :width 1 :low 9)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 11) -513))) (the (unsigned-byte 10) (ash (the (unsigned-byte 1) osfxsr) 9))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->osfxsr (b* ((new-x (!cr4bits->osfxsr$inline osfxsr x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->osfxsr$inline-of-bfix-osfxsr (equal (!cr4bits->osfxsr$inline (bfix osfxsr) x) (!cr4bits->osfxsr$inline osfxsr x)))
Theorem:
(defthm !cr4bits->osfxsr$inline-bit-equiv-congruence-on-osfxsr (implies (bit-equiv osfxsr osfxsr-equiv) (equal (!cr4bits->osfxsr$inline osfxsr x) (!cr4bits->osfxsr$inline osfxsr-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->osfxsr$inline-of-cr4bits-fix-x (equal (!cr4bits->osfxsr$inline osfxsr (cr4bits-fix x)) (!cr4bits->osfxsr$inline osfxsr x)))
Theorem:
(defthm !cr4bits->osfxsr$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->osfxsr$inline osfxsr x) (!cr4bits->osfxsr$inline osfxsr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->osfxsr-is-cr4bits (equal (!cr4bits->osfxsr osfxsr x) (change-cr4bits x :osfxsr osfxsr)))
Theorem:
(defthm cr4bits->osfxsr-of-!cr4bits->osfxsr (b* ((?new-x (!cr4bits->osfxsr$inline osfxsr x))) (equal (cr4bits->osfxsr new-x) (bfix osfxsr))))
Theorem:
(defthm !cr4bits->osfxsr-equiv-under-mask (b* ((?new-x (!cr4bits->osfxsr$inline osfxsr x))) (cr4bits-equiv-under-mask new-x x -513)))
Function:
(defun !cr4bits->osxmmexcpt$inline (osxmmexcpt x) (declare (xargs :guard (and (bitp osxmmexcpt) (cr4bits-p x)))) (mbe :logic (b* ((osxmmexcpt (mbe :logic (bfix osxmmexcpt) :exec osxmmexcpt)) (x (cr4bits-fix x))) (part-install osxmmexcpt x :width 1 :low 10)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 12) -1025))) (the (unsigned-byte 11) (ash (the (unsigned-byte 1) osxmmexcpt) 10))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->osxmmexcpt (b* ((new-x (!cr4bits->osxmmexcpt$inline osxmmexcpt x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->osxmmexcpt$inline-of-bfix-osxmmexcpt (equal (!cr4bits->osxmmexcpt$inline (bfix osxmmexcpt) x) (!cr4bits->osxmmexcpt$inline osxmmexcpt x)))
Theorem:
(defthm !cr4bits->osxmmexcpt$inline-bit-equiv-congruence-on-osxmmexcpt (implies (bit-equiv osxmmexcpt osxmmexcpt-equiv) (equal (!cr4bits->osxmmexcpt$inline osxmmexcpt x) (!cr4bits->osxmmexcpt$inline osxmmexcpt-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->osxmmexcpt$inline-of-cr4bits-fix-x (equal (!cr4bits->osxmmexcpt$inline osxmmexcpt (cr4bits-fix x)) (!cr4bits->osxmmexcpt$inline osxmmexcpt x)))
Theorem:
(defthm !cr4bits->osxmmexcpt$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->osxmmexcpt$inline osxmmexcpt x) (!cr4bits->osxmmexcpt$inline osxmmexcpt x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->osxmmexcpt-is-cr4bits (equal (!cr4bits->osxmmexcpt osxmmexcpt x) (change-cr4bits x :osxmmexcpt osxmmexcpt)))
Theorem:
(defthm cr4bits->osxmmexcpt-of-!cr4bits->osxmmexcpt (b* ((?new-x (!cr4bits->osxmmexcpt$inline osxmmexcpt x))) (equal (cr4bits->osxmmexcpt new-x) (bfix osxmmexcpt))))
Theorem:
(defthm !cr4bits->osxmmexcpt-equiv-under-mask (b* ((?new-x (!cr4bits->osxmmexcpt$inline osxmmexcpt x))) (cr4bits-equiv-under-mask new-x x -1025)))
Function:
(defun !cr4bits->umip$inline (umip x) (declare (xargs :guard (and (bitp umip) (cr4bits-p x)))) (mbe :logic (b* ((umip (mbe :logic (bfix umip) :exec umip)) (x (cr4bits-fix x))) (part-install umip x :width 1 :low 11)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 13) -2049))) (the (unsigned-byte 12) (ash (the (unsigned-byte 1) umip) 11))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->umip (b* ((new-x (!cr4bits->umip$inline umip x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->umip$inline-of-bfix-umip (equal (!cr4bits->umip$inline (bfix umip) x) (!cr4bits->umip$inline umip x)))
Theorem:
(defthm !cr4bits->umip$inline-bit-equiv-congruence-on-umip (implies (bit-equiv umip umip-equiv) (equal (!cr4bits->umip$inline umip x) (!cr4bits->umip$inline umip-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->umip$inline-of-cr4bits-fix-x (equal (!cr4bits->umip$inline umip (cr4bits-fix x)) (!cr4bits->umip$inline umip x)))
Theorem:
(defthm !cr4bits->umip$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->umip$inline umip x) (!cr4bits->umip$inline umip x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->umip-is-cr4bits (equal (!cr4bits->umip umip x) (change-cr4bits x :umip umip)))
Theorem:
(defthm cr4bits->umip-of-!cr4bits->umip (b* ((?new-x (!cr4bits->umip$inline umip x))) (equal (cr4bits->umip new-x) (bfix umip))))
Theorem:
(defthm !cr4bits->umip-equiv-under-mask (b* ((?new-x (!cr4bits->umip$inline umip x))) (cr4bits-equiv-under-mask new-x x -2049)))
Function:
(defun !cr4bits->la57$inline (la57 x) (declare (xargs :guard (and (bitp la57) (cr4bits-p x)))) (mbe :logic (b* ((la57 (mbe :logic (bfix la57) :exec la57)) (x (cr4bits-fix x))) (part-install la57 x :width 1 :low 12)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 14) -4097))) (the (unsigned-byte 13) (ash (the (unsigned-byte 1) la57) 12))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->la57 (b* ((new-x (!cr4bits->la57$inline la57 x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->la57$inline-of-bfix-la57 (equal (!cr4bits->la57$inline (bfix la57) x) (!cr4bits->la57$inline la57 x)))
Theorem:
(defthm !cr4bits->la57$inline-bit-equiv-congruence-on-la57 (implies (bit-equiv la57 la57-equiv) (equal (!cr4bits->la57$inline la57 x) (!cr4bits->la57$inline la57-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->la57$inline-of-cr4bits-fix-x (equal (!cr4bits->la57$inline la57 (cr4bits-fix x)) (!cr4bits->la57$inline la57 x)))
Theorem:
(defthm !cr4bits->la57$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->la57$inline la57 x) (!cr4bits->la57$inline la57 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->la57-is-cr4bits (equal (!cr4bits->la57 la57 x) (change-cr4bits x :la57 la57)))
Theorem:
(defthm cr4bits->la57-of-!cr4bits->la57 (b* ((?new-x (!cr4bits->la57$inline la57 x))) (equal (cr4bits->la57 new-x) (bfix la57))))
Theorem:
(defthm !cr4bits->la57-equiv-under-mask (b* ((?new-x (!cr4bits->la57$inline la57 x))) (cr4bits-equiv-under-mask new-x x -4097)))
Function:
(defun !cr4bits->vmxe$inline (vmxe x) (declare (xargs :guard (and (bitp vmxe) (cr4bits-p x)))) (mbe :logic (b* ((vmxe (mbe :logic (bfix vmxe) :exec vmxe)) (x (cr4bits-fix x))) (part-install vmxe x :width 1 :low 13)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 15) -8193))) (the (unsigned-byte 14) (ash (the (unsigned-byte 1) vmxe) 13))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->vmxe (b* ((new-x (!cr4bits->vmxe$inline vmxe x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->vmxe$inline-of-bfix-vmxe (equal (!cr4bits->vmxe$inline (bfix vmxe) x) (!cr4bits->vmxe$inline vmxe x)))
Theorem:
(defthm !cr4bits->vmxe$inline-bit-equiv-congruence-on-vmxe (implies (bit-equiv vmxe vmxe-equiv) (equal (!cr4bits->vmxe$inline vmxe x) (!cr4bits->vmxe$inline vmxe-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->vmxe$inline-of-cr4bits-fix-x (equal (!cr4bits->vmxe$inline vmxe (cr4bits-fix x)) (!cr4bits->vmxe$inline vmxe x)))
Theorem:
(defthm !cr4bits->vmxe$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->vmxe$inline vmxe x) (!cr4bits->vmxe$inline vmxe x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->vmxe-is-cr4bits (equal (!cr4bits->vmxe vmxe x) (change-cr4bits x :vmxe vmxe)))
Theorem:
(defthm cr4bits->vmxe-of-!cr4bits->vmxe (b* ((?new-x (!cr4bits->vmxe$inline vmxe x))) (equal (cr4bits->vmxe new-x) (bfix vmxe))))
Theorem:
(defthm !cr4bits->vmxe-equiv-under-mask (b* ((?new-x (!cr4bits->vmxe$inline vmxe x))) (cr4bits-equiv-under-mask new-x x -8193)))
Function:
(defun !cr4bits->smxe$inline (smxe x) (declare (xargs :guard (and (bitp smxe) (cr4bits-p x)))) (mbe :logic (b* ((smxe (mbe :logic (bfix smxe) :exec smxe)) (x (cr4bits-fix x))) (part-install smxe x :width 1 :low 14)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 16) -16385))) (the (unsigned-byte 15) (ash (the (unsigned-byte 1) smxe) 14))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->smxe (b* ((new-x (!cr4bits->smxe$inline smxe x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->smxe$inline-of-bfix-smxe (equal (!cr4bits->smxe$inline (bfix smxe) x) (!cr4bits->smxe$inline smxe x)))
Theorem:
(defthm !cr4bits->smxe$inline-bit-equiv-congruence-on-smxe (implies (bit-equiv smxe smxe-equiv) (equal (!cr4bits->smxe$inline smxe x) (!cr4bits->smxe$inline smxe-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->smxe$inline-of-cr4bits-fix-x (equal (!cr4bits->smxe$inline smxe (cr4bits-fix x)) (!cr4bits->smxe$inline smxe x)))
Theorem:
(defthm !cr4bits->smxe$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->smxe$inline smxe x) (!cr4bits->smxe$inline smxe x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->smxe-is-cr4bits (equal (!cr4bits->smxe smxe x) (change-cr4bits x :smxe smxe)))
Theorem:
(defthm cr4bits->smxe-of-!cr4bits->smxe (b* ((?new-x (!cr4bits->smxe$inline smxe x))) (equal (cr4bits->smxe new-x) (bfix smxe))))
Theorem:
(defthm !cr4bits->smxe-equiv-under-mask (b* ((?new-x (!cr4bits->smxe$inline smxe x))) (cr4bits-equiv-under-mask new-x x -16385)))
Function:
(defun !cr4bits->res1$inline (res1 x) (declare (xargs :guard (and (bitp res1) (cr4bits-p x)))) (mbe :logic (b* ((res1 (mbe :logic (bfix res1) :exec res1)) (x (cr4bits-fix x))) (part-install res1 x :width 1 :low 15)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 17) -32769))) (the (unsigned-byte 16) (ash (the (unsigned-byte 1) res1) 15))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->res1 (b* ((new-x (!cr4bits->res1$inline res1 x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->res1$inline-of-bfix-res1 (equal (!cr4bits->res1$inline (bfix res1) x) (!cr4bits->res1$inline res1 x)))
Theorem:
(defthm !cr4bits->res1$inline-bit-equiv-congruence-on-res1 (implies (bit-equiv res1 res1-equiv) (equal (!cr4bits->res1$inline res1 x) (!cr4bits->res1$inline res1-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->res1$inline-of-cr4bits-fix-x (equal (!cr4bits->res1$inline res1 (cr4bits-fix x)) (!cr4bits->res1$inline res1 x)))
Theorem:
(defthm !cr4bits->res1$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->res1$inline res1 x) (!cr4bits->res1$inline res1 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->res1-is-cr4bits (equal (!cr4bits->res1 res1 x) (change-cr4bits x :res1 res1)))
Theorem:
(defthm cr4bits->res1-of-!cr4bits->res1 (b* ((?new-x (!cr4bits->res1$inline res1 x))) (equal (cr4bits->res1 new-x) (bfix res1))))
Theorem:
(defthm !cr4bits->res1-equiv-under-mask (b* ((?new-x (!cr4bits->res1$inline res1 x))) (cr4bits-equiv-under-mask new-x x -32769)))
Function:
(defun !cr4bits->fsgsbase$inline (fsgsbase x) (declare (xargs :guard (and (bitp fsgsbase) (cr4bits-p x)))) (mbe :logic (b* ((fsgsbase (mbe :logic (bfix fsgsbase) :exec fsgsbase)) (x (cr4bits-fix x))) (part-install fsgsbase x :width 1 :low 16)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 18) -65537))) (the (unsigned-byte 17) (ash (the (unsigned-byte 1) fsgsbase) 16))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->fsgsbase (b* ((new-x (!cr4bits->fsgsbase$inline fsgsbase x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->fsgsbase$inline-of-bfix-fsgsbase (equal (!cr4bits->fsgsbase$inline (bfix fsgsbase) x) (!cr4bits->fsgsbase$inline fsgsbase x)))
Theorem:
(defthm !cr4bits->fsgsbase$inline-bit-equiv-congruence-on-fsgsbase (implies (bit-equiv fsgsbase fsgsbase-equiv) (equal (!cr4bits->fsgsbase$inline fsgsbase x) (!cr4bits->fsgsbase$inline fsgsbase-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->fsgsbase$inline-of-cr4bits-fix-x (equal (!cr4bits->fsgsbase$inline fsgsbase (cr4bits-fix x)) (!cr4bits->fsgsbase$inline fsgsbase x)))
Theorem:
(defthm !cr4bits->fsgsbase$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->fsgsbase$inline fsgsbase x) (!cr4bits->fsgsbase$inline fsgsbase x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->fsgsbase-is-cr4bits (equal (!cr4bits->fsgsbase fsgsbase x) (change-cr4bits x :fsgsbase fsgsbase)))
Theorem:
(defthm cr4bits->fsgsbase-of-!cr4bits->fsgsbase (b* ((?new-x (!cr4bits->fsgsbase$inline fsgsbase x))) (equal (cr4bits->fsgsbase new-x) (bfix fsgsbase))))
Theorem:
(defthm !cr4bits->fsgsbase-equiv-under-mask (b* ((?new-x (!cr4bits->fsgsbase$inline fsgsbase x))) (cr4bits-equiv-under-mask new-x x -65537)))
Function:
(defun !cr4bits->pcide$inline (pcide x) (declare (xargs :guard (and (bitp pcide) (cr4bits-p x)))) (mbe :logic (b* ((pcide (mbe :logic (bfix pcide) :exec pcide)) (x (cr4bits-fix x))) (part-install pcide x :width 1 :low 17)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 19) -131073))) (the (unsigned-byte 18) (ash (the (unsigned-byte 1) pcide) 17))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pcide (b* ((new-x (!cr4bits->pcide$inline pcide x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pcide$inline-of-bfix-pcide (equal (!cr4bits->pcide$inline (bfix pcide) x) (!cr4bits->pcide$inline pcide x)))
Theorem:
(defthm !cr4bits->pcide$inline-bit-equiv-congruence-on-pcide (implies (bit-equiv pcide pcide-equiv) (equal (!cr4bits->pcide$inline pcide x) (!cr4bits->pcide$inline pcide-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pcide$inline-of-cr4bits-fix-x (equal (!cr4bits->pcide$inline pcide (cr4bits-fix x)) (!cr4bits->pcide$inline pcide x)))
Theorem:
(defthm !cr4bits->pcide$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pcide$inline pcide x) (!cr4bits->pcide$inline pcide x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pcide-is-cr4bits (equal (!cr4bits->pcide pcide x) (change-cr4bits x :pcide pcide)))
Theorem:
(defthm cr4bits->pcide-of-!cr4bits->pcide (b* ((?new-x (!cr4bits->pcide$inline pcide x))) (equal (cr4bits->pcide new-x) (bfix pcide))))
Theorem:
(defthm !cr4bits->pcide-equiv-under-mask (b* ((?new-x (!cr4bits->pcide$inline pcide x))) (cr4bits-equiv-under-mask new-x x -131073)))
Function:
(defun !cr4bits->osxsave$inline (osxsave x) (declare (xargs :guard (and (bitp osxsave) (cr4bits-p x)))) (mbe :logic (b* ((osxsave (mbe :logic (bfix osxsave) :exec osxsave)) (x (cr4bits-fix x))) (part-install osxsave x :width 1 :low 18)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 20) -262145))) (the (unsigned-byte 19) (ash (the (unsigned-byte 1) osxsave) 18))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->osxsave (b* ((new-x (!cr4bits->osxsave$inline osxsave x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->osxsave$inline-of-bfix-osxsave (equal (!cr4bits->osxsave$inline (bfix osxsave) x) (!cr4bits->osxsave$inline osxsave x)))
Theorem:
(defthm !cr4bits->osxsave$inline-bit-equiv-congruence-on-osxsave (implies (bit-equiv osxsave osxsave-equiv) (equal (!cr4bits->osxsave$inline osxsave x) (!cr4bits->osxsave$inline osxsave-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->osxsave$inline-of-cr4bits-fix-x (equal (!cr4bits->osxsave$inline osxsave (cr4bits-fix x)) (!cr4bits->osxsave$inline osxsave x)))
Theorem:
(defthm !cr4bits->osxsave$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->osxsave$inline osxsave x) (!cr4bits->osxsave$inline osxsave x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->osxsave-is-cr4bits (equal (!cr4bits->osxsave osxsave x) (change-cr4bits x :osxsave osxsave)))
Theorem:
(defthm cr4bits->osxsave-of-!cr4bits->osxsave (b* ((?new-x (!cr4bits->osxsave$inline osxsave x))) (equal (cr4bits->osxsave new-x) (bfix osxsave))))
Theorem:
(defthm !cr4bits->osxsave-equiv-under-mask (b* ((?new-x (!cr4bits->osxsave$inline osxsave x))) (cr4bits-equiv-under-mask new-x x -262145)))
Function:
(defun !cr4bits->kl$inline (kl x) (declare (xargs :guard (and (bitp kl) (cr4bits-p x)))) (mbe :logic (b* ((kl (mbe :logic (bfix kl) :exec kl)) (x (cr4bits-fix x))) (part-install kl x :width 1 :low 19)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 21) -524289))) (the (unsigned-byte 20) (ash (the (unsigned-byte 1) kl) 19))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->kl (b* ((new-x (!cr4bits->kl$inline kl x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->kl$inline-of-bfix-kl (equal (!cr4bits->kl$inline (bfix kl) x) (!cr4bits->kl$inline kl x)))
Theorem:
(defthm !cr4bits->kl$inline-bit-equiv-congruence-on-kl (implies (bit-equiv kl kl-equiv) (equal (!cr4bits->kl$inline kl x) (!cr4bits->kl$inline kl-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->kl$inline-of-cr4bits-fix-x (equal (!cr4bits->kl$inline kl (cr4bits-fix x)) (!cr4bits->kl$inline kl x)))
Theorem:
(defthm !cr4bits->kl$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->kl$inline kl x) (!cr4bits->kl$inline kl x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->kl-is-cr4bits (equal (!cr4bits->kl kl x) (change-cr4bits x :kl kl)))
Theorem:
(defthm cr4bits->kl-of-!cr4bits->kl (b* ((?new-x (!cr4bits->kl$inline kl x))) (equal (cr4bits->kl new-x) (bfix kl))))
Theorem:
(defthm !cr4bits->kl-equiv-under-mask (b* ((?new-x (!cr4bits->kl$inline kl x))) (cr4bits-equiv-under-mask new-x x -524289)))
Function:
(defun !cr4bits->smep$inline (smep x) (declare (xargs :guard (and (bitp smep) (cr4bits-p x)))) (mbe :logic (b* ((smep (mbe :logic (bfix smep) :exec smep)) (x (cr4bits-fix x))) (part-install smep x :width 1 :low 20)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 22) -1048577))) (the (unsigned-byte 21) (ash (the (unsigned-byte 1) smep) 20))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->smep (b* ((new-x (!cr4bits->smep$inline smep x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->smep$inline-of-bfix-smep (equal (!cr4bits->smep$inline (bfix smep) x) (!cr4bits->smep$inline smep x)))
Theorem:
(defthm !cr4bits->smep$inline-bit-equiv-congruence-on-smep (implies (bit-equiv smep smep-equiv) (equal (!cr4bits->smep$inline smep x) (!cr4bits->smep$inline smep-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->smep$inline-of-cr4bits-fix-x (equal (!cr4bits->smep$inline smep (cr4bits-fix x)) (!cr4bits->smep$inline smep x)))
Theorem:
(defthm !cr4bits->smep$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->smep$inline smep x) (!cr4bits->smep$inline smep x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->smep-is-cr4bits (equal (!cr4bits->smep smep x) (change-cr4bits x :smep smep)))
Theorem:
(defthm cr4bits->smep-of-!cr4bits->smep (b* ((?new-x (!cr4bits->smep$inline smep x))) (equal (cr4bits->smep new-x) (bfix smep))))
Theorem:
(defthm !cr4bits->smep-equiv-under-mask (b* ((?new-x (!cr4bits->smep$inline smep x))) (cr4bits-equiv-under-mask new-x x -1048577)))
Function:
(defun !cr4bits->smap$inline (smap x) (declare (xargs :guard (and (bitp smap) (cr4bits-p x)))) (mbe :logic (b* ((smap (mbe :logic (bfix smap) :exec smap)) (x (cr4bits-fix x))) (part-install smap x :width 1 :low 21)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 23) -2097153))) (the (unsigned-byte 22) (ash (the (unsigned-byte 1) smap) 21))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->smap (b* ((new-x (!cr4bits->smap$inline smap x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->smap$inline-of-bfix-smap (equal (!cr4bits->smap$inline (bfix smap) x) (!cr4bits->smap$inline smap x)))
Theorem:
(defthm !cr4bits->smap$inline-bit-equiv-congruence-on-smap (implies (bit-equiv smap smap-equiv) (equal (!cr4bits->smap$inline smap x) (!cr4bits->smap$inline smap-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->smap$inline-of-cr4bits-fix-x (equal (!cr4bits->smap$inline smap (cr4bits-fix x)) (!cr4bits->smap$inline smap x)))
Theorem:
(defthm !cr4bits->smap$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->smap$inline smap x) (!cr4bits->smap$inline smap x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->smap-is-cr4bits (equal (!cr4bits->smap smap x) (change-cr4bits x :smap smap)))
Theorem:
(defthm cr4bits->smap-of-!cr4bits->smap (b* ((?new-x (!cr4bits->smap$inline smap x))) (equal (cr4bits->smap new-x) (bfix smap))))
Theorem:
(defthm !cr4bits->smap-equiv-under-mask (b* ((?new-x (!cr4bits->smap$inline smap x))) (cr4bits-equiv-under-mask new-x x -2097153)))
Function:
(defun !cr4bits->pke$inline (pke x) (declare (xargs :guard (and (bitp pke) (cr4bits-p x)))) (mbe :logic (b* ((pke (mbe :logic (bfix pke) :exec pke)) (x (cr4bits-fix x))) (part-install pke x :width 1 :low 22)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 24) -4194305))) (the (unsigned-byte 23) (ash (the (unsigned-byte 1) pke) 22))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pke (b* ((new-x (!cr4bits->pke$inline pke x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pke$inline-of-bfix-pke (equal (!cr4bits->pke$inline (bfix pke) x) (!cr4bits->pke$inline pke x)))
Theorem:
(defthm !cr4bits->pke$inline-bit-equiv-congruence-on-pke (implies (bit-equiv pke pke-equiv) (equal (!cr4bits->pke$inline pke x) (!cr4bits->pke$inline pke-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pke$inline-of-cr4bits-fix-x (equal (!cr4bits->pke$inline pke (cr4bits-fix x)) (!cr4bits->pke$inline pke x)))
Theorem:
(defthm !cr4bits->pke$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pke$inline pke x) (!cr4bits->pke$inline pke x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pke-is-cr4bits (equal (!cr4bits->pke pke x) (change-cr4bits x :pke pke)))
Theorem:
(defthm cr4bits->pke-of-!cr4bits->pke (b* ((?new-x (!cr4bits->pke$inline pke x))) (equal (cr4bits->pke new-x) (bfix pke))))
Theorem:
(defthm !cr4bits->pke-equiv-under-mask (b* ((?new-x (!cr4bits->pke$inline pke x))) (cr4bits-equiv-under-mask new-x x -4194305)))
Function:
(defun !cr4bits->cet$inline (cet x) (declare (xargs :guard (and (bitp cet) (cr4bits-p x)))) (mbe :logic (b* ((cet (mbe :logic (bfix cet) :exec cet)) (x (cr4bits-fix x))) (part-install cet x :width 1 :low 23)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 25) -8388609))) (the (unsigned-byte 24) (ash (the (unsigned-byte 1) cet) 23))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->cet (b* ((new-x (!cr4bits->cet$inline cet x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->cet$inline-of-bfix-cet (equal (!cr4bits->cet$inline (bfix cet) x) (!cr4bits->cet$inline cet x)))
Theorem:
(defthm !cr4bits->cet$inline-bit-equiv-congruence-on-cet (implies (bit-equiv cet cet-equiv) (equal (!cr4bits->cet$inline cet x) (!cr4bits->cet$inline cet-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->cet$inline-of-cr4bits-fix-x (equal (!cr4bits->cet$inline cet (cr4bits-fix x)) (!cr4bits->cet$inline cet x)))
Theorem:
(defthm !cr4bits->cet$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->cet$inline cet x) (!cr4bits->cet$inline cet x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->cet-is-cr4bits (equal (!cr4bits->cet cet x) (change-cr4bits x :cet cet)))
Theorem:
(defthm cr4bits->cet-of-!cr4bits->cet (b* ((?new-x (!cr4bits->cet$inline cet x))) (equal (cr4bits->cet new-x) (bfix cet))))
Theorem:
(defthm !cr4bits->cet-equiv-under-mask (b* ((?new-x (!cr4bits->cet$inline cet x))) (cr4bits-equiv-under-mask new-x x -8388609)))
Function:
(defun !cr4bits->pks$inline (pks x) (declare (xargs :guard (and (bitp pks) (cr4bits-p x)))) (mbe :logic (b* ((pks (mbe :logic (bfix pks) :exec pks)) (x (cr4bits-fix x))) (part-install pks x :width 1 :low 24)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 26) -16777217))) (the (unsigned-byte 25) (ash (the (unsigned-byte 1) pks) 24))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->pks (b* ((new-x (!cr4bits->pks$inline pks x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->pks$inline-of-bfix-pks (equal (!cr4bits->pks$inline (bfix pks) x) (!cr4bits->pks$inline pks x)))
Theorem:
(defthm !cr4bits->pks$inline-bit-equiv-congruence-on-pks (implies (bit-equiv pks pks-equiv) (equal (!cr4bits->pks$inline pks x) (!cr4bits->pks$inline pks-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pks$inline-of-cr4bits-fix-x (equal (!cr4bits->pks$inline pks (cr4bits-fix x)) (!cr4bits->pks$inline pks x)))
Theorem:
(defthm !cr4bits->pks$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->pks$inline pks x) (!cr4bits->pks$inline pks x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->pks-is-cr4bits (equal (!cr4bits->pks pks x) (change-cr4bits x :pks pks)))
Theorem:
(defthm cr4bits->pks-of-!cr4bits->pks (b* ((?new-x (!cr4bits->pks$inline pks x))) (equal (cr4bits->pks new-x) (bfix pks))))
Theorem:
(defthm !cr4bits->pks-equiv-under-mask (b* ((?new-x (!cr4bits->pks$inline pks x))) (cr4bits-equiv-under-mask new-x x -16777217)))
Function:
(defun !cr4bits->uintr$inline (uintr x) (declare (xargs :guard (and (bitp uintr) (cr4bits-p x)))) (mbe :logic (b* ((uintr (mbe :logic (bfix uintr) :exec uintr)) (x (cr4bits-fix x))) (part-install uintr x :width 1 :low 25)) :exec (the (unsigned-byte 26) (logior (the (unsigned-byte 26) (logand (the (unsigned-byte 26) x) (the (signed-byte 27) -33554433))) (the (unsigned-byte 26) (ash (the (unsigned-byte 1) uintr) 25))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->uintr (b* ((new-x (!cr4bits->uintr$inline uintr x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->uintr$inline-of-bfix-uintr (equal (!cr4bits->uintr$inline (bfix uintr) x) (!cr4bits->uintr$inline uintr x)))
Theorem:
(defthm !cr4bits->uintr$inline-bit-equiv-congruence-on-uintr (implies (bit-equiv uintr uintr-equiv) (equal (!cr4bits->uintr$inline uintr x) (!cr4bits->uintr$inline uintr-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->uintr$inline-of-cr4bits-fix-x (equal (!cr4bits->uintr$inline uintr (cr4bits-fix x)) (!cr4bits->uintr$inline uintr x)))
Theorem:
(defthm !cr4bits->uintr$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->uintr$inline uintr x) (!cr4bits->uintr$inline uintr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->uintr-is-cr4bits (equal (!cr4bits->uintr uintr x) (change-cr4bits x :uintr uintr)))
Theorem:
(defthm cr4bits->uintr-of-!cr4bits->uintr (b* ((?new-x (!cr4bits->uintr$inline uintr x))) (equal (cr4bits->uintr new-x) (bfix uintr))))
Theorem:
(defthm !cr4bits->uintr-equiv-under-mask (b* ((?new-x (!cr4bits->uintr$inline uintr x))) (cr4bits-equiv-under-mask new-x x 33554431)))
Function:
(defun cr4bits-debug$inline (x) (declare (xargs :guard (cr4bits-p x))) (b* (((cr4bits x))) (cons (cons 'vme x.vme) (cons (cons 'pvi x.pvi) (cons (cons 'tsd x.tsd) (cons (cons 'de x.de) (cons (cons 'pse x.pse) (cons (cons 'pae x.pae) (cons (cons 'mce x.mce) (cons (cons 'pge x.pge) (cons (cons 'pce x.pce) (cons (cons 'osfxsr x.osfxsr) (cons (cons 'osxmmexcpt x.osxmmexcpt) (cons (cons 'umip x.umip) (cons (cons 'la57 x.la57) (cons (cons 'vmxe x.vmxe) (cons (cons 'smxe x.smxe) (cons (cons 'res1 x.res1) (cons (cons 'fsgsbase x.fsgsbase) (cons (cons 'pcide x.pcide) (cons (cons 'osxsave x.osxsave) (cons (cons 'kl x.kl) (cons (cons 'smep x.smep) (cons (cons 'smap x.smap) (cons (cons 'pke x.pke) (cons (cons 'cet x.cet) (cons (cons 'pks x.pks) (cons (cons 'uintr x.uintr) nil))))))))))))))))))))))))))))