Update the |X86ISA|::|PD| field of a ia32e-pdpte-pg-dirbits bit structure.
(!ia32e-pdpte-pg-dirbits->pd pd x) → new-x
Function:
(defun !ia32e-pdpte-pg-dirbits->pd$inline (pd x) (declare (xargs :guard (and (40bits-p pd) (ia32e-pdpte-pg-dirbits-p x)))) (mbe :logic (b* ((pd (mbe :logic (40bits-fix pd) :exec pd)) (x (ia32e-pdpte-pg-dirbits-fix x))) (part-install pd x :width 40 :low 12)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 53) -4503599627366401))) (the (unsigned-byte 52) (ash (the (unsigned-byte 40) pd) 12))))))
Theorem:
(defthm ia32e-pdpte-pg-dirbits-p-of-!ia32e-pdpte-pg-dirbits->pd (b* ((new-x (!ia32e-pdpte-pg-dirbits->pd$inline pd x))) (ia32e-pdpte-pg-dirbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-pg-dirbits->pd$inline-of-40bits-fix-pd (equal (!ia32e-pdpte-pg-dirbits->pd$inline (40bits-fix pd) x) (!ia32e-pdpte-pg-dirbits->pd$inline pd x)))
Theorem:
(defthm !ia32e-pdpte-pg-dirbits->pd$inline-40bits-equiv-congruence-on-pd (implies (40bits-equiv pd pd-equiv) (equal (!ia32e-pdpte-pg-dirbits->pd$inline pd x) (!ia32e-pdpte-pg-dirbits->pd$inline pd-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-pg-dirbits->pd$inline-of-ia32e-pdpte-pg-dirbits-fix-x (equal (!ia32e-pdpte-pg-dirbits->pd$inline pd (ia32e-pdpte-pg-dirbits-fix x)) (!ia32e-pdpte-pg-dirbits->pd$inline pd x)))
Theorem:
(defthm !ia32e-pdpte-pg-dirbits->pd$inline-ia32e-pdpte-pg-dirbits-equiv-congruence-on-x (implies (ia32e-pdpte-pg-dirbits-equiv x x-equiv) (equal (!ia32e-pdpte-pg-dirbits->pd$inline pd x) (!ia32e-pdpte-pg-dirbits->pd$inline pd x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-pg-dirbits->pd-is-ia32e-pdpte-pg-dirbits (equal (!ia32e-pdpte-pg-dirbits->pd pd x) (change-ia32e-pdpte-pg-dirbits x :pd pd)))
Theorem:
(defthm ia32e-pdpte-pg-dirbits->pd-of-!ia32e-pdpte-pg-dirbits->pd (b* ((?new-x (!ia32e-pdpte-pg-dirbits->pd$inline pd x))) (equal (ia32e-pdpte-pg-dirbits->pd new-x) (40bits-fix pd))))
Theorem:
(defthm !ia32e-pdpte-pg-dirbits->pd-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-pg-dirbits->pd$inline pd x))) (ia32e-pdpte-pg-dirbits-equiv-under-mask new-x x -4503599627366401)))