An 64-bit unsigned bitstruct type.
This is a bitstruct type introduced by defbitstruct, represented as a unsigned 64-bit integer.
Function:
(defun ia32e-pdpte-1gb-pagebits-p (x) (declare (xargs :guard t)) (let ((__function__ 'ia32e-pdpte-1gb-pagebits-p)) (declare (ignorable __function__)) (mbe :logic (unsigned-byte-p 64 x) :exec (and (natp x) (< x 18446744073709551616)))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-when-unsigned-byte-p (implies (unsigned-byte-p 64 x) (ia32e-pdpte-1gb-pagebits-p x)))
Theorem:
(defthm unsigned-byte-p-when-ia32e-pdpte-1gb-pagebits-p (implies (ia32e-pdpte-1gb-pagebits-p x) (unsigned-byte-p 64 x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-compound-recognizer (implies (ia32e-pdpte-1gb-pagebits-p x) (natp x)) :rule-classes :compound-recognizer)
Function:
(defun ia32e-pdpte-1gb-pagebits-fix (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (let ((__function__ 'ia32e-pdpte-1gb-pagebits-fix)) (declare (ignorable __function__)) (mbe :logic (loghead 64 x) :exec x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-ia32e-pdpte-1gb-pagebits-fix (b* ((fty::fixed (ia32e-pdpte-1gb-pagebits-fix x))) (ia32e-pdpte-1gb-pagebits-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-fix-when-ia32e-pdpte-1gb-pagebits-p (implies (ia32e-pdpte-1gb-pagebits-p x) (equal (ia32e-pdpte-1gb-pagebits-fix x) x)))
Function:
(defun ia32e-pdpte-1gb-pagebits-equiv$inline (x y) (declare (xargs :guard (and (ia32e-pdpte-1gb-pagebits-p x) (ia32e-pdpte-1gb-pagebits-p y)))) (equal (ia32e-pdpte-1gb-pagebits-fix x) (ia32e-pdpte-1gb-pagebits-fix y)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-equiv-is-an-equivalence (and (booleanp (ia32e-pdpte-1gb-pagebits-equiv x y)) (ia32e-pdpte-1gb-pagebits-equiv x x) (implies (ia32e-pdpte-1gb-pagebits-equiv x y) (ia32e-pdpte-1gb-pagebits-equiv y x)) (implies (and (ia32e-pdpte-1gb-pagebits-equiv x y) (ia32e-pdpte-1gb-pagebits-equiv y z)) (ia32e-pdpte-1gb-pagebits-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-equiv-implies-equal-ia32e-pdpte-1gb-pagebits-fix-1 (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits-fix x) (ia32e-pdpte-1gb-pagebits-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-fix-under-ia32e-pdpte-1gb-pagebits-equiv (ia32e-pdpte-1gb-pagebits-equiv (ia32e-pdpte-1gb-pagebits-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Function:
(defun ia32e-pdpte-1gb-pagebits (p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (declare (xargs :guard (and (bitp p) (bitp r/w) (bitp u/s) (bitp pwt) (bitp pcd) (bitp a) (bitp d) (bitp ps) (bitp g) (3bits-p res1) (bitp pat) (17bits-p res2) (22bits-p page) (11bits-p res3) (bitp xd)))) (let ((__function__ 'ia32e-pdpte-1gb-pagebits)) (declare (ignorable __function__)) (b* ((p (mbe :logic (bfix p) :exec p)) (r/w (mbe :logic (bfix r/w) :exec r/w)) (u/s (mbe :logic (bfix u/s) :exec u/s)) (pwt (mbe :logic (bfix pwt) :exec pwt)) (pcd (mbe :logic (bfix pcd) :exec pcd)) (a (mbe :logic (bfix a) :exec a)) (d (mbe :logic (bfix d) :exec d)) (ps (mbe :logic (bfix ps) :exec ps)) (g (mbe :logic (bfix g) :exec g)) (res1 (mbe :logic (3bits-fix res1) :exec res1)) (pat (mbe :logic (bfix pat) :exec pat)) (res2 (mbe :logic (17bits-fix res2) :exec res2)) (page (mbe :logic (22bits-fix page) :exec page)) (res3 (mbe :logic (11bits-fix res3) :exec res3)) (xd (mbe :logic (bfix xd) :exec xd))) (logapp 1 p (logapp 1 r/w (logapp 1 u/s (logapp 1 pwt (logapp 1 pcd (logapp 1 a (logapp 1 d (logapp 1 ps (logapp 1 g (logapp 3 res1 (logapp 1 pat (logapp 17 res2 (logapp 22 page (logapp 11 res3 xd)))))))))))))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-ia32e-pdpte-1gb-pagebits (b* ((ia32e-pdpte-1gb-pagebits (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd))) (ia32e-pdpte-1gb-pagebits-p ia32e-pdpte-1gb-pagebits)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-p (equal (ia32e-pdpte-1gb-pagebits (bfix p) r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-p (implies (bit-equiv p p-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p-equiv r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-r/w (equal (ia32e-pdpte-1gb-pagebits p (bfix r/w) u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-r/w (implies (bit-equiv r/w r/w-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w-equiv u/s pwt pcd a d ps g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-u/s (equal (ia32e-pdpte-1gb-pagebits p r/w (bfix u/s) pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-u/s (implies (bit-equiv u/s u/s-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s-equiv pwt pcd a d ps g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-pwt (equal (ia32e-pdpte-1gb-pagebits p r/w u/s (bfix pwt) pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-pwt (implies (bit-equiv pwt pwt-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt-equiv pcd a d ps g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-pcd (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt (bfix pcd) a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-pcd (implies (bit-equiv pcd pcd-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd-equiv a d ps g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-a (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd (bfix a) d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-a (implies (bit-equiv a a-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a-equiv d ps g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-d (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a (bfix d) ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-d (implies (bit-equiv d d-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d-equiv ps g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-ps (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d (bfix ps) g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-ps (implies (bit-equiv ps ps-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps-equiv g res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-g (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps (bfix g) res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-g (implies (bit-equiv g g-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g-equiv res1 pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-3bits-fix-res1 (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g (3bits-fix res1) pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-3bits-equiv-congruence-on-res1 (implies (3bits-equiv res1 res1-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1-equiv pat res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-pat (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 (bfix pat) res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-pat (implies (bit-equiv pat pat-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat-equiv res2 page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-17bits-fix-res2 (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat (17bits-fix res2) page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-17bits-equiv-congruence-on-res2 (implies (17bits-equiv res2 res2-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2-equiv page res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-22bits-fix-page (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 (22bits-fix page) res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-22bits-equiv-congruence-on-page (implies (22bits-equiv page page-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page-equiv res3 xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-11bits-fix-res3 (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page (11bits-fix res3) xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-11bits-equiv-congruence-on-res3 (implies (11bits-equiv res3 res3-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3-equiv xd))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-of-bfix-xd (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 (bfix xd)) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-bit-equiv-congruence-on-xd (implies (bit-equiv xd xd-equiv) (equal (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd) (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd-equiv))) :rule-classes :congruence)
Function:
(defun ia32e-pdpte-1gb-pagebits-equiv-under-mask (x x1 mask) (declare (xargs :guard (and (ia32e-pdpte-1gb-pagebits-p x) (ia32e-pdpte-1gb-pagebits-p x1) (integerp mask)))) (let ((__function__ 'ia32e-pdpte-1gb-pagebits-equiv-under-mask)) (declare (ignorable __function__)) (fty::int-equiv-under-mask (ia32e-pdpte-1gb-pagebits-fix x) (ia32e-pdpte-1gb-pagebits-fix x1) mask)))
Function:
(defun ia32e-pdpte-1gb-pagebits->p$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 0 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 64) x)))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->p (b* ((p (ia32e-pdpte-1gb-pagebits->p$inline x))) (bitp p)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->p$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->p$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->p$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->p$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->p$inline x) (ia32e-pdpte-1gb-pagebits->p$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->p-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->p (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix p)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->p-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 1) 0)) (equal (ia32e-pdpte-1gb-pagebits->p x) (ia32e-pdpte-1gb-pagebits->p y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->r/w$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 1 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 63) (ash (the (unsigned-byte 64) x) -1))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->r/w (b* ((r/w (ia32e-pdpte-1gb-pagebits->r/w$inline x))) (bitp r/w)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->r/w$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->r/w$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->r/w$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->r/w$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->r/w$inline x) (ia32e-pdpte-1gb-pagebits->r/w$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->r/w-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->r/w (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix r/w)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->r/w-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 2) 0)) (equal (ia32e-pdpte-1gb-pagebits->r/w x) (ia32e-pdpte-1gb-pagebits->r/w y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->u/s$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 2 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 62) (ash (the (unsigned-byte 64) x) -2))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->u/s (b* ((u/s (ia32e-pdpte-1gb-pagebits->u/s$inline x))) (bitp u/s)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->u/s$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->u/s$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->u/s$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->u/s$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->u/s$inline x) (ia32e-pdpte-1gb-pagebits->u/s$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->u/s-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->u/s (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix u/s)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->u/s-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 4) 0)) (equal (ia32e-pdpte-1gb-pagebits->u/s x) (ia32e-pdpte-1gb-pagebits->u/s y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->pwt$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 3 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 61) (ash (the (unsigned-byte 64) x) -3))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->pwt (b* ((pwt (ia32e-pdpte-1gb-pagebits->pwt$inline x))) (bitp pwt)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pwt$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->pwt$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->pwt$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pwt$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->pwt$inline x) (ia32e-pdpte-1gb-pagebits->pwt$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pwt-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->pwt (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix pwt)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pwt-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 8) 0)) (equal (ia32e-pdpte-1gb-pagebits->pwt x) (ia32e-pdpte-1gb-pagebits->pwt y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->pcd$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 4 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 60) (ash (the (unsigned-byte 64) x) -4))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->pcd (b* ((pcd (ia32e-pdpte-1gb-pagebits->pcd$inline x))) (bitp pcd)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pcd$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->pcd$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->pcd$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pcd$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->pcd$inline x) (ia32e-pdpte-1gb-pagebits->pcd$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pcd-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->pcd (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix pcd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pcd-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 16) 0)) (equal (ia32e-pdpte-1gb-pagebits->pcd x) (ia32e-pdpte-1gb-pagebits->pcd y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->a$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 5 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 59) (ash (the (unsigned-byte 64) x) -5))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->a (b* ((a (ia32e-pdpte-1gb-pagebits->a$inline x))) (bitp a)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->a$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->a$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->a$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->a$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->a$inline x) (ia32e-pdpte-1gb-pagebits->a$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->a-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->a (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix a)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->a-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 32) 0)) (equal (ia32e-pdpte-1gb-pagebits->a x) (ia32e-pdpte-1gb-pagebits->a y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->d$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 6 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 58) (ash (the (unsigned-byte 64) x) -6))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->d (b* ((d (ia32e-pdpte-1gb-pagebits->d$inline x))) (bitp d)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->d$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->d$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->d$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->d$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->d$inline x) (ia32e-pdpte-1gb-pagebits->d$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->d-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->d (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix d)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->d-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 64) 0)) (equal (ia32e-pdpte-1gb-pagebits->d x) (ia32e-pdpte-1gb-pagebits->d y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->ps$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 7 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 57) (ash (the (unsigned-byte 64) x) -7))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->ps (b* ((ps (ia32e-pdpte-1gb-pagebits->ps$inline x))) (bitp ps)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->ps$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->ps$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->ps$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->ps$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->ps$inline x) (ia32e-pdpte-1gb-pagebits->ps$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->ps-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->ps (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix ps)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->ps-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 128) 0)) (equal (ia32e-pdpte-1gb-pagebits->ps x) (ia32e-pdpte-1gb-pagebits->ps y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->g$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 8 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 56) (ash (the (unsigned-byte 64) x) -8))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->g (b* ((g (ia32e-pdpte-1gb-pagebits->g$inline x))) (bitp g)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->g$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->g$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->g$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->g$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->g$inline x) (ia32e-pdpte-1gb-pagebits->g$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->g-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->g (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix g)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->g-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 256) 0)) (equal (ia32e-pdpte-1gb-pagebits->g x) (ia32e-pdpte-1gb-pagebits->g y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->res1$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 9 :width 3)) :exec (the (unsigned-byte 3) (logand (the (unsigned-byte 3) 7) (the (unsigned-byte 55) (ash (the (unsigned-byte 64) x) -9))))))
Theorem:
(defthm 3bits-p-of-ia32e-pdpte-1gb-pagebits->res1 (b* ((res1 (ia32e-pdpte-1gb-pagebits->res1$inline x))) (3bits-p res1)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res1$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->res1$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->res1$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res1$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->res1$inline x) (ia32e-pdpte-1gb-pagebits->res1$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res1-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->res1 (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (3bits-fix res1)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res1-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 3584) 0)) (equal (ia32e-pdpte-1gb-pagebits->res1 x) (ia32e-pdpte-1gb-pagebits->res1 y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->pat$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 12 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 52) (ash (the (unsigned-byte 64) x) -12))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->pat (b* ((pat (ia32e-pdpte-1gb-pagebits->pat$inline x))) (bitp pat)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pat$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->pat$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->pat$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pat$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->pat$inline x) (ia32e-pdpte-1gb-pagebits->pat$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pat-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->pat (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix pat)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pat-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 4096) 0)) (equal (ia32e-pdpte-1gb-pagebits->pat x) (ia32e-pdpte-1gb-pagebits->pat y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->res2$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 13 :width 17)) :exec (the (unsigned-byte 17) (logand (the (unsigned-byte 17) 131071) (the (unsigned-byte 51) (ash (the (unsigned-byte 64) x) -13))))))
Theorem:
(defthm 17bits-p-of-ia32e-pdpte-1gb-pagebits->res2 (b* ((res2 (ia32e-pdpte-1gb-pagebits->res2$inline x))) (17bits-p res2)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res2$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->res2$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->res2$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res2$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->res2$inline x) (ia32e-pdpte-1gb-pagebits->res2$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res2-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->res2 (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (17bits-fix res2)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res2-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 1073733632) 0)) (equal (ia32e-pdpte-1gb-pagebits->res2 x) (ia32e-pdpte-1gb-pagebits->res2 y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->page$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 30 :width 22)) :exec (the (unsigned-byte 22) (logand (the (unsigned-byte 22) 4194303) (the (unsigned-byte 34) (ash (the (unsigned-byte 64) x) -30))))))
Theorem:
(defthm 22bits-p-of-ia32e-pdpte-1gb-pagebits->page (b* ((page (ia32e-pdpte-1gb-pagebits->page$inline x))) (22bits-p page)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->page$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->page$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->page$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->page$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->page$inline x) (ia32e-pdpte-1gb-pagebits->page$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->page-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->page (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (22bits-fix page)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->page-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 4503598553628672) 0)) (equal (ia32e-pdpte-1gb-pagebits->page x) (ia32e-pdpte-1gb-pagebits->page y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->res3$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 52 :width 11)) :exec (the (unsigned-byte 11) (logand (the (unsigned-byte 11) 2047) (the (unsigned-byte 12) (ash (the (unsigned-byte 64) x) -52))))))
Theorem:
(defthm 11bits-p-of-ia32e-pdpte-1gb-pagebits->res3 (b* ((res3 (ia32e-pdpte-1gb-pagebits->res3$inline x))) (11bits-p res3)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res3$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->res3$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->res3$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res3$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->res3$inline x) (ia32e-pdpte-1gb-pagebits->res3$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res3-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->res3 (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (11bits-fix res3)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res3-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 9218868437227405312) 0)) (equal (ia32e-pdpte-1gb-pagebits->res3 x) (ia32e-pdpte-1gb-pagebits->res3 y))))
Function:
(defun ia32e-pdpte-1gb-pagebits->xd$inline (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (mbe :logic (let ((x (ia32e-pdpte-1gb-pagebits-fix x))) (part-select x :low 63 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 1) (ash (the (unsigned-byte 64) x) -63))))))
Theorem:
(defthm bitp-of-ia32e-pdpte-1gb-pagebits->xd (b* ((xd (ia32e-pdpte-1gb-pagebits->xd$inline x))) (bitp xd)) :rule-classes :rewrite)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->xd$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (ia32e-pdpte-1gb-pagebits->xd$inline (ia32e-pdpte-1gb-pagebits-fix x)) (ia32e-pdpte-1gb-pagebits->xd$inline x)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->xd$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (ia32e-pdpte-1gb-pagebits->xd$inline x) (ia32e-pdpte-1gb-pagebits->xd$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->xd-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits->xd (ia32e-pdpte-1gb-pagebits p r/w u/s pwt pcd a d ps g res1 pat res2 page res3 xd)) (bfix xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->xd-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x ia32e-pdpte-1gb-pagebits-equiv-under-mask) (ia32e-pdpte-1gb-pagebits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 9223372036854775808) 0)) (equal (ia32e-pdpte-1gb-pagebits->xd x) (ia32e-pdpte-1gb-pagebits->xd y))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-fix-in-terms-of-ia32e-pdpte-1gb-pagebits (equal (ia32e-pdpte-1gb-pagebits-fix x) (change-ia32e-pdpte-1gb-pagebits x)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->p$inline (p x) (declare (xargs :guard (and (bitp p) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((p (mbe :logic (bfix p) :exec p)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install p x :width 1 :low 0)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 2) -2))) (the (unsigned-byte 1) p)))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->p (b* ((new-x (!ia32e-pdpte-1gb-pagebits->p$inline p x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->p$inline-of-bfix-p (equal (!ia32e-pdpte-1gb-pagebits->p$inline (bfix p) x) (!ia32e-pdpte-1gb-pagebits->p$inline p x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->p$inline-bit-equiv-congruence-on-p (implies (bit-equiv p p-equiv) (equal (!ia32e-pdpte-1gb-pagebits->p$inline p x) (!ia32e-pdpte-1gb-pagebits->p$inline p-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->p$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->p$inline p (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->p$inline p x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->p$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->p$inline p x) (!ia32e-pdpte-1gb-pagebits->p$inline p x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->p-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->p p x) (change-ia32e-pdpte-1gb-pagebits x :p p)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->p-of-!ia32e-pdpte-1gb-pagebits->p (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->p$inline p x))) (equal (ia32e-pdpte-1gb-pagebits->p new-x) (bfix p))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->p-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->p$inline p x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -2)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->r/w$inline (r/w x) (declare (xargs :guard (and (bitp r/w) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((r/w (mbe :logic (bfix r/w) :exec r/w)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install r/w x :width 1 :low 1)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 3) -3))) (the (unsigned-byte 2) (ash (the (unsigned-byte 1) r/w) 1))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->r/w (b* ((new-x (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->r/w$inline-of-bfix-r/w (equal (!ia32e-pdpte-1gb-pagebits->r/w$inline (bfix r/w) x) (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->r/w$inline-bit-equiv-congruence-on-r/w (implies (bit-equiv r/w r/w-equiv) (equal (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x) (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->r/w$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->r/w$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x) (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->r/w-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->r/w r/w x) (change-ia32e-pdpte-1gb-pagebits x :r/w r/w)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->r/w-of-!ia32e-pdpte-1gb-pagebits->r/w (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x))) (equal (ia32e-pdpte-1gb-pagebits->r/w new-x) (bfix r/w))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->r/w-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->r/w$inline r/w x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -3)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->u/s$inline (u/s x) (declare (xargs :guard (and (bitp u/s) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((u/s (mbe :logic (bfix u/s) :exec u/s)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install u/s x :width 1 :low 2)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 4) -5))) (the (unsigned-byte 3) (ash (the (unsigned-byte 1) u/s) 2))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->u/s (b* ((new-x (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->u/s$inline-of-bfix-u/s (equal (!ia32e-pdpte-1gb-pagebits->u/s$inline (bfix u/s) x) (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->u/s$inline-bit-equiv-congruence-on-u/s (implies (bit-equiv u/s u/s-equiv) (equal (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x) (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->u/s$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->u/s$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x) (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->u/s-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->u/s u/s x) (change-ia32e-pdpte-1gb-pagebits x :u/s u/s)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->u/s-of-!ia32e-pdpte-1gb-pagebits->u/s (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x))) (equal (ia32e-pdpte-1gb-pagebits->u/s new-x) (bfix u/s))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->u/s-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->u/s$inline u/s x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -5)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->pwt$inline (pwt x) (declare (xargs :guard (and (bitp pwt) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((pwt (mbe :logic (bfix pwt) :exec pwt)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install pwt x :width 1 :low 3)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 5) -9))) (the (unsigned-byte 4) (ash (the (unsigned-byte 1) pwt) 3))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->pwt (b* ((new-x (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pwt$inline-of-bfix-pwt (equal (!ia32e-pdpte-1gb-pagebits->pwt$inline (bfix pwt) x) (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pwt$inline-bit-equiv-congruence-on-pwt (implies (bit-equiv pwt pwt-equiv) (equal (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x) (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pwt$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pwt$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x) (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pwt-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->pwt pwt x) (change-ia32e-pdpte-1gb-pagebits x :pwt pwt)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pwt-of-!ia32e-pdpte-1gb-pagebits->pwt (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x))) (equal (ia32e-pdpte-1gb-pagebits->pwt new-x) (bfix pwt))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pwt-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->pwt$inline pwt x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -9)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->pcd$inline (pcd x) (declare (xargs :guard (and (bitp pcd) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((pcd (mbe :logic (bfix pcd) :exec pcd)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install pcd x :width 1 :low 4)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 6) -17))) (the (unsigned-byte 5) (ash (the (unsigned-byte 1) pcd) 4))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->pcd (b* ((new-x (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pcd$inline-of-bfix-pcd (equal (!ia32e-pdpte-1gb-pagebits->pcd$inline (bfix pcd) x) (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pcd$inline-bit-equiv-congruence-on-pcd (implies (bit-equiv pcd pcd-equiv) (equal (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x) (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pcd$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pcd$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x) (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pcd-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->pcd pcd x) (change-ia32e-pdpte-1gb-pagebits x :pcd pcd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pcd-of-!ia32e-pdpte-1gb-pagebits->pcd (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x))) (equal (ia32e-pdpte-1gb-pagebits->pcd new-x) (bfix pcd))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pcd-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->pcd$inline pcd x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -17)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->a$inline (a x) (declare (xargs :guard (and (bitp a) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((a (mbe :logic (bfix a) :exec a)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install a x :width 1 :low 5)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 7) -33))) (the (unsigned-byte 6) (ash (the (unsigned-byte 1) a) 5))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->a (b* ((new-x (!ia32e-pdpte-1gb-pagebits->a$inline a x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->a$inline-of-bfix-a (equal (!ia32e-pdpte-1gb-pagebits->a$inline (bfix a) x) (!ia32e-pdpte-1gb-pagebits->a$inline a x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->a$inline-bit-equiv-congruence-on-a (implies (bit-equiv a a-equiv) (equal (!ia32e-pdpte-1gb-pagebits->a$inline a x) (!ia32e-pdpte-1gb-pagebits->a$inline a-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->a$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->a$inline a (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->a$inline a x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->a$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->a$inline a x) (!ia32e-pdpte-1gb-pagebits->a$inline a x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->a-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->a a x) (change-ia32e-pdpte-1gb-pagebits x :a a)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->a-of-!ia32e-pdpte-1gb-pagebits->a (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->a$inline a x))) (equal (ia32e-pdpte-1gb-pagebits->a new-x) (bfix a))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->a-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->a$inline a x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -33)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->d$inline (d x) (declare (xargs :guard (and (bitp d) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((d (mbe :logic (bfix d) :exec d)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install d x :width 1 :low 6)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 8) -65))) (the (unsigned-byte 7) (ash (the (unsigned-byte 1) d) 6))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->d (b* ((new-x (!ia32e-pdpte-1gb-pagebits->d$inline d x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->d$inline-of-bfix-d (equal (!ia32e-pdpte-1gb-pagebits->d$inline (bfix d) x) (!ia32e-pdpte-1gb-pagebits->d$inline d x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->d$inline-bit-equiv-congruence-on-d (implies (bit-equiv d d-equiv) (equal (!ia32e-pdpte-1gb-pagebits->d$inline d x) (!ia32e-pdpte-1gb-pagebits->d$inline d-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->d$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->d$inline d (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->d$inline d x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->d$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->d$inline d x) (!ia32e-pdpte-1gb-pagebits->d$inline d x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->d-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->d d x) (change-ia32e-pdpte-1gb-pagebits x :d d)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->d-of-!ia32e-pdpte-1gb-pagebits->d (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->d$inline d x))) (equal (ia32e-pdpte-1gb-pagebits->d new-x) (bfix d))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->d-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->d$inline d x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -65)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->ps$inline (ps x) (declare (xargs :guard (and (bitp ps) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((ps (mbe :logic (bfix ps) :exec ps)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install ps x :width 1 :low 7)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 9) -129))) (the (unsigned-byte 8) (ash (the (unsigned-byte 1) ps) 7))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->ps (b* ((new-x (!ia32e-pdpte-1gb-pagebits->ps$inline ps x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->ps$inline-of-bfix-ps (equal (!ia32e-pdpte-1gb-pagebits->ps$inline (bfix ps) x) (!ia32e-pdpte-1gb-pagebits->ps$inline ps x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->ps$inline-bit-equiv-congruence-on-ps (implies (bit-equiv ps ps-equiv) (equal (!ia32e-pdpte-1gb-pagebits->ps$inline ps x) (!ia32e-pdpte-1gb-pagebits->ps$inline ps-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->ps$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->ps$inline ps (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->ps$inline ps x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->ps$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->ps$inline ps x) (!ia32e-pdpte-1gb-pagebits->ps$inline ps x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->ps-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->ps ps x) (change-ia32e-pdpte-1gb-pagebits x :ps ps)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->ps-of-!ia32e-pdpte-1gb-pagebits->ps (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->ps$inline ps x))) (equal (ia32e-pdpte-1gb-pagebits->ps new-x) (bfix ps))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->ps-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->ps$inline ps x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -129)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->g$inline (g x) (declare (xargs :guard (and (bitp g) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((g (mbe :logic (bfix g) :exec g)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install g x :width 1 :low 8)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 10) -257))) (the (unsigned-byte 9) (ash (the (unsigned-byte 1) g) 8))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->g (b* ((new-x (!ia32e-pdpte-1gb-pagebits->g$inline g x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->g$inline-of-bfix-g (equal (!ia32e-pdpte-1gb-pagebits->g$inline (bfix g) x) (!ia32e-pdpte-1gb-pagebits->g$inline g x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->g$inline-bit-equiv-congruence-on-g (implies (bit-equiv g g-equiv) (equal (!ia32e-pdpte-1gb-pagebits->g$inline g x) (!ia32e-pdpte-1gb-pagebits->g$inline g-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->g$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->g$inline g (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->g$inline g x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->g$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->g$inline g x) (!ia32e-pdpte-1gb-pagebits->g$inline g x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->g-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->g g x) (change-ia32e-pdpte-1gb-pagebits x :g g)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->g-of-!ia32e-pdpte-1gb-pagebits->g (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->g$inline g x))) (equal (ia32e-pdpte-1gb-pagebits->g new-x) (bfix g))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->g-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->g$inline g x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -257)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->res1$inline (res1 x) (declare (xargs :guard (and (3bits-p res1) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((res1 (mbe :logic (3bits-fix res1) :exec res1)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install res1 x :width 3 :low 9)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 13) -3585))) (the (unsigned-byte 12) (ash (the (unsigned-byte 3) res1) 9))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->res1 (b* ((new-x (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res1$inline-of-3bits-fix-res1 (equal (!ia32e-pdpte-1gb-pagebits->res1$inline (3bits-fix res1) x) (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res1$inline-3bits-equiv-congruence-on-res1 (implies (3bits-equiv res1 res1-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x) (!ia32e-pdpte-1gb-pagebits->res1$inline res1-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res1$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->res1$inline res1 (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res1$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x) (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res1-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->res1 res1 x) (change-ia32e-pdpte-1gb-pagebits x :res1 res1)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res1-of-!ia32e-pdpte-1gb-pagebits->res1 (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x))) (equal (ia32e-pdpte-1gb-pagebits->res1 new-x) (3bits-fix res1))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res1-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res1$inline res1 x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -3585)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->pat$inline (pat x) (declare (xargs :guard (and (bitp pat) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((pat (mbe :logic (bfix pat) :exec pat)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install pat x :width 1 :low 12)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 14) -4097))) (the (unsigned-byte 13) (ash (the (unsigned-byte 1) pat) 12))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->pat (b* ((new-x (!ia32e-pdpte-1gb-pagebits->pat$inline pat x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pat$inline-of-bfix-pat (equal (!ia32e-pdpte-1gb-pagebits->pat$inline (bfix pat) x) (!ia32e-pdpte-1gb-pagebits->pat$inline pat x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pat$inline-bit-equiv-congruence-on-pat (implies (bit-equiv pat pat-equiv) (equal (!ia32e-pdpte-1gb-pagebits->pat$inline pat x) (!ia32e-pdpte-1gb-pagebits->pat$inline pat-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pat$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->pat$inline pat (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->pat$inline pat x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pat$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->pat$inline pat x) (!ia32e-pdpte-1gb-pagebits->pat$inline pat x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pat-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->pat pat x) (change-ia32e-pdpte-1gb-pagebits x :pat pat)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->pat-of-!ia32e-pdpte-1gb-pagebits->pat (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->pat$inline pat x))) (equal (ia32e-pdpte-1gb-pagebits->pat new-x) (bfix pat))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->pat-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->pat$inline pat x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -4097)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->res2$inline (res2 x) (declare (xargs :guard (and (17bits-p res2) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((res2 (mbe :logic (17bits-fix res2) :exec res2)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install res2 x :width 17 :low 13)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 31) -1073733633))) (the (unsigned-byte 30) (ash (the (unsigned-byte 17) res2) 13))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->res2 (b* ((new-x (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-of-17bits-fix-res2 (equal (!ia32e-pdpte-1gb-pagebits->res2$inline (17bits-fix res2) x) (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-17bits-equiv-congruence-on-res2 (implies (17bits-equiv res2 res2-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x) (!ia32e-pdpte-1gb-pagebits->res2$inline res2-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->res2$inline res2 (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x) (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->res2 res2 x) (change-ia32e-pdpte-1gb-pagebits x :res2 res2)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res2-of-!ia32e-pdpte-1gb-pagebits->res2 (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x))) (equal (ia32e-pdpte-1gb-pagebits->res2 new-x) (17bits-fix res2))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -1073733633)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->page$inline (page x) (declare (xargs :guard (and (22bits-p page) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((page (mbe :logic (22bits-fix page) :exec page)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install page x :width 22 :low 30)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 53) -4503598553628673))) (the (unsigned-byte 52) (ash (the (unsigned-byte 22) page) 30))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->page (b* ((new-x (!ia32e-pdpte-1gb-pagebits->page$inline page x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->page$inline-of-22bits-fix-page (equal (!ia32e-pdpte-1gb-pagebits->page$inline (22bits-fix page) x) (!ia32e-pdpte-1gb-pagebits->page$inline page x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->page$inline-22bits-equiv-congruence-on-page (implies (22bits-equiv page page-equiv) (equal (!ia32e-pdpte-1gb-pagebits->page$inline page x) (!ia32e-pdpte-1gb-pagebits->page$inline page-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->page$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->page$inline page (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->page$inline page x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->page$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->page$inline page x) (!ia32e-pdpte-1gb-pagebits->page$inline page x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->page-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->page page x) (change-ia32e-pdpte-1gb-pagebits x :page page)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->page-of-!ia32e-pdpte-1gb-pagebits->page (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->page$inline page x))) (equal (ia32e-pdpte-1gb-pagebits->page new-x) (22bits-fix page))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->page-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->page$inline page x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -4503598553628673)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->res3$inline (res3 x) (declare (xargs :guard (and (11bits-p res3) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((res3 (mbe :logic (11bits-fix res3) :exec res3)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install res3 x :width 11 :low 52)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 64) -9218868437227405313))) (the (unsigned-byte 63) (ash (the (unsigned-byte 11) res3) 52))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->res3 (b* ((new-x (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res3$inline-of-11bits-fix-res3 (equal (!ia32e-pdpte-1gb-pagebits->res3$inline (11bits-fix res3) x) (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res3$inline-11bits-equiv-congruence-on-res3 (implies (11bits-equiv res3 res3-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x) (!ia32e-pdpte-1gb-pagebits->res3$inline res3-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res3$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->res3$inline res3 (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res3$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x) (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res3-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->res3 res3 x) (change-ia32e-pdpte-1gb-pagebits x :res3 res3)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res3-of-!ia32e-pdpte-1gb-pagebits->res3 (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x))) (equal (ia32e-pdpte-1gb-pagebits->res3 new-x) (11bits-fix res3))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res3-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res3$inline res3 x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -9218868437227405313)))
Function:
(defun !ia32e-pdpte-1gb-pagebits->xd$inline (xd x) (declare (xargs :guard (and (bitp xd) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((xd (mbe :logic (bfix xd) :exec xd)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install xd x :width 1 :low 63)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 65) -9223372036854775809))) (the (unsigned-byte 64) (ash (the (unsigned-byte 1) xd) 63))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->xd (b* ((new-x (!ia32e-pdpte-1gb-pagebits->xd$inline xd x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->xd$inline-of-bfix-xd (equal (!ia32e-pdpte-1gb-pagebits->xd$inline (bfix xd) x) (!ia32e-pdpte-1gb-pagebits->xd$inline xd x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->xd$inline-bit-equiv-congruence-on-xd (implies (bit-equiv xd xd-equiv) (equal (!ia32e-pdpte-1gb-pagebits->xd$inline xd x) (!ia32e-pdpte-1gb-pagebits->xd$inline xd-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->xd$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->xd$inline xd (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->xd$inline xd x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->xd$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->xd$inline xd x) (!ia32e-pdpte-1gb-pagebits->xd$inline xd x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->xd-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->xd xd x) (change-ia32e-pdpte-1gb-pagebits x :xd xd)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->xd-of-!ia32e-pdpte-1gb-pagebits->xd (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->xd$inline xd x))) (equal (ia32e-pdpte-1gb-pagebits->xd new-x) (bfix xd))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->xd-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->xd$inline xd x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x 9223372036854775807)))
Function:
(defun ia32e-pdpte-1gb-pagebits-debug (x) (declare (xargs :guard (ia32e-pdpte-1gb-pagebits-p x))) (let ((__function__ 'ia32e-pdpte-1gb-pagebits-debug)) (declare (ignorable __function__)) (b* (((ia32e-pdpte-1gb-pagebits x))) (cons (cons 'p x.p) (cons (cons 'r/w x.r/w) (cons (cons 'u/s x.u/s) (cons (cons 'pwt x.pwt) (cons (cons 'pcd x.pcd) (cons (cons 'a x.a) (cons (cons 'd x.d) (cons (cons 'ps x.ps) (cons (cons 'g x.g) (cons (cons 'res1 x.res1) (cons (cons 'pat x.pat) (cons (cons 'res2 x.res2) (cons (cons 'page x.page) (cons (cons 'res3 x.res3) (cons (cons 'xd x.xd) nil))))))))))))))))))