		Search-engine friendly clone of the ACL2 documentation.

Paging-bitstructs

Ia32e-pte-4k-pagebits

An 64-bit unsigned bitstruct type.

This is a bitstruct type introduced by defbitstruct, represented as a unsigned 64-bit integer.

Fields

p — bit
r/w — bit
u/s — bit
pwt — bit
pcd — bit
a — bit
d — bit
pat — bit
g — bit
res1 — 3bits
page — 40bits
res2 — 11bits
xd — bit

Definitions and Theorems

Function: ia32e-pte-4k-pagebits-p

(defun ia32e-pte-4k-pagebits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'ia32e-pte-4k-pagebits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 64 x)
         :exec (and (natp x)
                    (< x 18446744073709551616)))))

Theorem: ia32e-pte-4k-pagebits-p-when-unsigned-byte-p

(defthm ia32e-pte-4k-pagebits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 64 x)
           (ia32e-pte-4k-pagebits-p x)))

Theorem: unsigned-byte-p-when-ia32e-pte-4k-pagebits-p

(defthm unsigned-byte-p-when-ia32e-pte-4k-pagebits-p
  (implies (ia32e-pte-4k-pagebits-p x)
           (unsigned-byte-p 64 x)))

Theorem: ia32e-pte-4k-pagebits-p-compound-recognizer

