• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
        • Tlb-key
          • !tlb-key->implicit-supervisor-access
          • Tlb-key-fast
          • Tlb-key-p
          • !tlb-key->r-w-x
          • !tlb-key->vpn
          • !tlb-key->smep
          • !tlb-key->smap
          • !tlb-key->cpl
          • !tlb-key->nxe
          • Tlb-key->implicit-supervisor-access
          • !tlb-key->wp
          • !tlb-key->ac
          • Tlb-key->vpn
          • Tlb-key->smep
          • Tlb-key->smap
          • Tlb-key->r-w-x
          • Tlb-key->cpl
          • Tlb-key-fix
          • Tlb-key->wp
          • Tlb-key->nxe
          • Tlb-key->ac
          • Good-tlb-key-p
        • Tlbp
        • Tlb-entryp
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Tlb

Tlb-key

A key for our TLB implementation.

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

Fields

wp — bit

the wp field of cr0

smep — bit

the smep field of cr4

smap — bit

the smap field of cr4

ac — bit

the ac field of rflags

nxe — bit

the nxe field of the IA32E_EFER MSR

implicit-supervisor-access — bit

0 or 1, corresponding to whether the the implicit-supervisor-access field of the x86 state is nil or t

r-w-x — 2bits

0, 1, or 2, which correspond to read, write, and execute translations respectively. 3 is invalid.

cpl — 2bits

the current privilege level when the access was made - except when implicit-supervisor-access is t, in which case it is 0.

vpn — 36bits

the virtual page number of the 4k page the corresponds to

TLB keys serve as keys into the tlb field of the x86 stobj.

Definitions and Theorems

Function: tlb-key-p

(defun tlb-key-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'tlb-key-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 46 x)
         :exec (and (natp x) (< x 70368744177664)))))

Theorem: tlb-key-p-when-unsigned-byte-p

(defthm tlb-key-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 46 x)
           (tlb-key-p x)))

Theorem: unsigned-byte-p-when-tlb-key-p

(defthm unsigned-byte-p-when-tlb-key-p
  (implies (tlb-key-p x)
           (unsigned-byte-p 46 x)))

Theorem: tlb-key-p-compound-recognizer

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

Function: tlb-key-fix

