• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • App-view
        • Top-level-memory
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
          • Ia32e-paging
            • Paging-entry-no-page-fault-p
            • Ia32e-la-to-pa-without-tlb-internal
            • Ia32e-la-to-pa-page-directory
            • Ia32e-la-to-pa-page-dir-ptr-table
            • Ia32e-la-to-pa-page-table
            • Ia32e-la-to-pa-pml4-table
            • Ia32e-la-to-pa-without-tlb
            • Ia32e-la-to-pa
            • Same-page
            • Page-fault-exception
            • Page-dir-ptr-table-entry-addr
            • Page-directory-entry-addr
            • Page-table-entry-addr
            • La-to-pa
            • Paging-entry-no-page-fault-p-did-fault?
            • Pml4-table-entry-addr
            • Same-page-offset
            • Page-user-supervisor
            • Page-execute-disable
            • Set-dirty-bit
            • Set-accessed-bit
            • Page-read-write
            • Page-present
            • Page-fault-err-no
            • Accessed-bit
            • Page-size
            • Find-similar-paging-entries-from-page-present-equality-aux
            • Dirty-bit
            • Good-lin-addr-p
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Ia32e-paging

Paging-entry-no-page-fault-p

Determining access rights and detecting page faults

Signature

(paging-entry-no-page-fault-p structure-type lin-addr 
                              entry u/s-acc r/w-acc x/d-acc wp smep 
                              smap ac nxe implicit-supervisor-access 
                              r-w-x cpl x86) 
 
  → 
(mv flg val x86)

Arguments

structure-type — 0: Page Table; 1: Page Directory; 2: Page Directory Pointer Table; 3: PML4 Table.

u/s-acc — logand of user-supervisor field of all superior paging entries.

r/w-acc — logand of read-write field of all superior paging entries.

x/d-acc — logand of execute-disable field of all superior paging entries.

smep — Supervisor Mode Execution Prevention.

smap — Supervisor Mode Access Prevention.

ac — AC field from RFLAGS.

implicit-supervisor-access — 0: Explicit; 1: Implicit.

Returns

x86 — Type (x86p x86), given (x86p x86).

Source for determining the access rights: Section 4.6 in the Intel Manuals, Vol. 3A.

It is important to differentiate between:

1. a supervisor-mode and a user-mode access
2. an implicit and an explicit supervisor-mode access
3. a supervisor-mode and a user-mode address

These concepts are defined below.

• Every access to a linear address is either a supervisor-mode access or a user-mode access. For all instruction fetches and most data accesses, accesses made while CPL < 3 are supervisor-mode accesses, while accesses made while CPL = 3 are user-mode accesses.
• Some operations implicitly access system data structures with linear addresses; the resulting accesses to those data structures are supervisor-mode accesses regardless of CPL. Examples of such accesses include the following: accesses to the global descriptor table (GDT) or local descriptor table (LDT) to load a segment descriptor; accesses to the interrupt descriptor table (IDT) when delivering an interrupt or exception; and accesses to the task-state segment (TSS) as part of a task switch or change of CPL. All these accesses are called implicit supervisor-mode accesses regardless of CPL. Other accesses made while CPL < 3 are called explicit supervisor-mode accesses.
• If the U/S flag (bit 2) is 0 in at least one of the paging-structure entries, the address is a supervisor-mode address. Otherwise, the address is a user-mode address.

TO-DO: For now, we are treating all supervisor-mode accesses as explicit. We need to detect and then account for implicit accesses.

Definitions and Theorems

Function: paging-entry-no-page-fault-p-did-fault?

