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