(defthm ia32e-pte-4k-pagebits-p-compound-recognizer
  (implies (ia32e-pte-4k-pagebits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: ia32e-pte-4k-pagebits-fix

(defun ia32e-pte-4k-pagebits-fix (x)
  (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
  (let ((__function__ 'ia32e-pte-4k-pagebits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 64 x) :exec x)))

Theorem: ia32e-pte-4k-pagebits-p-of-ia32e-pte-4k-pagebits-fix

(defthm ia32e-pte-4k-pagebits-p-of-ia32e-pte-4k-pagebits-fix
  (b* ((fty::fixed (ia32e-pte-4k-pagebits-fix x)))
    (ia32e-pte-4k-pagebits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits-fix-when-ia32e-pte-4k-pagebits-p

(defthm ia32e-pte-4k-pagebits-fix-when-ia32e-pte-4k-pagebits-p
  (implies (ia32e-pte-4k-pagebits-p x)
           (equal (ia32e-pte-4k-pagebits-fix x)
                  x)))

Function: ia32e-pte-4k-pagebits-equiv$inline

(defun ia32e-pte-4k-pagebits-equiv$inline (x y)
  (declare (xargs :guard (and (ia32e-pte-4k-pagebits-p x)
                              (ia32e-pte-4k-pagebits-p y))))
  (equal (ia32e-pte-4k-pagebits-fix x)
         (ia32e-pte-4k-pagebits-fix y)))

Theorem: ia32e-pte-4k-pagebits-equiv-is-an-equivalence

(defthm ia32e-pte-4k-pagebits-equiv-is-an-equivalence
  (and (booleanp (ia32e-pte-4k-pagebits-equiv x y))
       (ia32e-pte-4k-pagebits-equiv x x)
       (implies (ia32e-pte-4k-pagebits-equiv x y)
                (ia32e-pte-4k-pagebits-equiv y x))
       (implies (and (ia32e-pte-4k-pagebits-equiv x y)
                     (ia32e-pte-4k-pagebits-equiv y z))
                (ia32e-pte-4k-pagebits-equiv x z)))
  :rule-classes (:equivalence))

Theorem: ia32e-pte-4k-pagebits-equiv-implies-equal-ia32e-pte-4k-pagebits-fix-1

(defthm
 ia32e-pte-4k-pagebits-equiv-implies-equal-ia32e-pte-4k-pagebits-fix-1
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits-fix x)
                 (ia32e-pte-4k-pagebits-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: ia32e-pte-4k-pagebits-fix-under-ia32e-pte-4k-pagebits-equiv

(defthm ia32e-pte-4k-pagebits-fix-under-ia32e-pte-4k-pagebits-equiv
  (ia32e-pte-4k-pagebits-equiv (ia32e-pte-4k-pagebits-fix x)
                               x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: ia32e-pte-4k-pagebits

(defun ia32e-pte-4k-pagebits
       (p r/w
          u/s pwt pcd a d pat g res1 page res2 xd)
 (declare (xargs :guard (and (bitp p)
                             (bitp r/w)
                             (bitp u/s)
                             (bitp pwt)
                             (bitp pcd)
                             (bitp a)
                             (bitp d)
                             (bitp pat)
                             (bitp g)
                             (3bits-p res1)
                             (40bits-p page)
                             (11bits-p res2)
                             (bitp xd))))
 (let ((__function__ 'ia32e-pte-4k-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))
       (pat (mbe :logic (bfix pat) :exec pat))
       (g (mbe :logic (bfix g) :exec g))
       (res1 (mbe :logic (3bits-fix res1)
                  :exec res1))
       (page (mbe :logic (40bits-fix page)
                  :exec page))
       (res2 (mbe :logic (11bits-fix res2)
                  :exec res2))
       (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 pat
           (logapp
              1 g
              (logapp 3 res1
                      (logapp 40
                              page (logapp 11 res2 xd)))))))))))))))

Theorem: ia32e-pte-4k-pagebits-p-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits-p-of-ia32e-pte-4k-pagebits
 (b*
  ((ia32e-pte-4k-pagebits
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))
  (ia32e-pte-4k-pagebits-p ia32e-pte-4k-pagebits))
 :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits-of-bfix-p

(defthm ia32e-pte-4k-pagebits-of-bfix-p
 (equal
     (ia32e-pte-4k-pagebits (bfix p)
                            r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s
                            pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-p

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-p
 (implies
  (bit-equiv p p-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p-equiv r/w u/s
                            pwt pcd a d pat g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-r/w

(defthm ia32e-pte-4k-pagebits-of-bfix-r/w
 (equal
     (ia32e-pte-4k-pagebits p (bfix r/w)
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s
                            pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-r/w

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-r/w
 (implies
  (bit-equiv r/w r/w-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w-equiv u/s
                            pwt pcd a d pat g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-u/s

(defthm ia32e-pte-4k-pagebits-of-bfix-u/s
  (equal
       (ia32e-pte-4k-pagebits p r/w (bfix u/s)
                              pwt pcd a d pat g res1 page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-u/s

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-u/s
 (implies
  (bit-equiv u/s u/s-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s-equiv
                            pwt pcd a d pat g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-pwt

(defthm ia32e-pte-4k-pagebits-of-bfix-pwt
  (equal
       (ia32e-pte-4k-pagebits p r/w u/s (bfix pwt)
                              pcd a d pat g res1 page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-pwt

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-pwt
 (implies
  (bit-equiv pwt pwt-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt-equiv
                            pcd a d pat g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-pcd

(defthm ia32e-pte-4k-pagebits-of-bfix-pcd
  (equal
       (ia32e-pte-4k-pagebits p r/w u/s pwt (bfix pcd)
                              a d pat g res1 page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-pcd

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-pcd
 (implies
  (bit-equiv pcd pcd-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd-equiv a d pat g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-a

(defthm ia32e-pte-4k-pagebits-of-bfix-a
  (equal
       (ia32e-pte-4k-pagebits p r/w u/s pwt pcd (bfix a)
                              d pat g res1 page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-a

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-a
 (implies
  (bit-equiv a a-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a-equiv d pat g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-d

(defthm ia32e-pte-4k-pagebits-of-bfix-d
  (equal
       (ia32e-pte-4k-pagebits p r/w u/s pwt pcd a (bfix d)
                              pat g res1 page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-d

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-d
 (implies
  (bit-equiv d d-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a d-equiv pat g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-pat

(defthm ia32e-pte-4k-pagebits-of-bfix-pat
  (equal
       (ia32e-pte-4k-pagebits p r/w u/s pwt pcd a d (bfix pat)
                              g res1 page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-pat

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-pat
 (implies
  (bit-equiv pat pat-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a d pat-equiv g res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-g

(defthm ia32e-pte-4k-pagebits-of-bfix-g
  (equal
       (ia32e-pte-4k-pagebits p r/w u/s pwt pcd a d pat (bfix g)
                              res1 page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-g

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-g
 (implies
  (bit-equiv g g-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a d pat g-equiv res1 page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-3bits-fix-res1

(defthm ia32e-pte-4k-pagebits-of-3bits-fix-res1
  (equal
       (ia32e-pte-4k-pagebits p r/w
                              u/s pwt pcd a d pat g (3bits-fix res1)
                              page res2 xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-3bits-equiv-congruence-on-res1

(defthm ia32e-pte-4k-pagebits-3bits-equiv-congruence-on-res1
 (implies
  (3bits-equiv res1 res1-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a d pat g res1-equiv page res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-40bits-fix-page

(defthm ia32e-pte-4k-pagebits-of-40bits-fix-page
 (equal
     (ia32e-pte-4k-pagebits p r/w u/s
                            pwt pcd a d pat g res1 (40bits-fix page)
                            res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s
                            pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-40bits-equiv-congruence-on-page

(defthm ia32e-pte-4k-pagebits-40bits-equiv-congruence-on-page
 (implies
  (40bits-equiv page page-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a d pat g res1 page-equiv res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-11bits-fix-res2

(defthm ia32e-pte-4k-pagebits-of-11bits-fix-res2
  (equal
       (ia32e-pte-4k-pagebits p r/w u/s pwt pcd
                              a d pat g res1 page (11bits-fix res2)
                              xd)
       (ia32e-pte-4k-pagebits p r/w u/s
                              pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-11bits-equiv-congruence-on-res2

(defthm ia32e-pte-4k-pagebits-11bits-equiv-congruence-on-res2
 (implies
  (11bits-equiv res2 res2-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a d pat g res1 page res2-equiv xd)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits-of-bfix-xd

(defthm ia32e-pte-4k-pagebits-of-bfix-xd
 (equal
      (ia32e-pte-4k-pagebits p r/w u/s pwt
                             pcd a d pat g res1 page res2 (bfix xd))
      (ia32e-pte-4k-pagebits p r/w u/s
                             pwt pcd a d pat g res1 page res2 xd)))

Theorem: ia32e-pte-4k-pagebits-bit-equiv-congruence-on-xd

(defthm ia32e-pte-4k-pagebits-bit-equiv-congruence-on-xd
 (implies
  (bit-equiv xd xd-equiv)
  (equal
     (ia32e-pte-4k-pagebits p r/w
                            u/s pwt pcd a d pat g res1 page res2 xd)
     (ia32e-pte-4k-pagebits p r/w u/s pwt
                            pcd a d pat g res1 page res2 xd-equiv)))
 :rule-classes :congruence)

Function: ia32e-pte-4k-pagebits-equiv-under-mask

(defun ia32e-pte-4k-pagebits-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (ia32e-pte-4k-pagebits-p x)
                              (ia32e-pte-4k-pagebits-p x1)
                              (integerp mask))))
  (let ((__function__ 'ia32e-pte-4k-pagebits-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (ia32e-pte-4k-pagebits-fix x)
                               (ia32e-pte-4k-pagebits-fix x1)
                               mask)))

Function: ia32e-pte-4k-pagebits->p$inline

(defun ia32e-pte-4k-pagebits->p$inline (x)
  (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->p

(defthm bitp-of-ia32e-pte-4k-pagebits->p
  (b* ((p (ia32e-pte-4k-pagebits->p$inline x)))
    (bitp p))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->p$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
     ia32e-pte-4k-pagebits->p$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
     (ia32e-pte-4k-pagebits->p$inline (ia32e-pte-4k-pagebits-fix x))
     (ia32e-pte-4k-pagebits->p$inline x)))

Theorem: ia32e-pte-4k-pagebits->p$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->p$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->p$inline x)
                 (ia32e-pte-4k-pagebits->p$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->p-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->p-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->p
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix p)))

Theorem: ia32e-pte-4k-pagebits->p-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->p-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 1) 0))
       (equal (ia32e-pte-4k-pagebits->p x)
              (ia32e-pte-4k-pagebits->p y))))

Function: ia32e-pte-4k-pagebits->r/w$inline

(defun ia32e-pte-4k-pagebits->r/w$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->r/w

(defthm bitp-of-ia32e-pte-4k-pagebits->r/w
  (b* ((r/w (ia32e-pte-4k-pagebits->r/w$inline x)))
    (bitp r/w))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->r/w$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
   ia32e-pte-4k-pagebits->r/w$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
   (ia32e-pte-4k-pagebits->r/w$inline (ia32e-pte-4k-pagebits-fix x))
   (ia32e-pte-4k-pagebits->r/w$inline x)))

Theorem: ia32e-pte-4k-pagebits->r/w$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->r/w$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->r/w$inline x)
                 (ia32e-pte-4k-pagebits->r/w$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->r/w-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->r/w-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->r/w
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix r/w)))

Theorem: ia32e-pte-4k-pagebits->r/w-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->r/w-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 2) 0))
       (equal (ia32e-pte-4k-pagebits->r/w x)
              (ia32e-pte-4k-pagebits->r/w y))))

Function: ia32e-pte-4k-pagebits->u/s$inline

(defun ia32e-pte-4k-pagebits->u/s$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->u/s

(defthm bitp-of-ia32e-pte-4k-pagebits->u/s
  (b* ((u/s (ia32e-pte-4k-pagebits->u/s$inline x)))
    (bitp u/s))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->u/s$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
   ia32e-pte-4k-pagebits->u/s$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
   (ia32e-pte-4k-pagebits->u/s$inline (ia32e-pte-4k-pagebits-fix x))
   (ia32e-pte-4k-pagebits->u/s$inline x)))

Theorem: ia32e-pte-4k-pagebits->u/s$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->u/s$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->u/s$inline x)
                 (ia32e-pte-4k-pagebits->u/s$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->u/s-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->u/s-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->u/s
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix u/s)))

Theorem: ia32e-pte-4k-pagebits->u/s-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->u/s-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 4) 0))
       (equal (ia32e-pte-4k-pagebits->u/s x)
              (ia32e-pte-4k-pagebits->u/s y))))

Function: ia32e-pte-4k-pagebits->pwt$inline

(defun ia32e-pte-4k-pagebits->pwt$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->pwt

(defthm bitp-of-ia32e-pte-4k-pagebits->pwt
  (b* ((pwt (ia32e-pte-4k-pagebits->pwt$inline x)))
    (bitp pwt))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->pwt$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
   ia32e-pte-4k-pagebits->pwt$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
   (ia32e-pte-4k-pagebits->pwt$inline (ia32e-pte-4k-pagebits-fix x))
   (ia32e-pte-4k-pagebits->pwt$inline x)))

Theorem: ia32e-pte-4k-pagebits->pwt$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->pwt$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->pwt$inline x)
                 (ia32e-pte-4k-pagebits->pwt$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->pwt-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->pwt-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->pwt
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix pwt)))

Theorem: ia32e-pte-4k-pagebits->pwt-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->pwt-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 8) 0))
       (equal (ia32e-pte-4k-pagebits->pwt x)
              (ia32e-pte-4k-pagebits->pwt y))))

Function: ia32e-pte-4k-pagebits->pcd$inline

(defun ia32e-pte-4k-pagebits->pcd$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->pcd

(defthm bitp-of-ia32e-pte-4k-pagebits->pcd
  (b* ((pcd (ia32e-pte-4k-pagebits->pcd$inline x)))
    (bitp pcd))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->pcd$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
   ia32e-pte-4k-pagebits->pcd$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
   (ia32e-pte-4k-pagebits->pcd$inline (ia32e-pte-4k-pagebits-fix x))
   (ia32e-pte-4k-pagebits->pcd$inline x)))

Theorem: ia32e-pte-4k-pagebits->pcd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->pcd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->pcd$inline x)
                 (ia32e-pte-4k-pagebits->pcd$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->pcd-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->pcd-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->pcd
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix pcd)))

Theorem: ia32e-pte-4k-pagebits->pcd-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->pcd-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 16)
                   0))
       (equal (ia32e-pte-4k-pagebits->pcd x)
              (ia32e-pte-4k-pagebits->pcd y))))

Function: ia32e-pte-4k-pagebits->a$inline

(defun ia32e-pte-4k-pagebits->a$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->a

(defthm bitp-of-ia32e-pte-4k-pagebits->a
  (b* ((a (ia32e-pte-4k-pagebits->a$inline x)))
    (bitp a))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->a$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
     ia32e-pte-4k-pagebits->a$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
     (ia32e-pte-4k-pagebits->a$inline (ia32e-pte-4k-pagebits-fix x))
     (ia32e-pte-4k-pagebits->a$inline x)))

Theorem: ia32e-pte-4k-pagebits->a$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->a$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->a$inline x)
                 (ia32e-pte-4k-pagebits->a$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->a-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->a-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->a
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix a)))

Theorem: ia32e-pte-4k-pagebits->a-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->a-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 32)
                   0))
       (equal (ia32e-pte-4k-pagebits->a x)
              (ia32e-pte-4k-pagebits->a y))))

Function: ia32e-pte-4k-pagebits->d$inline

(defun ia32e-pte-4k-pagebits->d$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->d

(defthm bitp-of-ia32e-pte-4k-pagebits->d
  (b* ((d (ia32e-pte-4k-pagebits->d$inline x)))
    (bitp d))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->d$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
     ia32e-pte-4k-pagebits->d$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
     (ia32e-pte-4k-pagebits->d$inline (ia32e-pte-4k-pagebits-fix x))
     (ia32e-pte-4k-pagebits->d$inline x)))

Theorem: ia32e-pte-4k-pagebits->d$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->d$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->d$inline x)
                 (ia32e-pte-4k-pagebits->d$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->d-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->d-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->d
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix d)))

Theorem: ia32e-pte-4k-pagebits->d-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->d-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 64)
                   0))
       (equal (ia32e-pte-4k-pagebits->d x)
              (ia32e-pte-4k-pagebits->d y))))

Function: ia32e-pte-4k-pagebits->pat$inline

(defun ia32e-pte-4k-pagebits->pat$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->pat

(defthm bitp-of-ia32e-pte-4k-pagebits->pat
  (b* ((pat (ia32e-pte-4k-pagebits->pat$inline x)))
    (bitp pat))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->pat$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
   ia32e-pte-4k-pagebits->pat$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
   (ia32e-pte-4k-pagebits->pat$inline (ia32e-pte-4k-pagebits-fix x))
   (ia32e-pte-4k-pagebits->pat$inline x)))

Theorem: ia32e-pte-4k-pagebits->pat$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->pat$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->pat$inline x)
                 (ia32e-pte-4k-pagebits->pat$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->pat-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->pat-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->pat
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix pat)))

Theorem: ia32e-pte-4k-pagebits->pat-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->pat-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 128)
                   0))
       (equal (ia32e-pte-4k-pagebits->pat x)
              (ia32e-pte-4k-pagebits->pat y))))

Function: ia32e-pte-4k-pagebits->g$inline

(defun ia32e-pte-4k-pagebits->g$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->g

(defthm bitp-of-ia32e-pte-4k-pagebits->g
  (b* ((g (ia32e-pte-4k-pagebits->g$inline x)))
    (bitp g))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->g$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
     ia32e-pte-4k-pagebits->g$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
     (ia32e-pte-4k-pagebits->g$inline (ia32e-pte-4k-pagebits-fix x))
     (ia32e-pte-4k-pagebits->g$inline x)))

Theorem: ia32e-pte-4k-pagebits->g$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->g$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->g$inline x)
                 (ia32e-pte-4k-pagebits->g$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->g-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->g-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->g
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix g)))

Theorem: ia32e-pte-4k-pagebits->g-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->g-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 256)
                   0))
       (equal (ia32e-pte-4k-pagebits->g x)
              (ia32e-pte-4k-pagebits->g y))))

