		Search-engine friendly clone of the ACL2 documentation.

Structures

Cr3bits

An 64-bit unsigned bitstruct type.

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

Fields

res1 — 3bits
pwt — bit
pcd — bit
res2 — 7bits
pdb — 40bits
res3 — 12bits

Source: Intel Manual, Dec-23, Vol. 3A, Section 2.5

Definitions and Theorems

Function: cr3bits-p$inline

(defun cr3bits-p$inline (x)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 64 x)
       :exec (and (natp x)
                  (< x 18446744073709551616))))

Theorem: cr3bits-p-when-unsigned-byte-p

(defthm cr3bits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 64 x)
           (cr3bits-p x)))

Theorem: unsigned-byte-p-when-cr3bits-p

(defthm unsigned-byte-p-when-cr3bits-p
  (implies (cr3bits-p x)
           (unsigned-byte-p 64 x)))

Theorem: cr3bits-p-compound-recognizer

(defthm cr3bits-p-compound-recognizer
  (implies (cr3bits-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: cr3bits-fix$inline

(defun cr3bits-fix$inline (x)
  (declare (xargs :guard (cr3bits-p x)))
  (mbe :logic (loghead 64 x) :exec x))

Theorem: cr3bits-p-of-cr3bits-fix

(defthm cr3bits-p-of-cr3bits-fix
  (b* ((fty::fixed (cr3bits-fix$inline x)))
    (cr3bits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: cr3bits-fix-when-cr3bits-p

(defthm cr3bits-fix-when-cr3bits-p
  (implies (cr3bits-p x)
           (equal (cr3bits-fix x) x)))

Function: cr3bits-equiv$inline

(defun cr3bits-equiv$inline (x y)
  (declare (xargs :guard (and (cr3bits-p x) (cr3bits-p y))))
  (equal (cr3bits-fix x) (cr3bits-fix y)))

Theorem: cr3bits-equiv-is-an-equivalence

(defthm cr3bits-equiv-is-an-equivalence
  (and (booleanp (cr3bits-equiv x y))
       (cr3bits-equiv x x)
       (implies (cr3bits-equiv x y)
                (cr3bits-equiv y x))
       (implies (and (cr3bits-equiv x y)
                     (cr3bits-equiv y z))
                (cr3bits-equiv x z)))
  :rule-classes (:equivalence))

Theorem: cr3bits-equiv-implies-equal-cr3bits-fix-1

(defthm cr3bits-equiv-implies-equal-cr3bits-fix-1
  (implies (cr3bits-equiv x x-equiv)
           (equal (cr3bits-fix x)
                  (cr3bits-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: cr3bits-fix-under-cr3bits-equiv

(defthm cr3bits-fix-under-cr3bits-equiv
  (cr3bits-equiv (cr3bits-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: cr3bits$inline

(defun cr3bits$inline (res1 pwt pcd res2 pdb res3)
 (declare (xargs :guard (and (3bits-p res1)
                             (bitp pwt)
                             (bitp pcd)
                             (7bits-p res2)
                             (40bits-p pdb)
                             (12bits-p res3))))
 (b* ((res1 (mbe :logic (3bits-fix res1)
                 :exec res1))
      (pwt (mbe :logic (bfix pwt) :exec pwt))
      (pcd (mbe :logic (bfix pcd) :exec pcd))
      (res2 (mbe :logic (7bits-fix res2)
                 :exec res2))
      (pdb (mbe :logic (40bits-fix pdb) :exec pdb))
      (res3 (mbe :logic (12bits-fix res3)
                 :exec res3)))
   (logapp 3 res1
           (logapp 1 pwt
                   (logapp 1 pcd
                           (logapp 7 res2 (logapp 40 pdb res3)))))))

Theorem: cr3bits-p-of-cr3bits

(defthm cr3bits-p-of-cr3bits
  (b* ((cr3bits (cr3bits$inline res1 pwt pcd res2 pdb res3)))
    (cr3bits-p cr3bits))
  :rule-classes :rewrite)

Theorem: cr3bits$inline-of-3bits-fix-res1

(defthm cr3bits$inline-of-3bits-fix-res1
  (equal (cr3bits$inline (3bits-fix res1)
                         pwt pcd res2 pdb res3)
         (cr3bits$inline res1 pwt pcd res2 pdb res3)))

Theorem: cr3bits$inline-3bits-equiv-congruence-on-res1

(defthm cr3bits$inline-3bits-equiv-congruence-on-res1
 (implies (3bits-equiv res1 res1-equiv)
          (equal (cr3bits$inline res1 pwt pcd res2 pdb res3)
                 (cr3bits$inline res1-equiv pwt pcd res2 pdb res3)))
 :rule-classes :congruence)

Theorem: cr3bits$inline-of-bfix-pwt

(defthm cr3bits$inline-of-bfix-pwt
  (equal (cr3bits$inline res1 (bfix pwt)
                         pcd res2 pdb res3)
         (cr3bits$inline res1 pwt pcd res2 pdb res3)))

Theorem: cr3bits$inline-bit-equiv-congruence-on-pwt

(defthm cr3bits$inline-bit-equiv-congruence-on-pwt
 (implies (bit-equiv pwt pwt-equiv)
          (equal (cr3bits$inline res1 pwt pcd res2 pdb res3)
                 (cr3bits$inline res1 pwt-equiv pcd res2 pdb res3)))
 :rule-classes :congruence)

Theorem: cr3bits$inline-of-bfix-pcd

(defthm cr3bits$inline-of-bfix-pcd
  (equal (cr3bits$inline res1 pwt (bfix pcd)
                         res2 pdb res3)
         (cr3bits$inline res1 pwt pcd res2 pdb res3)))

Theorem: cr3bits$inline-bit-equiv-congruence-on-pcd

(defthm cr3bits$inline-bit-equiv-congruence-on-pcd
 (implies (bit-equiv pcd pcd-equiv)
          (equal (cr3bits$inline res1 pwt pcd res2 pdb res3)
                 (cr3bits$inline res1 pwt pcd-equiv res2 pdb res3)))
 :rule-classes :congruence)

Theorem: cr3bits$inline-of-7bits-fix-res2

(defthm cr3bits$inline-of-7bits-fix-res2
  (equal (cr3bits$inline res1 pwt pcd (7bits-fix res2)
                         pdb res3)
         (cr3bits$inline res1 pwt pcd res2 pdb res3)))

Theorem: cr3bits$inline-7bits-equiv-congruence-on-res2

(defthm cr3bits$inline-7bits-equiv-congruence-on-res2
 (implies (7bits-equiv res2 res2-equiv)
          (equal (cr3bits$inline res1 pwt pcd res2 pdb res3)
                 (cr3bits$inline res1 pwt pcd res2-equiv pdb res3)))
 :rule-classes :congruence)

Theorem: cr3bits$inline-of-40bits-fix-pdb

(defthm cr3bits$inline-of-40bits-fix-pdb
  (equal (cr3bits$inline res1 pwt pcd res2 (40bits-fix pdb)
                         res3)
         (cr3bits$inline res1 pwt pcd res2 pdb res3)))

Theorem: cr3bits$inline-40bits-equiv-congruence-on-pdb

(defthm cr3bits$inline-40bits-equiv-congruence-on-pdb
 (implies (40bits-equiv pdb pdb-equiv)
          (equal (cr3bits$inline res1 pwt pcd res2 pdb res3)
                 (cr3bits$inline res1 pwt pcd res2 pdb-equiv res3)))
 :rule-classes :congruence)

Theorem: cr3bits$inline-of-12bits-fix-res3

(defthm cr3bits$inline-of-12bits-fix-res3
  (equal (cr3bits$inline res1 pwt pcd res2 pdb (12bits-fix res3))
         (cr3bits$inline res1 pwt pcd res2 pdb res3)))

Theorem: cr3bits$inline-12bits-equiv-congruence-on-res3

(defthm cr3bits$inline-12bits-equiv-congruence-on-res3
 (implies (12bits-equiv res3 res3-equiv)
          (equal (cr3bits$inline res1 pwt pcd res2 pdb res3)
                 (cr3bits$inline res1 pwt pcd res2 pdb res3-equiv)))
 :rule-classes :congruence)

Function: cr3bits-equiv-under-mask$inline

(defun cr3bits-equiv-under-mask$inline (x x1 mask)
  (declare (xargs :guard (and (cr3bits-p x)
                              (cr3bits-p x1)
                              (integerp mask))))
  (fty::int-equiv-under-mask (cr3bits-fix x)
                             (cr3bits-fix x1)
                             mask))

Function: cr3bits->res1$inline

(defun cr3bits->res1$inline (x)
  (declare (xargs :guard (cr3bits-p x)))
  (mbe :logic
       (let ((x (cr3bits-fix x)))
         (part-select x :low 0 :width 3))
       :exec (the (unsigned-byte 3)
                  (logand (the (unsigned-byte 3) 7)
                          (the (unsigned-byte 64) x)))))

Theorem: 3bits-p-of-cr3bits->res1

(defthm 3bits-p-of-cr3bits->res1
  (b* ((res1 (cr3bits->res1$inline x)))
    (3bits-p res1))
  :rule-classes :rewrite)

Theorem: cr3bits->res1$inline-of-cr3bits-fix-x

(defthm cr3bits->res1$inline-of-cr3bits-fix-x
  (equal (cr3bits->res1$inline (cr3bits-fix x))
         (cr3bits->res1$inline x)))

Theorem: cr3bits->res1$inline-cr3bits-equiv-congruence-on-x

(defthm cr3bits->res1$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (cr3bits->res1$inline x)
                  (cr3bits->res1$inline x-equiv)))
  :rule-classes :congruence)

Theorem: cr3bits->res1-of-cr3bits

(defthm cr3bits->res1-of-cr3bits
  (equal (cr3bits->res1 (cr3bits res1 pwt pcd res2 pdb res3))
         (3bits-fix res1)))

Theorem: cr3bits->res1-of-write-with-mask

(defthm cr3bits->res1-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x cr3bits-equiv-under-mask)
    (cr3bits-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 7) 0))
  (equal (cr3bits->res1 x)
         (cr3bits->res1 y))))

Function: cr3bits->pwt$inline

(defun cr3bits->pwt$inline (x)
 (declare (xargs :guard (cr3bits-p x)))
 (mbe
    :logic
    (let ((x (cr3bits-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-cr3bits->pwt

(defthm bitp-of-cr3bits->pwt
  (b* ((pwt (cr3bits->pwt$inline x)))
    (bitp pwt))
  :rule-classes :rewrite)

Theorem: cr3bits->pwt$inline-of-cr3bits-fix-x

(defthm cr3bits->pwt$inline-of-cr3bits-fix-x
  (equal (cr3bits->pwt$inline (cr3bits-fix x))
         (cr3bits->pwt$inline x)))

Theorem: cr3bits->pwt$inline-cr3bits-equiv-congruence-on-x

(defthm cr3bits->pwt$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (cr3bits->pwt$inline x)
                  (cr3bits->pwt$inline x-equiv)))
  :rule-classes :congruence)

Theorem: cr3bits->pwt-of-cr3bits

(defthm cr3bits->pwt-of-cr3bits
  (equal (cr3bits->pwt (cr3bits res1 pwt pcd res2 pdb res3))
         (bfix pwt)))

Theorem: cr3bits->pwt-of-write-with-mask

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

Function: cr3bits->pcd$inline

(defun cr3bits->pcd$inline (x)
 (declare (xargs :guard (cr3bits-p x)))
 (mbe
    :logic
    (let ((x (cr3bits-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-cr3bits->pcd

(defthm bitp-of-cr3bits->pcd
  (b* ((pcd (cr3bits->pcd$inline x)))
    (bitp pcd))
  :rule-classes :rewrite)

Theorem: cr3bits->pcd$inline-of-cr3bits-fix-x

(defthm cr3bits->pcd$inline-of-cr3bits-fix-x
  (equal (cr3bits->pcd$inline (cr3bits-fix x))
         (cr3bits->pcd$inline x)))

Theorem: cr3bits->pcd$inline-cr3bits-equiv-congruence-on-x

(defthm cr3bits->pcd$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (cr3bits->pcd$inline x)
                  (cr3bits->pcd$inline x-equiv)))
  :rule-classes :congruence)

Theorem: cr3bits->pcd-of-cr3bits

(defthm cr3bits->pcd-of-cr3bits
  (equal (cr3bits->pcd (cr3bits res1 pwt pcd res2 pdb res3))
         (bfix pcd)))

Theorem: cr3bits->pcd-of-write-with-mask

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

Function: cr3bits->res2$inline

(defun cr3bits->res2$inline (x)
 (declare (xargs :guard (cr3bits-p x)))
 (mbe
    :logic
    (let ((x (cr3bits-fix x)))
      (part-select x :low 5 :width 7))
    :exec (the (unsigned-byte 7)
               (logand (the (unsigned-byte 7) 127)
                       (the (unsigned-byte 59)
                            (ash (the (unsigned-byte 64) x) -5))))))

Theorem: 7bits-p-of-cr3bits->res2

(defthm 7bits-p-of-cr3bits->res2
  (b* ((res2 (cr3bits->res2$inline x)))
    (7bits-p res2))
  :rule-classes :rewrite)

Theorem: cr3bits->res2$inline-of-cr3bits-fix-x

(defthm cr3bits->res2$inline-of-cr3bits-fix-x
  (equal (cr3bits->res2$inline (cr3bits-fix x))
         (cr3bits->res2$inline x)))

Theorem: cr3bits->res2$inline-cr3bits-equiv-congruence-on-x

(defthm cr3bits->res2$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (cr3bits->res2$inline x)
                  (cr3bits->res2$inline x-equiv)))
  :rule-classes :congruence)

Theorem: cr3bits->res2-of-cr3bits

(defthm cr3bits->res2-of-cr3bits
  (equal (cr3bits->res2 (cr3bits res1 pwt pcd res2 pdb res3))
         (7bits-fix res2)))

Theorem: cr3bits->res2-of-write-with-mask

(defthm cr3bits->res2-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x cr3bits-equiv-under-mask)
    (cr3bits-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 4064)
           0))
  (equal (cr3bits->res2 x)
         (cr3bits->res2 y))))

Function: cr3bits->pdb$inline

(defun cr3bits->pdb$inline (x)
  (declare (xargs :guard (cr3bits-p x)))
  (mbe :logic
       (let ((x (cr3bits-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-cr3bits->pdb

(defthm 40bits-p-of-cr3bits->pdb
  (b* ((pdb (cr3bits->pdb$inline x)))
    (40bits-p pdb))
  :rule-classes :rewrite)

Theorem: cr3bits->pdb$inline-of-cr3bits-fix-x

(defthm cr3bits->pdb$inline-of-cr3bits-fix-x
  (equal (cr3bits->pdb$inline (cr3bits-fix x))
         (cr3bits->pdb$inline x)))

Theorem: cr3bits->pdb$inline-cr3bits-equiv-congruence-on-x

(defthm cr3bits->pdb$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (cr3bits->pdb$inline x)
                  (cr3bits->pdb$inline x-equiv)))
  :rule-classes :congruence)

Theorem: cr3bits->pdb-of-cr3bits

(defthm cr3bits->pdb-of-cr3bits
  (equal (cr3bits->pdb (cr3bits res1 pwt pcd res2 pdb res3))
         (40bits-fix pdb)))

Theorem: cr3bits->pdb-of-write-with-mask

(defthm cr3bits->pdb-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x cr3bits-equiv-under-mask)
    (cr3bits-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask)
                   4503599627366400)
           0))
  (equal (cr3bits->pdb x)
         (cr3bits->pdb y))))

Function: cr3bits->res3$inline

(defun cr3bits->res3$inline (x)
  (declare (xargs :guard (cr3bits-p x)))
  (mbe :logic
       (let ((x (cr3bits-fix x)))
         (part-select x :low 52 :width 12))
       :exec (the (unsigned-byte 12)
                  (logand (the (unsigned-byte 12) 4095)
                          (the (unsigned-byte 12)
                               (ash (the (unsigned-byte 64) x)
                                    -52))))))

Theorem: 12bits-p-of-cr3bits->res3

(defthm 12bits-p-of-cr3bits->res3
  (b* ((res3 (cr3bits->res3$inline x)))
    (12bits-p res3))
  :rule-classes :rewrite)

Theorem: cr3bits->res3$inline-of-cr3bits-fix-x

(defthm cr3bits->res3$inline-of-cr3bits-fix-x
  (equal (cr3bits->res3$inline (cr3bits-fix x))
         (cr3bits->res3$inline x)))

Theorem: cr3bits->res3$inline-cr3bits-equiv-congruence-on-x

(defthm cr3bits->res3$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (cr3bits->res3$inline x)
                  (cr3bits->res3$inline x-equiv)))
  :rule-classes :congruence)

Theorem: cr3bits->res3-of-cr3bits

(defthm cr3bits->res3-of-cr3bits
  (equal (cr3bits->res3 (cr3bits res1 pwt pcd res2 pdb res3))
         (12bits-fix res3)))

Theorem: cr3bits->res3-of-write-with-mask

(defthm cr3bits->res3-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x cr3bits-equiv-under-mask)
    (cr3bits-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask)
                   18442240474082181120)
           0))
  (equal (cr3bits->res3 x)
         (cr3bits->res3 y))))

Theorem: cr3bits-fix-in-terms-of-cr3bits

(defthm cr3bits-fix-in-terms-of-cr3bits
  (equal (cr3bits-fix x)
         (change-cr3bits x)))

Function: !cr3bits->res1$inline

(defun !cr3bits->res1$inline (res1 x)
  (declare (xargs :guard (and (3bits-p res1) (cr3bits-p x))))
  (mbe :logic
       (b* ((res1 (mbe :logic (3bits-fix res1)
                       :exec res1))
            (x (cr3bits-fix x)))
         (part-install res1 x :width 3 :low 0))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 4) -8)))
                          (the (unsigned-byte 3) res1)))))

