Update the |X86ISA|::|PT| field of a ia32e-pde-pg-tablebits bit structure.
(!ia32e-pde-pg-tablebits->pt pt x) → new-x
Function:
(defun !ia32e-pde-pg-tablebits->pt$inline (pt x) (declare (xargs :guard (and (40bits-p pt) (ia32e-pde-pg-tablebits-p x)))) (mbe :logic (b* ((pt (mbe :logic (40bits-fix pt) :exec pt)) (x (ia32e-pde-pg-tablebits-fix x))) (part-install pt 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) pt) 12))))))
Theorem:
(defthm ia32e-pde-pg-tablebits-p-of-!ia32e-pde-pg-tablebits->pt (b* ((new-x (!ia32e-pde-pg-tablebits->pt$inline pt x))) (ia32e-pde-pg-tablebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pde-pg-tablebits->pt$inline-of-40bits-fix-pt (equal (!ia32e-pde-pg-tablebits->pt$inline (40bits-fix pt) x) (!ia32e-pde-pg-tablebits->pt$inline pt x)))
Theorem:
(defthm !ia32e-pde-pg-tablebits->pt$inline-40bits-equiv-congruence-on-pt (implies (40bits-equiv pt pt-equiv) (equal (!ia32e-pde-pg-tablebits->pt$inline pt x) (!ia32e-pde-pg-tablebits->pt$inline pt-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pde-pg-tablebits->pt$inline-of-ia32e-pde-pg-tablebits-fix-x (equal (!ia32e-pde-pg-tablebits->pt$inline pt (ia32e-pde-pg-tablebits-fix x)) (!ia32e-pde-pg-tablebits->pt$inline pt x)))
Theorem:
(defthm !ia32e-pde-pg-tablebits->pt$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x (implies (ia32e-pde-pg-tablebits-equiv x x-equiv) (equal (!ia32e-pde-pg-tablebits->pt$inline pt x) (!ia32e-pde-pg-tablebits->pt$inline pt x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pde-pg-tablebits->pt-is-ia32e-pde-pg-tablebits (equal (!ia32e-pde-pg-tablebits->pt pt x) (change-ia32e-pde-pg-tablebits x :pt pt)))
Theorem:
(defthm ia32e-pde-pg-tablebits->pt-of-!ia32e-pde-pg-tablebits->pt (b* ((?new-x (!ia32e-pde-pg-tablebits->pt$inline pt x))) (equal (ia32e-pde-pg-tablebits->pt new-x) (40bits-fix pt))))
Theorem:
(defthm !ia32e-pde-pg-tablebits->pt-equiv-under-mask (b* ((?new-x (!ia32e-pde-pg-tablebits->pt$inline pt x))) (ia32e-pde-pg-tablebits-equiv-under-mask new-x x -4503599627366401)))