Function: ia32e-pte-4k-pagebits->res1$inline

(defun ia32e-pte-4k-pagebits->res1$inline (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pte-4k-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: 3bits-p-of-ia32e-pte-4k-pagebits->res1

(defthm 3bits-p-of-ia32e-pte-4k-pagebits->res1
  (b* ((res1 (ia32e-pte-4k-pagebits->res1$inline x)))
    (3bits-p res1))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->res1$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  ia32e-pte-4k-pagebits->res1$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
  (ia32e-pte-4k-pagebits->res1$inline (ia32e-pte-4k-pagebits-fix x))
  (ia32e-pte-4k-pagebits->res1$inline x)))

Theorem: ia32e-pte-4k-pagebits->res1$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->res1$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->res1$inline x)
                 (ia32e-pte-4k-pagebits->res1$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->res1-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->res1-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->res1
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (3bits-fix res1)))

Theorem: ia32e-pte-4k-pagebits->res1-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->res1-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 3584)
                   0))
       (equal (ia32e-pte-4k-pagebits->res1 x)
              (ia32e-pte-4k-pagebits->res1 y))))

Function: ia32e-pte-4k-pagebits->page$inline

(defun ia32e-pte-4k-pagebits->page$inline (x)
  (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pte-4k-pagebits-fix x)))
         (part-select x :low 12 :width 40))
       :exec (the (unsigned-byte 40)
                  (logand (the (unsigned-byte 40) 1099511627775)
                          (the (unsigned-byte 52)
                               (ash (the (unsigned-byte 64) x)
                                    -12))))))

Theorem: 40bits-p-of-ia32e-pte-4k-pagebits->page

(defthm 40bits-p-of-ia32e-pte-4k-pagebits->page
  (b* ((page (ia32e-pte-4k-pagebits->page$inline x)))
    (40bits-p page))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->page$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  ia32e-pte-4k-pagebits->page$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
  (ia32e-pte-4k-pagebits->page$inline (ia32e-pte-4k-pagebits-fix x))
  (ia32e-pte-4k-pagebits->page$inline x)))

Theorem: ia32e-pte-4k-pagebits->page$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->page$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->page$inline x)
                 (ia32e-pte-4k-pagebits->page$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->page-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->page-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->page
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (40bits-fix page)))