Theorem: cr3bits-p-of-!cr3bits->res1

(defthm cr3bits-p-of-!cr3bits->res1
  (b* ((new-x (!cr3bits->res1$inline res1 x)))
    (cr3bits-p new-x))
  :rule-classes :rewrite)

Theorem: !cr3bits->res1$inline-of-3bits-fix-res1

(defthm !cr3bits->res1$inline-of-3bits-fix-res1
  (equal (!cr3bits->res1$inline (3bits-fix res1)
                                x)
         (!cr3bits->res1$inline res1 x)))

Theorem: !cr3bits->res1$inline-3bits-equiv-congruence-on-res1

(defthm !cr3bits->res1$inline-3bits-equiv-congruence-on-res1
  (implies (3bits-equiv res1 res1-equiv)
           (equal (!cr3bits->res1$inline res1 x)
                  (!cr3bits->res1$inline res1-equiv x)))
  :rule-classes :congruence)

Theorem: !cr3bits->res1$inline-of-cr3bits-fix-x

(defthm !cr3bits->res1$inline-of-cr3bits-fix-x
  (equal (!cr3bits->res1$inline res1 (cr3bits-fix x))
         (!cr3bits->res1$inline res1 x)))

Theorem: !cr3bits->res1$inline-cr3bits-equiv-congruence-on-x

