Update the |X86ISA|::|G| field of a ia32e-pde-2mb-pagebits bit structure.
(!ia32e-pde-2mb-pagebits->g g x) → new-x
Function:
(defun !ia32e-pde-2mb-pagebits->g$inline (g x) (declare (xargs :guard (and (bitp g) (ia32e-pde-2mb-pagebits-p x)))) (mbe :logic (b* ((g (mbe :logic (bfix g) :exec g)) (x (ia32e-pde-2mb-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->g (b* ((new-x (!ia32e-pde-2mb-pagebits->g$inline g x))) (ia32e-pde-2mb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pde-2mb-pagebits->g$inline-of-bfix-g (equal (!ia32e-pde-2mb-pagebits->g$inline (bfix g) x) (!ia32e-pde-2mb-pagebits->g$inline g x)))
Theorem:
(defthm !ia32e-pde-2mb-pagebits->g$inline-bit-equiv-congruence-on-g (implies (bit-equiv g g-equiv) (equal (!ia32e-pde-2mb-pagebits->g$inline g x) (!ia32e-pde-2mb-pagebits->g$inline g-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pde-2mb-pagebits->g$inline-of-ia32e-pde-2mb-pagebits-fix-x (equal (!ia32e-pde-2mb-pagebits->g$inline g (ia32e-pde-2mb-pagebits-fix x)) (!ia32e-pde-2mb-pagebits->g$inline g x)))
Theorem:
(defthm !ia32e-pde-2mb-pagebits->g$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv) (equal (!ia32e-pde-2mb-pagebits->g$inline g x) (!ia32e-pde-2mb-pagebits->g$inline g x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pde-2mb-pagebits->g-is-ia32e-pde-2mb-pagebits (equal (!ia32e-pde-2mb-pagebits->g g x) (change-ia32e-pde-2mb-pagebits x :g g)))
Theorem:
(defthm ia32e-pde-2mb-pagebits->g-of-!ia32e-pde-2mb-pagebits->g (b* ((?new-x (!ia32e-pde-2mb-pagebits->g$inline g x))) (equal (ia32e-pde-2mb-pagebits->g new-x) (bfix g))))
Theorem:
(defthm !ia32e-pde-2mb-pagebits->g-equiv-under-mask (b* ((?new-x (!ia32e-pde-2mb-pagebits->g$inline g x))) (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -257)))