Theorem: ia32e-pte-4k-pagebits->page-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->page-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask)
                           4503599627366400)
                   0))
       (equal (ia32e-pte-4k-pagebits->page x)
              (ia32e-pte-4k-pagebits->page y))))

Function: ia32e-pte-4k-pagebits->res2$inline

(defun ia32e-pte-4k-pagebits->res2$inline (x)
  (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pte-4k-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: 11bits-p-of-ia32e-pte-4k-pagebits->res2

(defthm 11bits-p-of-ia32e-pte-4k-pagebits->res2
  (b* ((res2 (ia32e-pte-4k-pagebits->res2$inline x)))
    (11bits-p res2))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->res2$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  ia32e-pte-4k-pagebits->res2$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
  (ia32e-pte-4k-pagebits->res2$inline (ia32e-pte-4k-pagebits-fix x))
  (ia32e-pte-4k-pagebits->res2$inline x)))

Theorem: ia32e-pte-4k-pagebits->res2$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->res2$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->res2$inline x)
                 (ia32e-pte-4k-pagebits->res2$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->res2-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->res2-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->res2
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (11bits-fix res2)))

Theorem: ia32e-pte-4k-pagebits->res2-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->res2-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask)
                           9218868437227405312)
                   0))
       (equal (ia32e-pte-4k-pagebits->res2 x)
              (ia32e-pte-4k-pagebits->res2 y))))

Function: ia32e-pte-4k-pagebits->xd$inline

(defun ia32e-pte-4k-pagebits->xd$inline (x)
  (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pte-4k-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: bitp-of-ia32e-pte-4k-pagebits->xd

(defthm bitp-of-ia32e-pte-4k-pagebits->xd
  (b* ((xd (ia32e-pte-4k-pagebits->xd$inline x)))
    (bitp xd))
  :rule-classes :rewrite)

Theorem: ia32e-pte-4k-pagebits->xd$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
    ia32e-pte-4k-pagebits->xd$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
    (ia32e-pte-4k-pagebits->xd$inline (ia32e-pte-4k-pagebits-fix x))
    (ia32e-pte-4k-pagebits->xd$inline x)))

Theorem: ia32e-pte-4k-pagebits->xd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pte-4k-pagebits->xd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (ia32e-pte-4k-pagebits->xd$inline x)
                 (ia32e-pte-4k-pagebits->xd$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pte-4k-pagebits->xd-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits->xd-of-ia32e-pte-4k-pagebits
 (equal
   (ia32e-pte-4k-pagebits->xd
        (ia32e-pte-4k-pagebits p r/w u/s
                               pwt pcd a d pat g res1 page res2 xd))
   (bfix xd)))

Theorem: ia32e-pte-4k-pagebits->xd-of-write-with-mask

(defthm ia32e-pte-4k-pagebits->xd-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pte-4k-pagebits-equiv-under-mask)
            (ia32e-pte-4k-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask)
                           9223372036854775808)
                   0))
       (equal (ia32e-pte-4k-pagebits->xd x)
              (ia32e-pte-4k-pagebits->xd y))))

Theorem: ia32e-pte-4k-pagebits-fix-in-terms-of-ia32e-pte-4k-pagebits

(defthm ia32e-pte-4k-pagebits-fix-in-terms-of-ia32e-pte-4k-pagebits
  (equal (ia32e-pte-4k-pagebits-fix x)
         (change-ia32e-pte-4k-pagebits x)))

Function: !ia32e-pte-4k-pagebits->p$inline