(defthm !cr3bits->res1$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (!cr3bits->res1$inline res1 x)
                  (!cr3bits->res1$inline res1 x-equiv)))
  :rule-classes :congruence)

Theorem: !cr3bits->res1-is-cr3bits

(defthm !cr3bits->res1-is-cr3bits
  (equal (!cr3bits->res1 res1 x)
         (change-cr3bits x :res1 res1)))

Theorem: cr3bits->res1-of-!cr3bits->res1

(defthm cr3bits->res1-of-!cr3bits->res1
  (b* ((?new-x (!cr3bits->res1$inline res1 x)))
    (equal (cr3bits->res1 new-x)
           (3bits-fix res1))))

Theorem: !cr3bits->res1-equiv-under-mask

(defthm !cr3bits->res1-equiv-under-mask
  (b* ((?new-x (!cr3bits->res1$inline res1 x)))
    (cr3bits-equiv-under-mask new-x x -8)))

Function: !cr3bits->pwt$inline

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

(defthm cr3bits-p-of-!cr3bits->pwt
  (b* ((new-x (!cr3bits->pwt$inline pwt x)))
    (cr3bits-p new-x))
  :rule-classes :rewrite)

Theorem: !cr3bits->pwt$inline-of-bfix-pwt

(defthm !cr3bits->pwt$inline-of-bfix-pwt
  (equal (!cr3bits->pwt$inline (bfix pwt) x)
         (!cr3bits->pwt$inline pwt x)))

