An 22-bit unsigned bitstruct type.
This is a bitstruct type introduced by defbitstruct, represented as a unsigned 22-bit integer.
Source: Intel Manual, Feb-14, Vol. 3A, Section 2.5
Function:
(defun cr4bits-p$inline (x) (declare (xargs :guard t)) (mbe :logic (unsigned-byte-p 22 x) :exec (and (natp x) (< x 4194304))))
Theorem:
(defthm cr4bits-p-when-unsigned-byte-p (implies (unsigned-byte-p 22 x) (cr4bits-p x)))
Theorem:
(defthm unsigned-byte-p-when-cr4bits-p (implies (cr4bits-p x) (unsigned-byte-p 22 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 22 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 res2 smep smap) (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 res2) (bitp smep) (bitp smap)))) (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)) (res2 (mbe :logic (bfix res2) :exec res2)) (smep (mbe :logic (bfix smep) :exec smep)) (smap (mbe :logic (bfix smap) :exec smap))) (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 res2 (logapp 1 smep smap)))))))))))))))))))))))
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 res2 smep smap))) (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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme-equiv pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi-equiv tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd-equiv de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de-equiv pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse-equiv pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae-equiv mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce-equiv pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge-equiv pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce-equiv osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr-equiv osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt-equiv umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip-equiv la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57-equiv vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe-equiv smxe res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe-equiv res1 fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1-equiv fsgsbase pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase-equiv pcide osxsave res2 smep smap))) :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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide-equiv osxsave res2 smep smap))) :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) res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave-equiv res2 smep smap))) :rule-classes :congruence)
Theorem:
(defthm cr4bits$inline-of-bfix-res2 (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave (bfix res2) smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
Theorem:
(defthm cr4bits$inline-bit-equiv-congruence-on-res2 (implies (bit-equiv res2 res2-equiv) (equal (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2-equiv smep smap))) :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 res2 (bfix smep) smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep-equiv smap))) :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 res2 smep (bfix smap)) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)))
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 res2 smep smap) (cr4bits$inline vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap-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 22) 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 res2 smep smap)) (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 21) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 20) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 19) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 18) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 17) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 16) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 15) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 14) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 13) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 12) (ash (the (unsigned-byte 22) x) -10))))))
Theorem:
(defthm bitp-of-cr4bits->osxmmexcpt (b* ((osxmmexcpt (cr4bits->osxmmexcpt$inline x))) (bitp osxmmexcpt)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->osxmmexcpt$inline-of-cr4bits-fix-x (equal (cr4bits->osxmmexcpt$inline (cr4bits-fix x)) (cr4bits->osxmmexcpt$inline x)))
Theorem:
(defthm cr4bits->osxmmexcpt$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->osxmmexcpt$inline x) (cr4bits->osxmmexcpt$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->osxmmexcpt-of-cr4bits (equal (cr4bits->osxmmexcpt (cr4bits vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)) (bfix osxmmexcpt)))
Theorem:
(defthm cr4bits->osxmmexcpt-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x cr4bits-equiv-under-mask) (cr4bits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 1024) 0)) (equal (cr4bits->osxmmexcpt x) (cr4bits->osxmmexcpt y))))
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 11) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 10) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 9) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 8) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 7) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 6) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 5) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 4) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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->res2$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 3) (ash (the (unsigned-byte 22) x) -19))))))
Theorem:
(defthm bitp-of-cr4bits->res2 (b* ((res2 (cr4bits->res2$inline x))) (bitp res2)) :rule-classes :rewrite)
Theorem:
(defthm cr4bits->res2$inline-of-cr4bits-fix-x (equal (cr4bits->res2$inline (cr4bits-fix x)) (cr4bits->res2$inline x)))
Theorem:
(defthm cr4bits->res2$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (cr4bits->res2$inline x) (cr4bits->res2$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cr4bits->res2-of-cr4bits (equal (cr4bits->res2 (cr4bits vme pvi tsd de pse pae mce pge pce osfxsr osxmmexcpt umip la57 vmxe smxe res1 fsgsbase pcide osxsave res2 smep smap)) (bfix res2)))
Theorem:
(defthm cr4bits->res2-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->res2 x) (cr4bits->res2 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 2) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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 1) (ash (the (unsigned-byte 22) 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 res2 smep smap)) (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))))
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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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->res2$inline (res2 x) (declare (xargs :guard (and (bitp res2) (cr4bits-p x)))) (mbe :logic (b* ((res2 (mbe :logic (bfix res2) :exec res2)) (x (cr4bits-fix x))) (part-install res2 x :width 1 :low 19)) :exec (the (unsigned-byte 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) x) (the (signed-byte 21) -524289))) (the (unsigned-byte 20) (ash (the (unsigned-byte 1) res2) 19))))))
Theorem:
(defthm cr4bits-p-of-!cr4bits->res2 (b* ((new-x (!cr4bits->res2$inline res2 x))) (cr4bits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cr4bits->res2$inline-of-bfix-res2 (equal (!cr4bits->res2$inline (bfix res2) x) (!cr4bits->res2$inline res2 x)))
Theorem:
(defthm !cr4bits->res2$inline-bit-equiv-congruence-on-res2 (implies (bit-equiv res2 res2-equiv) (equal (!cr4bits->res2$inline res2 x) (!cr4bits->res2$inline res2-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->res2$inline-of-cr4bits-fix-x (equal (!cr4bits->res2$inline res2 (cr4bits-fix x)) (!cr4bits->res2$inline res2 x)))
Theorem:
(defthm !cr4bits->res2$inline-cr4bits-equiv-congruence-on-x (implies (cr4bits-equiv x x-equiv) (equal (!cr4bits->res2$inline res2 x) (!cr4bits->res2$inline res2 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cr4bits->res2-is-cr4bits (equal (!cr4bits->res2 res2 x) (change-cr4bits x :res2 res2)))
Theorem:
(defthm cr4bits->res2-of-!cr4bits->res2 (b* ((?new-x (!cr4bits->res2$inline res2 x))) (equal (cr4bits->res2 new-x) (bfix res2))))
Theorem:
(defthm !cr4bits->res2-equiv-under-mask (b* ((?new-x (!cr4bits->res2$inline res2 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 22) (logior (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 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 2097151)))
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 'res2 x.res2) (cons (cons 'smep x.smep) (cons (cons 'smap x.smap) nil))))))))))))))))))))))))