(defun paging-entry-no-page-fault-p-did-fault?
       (u/s-all r/w-all x/d-all wp smep smap ac nxe
                implicit-supervisor-access r-w-x cpl)
  (declare (type (unsigned-byte 1) u/s-all)
           (type (unsigned-byte 1) r/w-all)
           (type (unsigned-byte 1) x/d-all)
           (type (unsigned-byte 1) wp)
           (type (unsigned-byte 1) smep)
           (type (unsigned-byte 1) smap)
           (type (unsigned-byte 1) ac)
           (type (unsigned-byte 1) nxe)
           (type (unsigned-byte 1)
                 implicit-supervisor-access)
           (type (member :r :w :x) r-w-x)
           (type (unsigned-byte 2) cpl))
  (declare
       (xargs :guard (or (not (equal implicit-supervisor-access 1))
                         (< cpl 3))))
  (let ((__function__ 'paging-entry-no-page-fault-p-did-fault?))
    (declare (ignorable __function__))
    (or (and (equal r-w-x :r)
             (if (< cpl 3)
                 (if (equal u/s-all 0)
                     nil
                   (if (equal smap 0)
                       nil
                     (or (equal implicit-supervisor-access 1)
                         (equal ac 0))))
               (equal u/s-all 0)))
        (and (equal r-w-x :w)
             (if (< cpl 3)
                 (if (equal u/s-all 0)
                     (and (equal wp 1) (equal r/w-all 0))
                   (if (equal wp 0)
                       (if (equal smap 0)
                           nil
                         (or (equal implicit-supervisor-access 1)
                             (equal ac 0)))
                     (if (equal smap 0)
                         (equal r/w-all 0)
                       (if (and (equal implicit-supervisor-access 0)
                                (equal ac 1))
                           (equal r/w-all 0)
                         t))))
               (or (equal u/s-all 0)
                   (equal r/w-all 0))))
        (and (equal r-w-x :x)
             (if (< cpl 3)
                 (if (equal u/s-all 0)
                     (if (equal nxe 0) nil (equal x/d-all 1))
                   (if (equal smep 0)
                       (if (equal nxe 0) nil (equal x/d-all 1))
                     t))
               (or (equal u/s-all 0)
                   (and (equal nxe 1)
                        (equal x/d-all 1))))))))

Theorem: booleanp-of-paging-entry-no-page-fault-p-did-fault?

(defthm booleanp-of-paging-entry-no-page-fault-p-did-fault?
  (b* ((fault? (paging-entry-no-page-fault-p-did-fault?
                    u/s-all
                    r/w-all x/d-all wp smep smap ac nxe
                    implicit-supervisor-access r-w-x cpl)))
    (booleanp fault?))
  :rule-classes :rewrite)

Function: paging-entry-no-page-fault-p

(defun paging-entry-no-page-fault-p
       (structure-type lin-addr
                       entry u/s-acc r/w-acc x/d-acc wp smep
                       smap ac nxe implicit-supervisor-access
                       r-w-x cpl x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 2) structure-type)
          (type (signed-byte 48) lin-addr)
          (type (unsigned-byte 64) entry)
          (type (unsigned-byte 1) u/s-acc)
          (type (unsigned-byte 1) r/w-acc)
          (type (unsigned-byte 1) x/d-acc)
          (type (unsigned-byte 1) wp)
          (type (unsigned-byte 1) smep)
          (type (unsigned-byte 1) smap)
          (type (unsigned-byte 1) ac)
          (type (unsigned-byte 1) nxe)
          (type (unsigned-byte 1)
                implicit-supervisor-access)
          (type (member :r :w :x) r-w-x)
          (type (unsigned-byte 2) cpl))
 (declare
   (xargs :guard (and (not (app-view x86))
                      (or (not (equal implicit-supervisor-access 1))
                          (< cpl 3)))))
 (let ((__function__ 'paging-entry-no-page-fault-p))
  (declare (ignorable __function__))
  (b*
   ((entry (mbe :logic (loghead 64 entry)
                :exec entry))
    (page-present (mbe :logic (page-present entry)
                       :exec (ia32e-page-tablesbits->p entry)))
    ((when (equal page-present 0))
     (let
      ((err-no
           (page-fault-err-no page-present r-w-x cpl 0 smep 1 nxe)))
      (page-fault-exception lin-addr err-no x86)))
    (read-write (mbe :logic (page-read-write entry)
                     :exec (ia32e-page-tablesbits->r/w entry)))
    (r/w-all (the (unsigned-byte 1)
                  (logand read-write r/w-acc)))
    (user-supervisor (mbe :logic (page-user-supervisor entry)
                          :exec (ia32e-page-tablesbits->u/s entry)))
    (u/s-all (the (unsigned-byte 1)
                  (logand user-supervisor u/s-acc)))
    (execute-disable (mbe :logic (page-execute-disable entry)
                          :exec (ia32e-page-tablesbits->xd entry)))
    (x/d-all (the (unsigned-byte 1)
                  (logand execute-disable x/d-acc)))
    (page-size (mbe :logic (page-size entry)
                    :exec (ia32e-page-tablesbits->ps entry)))
    (rsvd
     (mbe
      :logic
      (if
       (or (and (equal structure-type 3)
                (equal page-size 1))
           (and (not (equal structure-type 0))
                (not (equal structure-type 3))
                (equal page-size 1)
                (if (equal structure-type 1)
                    (not (equal (part-select entry :low 13 :high 20)
                                0))
                  (not (equal (part-select entry :low 13 :high 29)
                              0))))
           (and (equal nxe 0)
                (not (equal execute-disable 0))))
       1
       0)
      :exec
      (if
       (or
        (and (equal structure-type 3)
             (equal page-size 1))
        (and (not (equal structure-type 0))
             (not (equal structure-type 3))
             (equal page-size 1)
             (if (equal structure-type 1)
                 (not (equal (the (unsigned-byte 8)
                                  (logand 255
                                          (the (unsigned-byte 51)
                                               (ash entry (- 13)))))
                             0))
               (not (equal (the (unsigned-byte 17)
                                (logand 131071
                                        (the (unsigned-byte 51)
                                             (ash entry (- 13)))))
                           0))))
        (and (equal nxe 0)
             (not (equal (ia32e-page-tablesbits->xd entry)
                         0))))
       1
       0)))
    ((when (equal rsvd 1))
     (let ((err-no (page-fault-err-no page-present
                                      r-w-x cpl rsvd smep 1 nxe)))
       (page-fault-exception lin-addr err-no x86)))
    ((when (paging-entry-no-page-fault-p-did-fault?
                u/s-all
                r/w-all x/d-all wp smep smap ac nxe
                implicit-supervisor-access r-w-x cpl))
     (let ((err-no (page-fault-err-no page-present
                                      r-w-x cpl rsvd smep 1 nxe)))
       (page-fault-exception lin-addr err-no x86))))
   (mv nil 0 x86))))

Theorem: x86p-of-paging-entry-no-page-fault-p.x86

(defthm x86p-of-paging-entry-no-page-fault-p.x86
  (implies (x86p x86)
           (b* (((mv ?flg ?val ?x86)
                 (paging-entry-no-page-fault-p
                      structure-type lin-addr
                      entry u/s-acc r/w-acc x/d-acc wp smep
                      smap ac nxe implicit-supervisor-access
                      r-w-x cpl x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Theorem: mv-nth-1-paging-entry-no-page-fault-p-value

(defthm mv-nth-1-paging-entry-no-page-fault-p-value
  (equal (mv-nth 1
                 (paging-entry-no-page-fault-p
                      structure-type lin-addr
                      entry u/s-acc r/w-acc x/d-acc wp smep
                      smap ac nxe implicit-supervisor-access
                      r-w-x cpl x86))
         0))

Theorem: xr-paging-entry-no-page-fault-p

(defthm xr-paging-entry-no-page-fault-p
 (implies
      (not (equal fld :fault))
      (equal (xr fld index
                 (mv-nth 2
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86)))
             (xr fld index x86))))

Theorem: rm-low-64-paging-entry-no-page-fault-p

(defthm rm-low-64-paging-entry-no-page-fault-p
 (equal
      (rm-low-64 addr
                 (mv-nth 2
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86)))
      (rm-low-64 addr x86)))

Theorem: paging-entry-no-page-fault-p-xw-values

(defthm paging-entry-no-page-fault-p-xw-values
  (and (equal (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl (xw fld index value x86)))
              (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))
       (equal (mv-nth 1
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl (xw fld index value x86)))
              (mv-nth 1
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))))

Theorem: paging-entry-no-page-fault-p-xw-state

(defthm paging-entry-no-page-fault-p-xw-state
 (implies
      (not (equal fld :fault))
      (equal (mv-nth 2
                     (paging-entry-no-page-fault-p
                          structure-type lin-addr
                          entry u/s-acc r/w-acc x/d-acc wp smep
                          smap ac nxe implicit-supervisor-access
                          r-w-x cpl (xw fld index value x86)))
             (xw fld index value
                 (mv-nth 2
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86))))))

Theorem: mv-nth-2-paging-entry-no-page-fault-p-does-not-modify-x86-if-no-fault

(defthm
 mv-nth-2-paging-entry-no-page-fault-p-does-not-modify-x86-if-no-fault
 (implies (not (mv-nth 0
                       (paging-entry-no-page-fault-p
                            structure-type lin-addr
                            entry u/s-acc r/w-acc x/d-acc wp smep
                            smap ac nxe implicit-supervisor-access
                            r-w-x cpl x86)))
          (equal (mv-nth 2
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86))
                 x86)))

Function: find-similar-paging-entries-from-page-present-equality-aux

(defun find-similar-paging-entries-from-page-present-equality-aux
       (index entry-var calls)
 (declare (xargs :guard (natp index)))
 (let
  ((__function__
       'find-similar-paging-entries-from-page-present-equality-aux))
  (declare (ignorable __function__))
  (if (atom calls)
      nil
    (b* ((one-call (car calls))
         ((unless (and (true-listp one-call)
                       (true-listp (nth index one-call))
                       (equal (len (nth index one-call)) 2)))
          nil))
      (cons (list (cons entry-var (nth 1 (nth index one-call))))
            (find-similar-paging-entries-from-page-present-equality-aux
                 index entry-var (cdr calls)))))))

Function: find-similar-paging-entries-from-page-present-equality

(defun find-similar-paging-entries-from-page-present-equality
       (bound-entry-val entry-var mfc state)
  (declare (xargs :stobjs (state))
           (ignorable state))
  (b*
   (((mv index calls)
     (mv 2
         (acl2::find-matches-list
              (cons 'equal
                    (cons (cons 'page-present
                                (cons bound-entry-val 'nil))
                          '((page-present e))))
              (mfc-clause mfc)
              nil)))
    ((mv index calls)
     (if
       (not calls)
       (mv 1
           (acl2::find-matches-list
                (cons 'equal
                      (cons '(page-present e)
                            (cons (cons 'page-present
                                        (cons bound-entry-val 'nil))
                                  'nil)))
                (mfc-clause mfc)
                nil))
       (mv index calls)))
    ((when (not calls)) nil))
   (find-similar-paging-entries-from-page-present-equality-aux
        index entry-var calls)))

Theorem: mv-nth-0-paging-entry-no-page-fault-p-and-similar-entries

(defthm mv-nth-0-paging-entry-no-page-fault-p-and-similar-entries
  (implies
       (and (bind-free (find-similar-paging-entries-from-page-present-equality
                            entry-1 'entry-2
                            mfc state)
                       (entry-2))
            (syntaxp (not (eq entry-1 entry-2)))
            (equal (page-present entry-1)
                   (page-present entry-2))
            (equal (page-read-write entry-1)
                   (page-read-write entry-2))
            (equal (page-user-supervisor entry-1)
                   (page-user-supervisor entry-2))
            (equal (page-execute-disable entry-1)
                   (page-execute-disable entry-2))
            (equal (page-size entry-1)
                   (page-size entry-2))
            (if (equal structure-type 1)
                (equal (part-select entry-1 :low 13 :high 20)
                       (part-select entry-2 :low 13 :high 20))
              (if (equal structure-type 2)
                  (equal (part-select entry-1 :low 13 :high 29)
                         (part-select entry-2 :low 13 :high 29))
                t))
            (unsigned-byte-p 2 structure-type)
            (unsigned-byte-p 64 entry-1)
            (unsigned-byte-p 64 entry-2))
       (equal (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry-1 u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86))
              (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry-2 u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))))

Theorem: mv-nth-0-paging-entry-no-page-fault-p-is-independent-of-lin-addr

(defthm
   mv-nth-0-paging-entry-no-page-fault-p-is-independent-of-lin-addr
 (implies (not (mv-nth 0
                       (paging-entry-no-page-fault-p
                            structure-type lin-addr
                            entry u/s-acc r/w-acc x/d-acc wp smep
                            smap ac nxe implicit-supervisor-access
                            r-w-x cpl x86)))
          (equal (mv-nth 0
                         (paging-entry-no-page-fault-p
                              structure-type (+ n lin-addr)
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86))
                 nil)))

Theorem: 64-bit-modep-of-paging-entry-no-page-fault-p

(defthm 64-bit-modep-of-paging-entry-no-page-fault-p
 (equal
   (64-bit-modep (mv-nth 2
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86)))
   (64-bit-modep x86)))

Theorem: x86-operation-mode-of-paging-entry-no-page-fault-p

(defthm x86-operation-mode-of-paging-entry-no-page-fault-p
  (equal (x86-operation-mode
              (mv-nth 2
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))
         (x86-operation-mode x86)))

Theorem: paging-entry-no-page-fault-flg-same-if-virt-addr-same-page

(defthm paging-entry-no-page-fault-flg-same-if-virt-addr-same-page
 (implies (same-page lin-addr lin-addr-2)
          (equal (mv-nth 0
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86))
                 (mv-nth 0
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr-2
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86))))
 :rule-classes :congruence)

Theorem: paging-entry-no-page-fault-val-same-if-virt-addr-same-page

(defthm paging-entry-no-page-fault-val-same-if-virt-addr-same-page
 (implies (same-page lin-addr lin-addr-2)
          (equal (mv-nth 1
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86))
                 (mv-nth 1
                         (paging-entry-no-page-fault-p
                              structure-type lin-addr-2
                              entry u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl x86))))
 :rule-classes :congruence)

Theorem: paging-entry-no-page-fault-p-invariant-under-paging-entry-no-page-fault-p

(defthm
 paging-entry-no-page-fault-p-invariant-under-paging-entry-no-page-fault-p
 (and
  (equal
      (mv-nth 0
              (paging-entry-no-page-fault-p
                   structure-type lin-addr entry
                   u/s-acc r/w-acc x/d-acc wp smep smap ac
                   nxe implicit-supervisor-access r-w-x cpl
                   (mv-nth 2
                           (paging-entry-no-page-fault-p
                                structure-type2
                                lin-addr2 entry2 u/s-acc2
                                r/w-acc2 x/d-acc2 wp2 smep2 smap2
                                ac2 nxe2 implicit-supervisor-access2
                                r-w-x2 cpl2 x86))))
      (mv-nth 0
              (paging-entry-no-page-fault-p
                   structure-type lin-addr
                   entry u/s-acc r/w-acc x/d-acc wp smep
                   smap ac nxe implicit-supervisor-access
                   r-w-x cpl x86)))
  (equal
      (mv-nth 1
              (paging-entry-no-page-fault-p
                   structure-type lin-addr entry
                   u/s-acc r/w-acc x/d-acc wp smep smap ac
                   nxe implicit-supervisor-access r-w-x cpl
                   (mv-nth 2
                           (paging-entry-no-page-fault-p
                                structure-type2
                                lin-addr2 entry2 u/s-acc2
                                r/w-acc2 x/d-acc2 wp2 smep2 smap2
                                ac2 nxe2 implicit-supervisor-access2
                                r-w-x2 cpl2 x86))))
      (mv-nth 1
              (paging-entry-no-page-fault-p
                   structure-type lin-addr
                   entry u/s-acc r/w-acc x/d-acc wp smep
                   smap ac nxe implicit-supervisor-access
                   r-w-x cpl x86)))))

Theorem: paging-entry-no-page-fault-p-invariant-under-setting-dirty-bit

(defthm
     paging-entry-no-page-fault-p-invariant-under-setting-dirty-bit
  (and (equal (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type
                           lin-addr (set-dirty-bit entry)
                           u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86))
              (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))
       (equal (mv-nth 1
                      (paging-entry-no-page-fault-p
                           structure-type
                           lin-addr (set-dirty-bit entry)
                           u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86))
              (mv-nth 1
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))))

Theorem: paging-entry-no-page-fault-p-invariant-under-setting-accessed-bit

(defthm
  paging-entry-no-page-fault-p-invariant-under-setting-accessed-bit
  (and (equal (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type
                           lin-addr (set-accessed-bit entry)
                           u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86))
              (mv-nth 0
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))
       (equal (mv-nth 1
                      (paging-entry-no-page-fault-p
                           structure-type
                           lin-addr (set-accessed-bit entry)
                           u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86))
              (mv-nth 1
                      (paging-entry-no-page-fault-p
                           structure-type lin-addr
                           entry u/s-acc r/w-acc x/d-acc wp smep
                           smap ac nxe implicit-supervisor-access
                           r-w-x cpl x86)))))