Theorem: !cr3bits->pwt$inline-bit-equiv-congruence-on-pwt

(defthm !cr3bits->pwt$inline-bit-equiv-congruence-on-pwt
  (implies (bit-equiv pwt pwt-equiv)
           (equal (!cr3bits->pwt$inline pwt x)
                  (!cr3bits->pwt$inline pwt-equiv x)))
  :rule-classes :congruence)

Theorem: !cr3bits->pwt$inline-of-cr3bits-fix-x

(defthm !cr3bits->pwt$inline-of-cr3bits-fix-x
  (equal (!cr3bits->pwt$inline pwt (cr3bits-fix x))
         (!cr3bits->pwt$inline pwt x)))

Theorem: !cr3bits->pwt$inline-cr3bits-equiv-congruence-on-x

(defthm !cr3bits->pwt$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (!cr3bits->pwt$inline pwt x)
                  (!cr3bits->pwt$inline pwt x-equiv)))
  :rule-classes :congruence)

Theorem: !cr3bits->pwt-is-cr3bits

(defthm !cr3bits->pwt-is-cr3bits
  (equal (!cr3bits->pwt pwt x)
         (change-cr3bits x :pwt pwt)))

Theorem: cr3bits->pwt-of-!cr3bits->pwt

(defthm cr3bits->pwt-of-!cr3bits->pwt
  (b* ((?new-x (!cr3bits->pwt$inline pwt x)))
    (equal (cr3bits->pwt new-x)
           (bfix pwt))))