(defun !ia32e-pte-4k-pagebits->p$inline (p x)
  (declare (xargs :guard (and (bitp p)
                              (ia32e-pte-4k-pagebits-p x))))
  (mbe :logic
       (b* ((p (mbe :logic (bfix p) :exec p))
            (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->p

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->p
  (b* ((new-x (!ia32e-pte-4k-pagebits->p$inline p x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->p$inline-of-bfix-p

(defthm !ia32e-pte-4k-pagebits->p$inline-of-bfix-p
  (equal (!ia32e-pte-4k-pagebits->p$inline (bfix p)
                                           x)
         (!ia32e-pte-4k-pagebits->p$inline p x)))

Theorem: !ia32e-pte-4k-pagebits->p$inline-bit-equiv-congruence-on-p

(defthm !ia32e-pte-4k-pagebits->p$inline-bit-equiv-congruence-on-p
  (implies (bit-equiv p p-equiv)
           (equal (!ia32e-pte-4k-pagebits->p$inline p x)
                  (!ia32e-pte-4k-pagebits->p$inline p-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->p$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
    !ia32e-pte-4k-pagebits->p$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
  (!ia32e-pte-4k-pagebits->p$inline p (ia32e-pte-4k-pagebits-fix x))
  (!ia32e-pte-4k-pagebits->p$inline p x)))

Theorem: !ia32e-pte-4k-pagebits->p$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->p$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->p$inline p x)
                 (!ia32e-pte-4k-pagebits->p$inline p x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->p-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->p-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->p p x)
         (change-ia32e-pte-4k-pagebits x :p p)))

Theorem: ia32e-pte-4k-pagebits->p-of-!ia32e-pte-4k-pagebits->p

(defthm ia32e-pte-4k-pagebits->p-of-!ia32e-pte-4k-pagebits->p
  (b* ((?new-x (!ia32e-pte-4k-pagebits->p$inline p x)))
    (equal (ia32e-pte-4k-pagebits->p new-x)
           (bfix p))))

Theorem: !ia32e-pte-4k-pagebits->p-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->p-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->p$inline p x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -2)))

Function: !ia32e-pte-4k-pagebits->r/w$inline

(defun !ia32e-pte-4k-pagebits->r/w$inline (r/w x)
 (declare (xargs :guard (and (bitp r/w)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe
    :logic
    (b* ((r/w (mbe :logic (bfix r/w) :exec r/w))
         (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->r/w

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->r/w
  (b* ((new-x (!ia32e-pte-4k-pagebits->r/w$inline r/w x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->r/w$inline-of-bfix-r/w

(defthm !ia32e-pte-4k-pagebits->r/w$inline-of-bfix-r/w
  (equal (!ia32e-pte-4k-pagebits->r/w$inline (bfix r/w)
                                             x)
         (!ia32e-pte-4k-pagebits->r/w$inline r/w x)))

Theorem: !ia32e-pte-4k-pagebits->r/w$inline-bit-equiv-congruence-on-r/w

(defthm
     !ia32e-pte-4k-pagebits->r/w$inline-bit-equiv-congruence-on-r/w
  (implies (bit-equiv r/w r/w-equiv)
           (equal (!ia32e-pte-4k-pagebits->r/w$inline r/w x)
                  (!ia32e-pte-4k-pagebits->r/w$inline r/w-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->r/w$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  !ia32e-pte-4k-pagebits->r/w$inline-of-ia32e-pte-4k-pagebits-fix-x
  (equal (!ia32e-pte-4k-pagebits->r/w$inline
              r/w (ia32e-pte-4k-pagebits-fix x))
         (!ia32e-pte-4k-pagebits->r/w$inline r/w x)))

Theorem: !ia32e-pte-4k-pagebits->r/w$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->r/w$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->r/w$inline r/w x)
                 (!ia32e-pte-4k-pagebits->r/w$inline r/w x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->r/w-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->r/w-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->r/w r/w x)
         (change-ia32e-pte-4k-pagebits x
                                       :r/w r/w)))

Theorem: ia32e-pte-4k-pagebits->r/w-of-!ia32e-pte-4k-pagebits->r/w

(defthm ia32e-pte-4k-pagebits->r/w-of-!ia32e-pte-4k-pagebits->r/w
  (b* ((?new-x (!ia32e-pte-4k-pagebits->r/w$inline r/w x)))
    (equal (ia32e-pte-4k-pagebits->r/w new-x)
           (bfix r/w))))

Theorem: !ia32e-pte-4k-pagebits->r/w-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->r/w-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->r/w$inline r/w x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -3)))

Function: !ia32e-pte-4k-pagebits->u/s$inline

(defun !ia32e-pte-4k-pagebits->u/s$inline (u/s x)
 (declare (xargs :guard (and (bitp u/s)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe
    :logic
    (b* ((u/s (mbe :logic (bfix u/s) :exec u/s))
         (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->u/s

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->u/s
  (b* ((new-x (!ia32e-pte-4k-pagebits->u/s$inline u/s x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->u/s$inline-of-bfix-u/s

(defthm !ia32e-pte-4k-pagebits->u/s$inline-of-bfix-u/s
  (equal (!ia32e-pte-4k-pagebits->u/s$inline (bfix u/s)
                                             x)
         (!ia32e-pte-4k-pagebits->u/s$inline u/s x)))

Theorem: !ia32e-pte-4k-pagebits->u/s$inline-bit-equiv-congruence-on-u/s

(defthm
     !ia32e-pte-4k-pagebits->u/s$inline-bit-equiv-congruence-on-u/s
  (implies (bit-equiv u/s u/s-equiv)
           (equal (!ia32e-pte-4k-pagebits->u/s$inline u/s x)
                  (!ia32e-pte-4k-pagebits->u/s$inline u/s-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->u/s$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  !ia32e-pte-4k-pagebits->u/s$inline-of-ia32e-pte-4k-pagebits-fix-x
  (equal (!ia32e-pte-4k-pagebits->u/s$inline
              u/s (ia32e-pte-4k-pagebits-fix x))
         (!ia32e-pte-4k-pagebits->u/s$inline u/s x)))

Theorem: !ia32e-pte-4k-pagebits->u/s$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->u/s$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->u/s$inline u/s x)
                 (!ia32e-pte-4k-pagebits->u/s$inline u/s x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->u/s-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->u/s-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->u/s u/s x)
         (change-ia32e-pte-4k-pagebits x
                                       :u/s u/s)))

Theorem: ia32e-pte-4k-pagebits->u/s-of-!ia32e-pte-4k-pagebits->u/s

(defthm ia32e-pte-4k-pagebits->u/s-of-!ia32e-pte-4k-pagebits->u/s
  (b* ((?new-x (!ia32e-pte-4k-pagebits->u/s$inline u/s x)))
    (equal (ia32e-pte-4k-pagebits->u/s new-x)
           (bfix u/s))))

Theorem: !ia32e-pte-4k-pagebits->u/s-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->u/s-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->u/s$inline u/s x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -5)))

Function: !ia32e-pte-4k-pagebits->pwt$inline

(defun !ia32e-pte-4k-pagebits->pwt$inline (pwt x)
 (declare (xargs :guard (and (bitp pwt)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe
    :logic
    (b* ((pwt (mbe :logic (bfix pwt) :exec pwt))
         (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->pwt

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->pwt
  (b* ((new-x (!ia32e-pte-4k-pagebits->pwt$inline pwt x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->pwt$inline-of-bfix-pwt

(defthm !ia32e-pte-4k-pagebits->pwt$inline-of-bfix-pwt
  (equal (!ia32e-pte-4k-pagebits->pwt$inline (bfix pwt)
                                             x)
         (!ia32e-pte-4k-pagebits->pwt$inline pwt x)))

Theorem: !ia32e-pte-4k-pagebits->pwt$inline-bit-equiv-congruence-on-pwt

(defthm
     !ia32e-pte-4k-pagebits->pwt$inline-bit-equiv-congruence-on-pwt
  (implies (bit-equiv pwt pwt-equiv)
           (equal (!ia32e-pte-4k-pagebits->pwt$inline pwt x)
                  (!ia32e-pte-4k-pagebits->pwt$inline pwt-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->pwt$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  !ia32e-pte-4k-pagebits->pwt$inline-of-ia32e-pte-4k-pagebits-fix-x
  (equal (!ia32e-pte-4k-pagebits->pwt$inline
              pwt (ia32e-pte-4k-pagebits-fix x))
         (!ia32e-pte-4k-pagebits->pwt$inline pwt x)))

Theorem: !ia32e-pte-4k-pagebits->pwt$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->pwt$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->pwt$inline pwt x)
                 (!ia32e-pte-4k-pagebits->pwt$inline pwt x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->pwt-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->pwt-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->pwt pwt x)
         (change-ia32e-pte-4k-pagebits x
                                       :pwt pwt)))

Theorem: ia32e-pte-4k-pagebits->pwt-of-!ia32e-pte-4k-pagebits->pwt

(defthm ia32e-pte-4k-pagebits->pwt-of-!ia32e-pte-4k-pagebits->pwt
  (b* ((?new-x (!ia32e-pte-4k-pagebits->pwt$inline pwt x)))
    (equal (ia32e-pte-4k-pagebits->pwt new-x)
           (bfix pwt))))

Theorem: !ia32e-pte-4k-pagebits->pwt-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->pwt-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->pwt$inline pwt x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -9)))

Function: !ia32e-pte-4k-pagebits->pcd$inline

(defun !ia32e-pte-4k-pagebits->pcd$inline (pcd x)
 (declare (xargs :guard (and (bitp pcd)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe
    :logic
    (b* ((pcd (mbe :logic (bfix pcd) :exec pcd))
         (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->pcd

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->pcd
  (b* ((new-x (!ia32e-pte-4k-pagebits->pcd$inline pcd x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->pcd$inline-of-bfix-pcd

(defthm !ia32e-pte-4k-pagebits->pcd$inline-of-bfix-pcd
  (equal (!ia32e-pte-4k-pagebits->pcd$inline (bfix pcd)
                                             x)
         (!ia32e-pte-4k-pagebits->pcd$inline pcd x)))

Theorem: !ia32e-pte-4k-pagebits->pcd$inline-bit-equiv-congruence-on-pcd

(defthm
     !ia32e-pte-4k-pagebits->pcd$inline-bit-equiv-congruence-on-pcd
  (implies (bit-equiv pcd pcd-equiv)
           (equal (!ia32e-pte-4k-pagebits->pcd$inline pcd x)
                  (!ia32e-pte-4k-pagebits->pcd$inline pcd-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->pcd$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  !ia32e-pte-4k-pagebits->pcd$inline-of-ia32e-pte-4k-pagebits-fix-x
  (equal (!ia32e-pte-4k-pagebits->pcd$inline
              pcd (ia32e-pte-4k-pagebits-fix x))
         (!ia32e-pte-4k-pagebits->pcd$inline pcd x)))

Theorem: !ia32e-pte-4k-pagebits->pcd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->pcd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->pcd$inline pcd x)
                 (!ia32e-pte-4k-pagebits->pcd$inline pcd x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->pcd-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->pcd-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->pcd pcd x)
         (change-ia32e-pte-4k-pagebits x
                                       :pcd pcd)))

Theorem: ia32e-pte-4k-pagebits->pcd-of-!ia32e-pte-4k-pagebits->pcd

(defthm ia32e-pte-4k-pagebits->pcd-of-!ia32e-pte-4k-pagebits->pcd
  (b* ((?new-x (!ia32e-pte-4k-pagebits->pcd$inline pcd x)))
    (equal (ia32e-pte-4k-pagebits->pcd new-x)
           (bfix pcd))))

Theorem: !ia32e-pte-4k-pagebits->pcd-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->pcd-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->pcd$inline pcd x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -17)))

Function: !ia32e-pte-4k-pagebits->a$inline

(defun !ia32e-pte-4k-pagebits->a$inline (a x)
 (declare (xargs :guard (and (bitp a)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe :logic
      (b* ((a (mbe :logic (bfix a) :exec a))
           (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->a

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->a
  (b* ((new-x (!ia32e-pte-4k-pagebits->a$inline a x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->a$inline-of-bfix-a

(defthm !ia32e-pte-4k-pagebits->a$inline-of-bfix-a
  (equal (!ia32e-pte-4k-pagebits->a$inline (bfix a)
                                           x)
         (!ia32e-pte-4k-pagebits->a$inline a x)))

Theorem: !ia32e-pte-4k-pagebits->a$inline-bit-equiv-congruence-on-a

(defthm !ia32e-pte-4k-pagebits->a$inline-bit-equiv-congruence-on-a
  (implies (bit-equiv a a-equiv)
           (equal (!ia32e-pte-4k-pagebits->a$inline a x)
                  (!ia32e-pte-4k-pagebits->a$inline a-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->a$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
    !ia32e-pte-4k-pagebits->a$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
  (!ia32e-pte-4k-pagebits->a$inline a (ia32e-pte-4k-pagebits-fix x))
  (!ia32e-pte-4k-pagebits->a$inline a x)))

Theorem: !ia32e-pte-4k-pagebits->a$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->a$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->a$inline a x)
                 (!ia32e-pte-4k-pagebits->a$inline a x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->a-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->a-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->a a x)
         (change-ia32e-pte-4k-pagebits x :a a)))

Theorem: ia32e-pte-4k-pagebits->a-of-!ia32e-pte-4k-pagebits->a

(defthm ia32e-pte-4k-pagebits->a-of-!ia32e-pte-4k-pagebits->a
  (b* ((?new-x (!ia32e-pte-4k-pagebits->a$inline a x)))
    (equal (ia32e-pte-4k-pagebits->a new-x)
           (bfix a))))

Theorem: !ia32e-pte-4k-pagebits->a-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->a-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->a$inline a x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -33)))

Function: !ia32e-pte-4k-pagebits->d$inline

(defun !ia32e-pte-4k-pagebits->d$inline (d x)
 (declare (xargs :guard (and (bitp d)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe :logic
      (b* ((d (mbe :logic (bfix d) :exec d))
           (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->d

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->d
  (b* ((new-x (!ia32e-pte-4k-pagebits->d$inline d x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->d$inline-of-bfix-d

(defthm !ia32e-pte-4k-pagebits->d$inline-of-bfix-d
  (equal (!ia32e-pte-4k-pagebits->d$inline (bfix d)
                                           x)
         (!ia32e-pte-4k-pagebits->d$inline d x)))

Theorem: !ia32e-pte-4k-pagebits->d$inline-bit-equiv-congruence-on-d

(defthm !ia32e-pte-4k-pagebits->d$inline-bit-equiv-congruence-on-d
  (implies (bit-equiv d d-equiv)
           (equal (!ia32e-pte-4k-pagebits->d$inline d x)
                  (!ia32e-pte-4k-pagebits->d$inline d-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->d$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
    !ia32e-pte-4k-pagebits->d$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
  (!ia32e-pte-4k-pagebits->d$inline d (ia32e-pte-4k-pagebits-fix x))
  (!ia32e-pte-4k-pagebits->d$inline d x)))

Theorem: !ia32e-pte-4k-pagebits->d$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->d$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->d$inline d x)
                 (!ia32e-pte-4k-pagebits->d$inline d x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->d-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->d-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->d d x)
         (change-ia32e-pte-4k-pagebits x :d d)))

Theorem: ia32e-pte-4k-pagebits->d-of-!ia32e-pte-4k-pagebits->d

(defthm ia32e-pte-4k-pagebits->d-of-!ia32e-pte-4k-pagebits->d
  (b* ((?new-x (!ia32e-pte-4k-pagebits->d$inline d x)))
    (equal (ia32e-pte-4k-pagebits->d new-x)
           (bfix d))))

Theorem: !ia32e-pte-4k-pagebits->d-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->d-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->d$inline d x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -65)))

Function: !ia32e-pte-4k-pagebits->pat$inline

(defun !ia32e-pte-4k-pagebits->pat$inline (pat x)
 (declare (xargs :guard (and (bitp pat)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe
    :logic
    (b* ((pat (mbe :logic (bfix pat) :exec pat))
         (x (ia32e-pte-4k-pagebits-fix x)))
      (part-install pat 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) pat) 7))))))

Theorem: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->pat

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->pat
  (b* ((new-x (!ia32e-pte-4k-pagebits->pat$inline pat x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->pat$inline-of-bfix-pat

(defthm !ia32e-pte-4k-pagebits->pat$inline-of-bfix-pat
  (equal (!ia32e-pte-4k-pagebits->pat$inline (bfix pat)
                                             x)
         (!ia32e-pte-4k-pagebits->pat$inline pat x)))

Theorem: !ia32e-pte-4k-pagebits->pat$inline-bit-equiv-congruence-on-pat

(defthm
     !ia32e-pte-4k-pagebits->pat$inline-bit-equiv-congruence-on-pat
  (implies (bit-equiv pat pat-equiv)
           (equal (!ia32e-pte-4k-pagebits->pat$inline pat x)
                  (!ia32e-pte-4k-pagebits->pat$inline pat-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->pat$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
  !ia32e-pte-4k-pagebits->pat$inline-of-ia32e-pte-4k-pagebits-fix-x
  (equal (!ia32e-pte-4k-pagebits->pat$inline
              pat (ia32e-pte-4k-pagebits-fix x))
         (!ia32e-pte-4k-pagebits->pat$inline pat x)))

Theorem: !ia32e-pte-4k-pagebits->pat$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->pat$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->pat$inline pat x)
                 (!ia32e-pte-4k-pagebits->pat$inline pat x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->pat-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->pat-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->pat pat x)
         (change-ia32e-pte-4k-pagebits x
                                       :pat pat)))

Theorem: ia32e-pte-4k-pagebits->pat-of-!ia32e-pte-4k-pagebits->pat

(defthm ia32e-pte-4k-pagebits->pat-of-!ia32e-pte-4k-pagebits->pat
  (b* ((?new-x (!ia32e-pte-4k-pagebits->pat$inline pat x)))
    (equal (ia32e-pte-4k-pagebits->pat new-x)
           (bfix pat))))

Theorem: !ia32e-pte-4k-pagebits->pat-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->pat-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->pat$inline pat x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -129)))

Function: !ia32e-pte-4k-pagebits->g$inline

(defun !ia32e-pte-4k-pagebits->g$inline (g x)
 (declare (xargs :guard (and (bitp g)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe :logic
      (b* ((g (mbe :logic (bfix g) :exec g))
           (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->g

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->g
  (b* ((new-x (!ia32e-pte-4k-pagebits->g$inline g x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->g$inline-of-bfix-g

(defthm !ia32e-pte-4k-pagebits->g$inline-of-bfix-g
  (equal (!ia32e-pte-4k-pagebits->g$inline (bfix g)
                                           x)
         (!ia32e-pte-4k-pagebits->g$inline g x)))

Theorem: !ia32e-pte-4k-pagebits->g$inline-bit-equiv-congruence-on-g

(defthm !ia32e-pte-4k-pagebits->g$inline-bit-equiv-congruence-on-g
  (implies (bit-equiv g g-equiv)
           (equal (!ia32e-pte-4k-pagebits->g$inline g x)
                  (!ia32e-pte-4k-pagebits->g$inline g-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->g$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
    !ia32e-pte-4k-pagebits->g$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal
  (!ia32e-pte-4k-pagebits->g$inline g (ia32e-pte-4k-pagebits-fix x))
  (!ia32e-pte-4k-pagebits->g$inline g x)))

Theorem: !ia32e-pte-4k-pagebits->g$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->g$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->g$inline g x)
                 (!ia32e-pte-4k-pagebits->g$inline g x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->g-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->g-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->g g x)
         (change-ia32e-pte-4k-pagebits x :g g)))

Theorem: ia32e-pte-4k-pagebits->g-of-!ia32e-pte-4k-pagebits->g

(defthm ia32e-pte-4k-pagebits->g-of-!ia32e-pte-4k-pagebits->g
  (b* ((?new-x (!ia32e-pte-4k-pagebits->g$inline g x)))
    (equal (ia32e-pte-4k-pagebits->g new-x)
           (bfix g))))

Theorem: !ia32e-pte-4k-pagebits->g-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->g-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->g$inline g x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -257)))

Function: !ia32e-pte-4k-pagebits->res1$inline

(defun !ia32e-pte-4k-pagebits->res1$inline (res1 x)
 (declare (xargs :guard (and (3bits-p res1)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe :logic
      (b* ((res1 (mbe :logic (3bits-fix res1)
                      :exec res1))
           (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->res1

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->res1
  (b* ((new-x (!ia32e-pte-4k-pagebits->res1$inline res1 x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->res1$inline-of-3bits-fix-res1

(defthm !ia32e-pte-4k-pagebits->res1$inline-of-3bits-fix-res1
  (equal (!ia32e-pte-4k-pagebits->res1$inline (3bits-fix res1)
                                              x)
         (!ia32e-pte-4k-pagebits->res1$inline res1 x)))

Theorem: !ia32e-pte-4k-pagebits->res1$inline-3bits-equiv-congruence-on-res1

(defthm
 !ia32e-pte-4k-pagebits->res1$inline-3bits-equiv-congruence-on-res1
 (implies
      (3bits-equiv res1 res1-equiv)
      (equal (!ia32e-pte-4k-pagebits->res1$inline res1 x)
             (!ia32e-pte-4k-pagebits->res1$inline res1-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->res1$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
 !ia32e-pte-4k-pagebits->res1$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal (!ia32e-pte-4k-pagebits->res1$inline
             res1 (ia32e-pte-4k-pagebits-fix x))
        (!ia32e-pte-4k-pagebits->res1$inline res1 x)))

Theorem: !ia32e-pte-4k-pagebits->res1$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->res1$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies
      (ia32e-pte-4k-pagebits-equiv x x-equiv)
      (equal (!ia32e-pte-4k-pagebits->res1$inline res1 x)
             (!ia32e-pte-4k-pagebits->res1$inline res1 x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->res1-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->res1-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->res1 res1 x)
         (change-ia32e-pte-4k-pagebits x
                                       :res1 res1)))

Theorem: ia32e-pte-4k-pagebits->res1-of-!ia32e-pte-4k-pagebits->res1

(defthm ia32e-pte-4k-pagebits->res1-of-!ia32e-pte-4k-pagebits->res1
  (b* ((?new-x (!ia32e-pte-4k-pagebits->res1$inline res1 x)))
    (equal (ia32e-pte-4k-pagebits->res1 new-x)
           (3bits-fix res1))))

Theorem: !ia32e-pte-4k-pagebits->res1-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->res1-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->res1$inline res1 x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask new-x x -3585)))

Function: !ia32e-pte-4k-pagebits->page$inline

(defun !ia32e-pte-4k-pagebits->page$inline (page x)
  (declare (xargs :guard (and (40bits-p page)
                              (ia32e-pte-4k-pagebits-p x))))
  (mbe :logic
       (b* ((page (mbe :logic (40bits-fix page)
                       :exec page))
            (x (ia32e-pte-4k-pagebits-fix x)))
         (part-install page 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) page)
                                    12))))))

Theorem: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->page

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->page
  (b* ((new-x (!ia32e-pte-4k-pagebits->page$inline page x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->page$inline-of-40bits-fix-page

(defthm !ia32e-pte-4k-pagebits->page$inline-of-40bits-fix-page
  (equal (!ia32e-pte-4k-pagebits->page$inline (40bits-fix page)
                                              x)
         (!ia32e-pte-4k-pagebits->page$inline page x)))

Theorem: !ia32e-pte-4k-pagebits->page$inline-40bits-equiv-congruence-on-page

(defthm
 !ia32e-pte-4k-pagebits->page$inline-40bits-equiv-congruence-on-page
 (implies
      (40bits-equiv page page-equiv)
      (equal (!ia32e-pte-4k-pagebits->page$inline page x)
             (!ia32e-pte-4k-pagebits->page$inline page-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->page$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
 !ia32e-pte-4k-pagebits->page$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal (!ia32e-pte-4k-pagebits->page$inline
             page (ia32e-pte-4k-pagebits-fix x))
        (!ia32e-pte-4k-pagebits->page$inline page x)))

Theorem: !ia32e-pte-4k-pagebits->page$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->page$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies
      (ia32e-pte-4k-pagebits-equiv x x-equiv)
      (equal (!ia32e-pte-4k-pagebits->page$inline page x)
             (!ia32e-pte-4k-pagebits->page$inline page x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->page-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->page-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->page page x)
         (change-ia32e-pte-4k-pagebits x
                                       :page page)))

Theorem: ia32e-pte-4k-pagebits->page-of-!ia32e-pte-4k-pagebits->page

(defthm ia32e-pte-4k-pagebits->page-of-!ia32e-pte-4k-pagebits->page
  (b* ((?new-x (!ia32e-pte-4k-pagebits->page$inline page x)))
    (equal (ia32e-pte-4k-pagebits->page new-x)
           (40bits-fix page))))

Theorem: !ia32e-pte-4k-pagebits->page-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->page-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->page$inline page x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask
         new-x x -4503599627366401)))

Function: !ia32e-pte-4k-pagebits->res2$inline

(defun !ia32e-pte-4k-pagebits->res2$inline (res2 x)
  (declare (xargs :guard (and (11bits-p res2)
                              (ia32e-pte-4k-pagebits-p x))))
  (mbe :logic
       (b* ((res2 (mbe :logic (11bits-fix res2)
                       :exec res2))
            (x (ia32e-pte-4k-pagebits-fix x)))
         (part-install res2 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) res2)
                                    52))))))

Theorem: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->res2

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->res2
  (b* ((new-x (!ia32e-pte-4k-pagebits->res2$inline res2 x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->res2$inline-of-11bits-fix-res2

(defthm !ia32e-pte-4k-pagebits->res2$inline-of-11bits-fix-res2
  (equal (!ia32e-pte-4k-pagebits->res2$inline (11bits-fix res2)
                                              x)
         (!ia32e-pte-4k-pagebits->res2$inline res2 x)))

Theorem: !ia32e-pte-4k-pagebits->res2$inline-11bits-equiv-congruence-on-res2

(defthm
 !ia32e-pte-4k-pagebits->res2$inline-11bits-equiv-congruence-on-res2
 (implies
      (11bits-equiv res2 res2-equiv)
      (equal (!ia32e-pte-4k-pagebits->res2$inline res2 x)
             (!ia32e-pte-4k-pagebits->res2$inline res2-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->res2$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
 !ia32e-pte-4k-pagebits->res2$inline-of-ia32e-pte-4k-pagebits-fix-x
 (equal (!ia32e-pte-4k-pagebits->res2$inline
             res2 (ia32e-pte-4k-pagebits-fix x))
        (!ia32e-pte-4k-pagebits->res2$inline res2 x)))

Theorem: !ia32e-pte-4k-pagebits->res2$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->res2$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies
      (ia32e-pte-4k-pagebits-equiv x x-equiv)
      (equal (!ia32e-pte-4k-pagebits->res2$inline res2 x)
             (!ia32e-pte-4k-pagebits->res2$inline res2 x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->res2-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->res2-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->res2 res2 x)
         (change-ia32e-pte-4k-pagebits x
                                       :res2 res2)))

Theorem: ia32e-pte-4k-pagebits->res2-of-!ia32e-pte-4k-pagebits->res2

(defthm ia32e-pte-4k-pagebits->res2-of-!ia32e-pte-4k-pagebits->res2
  (b* ((?new-x (!ia32e-pte-4k-pagebits->res2$inline res2 x)))
    (equal (ia32e-pte-4k-pagebits->res2 new-x)
           (11bits-fix res2))))

Theorem: !ia32e-pte-4k-pagebits->res2-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->res2-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->res2$inline res2 x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask
         new-x x -9218868437227405313)))

Function: !ia32e-pte-4k-pagebits->xd$inline

(defun !ia32e-pte-4k-pagebits->xd$inline (xd x)
 (declare (xargs :guard (and (bitp xd)
                             (ia32e-pte-4k-pagebits-p x))))
 (mbe
    :logic
    (b* ((xd (mbe :logic (bfix xd) :exec xd))
         (x (ia32e-pte-4k-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: ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->xd

(defthm ia32e-pte-4k-pagebits-p-of-!ia32e-pte-4k-pagebits->xd
  (b* ((new-x (!ia32e-pte-4k-pagebits->xd$inline xd x)))
    (ia32e-pte-4k-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pte-4k-pagebits->xd$inline-of-bfix-xd

(defthm !ia32e-pte-4k-pagebits->xd$inline-of-bfix-xd
  (equal (!ia32e-pte-4k-pagebits->xd$inline (bfix xd)
                                            x)
         (!ia32e-pte-4k-pagebits->xd$inline xd x)))

Theorem: !ia32e-pte-4k-pagebits->xd$inline-bit-equiv-congruence-on-xd

(defthm !ia32e-pte-4k-pagebits->xd$inline-bit-equiv-congruence-on-xd
  (implies (bit-equiv xd xd-equiv)
           (equal (!ia32e-pte-4k-pagebits->xd$inline xd x)
                  (!ia32e-pte-4k-pagebits->xd$inline xd-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->xd$inline-of-ia32e-pte-4k-pagebits-fix-x

(defthm
   !ia32e-pte-4k-pagebits->xd$inline-of-ia32e-pte-4k-pagebits-fix-x
  (equal (!ia32e-pte-4k-pagebits->xd$inline
              xd (ia32e-pte-4k-pagebits-fix x))
         (!ia32e-pte-4k-pagebits->xd$inline xd x)))

Theorem: !ia32e-pte-4k-pagebits->xd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pte-4k-pagebits->xd$inline-ia32e-pte-4k-pagebits-equiv-congruence-on-x
 (implies (ia32e-pte-4k-pagebits-equiv x x-equiv)
          (equal (!ia32e-pte-4k-pagebits->xd$inline xd x)
                 (!ia32e-pte-4k-pagebits->xd$inline xd x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pte-4k-pagebits->xd-is-ia32e-pte-4k-pagebits

(defthm !ia32e-pte-4k-pagebits->xd-is-ia32e-pte-4k-pagebits
  (equal (!ia32e-pte-4k-pagebits->xd xd x)
         (change-ia32e-pte-4k-pagebits x
                                       :xd xd)))

Theorem: ia32e-pte-4k-pagebits->xd-of-!ia32e-pte-4k-pagebits->xd

(defthm ia32e-pte-4k-pagebits->xd-of-!ia32e-pte-4k-pagebits->xd
  (b* ((?new-x (!ia32e-pte-4k-pagebits->xd$inline xd x)))
    (equal (ia32e-pte-4k-pagebits->xd new-x)
           (bfix xd))))

Theorem: !ia32e-pte-4k-pagebits->xd-equiv-under-mask

(defthm !ia32e-pte-4k-pagebits->xd-equiv-under-mask
  (b* ((?new-x (!ia32e-pte-4k-pagebits->xd$inline xd x)))
    (ia32e-pte-4k-pagebits-equiv-under-mask
         new-x x 9223372036854775807)))

Function: ia32e-pte-4k-pagebits-debug

(defun ia32e-pte-4k-pagebits-debug (x)
 (declare (xargs :guard (ia32e-pte-4k-pagebits-p x)))
 (let ((__function__ 'ia32e-pte-4k-pagebits-debug))
  (declare (ignorable __function__))
  (b* (((ia32e-pte-4k-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 'pat x.pat)
                   (cons (cons 'g x.g)
                         (cons (cons 'res1 x.res1)
                               (cons (cons 'page x.page)
                                     (cons (cons 'res2 x.res2)
                                           (cons (cons 'xd x.xd)
                                                 nil))))))))))))))))

Subtopics

Ia32e-pte-4k-pagebits-p: Recognizer for ia32e-pte-4k-pagebits bit structures.
!ia32e-pte-4k-pagebits->res2: Update the |X86ISA|::|RES2| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->page: Update the |X86ISA|::|PAGE| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->res1: Update the |X86ISA|::|RES1| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->xd: Update the |X86ISA|::|XD| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->u/s: Update the |X86ISA|::|U/S| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->r/w: Update the |X86ISA|::|R/W| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->pwt: Update the |X86ISA|::|PWT| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->pcd: Update the |X86ISA|::|PCD| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->pat: Update the |X86ISA|::|PAT| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->g: Update the |X86ISA|::|G| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->d: Update the |ACL2|::|D| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->a: Update the |ACL2|::|A| field of a ia32e-pte-4k-pagebits bit structure.
!ia32e-pte-4k-pagebits->p: Update the |ACL2|::|P| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits-fix: Fixing function for ia32e-pte-4k-pagebits bit structures.
Ia32e-pte-4k-pagebits->res2: Access the |X86ISA|::|RES2| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->res1: Access the |X86ISA|::|RES1| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->page: Access the |X86ISA|::|PAGE| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->xd: Access the |X86ISA|::|XD| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->u/s: Access the |X86ISA|::|U/S| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->r/w: Access the |X86ISA|::|R/W| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->pwt: Access the |X86ISA|::|PWT| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->pcd: Access the |X86ISA|::|PCD| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->pat: Access the |X86ISA|::|PAT| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->g: Access the |X86ISA|::|G| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->p: Access the |ACL2|::|P| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->d: Access the |ACL2|::|D| field of a ia32e-pte-4k-pagebits bit structure.
Ia32e-pte-4k-pagebits->a: Access the |ACL2|::|A| field of a ia32e-pte-4k-pagebits bit structure.