(defun tlb-key-fix (x)
  (declare (xargs :guard (tlb-key-p x)))
  (let ((__function__ 'tlb-key-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 46 x) :exec x)))

Theorem: tlb-key-p-of-tlb-key-fix

(defthm tlb-key-p-of-tlb-key-fix
  (b* ((fty::fixed (tlb-key-fix x)))
    (tlb-key-p fty::fixed))
  :rule-classes :rewrite)

Theorem: tlb-key-fix-when-tlb-key-p

(defthm tlb-key-fix-when-tlb-key-p
  (implies (tlb-key-p x)
           (equal (tlb-key-fix x) x)))

Function: tlb-key-equiv$inline

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

Theorem: tlb-key-equiv-is-an-equivalence

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

Theorem: tlb-key-equiv-implies-equal-tlb-key-fix-1

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

Theorem: tlb-key-fix-under-tlb-key-equiv

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

Function: tlb-key

(defun tlb-key (wp smep
                   smap ac nxe implicit-supervisor-access
                   r-w-x cpl vpn)
 (declare (xargs :guard (and (bitp wp)
                             (bitp smep)
                             (bitp smap)
                             (bitp ac)
                             (bitp nxe)
                             (bitp implicit-supervisor-access)
                             (2bits-p r-w-x)
                             (2bits-p cpl)
                             (36bits-p vpn))))
 (let ((__function__ 'tlb-key))
  (declare (ignorable __function__))
  (b* ((wp (mbe :logic (bfix wp) :exec wp))
       (smep (mbe :logic (bfix smep) :exec smep))
       (smap (mbe :logic (bfix smap) :exec smap))
       (ac (mbe :logic (bfix ac) :exec ac))
       (nxe (mbe :logic (bfix nxe) :exec nxe))
       (implicit-supervisor-access
            (mbe :logic (bfix implicit-supervisor-access)
                 :exec implicit-supervisor-access))
       (r-w-x (mbe :logic (2bits-fix r-w-x)
                   :exec r-w-x))
       (cpl (mbe :logic (2bits-fix cpl) :exec cpl))
       (vpn (mbe :logic (36bits-fix vpn)
                 :exec vpn)))
   (logapp
    1 wp
    (logapp
     1 smep
     (logapp
      1 smap
      (logapp
        1 ac
        (logapp 1 nxe
                (logapp 1 implicit-supervisor-access
                        (logapp 2 r-w-x (logapp 2 cpl vpn)))))))))))

Theorem: tlb-key-p-of-tlb-key

(defthm tlb-key-p-of-tlb-key
  (b* ((tlb-key (tlb-key wp smep
                         smap ac nxe implicit-supervisor-access
                         r-w-x cpl vpn)))
    (tlb-key-p tlb-key))
  :rule-classes :rewrite)

Theorem: tlb-key-of-bfix-wp

(defthm tlb-key-of-bfix-wp
  (equal (tlb-key (bfix wp)
                  smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-bit-equiv-congruence-on-wp

(defthm tlb-key-bit-equiv-congruence-on-wp
  (implies (bit-equiv wp wp-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp-equiv smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-bfix-smep

(defthm tlb-key-of-bfix-smep
  (equal (tlb-key wp (bfix smep)
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-bit-equiv-congruence-on-smep

(defthm tlb-key-bit-equiv-congruence-on-smep
  (implies (bit-equiv smep smep-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep-equiv
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-bfix-smap

(defthm tlb-key-of-bfix-smap
  (equal (tlb-key wp smep (bfix smap)
                  ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-bit-equiv-congruence-on-smap

(defthm tlb-key-bit-equiv-congruence-on-smap
  (implies (bit-equiv smap smap-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep smap-equiv
                           ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-bfix-ac

(defthm tlb-key-of-bfix-ac
  (equal (tlb-key wp smep smap (bfix ac)
                  nxe implicit-supervisor-access
                  r-w-x cpl vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-bit-equiv-congruence-on-ac

(defthm tlb-key-bit-equiv-congruence-on-ac
  (implies (bit-equiv ac ac-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep smap
                           ac-equiv nxe implicit-supervisor-access
                           r-w-x cpl vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-bfix-nxe

(defthm tlb-key-of-bfix-nxe
  (equal (tlb-key wp smep smap ac (bfix nxe)
                  implicit-supervisor-access
                  r-w-x cpl vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-bit-equiv-congruence-on-nxe

(defthm tlb-key-bit-equiv-congruence-on-nxe
  (implies (bit-equiv nxe nxe-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep smap
                           ac nxe-equiv implicit-supervisor-access
                           r-w-x cpl vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-bfix-implicit-supervisor-access

(defthm tlb-key-of-bfix-implicit-supervisor-access
  (equal (tlb-key wp smep smap
                  ac nxe (bfix implicit-supervisor-access)
                  r-w-x cpl vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-bit-equiv-congruence-on-implicit-supervisor-access

(defthm tlb-key-bit-equiv-congruence-on-implicit-supervisor-access
  (implies (bit-equiv implicit-supervisor-access
                      implicit-supervisor-access-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep smap
                           ac nxe implicit-supervisor-access-equiv
                           r-w-x cpl vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-2bits-fix-r-w-x

(defthm tlb-key-of-2bits-fix-r-w-x
  (equal (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  (2bits-fix r-w-x)
                  cpl vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-2bits-equiv-congruence-on-r-w-x

(defthm tlb-key-2bits-equiv-congruence-on-r-w-x
  (implies (2bits-equiv r-w-x r-w-x-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x-equiv cpl vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-2bits-fix-cpl

(defthm tlb-key-of-2bits-fix-cpl
  (equal (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x (2bits-fix cpl)
                  vpn)
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-2bits-equiv-congruence-on-cpl

(defthm tlb-key-2bits-equiv-congruence-on-cpl
  (implies (2bits-equiv cpl cpl-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl-equiv vpn)))
  :rule-classes :congruence)

Theorem: tlb-key-of-36bits-fix-vpn

(defthm tlb-key-of-36bits-fix-vpn
  (equal (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl (36bits-fix vpn))
         (tlb-key wp smep
                  smap ac nxe implicit-supervisor-access
                  r-w-x cpl vpn)))

Theorem: tlb-key-36bits-equiv-congruence-on-vpn

(defthm tlb-key-36bits-equiv-congruence-on-vpn
  (implies (36bits-equiv vpn vpn-equiv)
           (equal (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn)
                  (tlb-key wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl vpn-equiv)))
  :rule-classes :congruence)

Function: tlb-key-equiv-under-mask

(defun tlb-key-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (tlb-key-p x)
                              (tlb-key-p x1)
                              (integerp mask))))
  (let ((__function__ 'tlb-key-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (tlb-key-fix x)
                               (tlb-key-fix x1)
                               mask)))

Function: tlb-key->wp$inline

(defun tlb-key->wp$inline (x)
  (declare (xargs :guard (tlb-key-p x)))
  (mbe :logic
       (let ((x (tlb-key-fix x)))
         (part-select x :low 0 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 46) x)))))

Theorem: bitp-of-tlb-key->wp

(defthm bitp-of-tlb-key->wp
  (b* ((wp (tlb-key->wp$inline x)))
    (bitp wp))
  :rule-classes :rewrite)

Theorem: tlb-key->wp$inline-of-tlb-key-fix-x

(defthm tlb-key->wp$inline-of-tlb-key-fix-x
  (equal (tlb-key->wp$inline (tlb-key-fix x))
         (tlb-key->wp$inline x)))

Theorem: tlb-key->wp$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->wp$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->wp$inline x)
                  (tlb-key->wp$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->wp-of-tlb-key

(defthm tlb-key->wp-of-tlb-key
 (equal (tlb-key->wp (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
        (bfix wp)))

Theorem: tlb-key->wp-of-write-with-mask

(defthm tlb-key->wp-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x tlb-key-equiv-under-mask)
    (tlb-key-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 1) 0))
  (equal (tlb-key->wp x)
         (tlb-key->wp y))))

Function: tlb-key->smep$inline

(defun tlb-key->smep$inline (x)
 (declare (xargs :guard (tlb-key-p x)))
 (mbe
    :logic
    (let ((x (tlb-key-fix x)))
      (part-select x :low 1 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 45)
                            (ash (the (unsigned-byte 46) x) -1))))))

Theorem: bitp-of-tlb-key->smep

(defthm bitp-of-tlb-key->smep
  (b* ((smep (tlb-key->smep$inline x)))
    (bitp smep))
  :rule-classes :rewrite)

Theorem: tlb-key->smep$inline-of-tlb-key-fix-x

(defthm tlb-key->smep$inline-of-tlb-key-fix-x
  (equal (tlb-key->smep$inline (tlb-key-fix x))
         (tlb-key->smep$inline x)))

Theorem: tlb-key->smep$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->smep$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->smep$inline x)
                  (tlb-key->smep$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->smep-of-tlb-key

(defthm tlb-key->smep-of-tlb-key
 (equal
      (tlb-key->smep (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
      (bfix smep)))

Theorem: tlb-key->smep-of-write-with-mask

(defthm tlb-key->smep-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x tlb-key-equiv-under-mask)
    (tlb-key-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 2) 0))
  (equal (tlb-key->smep x)
         (tlb-key->smep y))))

Function: tlb-key->smap$inline

(defun tlb-key->smap$inline (x)
 (declare (xargs :guard (tlb-key-p x)))
 (mbe
    :logic
    (let ((x (tlb-key-fix x)))
      (part-select x :low 2 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 44)
                            (ash (the (unsigned-byte 46) x) -2))))))

Theorem: bitp-of-tlb-key->smap

(defthm bitp-of-tlb-key->smap
  (b* ((smap (tlb-key->smap$inline x)))
    (bitp smap))
  :rule-classes :rewrite)

Theorem: tlb-key->smap$inline-of-tlb-key-fix-x

(defthm tlb-key->smap$inline-of-tlb-key-fix-x
  (equal (tlb-key->smap$inline (tlb-key-fix x))
         (tlb-key->smap$inline x)))

Theorem: tlb-key->smap$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->smap$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->smap$inline x)
                  (tlb-key->smap$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->smap-of-tlb-key

(defthm tlb-key->smap-of-tlb-key
 (equal
      (tlb-key->smap (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
      (bfix smap)))

Theorem: tlb-key->smap-of-write-with-mask

(defthm tlb-key->smap-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x tlb-key-equiv-under-mask)
    (tlb-key-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 4) 0))
  (equal (tlb-key->smap x)
         (tlb-key->smap y))))

Function: tlb-key->ac$inline

(defun tlb-key->ac$inline (x)
 (declare (xargs :guard (tlb-key-p x)))
 (mbe
    :logic
    (let ((x (tlb-key-fix x)))
      (part-select x :low 3 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 43)
                            (ash (the (unsigned-byte 46) x) -3))))))

Theorem: bitp-of-tlb-key->ac

(defthm bitp-of-tlb-key->ac
  (b* ((ac (tlb-key->ac$inline x)))
    (bitp ac))
  :rule-classes :rewrite)

Theorem: tlb-key->ac$inline-of-tlb-key-fix-x

(defthm tlb-key->ac$inline-of-tlb-key-fix-x
  (equal (tlb-key->ac$inline (tlb-key-fix x))
         (tlb-key->ac$inline x)))

Theorem: tlb-key->ac$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->ac$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->ac$inline x)
                  (tlb-key->ac$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->ac-of-tlb-key

(defthm tlb-key->ac-of-tlb-key
 (equal (tlb-key->ac (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
        (bfix ac)))

Theorem: tlb-key->ac-of-write-with-mask

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

Function: tlb-key->nxe$inline

(defun tlb-key->nxe$inline (x)
 (declare (xargs :guard (tlb-key-p x)))
 (mbe
    :logic
    (let ((x (tlb-key-fix x)))
      (part-select x :low 4 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 42)
                            (ash (the (unsigned-byte 46) x) -4))))))

Theorem: bitp-of-tlb-key->nxe

(defthm bitp-of-tlb-key->nxe
  (b* ((nxe (tlb-key->nxe$inline x)))
    (bitp nxe))
  :rule-classes :rewrite)

Theorem: tlb-key->nxe$inline-of-tlb-key-fix-x

(defthm tlb-key->nxe$inline-of-tlb-key-fix-x
  (equal (tlb-key->nxe$inline (tlb-key-fix x))
         (tlb-key->nxe$inline x)))

Theorem: tlb-key->nxe$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->nxe$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->nxe$inline x)
                  (tlb-key->nxe$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->nxe-of-tlb-key

(defthm tlb-key->nxe-of-tlb-key
  (equal
       (tlb-key->nxe (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
       (bfix nxe)))

Theorem: tlb-key->nxe-of-write-with-mask

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

Function: tlb-key->implicit-supervisor-access$inline

(defun tlb-key->implicit-supervisor-access$inline (x)
 (declare (xargs :guard (tlb-key-p x)))
 (mbe
    :logic
    (let ((x (tlb-key-fix x)))
      (part-select x :low 5 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 41)
                            (ash (the (unsigned-byte 46) x) -5))))))

Theorem: bitp-of-tlb-key->implicit-supervisor-access

(defthm bitp-of-tlb-key->implicit-supervisor-access
  (b* ((implicit-supervisor-access
            (tlb-key->implicit-supervisor-access$inline x)))
    (bitp implicit-supervisor-access))
  :rule-classes :rewrite)

Theorem: tlb-key->implicit-supervisor-access$inline-of-tlb-key-fix-x

(defthm tlb-key->implicit-supervisor-access$inline-of-tlb-key-fix-x
 (equal (tlb-key->implicit-supervisor-access$inline (tlb-key-fix x))
        (tlb-key->implicit-supervisor-access$inline x)))

Theorem: tlb-key->implicit-supervisor-access$inline-tlb-key-equiv-congruence-on-x

(defthm
 tlb-key->implicit-supervisor-access$inline-tlb-key-equiv-congruence-on-x
 (implies
      (tlb-key-equiv x x-equiv)
      (equal (tlb-key->implicit-supervisor-access$inline x)
             (tlb-key->implicit-supervisor-access$inline x-equiv)))
 :rule-classes :congruence)

Theorem: tlb-key->implicit-supervisor-access-of-tlb-key

(defthm tlb-key->implicit-supervisor-access-of-tlb-key
  (equal (tlb-key->implicit-supervisor-access
              (tlb-key wp smep
                       smap ac nxe implicit-supervisor-access
                       r-w-x cpl vpn))
         (bfix implicit-supervisor-access)))

Theorem: tlb-key->implicit-supervisor-access-of-write-with-mask

(defthm tlb-key->implicit-supervisor-access-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x tlb-key-equiv-under-mask)
    (tlb-key-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 32)
           0))
  (equal (tlb-key->implicit-supervisor-access x)
         (tlb-key->implicit-supervisor-access y))))

Function: tlb-key->r-w-x$inline

(defun tlb-key->r-w-x$inline (x)
 (declare (xargs :guard (tlb-key-p x)))
 (mbe
    :logic
    (let ((x (tlb-key-fix x)))
      (part-select x :low 6 :width 2))
    :exec (the (unsigned-byte 2)
               (logand (the (unsigned-byte 2) 3)
                       (the (unsigned-byte 40)
                            (ash (the (unsigned-byte 46) x) -6))))))

Theorem: 2bits-p-of-tlb-key->r-w-x

(defthm 2bits-p-of-tlb-key->r-w-x
  (b* ((r-w-x (tlb-key->r-w-x$inline x)))
    (2bits-p r-w-x))
  :rule-classes :rewrite)

Theorem: tlb-key->r-w-x$inline-of-tlb-key-fix-x

(defthm tlb-key->r-w-x$inline-of-tlb-key-fix-x
  (equal (tlb-key->r-w-x$inline (tlb-key-fix x))
         (tlb-key->r-w-x$inline x)))

Theorem: tlb-key->r-w-x$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->r-w-x$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->r-w-x$inline x)
                  (tlb-key->r-w-x$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->r-w-x-of-tlb-key

(defthm tlb-key->r-w-x-of-tlb-key
 (equal
     (tlb-key->r-w-x (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
     (2bits-fix r-w-x)))

Theorem: tlb-key->r-w-x-of-write-with-mask

(defthm tlb-key->r-w-x-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x tlb-key-equiv-under-mask)
    (tlb-key-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 192)
           0))
  (equal (tlb-key->r-w-x x)
         (tlb-key->r-w-x y))))

Function: tlb-key->cpl$inline

(defun tlb-key->cpl$inline (x)
 (declare (xargs :guard (tlb-key-p x)))
 (mbe
    :logic
    (let ((x (tlb-key-fix x)))
      (part-select x :low 8 :width 2))
    :exec (the (unsigned-byte 2)
               (logand (the (unsigned-byte 2) 3)
                       (the (unsigned-byte 38)
                            (ash (the (unsigned-byte 46) x) -8))))))

Theorem: 2bits-p-of-tlb-key->cpl

(defthm 2bits-p-of-tlb-key->cpl
  (b* ((cpl (tlb-key->cpl$inline x)))
    (2bits-p cpl))
  :rule-classes :rewrite)

Theorem: tlb-key->cpl$inline-of-tlb-key-fix-x

(defthm tlb-key->cpl$inline-of-tlb-key-fix-x
  (equal (tlb-key->cpl$inline (tlb-key-fix x))
         (tlb-key->cpl$inline x)))

Theorem: tlb-key->cpl$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->cpl$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->cpl$inline x)
                  (tlb-key->cpl$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->cpl-of-tlb-key

(defthm tlb-key->cpl-of-tlb-key
  (equal
       (tlb-key->cpl (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
       (2bits-fix cpl)))

Theorem: tlb-key->cpl-of-write-with-mask

(defthm tlb-key->cpl-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x tlb-key-equiv-under-mask)
    (tlb-key-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 768)
           0))
  (equal (tlb-key->cpl x)
         (tlb-key->cpl y))))

Function: tlb-key->vpn$inline

(defun tlb-key->vpn$inline (x)
  (declare (xargs :guard (tlb-key-p x)))
  (mbe :logic
       (let ((x (tlb-key-fix x)))
         (part-select x :low 10 :width 36))
       :exec (the (unsigned-byte 36)
                  (logand (the (unsigned-byte 36) 68719476735)
                          (the (unsigned-byte 36)
                               (ash (the (unsigned-byte 46) x)
                                    -10))))))

Theorem: 36bits-p-of-tlb-key->vpn

(defthm 36bits-p-of-tlb-key->vpn
  (b* ((vpn (tlb-key->vpn$inline x)))
    (36bits-p vpn))
  :rule-classes :rewrite)

Theorem: tlb-key->vpn$inline-of-tlb-key-fix-x

(defthm tlb-key->vpn$inline-of-tlb-key-fix-x
  (equal (tlb-key->vpn$inline (tlb-key-fix x))
         (tlb-key->vpn$inline x)))

Theorem: tlb-key->vpn$inline-tlb-key-equiv-congruence-on-x

(defthm tlb-key->vpn$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (tlb-key->vpn$inline x)
                  (tlb-key->vpn$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tlb-key->vpn-of-tlb-key

(defthm tlb-key->vpn-of-tlb-key
  (equal
       (tlb-key->vpn (tlb-key wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl vpn))
       (36bits-fix vpn)))

Theorem: tlb-key->vpn-of-write-with-mask

(defthm tlb-key->vpn-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x tlb-key-equiv-under-mask)
    (tlb-key-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask)
                   70368744176640)
           0))
  (equal (tlb-key->vpn x)
         (tlb-key->vpn y))))

Theorem: tlb-key-fix-in-terms-of-tlb-key

(defthm tlb-key-fix-in-terms-of-tlb-key
  (equal (tlb-key-fix x)
         (change-tlb-key x)))

Function: !tlb-key->wp$inline

(defun !tlb-key->wp$inline (wp x)
  (declare (xargs :guard (and (bitp wp) (tlb-key-p x))))
  (mbe :logic
       (b* ((wp (mbe :logic (bfix wp) :exec wp))
            (x (tlb-key-fix x)))
         (part-install wp x :width 1 :low 0))
       :exec (the (unsigned-byte 46)
                  (logior (the (unsigned-byte 46)
                               (logand (the (unsigned-byte 46) x)
                                       (the (signed-byte 2) -2)))
                          (the (unsigned-byte 1) wp)))))

Theorem: tlb-key-p-of-!tlb-key->wp

(defthm tlb-key-p-of-!tlb-key->wp
  (b* ((new-x (!tlb-key->wp$inline wp x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->wp$inline-of-bfix-wp

(defthm !tlb-key->wp$inline-of-bfix-wp
  (equal (!tlb-key->wp$inline (bfix wp) x)
         (!tlb-key->wp$inline wp x)))

Theorem: !tlb-key->wp$inline-bit-equiv-congruence-on-wp

(defthm !tlb-key->wp$inline-bit-equiv-congruence-on-wp
  (implies (bit-equiv wp wp-equiv)
           (equal (!tlb-key->wp$inline wp x)
                  (!tlb-key->wp$inline wp-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->wp$inline-of-tlb-key-fix-x

(defthm !tlb-key->wp$inline-of-tlb-key-fix-x
  (equal (!tlb-key->wp$inline wp (tlb-key-fix x))
         (!tlb-key->wp$inline wp x)))

Theorem: !tlb-key->wp$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->wp$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->wp$inline wp x)
                  (!tlb-key->wp$inline wp x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->wp-is-tlb-key

(defthm !tlb-key->wp-is-tlb-key
  (equal (!tlb-key->wp wp x)
         (change-tlb-key x :wp wp)))

Theorem: tlb-key->wp-of-!tlb-key->wp

(defthm tlb-key->wp-of-!tlb-key->wp
  (b* ((?new-x (!tlb-key->wp$inline wp x)))
    (equal (tlb-key->wp new-x) (bfix wp))))

Theorem: !tlb-key->wp-equiv-under-mask

(defthm !tlb-key->wp-equiv-under-mask
  (b* ((?new-x (!tlb-key->wp$inline wp x)))
    (tlb-key-equiv-under-mask new-x x -2)))

Function: !tlb-key->smep$inline

(defun !tlb-key->smep$inline (smep x)
  (declare (xargs :guard (and (bitp smep) (tlb-key-p x))))
  (mbe :logic
       (b* ((smep (mbe :logic (bfix smep) :exec smep))
            (x (tlb-key-fix x)))
         (part-install smep x :width 1 :low 1))
       :exec (the (unsigned-byte 46)
                  (logior (the (unsigned-byte 46)
                               (logand (the (unsigned-byte 46) x)
                                       (the (signed-byte 3) -3)))
                          (the (unsigned-byte 2)
                               (ash (the (unsigned-byte 1) smep)
                                    1))))))

Theorem: tlb-key-p-of-!tlb-key->smep

(defthm tlb-key-p-of-!tlb-key->smep
  (b* ((new-x (!tlb-key->smep$inline smep x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->smep$inline-of-bfix-smep

(defthm !tlb-key->smep$inline-of-bfix-smep
  (equal (!tlb-key->smep$inline (bfix smep) x)
         (!tlb-key->smep$inline smep x)))

Theorem: !tlb-key->smep$inline-bit-equiv-congruence-on-smep

(defthm !tlb-key->smep$inline-bit-equiv-congruence-on-smep
  (implies (bit-equiv smep smep-equiv)
           (equal (!tlb-key->smep$inline smep x)
                  (!tlb-key->smep$inline smep-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->smep$inline-of-tlb-key-fix-x

(defthm !tlb-key->smep$inline-of-tlb-key-fix-x
  (equal (!tlb-key->smep$inline smep (tlb-key-fix x))
         (!tlb-key->smep$inline smep x)))

Theorem: !tlb-key->smep$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->smep$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->smep$inline smep x)
                  (!tlb-key->smep$inline smep x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->smep-is-tlb-key

(defthm !tlb-key->smep-is-tlb-key
  (equal (!tlb-key->smep smep x)
         (change-tlb-key x :smep smep)))

Theorem: tlb-key->smep-of-!tlb-key->smep

(defthm tlb-key->smep-of-!tlb-key->smep
  (b* ((?new-x (!tlb-key->smep$inline smep x)))
    (equal (tlb-key->smep new-x)
           (bfix smep))))

Theorem: !tlb-key->smep-equiv-under-mask

(defthm !tlb-key->smep-equiv-under-mask
  (b* ((?new-x (!tlb-key->smep$inline smep x)))
    (tlb-key-equiv-under-mask new-x x -3)))

Function: !tlb-key->smap$inline

(defun !tlb-key->smap$inline (smap x)
  (declare (xargs :guard (and (bitp smap) (tlb-key-p x))))
  (mbe :logic
       (b* ((smap (mbe :logic (bfix smap) :exec smap))
            (x (tlb-key-fix x)))
         (part-install smap x :width 1 :low 2))
       :exec (the (unsigned-byte 46)
                  (logior (the (unsigned-byte 46)
                               (logand (the (unsigned-byte 46) x)
                                       (the (signed-byte 4) -5)))
                          (the (unsigned-byte 3)
                               (ash (the (unsigned-byte 1) smap)
                                    2))))))

Theorem: tlb-key-p-of-!tlb-key->smap

(defthm tlb-key-p-of-!tlb-key->smap
  (b* ((new-x (!tlb-key->smap$inline smap x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->smap$inline-of-bfix-smap

(defthm !tlb-key->smap$inline-of-bfix-smap
  (equal (!tlb-key->smap$inline (bfix smap) x)
         (!tlb-key->smap$inline smap x)))

Theorem: !tlb-key->smap$inline-bit-equiv-congruence-on-smap

(defthm !tlb-key->smap$inline-bit-equiv-congruence-on-smap
  (implies (bit-equiv smap smap-equiv)
           (equal (!tlb-key->smap$inline smap x)
                  (!tlb-key->smap$inline smap-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->smap$inline-of-tlb-key-fix-x

(defthm !tlb-key->smap$inline-of-tlb-key-fix-x
  (equal (!tlb-key->smap$inline smap (tlb-key-fix x))
         (!tlb-key->smap$inline smap x)))

Theorem: !tlb-key->smap$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->smap$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->smap$inline smap x)
                  (!tlb-key->smap$inline smap x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->smap-is-tlb-key

(defthm !tlb-key->smap-is-tlb-key
  (equal (!tlb-key->smap smap x)
         (change-tlb-key x :smap smap)))

Theorem: tlb-key->smap-of-!tlb-key->smap

(defthm tlb-key->smap-of-!tlb-key->smap
  (b* ((?new-x (!tlb-key->smap$inline smap x)))
    (equal (tlb-key->smap new-x)
           (bfix smap))))

Theorem: !tlb-key->smap-equiv-under-mask

(defthm !tlb-key->smap-equiv-under-mask
  (b* ((?new-x (!tlb-key->smap$inline smap x)))
    (tlb-key-equiv-under-mask new-x x -5)))

Function: !tlb-key->ac$inline

(defun !tlb-key->ac$inline (ac x)
 (declare (xargs :guard (and (bitp ac) (tlb-key-p x))))
 (mbe
     :logic
     (b* ((ac (mbe :logic (bfix ac) :exec ac))
          (x (tlb-key-fix x)))
       (part-install ac x :width 1 :low 3))
     :exec (the (unsigned-byte 46)
                (logior (the (unsigned-byte 46)
                             (logand (the (unsigned-byte 46) x)
                                     (the (signed-byte 5) -9)))
                        (the (unsigned-byte 4)
                             (ash (the (unsigned-byte 1) ac) 3))))))

Theorem: tlb-key-p-of-!tlb-key->ac

(defthm tlb-key-p-of-!tlb-key->ac
  (b* ((new-x (!tlb-key->ac$inline ac x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->ac$inline-of-bfix-ac

(defthm !tlb-key->ac$inline-of-bfix-ac
  (equal (!tlb-key->ac$inline (bfix ac) x)
         (!tlb-key->ac$inline ac x)))

Theorem: !tlb-key->ac$inline-bit-equiv-congruence-on-ac

(defthm !tlb-key->ac$inline-bit-equiv-congruence-on-ac
  (implies (bit-equiv ac ac-equiv)
           (equal (!tlb-key->ac$inline ac x)
                  (!tlb-key->ac$inline ac-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->ac$inline-of-tlb-key-fix-x

(defthm !tlb-key->ac$inline-of-tlb-key-fix-x
  (equal (!tlb-key->ac$inline ac (tlb-key-fix x))
         (!tlb-key->ac$inline ac x)))

Theorem: !tlb-key->ac$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->ac$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->ac$inline ac x)
                  (!tlb-key->ac$inline ac x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->ac-is-tlb-key

(defthm !tlb-key->ac-is-tlb-key
  (equal (!tlb-key->ac ac x)
         (change-tlb-key x :ac ac)))

Theorem: tlb-key->ac-of-!tlb-key->ac

(defthm tlb-key->ac-of-!tlb-key->ac
  (b* ((?new-x (!tlb-key->ac$inline ac x)))
    (equal (tlb-key->ac new-x) (bfix ac))))

Theorem: !tlb-key->ac-equiv-under-mask

(defthm !tlb-key->ac-equiv-under-mask
  (b* ((?new-x (!tlb-key->ac$inline ac x)))
    (tlb-key-equiv-under-mask new-x x -9)))

Function: !tlb-key->nxe$inline

(defun !tlb-key->nxe$inline (nxe x)
 (declare (xargs :guard (and (bitp nxe) (tlb-key-p x))))
 (mbe
    :logic
    (b* ((nxe (mbe :logic (bfix nxe) :exec nxe))
         (x (tlb-key-fix x)))
      (part-install nxe x :width 1 :low 4))
    :exec (the (unsigned-byte 46)
               (logior (the (unsigned-byte 46)
                            (logand (the (unsigned-byte 46) x)
                                    (the (signed-byte 6) -17)))
                       (the (unsigned-byte 5)
                            (ash (the (unsigned-byte 1) nxe) 4))))))

Theorem: tlb-key-p-of-!tlb-key->nxe

(defthm tlb-key-p-of-!tlb-key->nxe
  (b* ((new-x (!tlb-key->nxe$inline nxe x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->nxe$inline-of-bfix-nxe

(defthm !tlb-key->nxe$inline-of-bfix-nxe
  (equal (!tlb-key->nxe$inline (bfix nxe) x)
         (!tlb-key->nxe$inline nxe x)))

Theorem: !tlb-key->nxe$inline-bit-equiv-congruence-on-nxe

(defthm !tlb-key->nxe$inline-bit-equiv-congruence-on-nxe
  (implies (bit-equiv nxe nxe-equiv)
           (equal (!tlb-key->nxe$inline nxe x)
                  (!tlb-key->nxe$inline nxe-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->nxe$inline-of-tlb-key-fix-x

(defthm !tlb-key->nxe$inline-of-tlb-key-fix-x
  (equal (!tlb-key->nxe$inline nxe (tlb-key-fix x))
         (!tlb-key->nxe$inline nxe x)))

Theorem: !tlb-key->nxe$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->nxe$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->nxe$inline nxe x)
                  (!tlb-key->nxe$inline nxe x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->nxe-is-tlb-key

(defthm !tlb-key->nxe-is-tlb-key
  (equal (!tlb-key->nxe nxe x)
         (change-tlb-key x :nxe nxe)))

Theorem: tlb-key->nxe-of-!tlb-key->nxe

(defthm tlb-key->nxe-of-!tlb-key->nxe
  (b* ((?new-x (!tlb-key->nxe$inline nxe x)))
    (equal (tlb-key->nxe new-x)
           (bfix nxe))))

Theorem: !tlb-key->nxe-equiv-under-mask

(defthm !tlb-key->nxe-equiv-under-mask
  (b* ((?new-x (!tlb-key->nxe$inline nxe x)))
    (tlb-key-equiv-under-mask new-x x -17)))

Function: !tlb-key->implicit-supervisor-access$inline

(defun !tlb-key->implicit-supervisor-access$inline
       (implicit-supervisor-access x)
  (declare (xargs :guard (and (bitp implicit-supervisor-access)
                              (tlb-key-p x))))
  (mbe :logic
       (b* ((implicit-supervisor-access
                 (mbe :logic (bfix implicit-supervisor-access)
                      :exec implicit-supervisor-access))
            (x (tlb-key-fix x)))
         (part-install implicit-supervisor-access x
                       :width 1
                       :low 5))
       :exec (the (unsigned-byte 46)
                  (logior (the (unsigned-byte 46)
                               (logand (the (unsigned-byte 46) x)
                                       (the (signed-byte 7) -33)))
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 1)
                                         implicit-supervisor-access)
                                    5))))))

Theorem: tlb-key-p-of-!tlb-key->implicit-supervisor-access

(defthm tlb-key-p-of-!tlb-key->implicit-supervisor-access
  (b* ((new-x (!tlb-key->implicit-supervisor-access$inline
                   implicit-supervisor-access x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->implicit-supervisor-access$inline-of-bfix-implicit-supervisor-access

(defthm
 !tlb-key->implicit-supervisor-access$inline-of-bfix-implicit-supervisor-access
 (equal (!tlb-key->implicit-supervisor-access$inline
             (bfix implicit-supervisor-access)
             x)
        (!tlb-key->implicit-supervisor-access$inline
             implicit-supervisor-access x)))

Theorem: !tlb-key->implicit-supervisor-access$inline-bit-equiv-congruence-on-implicit-supervisor-access

(defthm
 !tlb-key->implicit-supervisor-access$inline-bit-equiv-congruence-on-implicit-supervisor-access
 (implies (bit-equiv implicit-supervisor-access
                     implicit-supervisor-access-equiv)
          (equal (!tlb-key->implicit-supervisor-access$inline
                      implicit-supervisor-access x)
                 (!tlb-key->implicit-supervisor-access$inline
                      implicit-supervisor-access-equiv x)))
 :rule-classes :congruence)

Theorem: !tlb-key->implicit-supervisor-access$inline-of-tlb-key-fix-x

(defthm !tlb-key->implicit-supervisor-access$inline-of-tlb-key-fix-x
  (equal (!tlb-key->implicit-supervisor-access$inline
              implicit-supervisor-access
              (tlb-key-fix x))
         (!tlb-key->implicit-supervisor-access$inline
              implicit-supervisor-access x)))

Theorem: !tlb-key->implicit-supervisor-access$inline-tlb-key-equiv-congruence-on-x

(defthm
 !tlb-key->implicit-supervisor-access$inline-tlb-key-equiv-congruence-on-x
 (implies (tlb-key-equiv x x-equiv)
          (equal (!tlb-key->implicit-supervisor-access$inline
                      implicit-supervisor-access x)
                 (!tlb-key->implicit-supervisor-access$inline
                      implicit-supervisor-access x-equiv)))
 :rule-classes :congruence)

Theorem: !tlb-key->implicit-supervisor-access-is-tlb-key

(defthm !tlb-key->implicit-supervisor-access-is-tlb-key
 (equal
      (!tlb-key->implicit-supervisor-access
           implicit-supervisor-access x)
      (change-tlb-key
           x
           :implicit-supervisor-access implicit-supervisor-access)))

Theorem: tlb-key->implicit-supervisor-access-of-!tlb-key->implicit-supervisor-access

(defthm
 tlb-key->implicit-supervisor-access-of-!tlb-key->implicit-supervisor-access
 (b* ((?new-x (!tlb-key->implicit-supervisor-access$inline
                   implicit-supervisor-access x)))
   (equal (tlb-key->implicit-supervisor-access new-x)
          (bfix implicit-supervisor-access))))

Theorem: !tlb-key->implicit-supervisor-access-equiv-under-mask

(defthm !tlb-key->implicit-supervisor-access-equiv-under-mask
  (b* ((?new-x (!tlb-key->implicit-supervisor-access$inline
                    implicit-supervisor-access x)))
    (tlb-key-equiv-under-mask new-x x -33)))

Function: !tlb-key->r-w-x$inline

(defun !tlb-key->r-w-x$inline (r-w-x x)
  (declare (xargs :guard (and (2bits-p r-w-x) (tlb-key-p x))))
  (mbe :logic
       (b* ((r-w-x (mbe :logic (2bits-fix r-w-x)
                        :exec r-w-x))
            (x (tlb-key-fix x)))
         (part-install r-w-x x :width 2 :low 6))
       :exec (the (unsigned-byte 46)
                  (logior (the (unsigned-byte 46)
                               (logand (the (unsigned-byte 46) x)
                                       (the (signed-byte 9) -193)))
                          (the (unsigned-byte 8)
                               (ash (the (unsigned-byte 2) r-w-x)
                                    6))))))

Theorem: tlb-key-p-of-!tlb-key->r-w-x

(defthm tlb-key-p-of-!tlb-key->r-w-x
  (b* ((new-x (!tlb-key->r-w-x$inline r-w-x x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->r-w-x$inline-of-2bits-fix-r-w-x

(defthm !tlb-key->r-w-x$inline-of-2bits-fix-r-w-x
  (equal (!tlb-key->r-w-x$inline (2bits-fix r-w-x)
                                 x)
         (!tlb-key->r-w-x$inline r-w-x x)))

Theorem: !tlb-key->r-w-x$inline-2bits-equiv-congruence-on-r-w-x

(defthm !tlb-key->r-w-x$inline-2bits-equiv-congruence-on-r-w-x
  (implies (2bits-equiv r-w-x r-w-x-equiv)
           (equal (!tlb-key->r-w-x$inline r-w-x x)
                  (!tlb-key->r-w-x$inline r-w-x-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->r-w-x$inline-of-tlb-key-fix-x

(defthm !tlb-key->r-w-x$inline-of-tlb-key-fix-x
  (equal (!tlb-key->r-w-x$inline r-w-x (tlb-key-fix x))
         (!tlb-key->r-w-x$inline r-w-x x)))

Theorem: !tlb-key->r-w-x$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->r-w-x$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->r-w-x$inline r-w-x x)
                  (!tlb-key->r-w-x$inline r-w-x x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->r-w-x-is-tlb-key

(defthm !tlb-key->r-w-x-is-tlb-key
  (equal (!tlb-key->r-w-x r-w-x x)
         (change-tlb-key x :r-w-x r-w-x)))

Theorem: tlb-key->r-w-x-of-!tlb-key->r-w-x

(defthm tlb-key->r-w-x-of-!tlb-key->r-w-x
  (b* ((?new-x (!tlb-key->r-w-x$inline r-w-x x)))
    (equal (tlb-key->r-w-x new-x)
           (2bits-fix r-w-x))))

Theorem: !tlb-key->r-w-x-equiv-under-mask

(defthm !tlb-key->r-w-x-equiv-under-mask
  (b* ((?new-x (!tlb-key->r-w-x$inline r-w-x x)))
    (tlb-key-equiv-under-mask new-x x -193)))

Function: !tlb-key->cpl$inline

(defun !tlb-key->cpl$inline (cpl x)
 (declare (xargs :guard (and (2bits-p cpl) (tlb-key-p x))))
 (mbe
    :logic
    (b* ((cpl (mbe :logic (2bits-fix cpl) :exec cpl))
         (x (tlb-key-fix x)))
      (part-install cpl x :width 2 :low 8))
    :exec (the (unsigned-byte 46)
               (logior (the (unsigned-byte 46)
                            (logand (the (unsigned-byte 46) x)
                                    (the (signed-byte 11) -769)))
                       (the (unsigned-byte 10)
                            (ash (the (unsigned-byte 2) cpl) 8))))))

Theorem: tlb-key-p-of-!tlb-key->cpl

(defthm tlb-key-p-of-!tlb-key->cpl
  (b* ((new-x (!tlb-key->cpl$inline cpl x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->cpl$inline-of-2bits-fix-cpl

(defthm !tlb-key->cpl$inline-of-2bits-fix-cpl
  (equal (!tlb-key->cpl$inline (2bits-fix cpl) x)
         (!tlb-key->cpl$inline cpl x)))

Theorem: !tlb-key->cpl$inline-2bits-equiv-congruence-on-cpl

(defthm !tlb-key->cpl$inline-2bits-equiv-congruence-on-cpl
  (implies (2bits-equiv cpl cpl-equiv)
           (equal (!tlb-key->cpl$inline cpl x)
                  (!tlb-key->cpl$inline cpl-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->cpl$inline-of-tlb-key-fix-x

(defthm !tlb-key->cpl$inline-of-tlb-key-fix-x
  (equal (!tlb-key->cpl$inline cpl (tlb-key-fix x))
         (!tlb-key->cpl$inline cpl x)))

Theorem: !tlb-key->cpl$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->cpl$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->cpl$inline cpl x)
                  (!tlb-key->cpl$inline cpl x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->cpl-is-tlb-key

(defthm !tlb-key->cpl-is-tlb-key
  (equal (!tlb-key->cpl cpl x)
         (change-tlb-key x :cpl cpl)))

Theorem: tlb-key->cpl-of-!tlb-key->cpl

(defthm tlb-key->cpl-of-!tlb-key->cpl
  (b* ((?new-x (!tlb-key->cpl$inline cpl x)))
    (equal (tlb-key->cpl new-x)
           (2bits-fix cpl))))

Theorem: !tlb-key->cpl-equiv-under-mask

(defthm !tlb-key->cpl-equiv-under-mask
  (b* ((?new-x (!tlb-key->cpl$inline cpl x)))
    (tlb-key-equiv-under-mask new-x x -769)))

Function: !tlb-key->vpn$inline

(defun !tlb-key->vpn$inline (vpn x)
 (declare (xargs :guard (and (36bits-p vpn) (tlb-key-p x))))
 (mbe
  :logic
  (b* ((vpn (mbe :logic (36bits-fix vpn) :exec vpn))
       (x (tlb-key-fix x)))
    (part-install vpn x :width 36 :low 10))
  :exec
  (the (unsigned-byte 46)
       (logior (the (unsigned-byte 46)
                    (logand (the (unsigned-byte 46) x)
                            (the (signed-byte 47) -70368744176641)))
               (the (unsigned-byte 46)
                    (ash (the (unsigned-byte 36) vpn)
                         10))))))

Theorem: tlb-key-p-of-!tlb-key->vpn

(defthm tlb-key-p-of-!tlb-key->vpn
  (b* ((new-x (!tlb-key->vpn$inline vpn x)))
    (tlb-key-p new-x))
  :rule-classes :rewrite)

Theorem: !tlb-key->vpn$inline-of-36bits-fix-vpn

(defthm !tlb-key->vpn$inline-of-36bits-fix-vpn
  (equal (!tlb-key->vpn$inline (36bits-fix vpn)
                               x)
         (!tlb-key->vpn$inline vpn x)))

Theorem: !tlb-key->vpn$inline-36bits-equiv-congruence-on-vpn

(defthm !tlb-key->vpn$inline-36bits-equiv-congruence-on-vpn
  (implies (36bits-equiv vpn vpn-equiv)
           (equal (!tlb-key->vpn$inline vpn x)
                  (!tlb-key->vpn$inline vpn-equiv x)))
  :rule-classes :congruence)

Theorem: !tlb-key->vpn$inline-of-tlb-key-fix-x

(defthm !tlb-key->vpn$inline-of-tlb-key-fix-x
  (equal (!tlb-key->vpn$inline vpn (tlb-key-fix x))
         (!tlb-key->vpn$inline vpn x)))

Theorem: !tlb-key->vpn$inline-tlb-key-equiv-congruence-on-x

(defthm !tlb-key->vpn$inline-tlb-key-equiv-congruence-on-x
  (implies (tlb-key-equiv x x-equiv)
           (equal (!tlb-key->vpn$inline vpn x)
                  (!tlb-key->vpn$inline vpn x-equiv)))
  :rule-classes :congruence)

Theorem: !tlb-key->vpn-is-tlb-key

(defthm !tlb-key->vpn-is-tlb-key
  (equal (!tlb-key->vpn vpn x)
         (change-tlb-key x :vpn vpn)))

Theorem: tlb-key->vpn-of-!tlb-key->vpn

(defthm tlb-key->vpn-of-!tlb-key->vpn
  (b* ((?new-x (!tlb-key->vpn$inline vpn x)))
    (equal (tlb-key->vpn new-x)
           (36bits-fix vpn))))

Theorem: !tlb-key->vpn-equiv-under-mask

(defthm !tlb-key->vpn-equiv-under-mask
  (b* ((?new-x (!tlb-key->vpn$inline vpn x)))
    (tlb-key-equiv-under-mask new-x x 1023)))

Function: tlb-key-debug

(defun tlb-key-debug (x)
 (declare (xargs :guard (tlb-key-p x)))
 (let ((__function__ 'tlb-key-debug))
  (declare (ignorable __function__))
  (b* (((tlb-key x)))
   (cons
    (cons 'wp x.wp)
    (cons
     (cons 'smep x.smep)
     (cons
      (cons 'smap x.smap)
      (cons
       (cons 'ac x.ac)
       (cons
           (cons 'nxe x.nxe)
           (cons (cons 'implicit-supervisor-access
                       x.implicit-supervisor-access)
                 (cons (cons 'r-w-x x.r-w-x)
                       (cons (cons 'cpl x.cpl)
                             (cons (cons 'vpn x.vpn) nil))))))))))))

Subtopics

!tlb-key->implicit-supervisor-access

Update the |X86ISA|::|IMPLICIT-SUPERVISOR-ACCESS| field of a tlb-key bit structure.

Tlb-key-fast

A faster constructor for tlb-keys.

Tlb-key-p

Recognizer for tlb-key bit structures.

!tlb-key->r-w-x

Update the |X86ISA|::|R-W-X| field of a tlb-key bit structure.

!tlb-key->vpn

Update the |X86ISA|::|VPN| field of a tlb-key bit structure.

!tlb-key->smep

Update the |X86ISA|::|SMEP| field of a tlb-key bit structure.

!tlb-key->smap

Update the |X86ISA|::|SMAP| field of a tlb-key bit structure.

!tlb-key->cpl

Update the |X86ISA|::|CPL| field of a tlb-key bit structure.

!tlb-key->nxe

Update the |X86ISA|::|NXE| field of a tlb-key bit structure.

Tlb-key->implicit-supervisor-access

Access the |X86ISA|::|IMPLICIT-SUPERVISOR-ACCESS| field of a tlb-key bit structure.

!tlb-key->wp

Update the |X86ISA|::|WP| field of a tlb-key bit structure.

!tlb-key->ac

Update the |X86ISA|::|AC| field of a tlb-key bit structure.

Tlb-key->vpn

Access the |X86ISA|::|VPN| field of a tlb-key bit structure.

Tlb-key->smep

Access the |X86ISA|::|SMEP| field of a tlb-key bit structure.

Tlb-key->smap

Access the |X86ISA|::|SMAP| field of a tlb-key bit structure.

Tlb-key->r-w-x

Access the |X86ISA|::|R-W-X| field of a tlb-key bit structure.

Tlb-key->cpl

Access the |X86ISA|::|CPL| field of a tlb-key bit structure.

Tlb-key-fix

Fixing function for tlb-key bit structures.

Tlb-key->wp

Access the |X86ISA|::|WP| field of a tlb-key bit structure.

Tlb-key->nxe

Access the |X86ISA|::|NXE| field of a tlb-key bit structure.

Tlb-key->ac

Access the |X86ISA|::|AC| field of a tlb-key bit structure.

Good-tlb-key-p

Recongnizer for a valid TLB key.