Theorem: !cr3bits->pwt-equiv-under-mask

(defthm !cr3bits->pwt-equiv-under-mask
  (b* ((?new-x (!cr3bits->pwt$inline pwt x)))
    (cr3bits-equiv-under-mask new-x x -9)))

Function: !cr3bits->pcd$inline

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

(defthm cr3bits-p-of-!cr3bits->pcd
  (b* ((new-x (!cr3bits->pcd$inline pcd x)))
    (cr3bits-p new-x))
  :rule-classes :rewrite)

Theorem: !cr3bits->pcd$inline-of-bfix-pcd

(defthm !cr3bits->pcd$inline-of-bfix-pcd
  (equal (!cr3bits->pcd$inline (bfix pcd) x)
         (!cr3bits->pcd$inline pcd x)))

Theorem: !cr3bits->pcd$inline-bit-equiv-congruence-on-pcd

(defthm !cr3bits->pcd$inline-bit-equiv-congruence-on-pcd
  (implies (bit-equiv pcd pcd-equiv)
           (equal (!cr3bits->pcd$inline pcd x)
                  (!cr3bits->pcd$inline pcd-equiv x)))
  :rule-classes :congruence)

Theorem: !cr3bits->pcd$inline-of-cr3bits-fix-x

(defthm !cr3bits->pcd$inline-of-cr3bits-fix-x
  (equal (!cr3bits->pcd$inline pcd (cr3bits-fix x))
         (!cr3bits->pcd$inline pcd x)))

