• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Tlb
      • Booting-linux
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
        • System-level-marking-view-proof-utilities
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Program-at-alt
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • Rb-in-system-level-marking-view
          • Xlate-equiv-memory-and-rml08
          • Reasoning-about-page-tables
            • Create-qword-address-list
            • Mult-8-qword-paddr-listp
            • Gather-paging-structures
              • Gather-all-paging-structure-qword-addresses
              • All-mem-except-paging-structures-equal
              • Gather-qword-addresses-corresponding-to-1-entry
              • Xlation-governing-entries-paddrs
              • Xlate-equiv-structures
                • Xlate-equiv-entries
                • Xlate-equiv-entries-at-qword-addresses
              • Xlation-governing-entries-paddrs-for-page-dir-ptr-table
              • Xlation-governing-entries-paddrs-for-page-directory
              • All-xlation-governing-entries-paddrs
              • Xlation-governing-entries-paddrs-for-pml4-table
              • Xlation-governing-entries-paddrs-for-page-table
              • Gather-pml4-table-qword-addresses
              • Xlate-equiv-memory
              • Open-qword-paddr-list
            • Qword-paddr-listp
            • Find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux
            • Find-first-arg-of-disjoint-p$-candidates
            • Paging-basics
          • Las-to-pas-two-n-ind-hint
          • Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
          • Replace-element
          • Phys-mem-values-same
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
        • Debugging-code-proofs
        • General-memory-utils
        • X86-row-wow-thms
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Gather-paging-structures

Xlate-equiv-structures

Signature

(xlate-equiv-structures x86-1 x86-2) → *

Two x86 states are xlate-equiv-structures if their paging structures are equal, modulo the accessed and dirty bits (See xlate-equiv-entries).

Definitions and Theorems

Function: xlate-equiv-structures

(defun xlate-equiv-structures (x86-1 x86-2)
 (declare (xargs :non-executable t
                 :guard (and (x86p x86-1) (x86p x86-2))))
 (prog2$
  (acl2::throw-nonexec-error 'xlate-equiv-structures
                             (list x86-1 x86-2))
  (let ((__function__ 'xlate-equiv-structures))
   (declare (ignorable __function__))
   (if
    (and (equal (xr :app-view nil x86-1) nil)
         (equal (xr :app-view nil x86-2) nil))
    (let*
        ((paging-qword-addresses-1
              (gather-all-paging-structure-qword-addresses x86-1))
         (paging-qword-addresses-2
              (gather-all-paging-structure-qword-addresses x86-2)))
     (and
       (equal (segment-selectorbits->rpl (seg-visiblei *cs* x86-1))
              (segment-selectorbits->rpl (seg-visiblei *cs* x86-2)))
       (equal (cr0bits->wp (n32 (ctri *cr0* x86-1)))
              (cr0bits->wp (n32 (ctri *cr0* x86-2))))
       (equal (cr3bits->pdb (ctri *cr3* x86-1))
              (cr3bits->pdb (ctri *cr3* x86-2)))
       (equal (cr4bits->smep (loghead 22 (ctri *cr4* x86-1)))
              (cr4bits->smep (loghead 22 (ctri *cr4* x86-2))))
       (equal (cr4bits->smap (loghead 22 (ctri *cr4* x86-1)))
              (cr4bits->smap (loghead 22 (ctri *cr4* x86-2))))
       (equal
            (ia32_eferbits->nxe (n12 (msri *ia32_efer-idx* x86-1)))
            (ia32_eferbits->nxe (n12 (msri *ia32_efer-idx* x86-2))))
       (equal (rflagsbits->ac (rflags x86-1))
              (rflagsbits->ac (rflags x86-2)))
       (equal (xr :marking-view nil x86-1)
              (xr :marking-view nil x86-2))
       (equal paging-qword-addresses-1
              paging-qword-addresses-2)
       (equal (implicit-supervisor-access x86-1)
              (implicit-supervisor-access x86-2))
       (xlate-equiv-entries-at-qword-addresses
            paging-qword-addresses-1
            paging-qword-addresses-2 x86-1 x86-2)))
    (and (equal (xr :app-view nil x86-2)
                (xr :app-view nil x86-1)))))))

Theorem: xlate-equiv-structures-is-an-equivalence

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

Theorem: xlate-equiv-structures-and-xw

(defthm xlate-equiv-structures-and-xw
  (implies (and (not (equal fld :mem))
                (not (equal fld :seg-visible))
                (not (equal fld :msr))
                (not (equal fld :ctr))
                (not (equal fld :rflags))
                (not (equal fld :app-view))
                (not (equal fld :marking-view))
                (not (equal fld :implicit-supervisor-access)))
           (xlate-equiv-structures (xw fld index val x86)
                                   (double-rewrite x86))))

Theorem: xlate-equiv-structures-and-xw-rflags

(defthm xlate-equiv-structures-and-xw-rflags
  (implies (equal (rflagsbits->ac val)
                  (rflagsbits->ac (xr :rflags nil x86)))
           (xlate-equiv-structures (xw :rflags nil val x86)
                                   (double-rewrite x86))))

Theorem: xlate-equiv-structures-and-app-view-cong

(defthm xlate-equiv-structures-and-app-view-cong
  (implies (xlate-equiv-structures x86-1 x86-2)
           (equal (xr :app-view nil x86-1)
                  (xr :app-view nil x86-2)))
  :rule-classes :congruence)

Subtopics

Xlate-equiv-entries

Xlate-equiv-entries-at-qword-addresses