Theorem: !cr3bits->pcd$inline-cr3bits-equiv-congruence-on-x

(defthm !cr3bits->pcd$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (!cr3bits->pcd$inline pcd x)
                  (!cr3bits->pcd$inline pcd x-equiv)))
  :rule-classes :congruence)

Theorem: !cr3bits->pcd-is-cr3bits

(defthm !cr3bits->pcd-is-cr3bits
  (equal (!cr3bits->pcd pcd x)
         (change-cr3bits x :pcd pcd)))

Theorem: cr3bits->pcd-of-!cr3bits->pcd

(defthm cr3bits->pcd-of-!cr3bits->pcd
  (b* ((?new-x (!cr3bits->pcd$inline pcd x)))
    (equal (cr3bits->pcd new-x)
           (bfix pcd))))

Theorem: !cr3bits->pcd-equiv-under-mask

(defthm !cr3bits->pcd-equiv-under-mask
  (b* ((?new-x (!cr3bits->pcd$inline pcd x)))
    (cr3bits-equiv-under-mask new-x x -17)))

Function: !cr3bits->res2$inline

(defun !cr3bits->res2$inline (res2 x)
 (declare (xargs :guard (and (7bits-p res2) (cr3bits-p x))))
 (mbe :logic
      (b* ((res2 (mbe :logic (7bits-fix res2)
                      :exec res2))
           (x (cr3bits-fix x)))
        (part-install res2 x :width 7 :low 5))
      :exec (the (unsigned-byte 64)
                 (logior (the (unsigned-byte 64)
                              (logand (the (unsigned-byte 64) x)
                                      (the (signed-byte 13) -4065)))
                         (the (unsigned-byte 12)
                              (ash (the (unsigned-byte 7) res2)
                                   5))))))

Theorem: cr3bits-p-of-!cr3bits->res2

(defthm cr3bits-p-of-!cr3bits->res2
  (b* ((new-x (!cr3bits->res2$inline res2 x)))
    (cr3bits-p new-x))
  :rule-classes :rewrite)

Theorem: !cr3bits->res2$inline-of-7bits-fix-res2

(defthm !cr3bits->res2$inline-of-7bits-fix-res2
  (equal (!cr3bits->res2$inline (7bits-fix res2)
                                x)
         (!cr3bits->res2$inline res2 x)))

Theorem: !cr3bits->res2$inline-7bits-equiv-congruence-on-res2

(defthm !cr3bits->res2$inline-7bits-equiv-congruence-on-res2
  (implies (7bits-equiv res2 res2-equiv)
           (equal (!cr3bits->res2$inline res2 x)
                  (!cr3bits->res2$inline res2-equiv x)))
  :rule-classes :congruence)

Theorem: !cr3bits->res2$inline-of-cr3bits-fix-x

(defthm !cr3bits->res2$inline-of-cr3bits-fix-x
  (equal (!cr3bits->res2$inline res2 (cr3bits-fix x))
         (!cr3bits->res2$inline res2 x)))

Theorem: !cr3bits->res2$inline-cr3bits-equiv-congruence-on-x

(defthm !cr3bits->res2$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (!cr3bits->res2$inline res2 x)
                  (!cr3bits->res2$inline res2 x-equiv)))
  :rule-classes :congruence)

Theorem: !cr3bits->res2-is-cr3bits

(defthm !cr3bits->res2-is-cr3bits
  (equal (!cr3bits->res2 res2 x)
         (change-cr3bits x :res2 res2)))

Theorem: cr3bits->res2-of-!cr3bits->res2

(defthm cr3bits->res2-of-!cr3bits->res2
  (b* ((?new-x (!cr3bits->res2$inline res2 x)))
    (equal (cr3bits->res2 new-x)
           (7bits-fix res2))))

Theorem: !cr3bits->res2-equiv-under-mask

(defthm !cr3bits->res2-equiv-under-mask
  (b* ((?new-x (!cr3bits->res2$inline res2 x)))
    (cr3bits-equiv-under-mask new-x x -4065)))

Function: !cr3bits->pdb$inline

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

Theorem: cr3bits-p-of-!cr3bits->pdb

(defthm cr3bits-p-of-!cr3bits->pdb
  (b* ((new-x (!cr3bits->pdb$inline pdb x)))
    (cr3bits-p new-x))
  :rule-classes :rewrite)

Theorem: !cr3bits->pdb$inline-of-40bits-fix-pdb

(defthm !cr3bits->pdb$inline-of-40bits-fix-pdb
  (equal (!cr3bits->pdb$inline (40bits-fix pdb)
                               x)
         (!cr3bits->pdb$inline pdb x)))

Theorem: !cr3bits->pdb$inline-40bits-equiv-congruence-on-pdb

(defthm !cr3bits->pdb$inline-40bits-equiv-congruence-on-pdb
  (implies (40bits-equiv pdb pdb-equiv)
           (equal (!cr3bits->pdb$inline pdb x)
                  (!cr3bits->pdb$inline pdb-equiv x)))
  :rule-classes :congruence)

Theorem: !cr3bits->pdb$inline-of-cr3bits-fix-x

(defthm !cr3bits->pdb$inline-of-cr3bits-fix-x
  (equal (!cr3bits->pdb$inline pdb (cr3bits-fix x))
         (!cr3bits->pdb$inline pdb x)))

Theorem: !cr3bits->pdb$inline-cr3bits-equiv-congruence-on-x

(defthm !cr3bits->pdb$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (!cr3bits->pdb$inline pdb x)
                  (!cr3bits->pdb$inline pdb x-equiv)))
  :rule-classes :congruence)

Theorem: !cr3bits->pdb-is-cr3bits

(defthm !cr3bits->pdb-is-cr3bits
  (equal (!cr3bits->pdb pdb x)
         (change-cr3bits x :pdb pdb)))

Theorem: cr3bits->pdb-of-!cr3bits->pdb

(defthm cr3bits->pdb-of-!cr3bits->pdb
  (b* ((?new-x (!cr3bits->pdb$inline pdb x)))
    (equal (cr3bits->pdb new-x)
           (40bits-fix pdb))))

Theorem: !cr3bits->pdb-equiv-under-mask

(defthm !cr3bits->pdb-equiv-under-mask
  (b* ((?new-x (!cr3bits->pdb$inline pdb x)))
    (cr3bits-equiv-under-mask new-x x -4503599627366401)))

Function: !cr3bits->res3$inline

(defun !cr3bits->res3$inline (res3 x)
  (declare (xargs :guard (and (12bits-p res3) (cr3bits-p x))))
  (mbe :logic
       (b* ((res3 (mbe :logic (12bits-fix res3)
                       :exec res3))
            (x (cr3bits-fix x)))
         (part-install res3 x :width 12 :low 52))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 65)
                                            -18442240474082181121)))
                          (the (unsigned-byte 64)
                               (ash (the (unsigned-byte 12) res3)
                                    52))))))

Theorem: cr3bits-p-of-!cr3bits->res3

(defthm cr3bits-p-of-!cr3bits->res3
  (b* ((new-x (!cr3bits->res3$inline res3 x)))
    (cr3bits-p new-x))
  :rule-classes :rewrite)

Theorem: !cr3bits->res3$inline-of-12bits-fix-res3

(defthm !cr3bits->res3$inline-of-12bits-fix-res3
  (equal (!cr3bits->res3$inline (12bits-fix res3)
                                x)
         (!cr3bits->res3$inline res3 x)))

Theorem: !cr3bits->res3$inline-12bits-equiv-congruence-on-res3

(defthm !cr3bits->res3$inline-12bits-equiv-congruence-on-res3
  (implies (12bits-equiv res3 res3-equiv)
           (equal (!cr3bits->res3$inline res3 x)
                  (!cr3bits->res3$inline res3-equiv x)))
  :rule-classes :congruence)

Theorem: !cr3bits->res3$inline-of-cr3bits-fix-x

(defthm !cr3bits->res3$inline-of-cr3bits-fix-x
  (equal (!cr3bits->res3$inline res3 (cr3bits-fix x))
         (!cr3bits->res3$inline res3 x)))

Theorem: !cr3bits->res3$inline-cr3bits-equiv-congruence-on-x

(defthm !cr3bits->res3$inline-cr3bits-equiv-congruence-on-x
  (implies (cr3bits-equiv x x-equiv)
           (equal (!cr3bits->res3$inline res3 x)
                  (!cr3bits->res3$inline res3 x-equiv)))
  :rule-classes :congruence)

Theorem: !cr3bits->res3-is-cr3bits

(defthm !cr3bits->res3-is-cr3bits
  (equal (!cr3bits->res3 res3 x)
         (change-cr3bits x :res3 res3)))

Theorem: cr3bits->res3-of-!cr3bits->res3

(defthm cr3bits->res3-of-!cr3bits->res3
  (b* ((?new-x (!cr3bits->res3$inline res3 x)))
    (equal (cr3bits->res3 new-x)
           (12bits-fix res3))))

Theorem: !cr3bits->res3-equiv-under-mask

(defthm !cr3bits->res3-equiv-under-mask
  (b* ((?new-x (!cr3bits->res3$inline res3 x)))
    (cr3bits-equiv-under-mask new-x x 4503599627370495)))

Function: cr3bits-debug$inline

(defun cr3bits-debug$inline (x)
 (declare (xargs :guard (cr3bits-p x)))
 (b* (((cr3bits x)))
  (cons
       (cons 'res1 x.res1)
       (cons (cons 'pwt x.pwt)
             (cons (cons 'pcd x.pcd)
                   (cons (cons 'res2 x.res2)
                         (cons (cons 'pdb x.pdb)
                               (cons (cons 'res3 x.res3) nil))))))))

Subtopics

!cr3bits->res3: Update the |X86ISA|::|RES3| field of a cr3bits bit structure.
!cr3bits->res2: Update the |X86ISA|::|RES2| field of a cr3bits bit structure.
!cr3bits->pdb: Update the |X86ISA|::|PDB| field of a cr3bits bit structure.
!cr3bits->res1: Update the |X86ISA|::|RES1| field of a cr3bits bit structure.
Cr3bits-p: Recognizer for cr3bits bit structures.
!cr3bits->pwt: Update the |X86ISA|::|PWT| field of a cr3bits bit structure.
!cr3bits->pcd: Update the |X86ISA|::|PCD| field of a cr3bits bit structure.
Cr3bits->res3: Access the |X86ISA|::|RES3| field of a cr3bits bit structure.
Cr3bits->pdb: Access the |X86ISA|::|PDB| field of a cr3bits bit structure.
Cr3bits-fix: Fixing function for cr3bits bit structures.
Cr3bits->res2: Access the |X86ISA|::|RES2| field of a cr3bits bit structure.
Cr3bits->res1: Access the |X86ISA|::|RES1| field of a cr3bits bit structure.
Cr3bits->pwt: Access the |X86ISA|::|PWT| field of a cr3bits bit structure.
Cr3bits->pcd: Access the |X86ISA|::|PCD| field of a cr3bits bit structure.