• 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
      • Implemented-opcodes
      • To-do
      • 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
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Xlate-equiv-structures

Xlate-equiv-entries

Signature

(xlate-equiv-entries e-1 e-2) → *

Two paging structure entries are xlate-equiv-entries if they are equal for all bits except the accessed and dirty bits (bits 5 and 6, respectively). Additionally, the tlb and paging entries on the states must be arranged so that address translations are the same on both states.

Definitions and Theorems

Function: xlate-equiv-entries

(defun xlate-equiv-entries (e-1 e-2)
  (declare (type (unsigned-byte 64) e-1)
           (type (unsigned-byte 64) e-2))
  (let ((__function__ 'xlate-equiv-entries))
    (declare (ignorable __function__))
    (and (equal (ia32e-page-tablesbits->p e-1)
                (ia32e-page-tablesbits->p e-2))
         (equal (ia32e-page-tablesbits->r/w e-1)
                (ia32e-page-tablesbits->r/w e-2))
         (equal (ia32e-page-tablesbits->u/s e-1)
                (ia32e-page-tablesbits->u/s e-2))
         (equal (ia32e-page-tablesbits->pwt e-1)
                (ia32e-page-tablesbits->pwt e-2))
         (equal (ia32e-page-tablesbits->pcd e-1)
                (ia32e-page-tablesbits->pcd e-2))
         (equal (ia32e-page-tablesbits->ps e-1)
                (ia32e-page-tablesbits->ps e-2))
         (equal (ia32e-page-tablesbits->res1 e-1)
                (ia32e-page-tablesbits->res1 e-2))
         (equal (ia32e-page-tablesbits->reference-addr e-1)
                (ia32e-page-tablesbits->reference-addr e-2))
         (equal (ia32e-page-tablesbits->res2 e-1)
                (ia32e-page-tablesbits->res2 e-2))
         (equal (ia32e-page-tablesbits->xd e-1)
                (ia32e-page-tablesbits->xd e-2)))))

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

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

Theorem: xlate-equiv-entries-self-set-accessed-bit

(defthm xlate-equiv-entries-self-set-accessed-bit
  (and (xlate-equiv-entries e (set-accessed-bit (double-rewrite e)))
       (xlate-equiv-entries (set-accessed-bit e)
                            (double-rewrite e))))

Theorem: xlate-equiv-entries-self-set-dirty-bit

(defthm xlate-equiv-entries-self-set-dirty-bit
  (and (xlate-equiv-entries e (set-dirty-bit (double-rewrite e)))
       (xlate-equiv-entries (set-dirty-bit e)
                            (double-rewrite e))))

Function: find-xlate-equiv-entries

(defun find-xlate-equiv-entries (e-1-equiv e-2-equiv)
  (cond ((equal e-1-equiv e-2-equiv)
         (cons (cons 'e-1 e-1-equiv)
               (cons (cons 'e-2 e-2-equiv) 'nil)))
        ((equal (first e-1-equiv) 'rm-low-64)
         (cond ((equal (first e-2-equiv) 'rm-low-64)
                (cons (cons 'e-1 e-1-equiv)
                      (cons (cons 'e-2 e-2-equiv) 'nil)))
               ((equal (first e-2-equiv)
                       'set-accessed-bit)
                (b* ((e-2 (if (equal (car (second e-2-equiv))
                                     'set-dirty-bit)
                              (second (second e-2-equiv))
                            (second e-2-equiv))))
                  (cons (cons 'e-1 e-1-equiv)
                        (cons (cons 'e-2 e-2) 'nil))))
               ((equal (first e-2-equiv) 'set-dirty-bit)
                (b* ((e-2 (if (equal (car (second e-2-equiv))
                                     'set-accessed-bit)
                              (second (second e-2-equiv))
                            (second (second e-2-equiv)))))
                  (cons (cons 'e-1 e-1-equiv)
                        (cons (cons 'e-2 e-2) 'nil))))
               (t (cons (cons 'e-1 e-1-equiv)
                        (cons (cons 'e-2 e-2-equiv) 'nil)))))
        ((equal (first e-2-equiv) 'rm-low-64)
         (cond ((equal (first e-1-equiv) 'rm-low-64)
                (cons (cons 'e-2 e-2-equiv)
                      (cons (cons 'e-1 e-1-equiv) 'nil)))
               ((equal (first e-1-equiv)
                       'set-accessed-bit)
                (b* ((e-1 (if (equal (car (second e-1-equiv))
                                     'set-dirty-bit)
                              (second (second e-1-equiv))
                            (second e-1-equiv))))
                  (cons (cons 'e-2 e-2-equiv)
                        (cons (cons 'e-1 e-1) 'nil))))
               ((equal (first e-1-equiv) 'set-dirty-bit)
                (b* ((e-1 (if (equal (car (second e-1-equiv))
                                     'set-accessed-bit)
                              (second (second e-1-equiv))
                            (second e-1-equiv))))
                  (cons (cons 'e-2 e-2-equiv)
                        (cons (cons 'e-1 e-1) 'nil))))
               (t (cons (cons 'e-2 e-2-equiv)
                        (cons (cons 'e-1 e-1-equiv) 'nil)))))))

Theorem: xlate-equiv-entries-and-set-accessed-and/or-dirty-bit

(defthm xlate-equiv-entries-and-set-accessed-and/or-dirty-bit
 (implies
      (and (bind-free (find-xlate-equiv-entries e-1-equiv e-2-equiv)
                      (e-1 e-2))
           (xlate-equiv-entries e-1 e-2)
           (or (equal e-1-equiv e-1)
               (equal e-1-equiv (set-accessed-bit e-1))
               (equal e-1-equiv (set-dirty-bit e-1))
               (equal e-1-equiv
                      (set-dirty-bit (set-accessed-bit e-1))))
           (or (equal e-2-equiv e-2)
               (equal e-2-equiv (set-accessed-bit e-2))
               (equal e-2-equiv (set-dirty-bit e-2))
               (equal e-2-equiv
                      (set-dirty-bit (set-accessed-bit e-2)))))
      (xlate-equiv-entries e-1-equiv e-2-equiv)))

Theorem: xlate-equiv-entries-and-page-present-cong

(defthm xlate-equiv-entries-and-page-present-cong
  (implies (xlate-equiv-entries e-1 e-2)
           (equal (page-present e-1)
                  (page-present e-2)))
  :rule-classes :congruence)

Theorem: xlate-equiv-entries-and-page-read-write-cong

(defthm xlate-equiv-entries-and-page-read-write-cong
  (implies (xlate-equiv-entries e-1 e-2)
           (equal (page-read-write e-1)
                  (page-read-write e-2)))
  :rule-classes :congruence)

Theorem: xlate-equiv-entries-and-page-user-supervisor-cong

(defthm xlate-equiv-entries-and-page-user-supervisor-cong
  (implies (xlate-equiv-entries e-1 e-2)
           (equal (page-user-supervisor e-1)
                  (page-user-supervisor e-2)))
  :rule-classes :congruence)

Theorem: xlate-equiv-entries-and-reference-addr

(defthm xlate-equiv-entries-and-reference-addr
  (implies (xlate-equiv-entries e-1 e-2)
           (equal (ia32e-page-tablesbits->reference-addr e-1)
                  (ia32e-page-tablesbits->reference-addr e-2)))
  :rule-classes :congruence)

Theorem: xlate-equiv-entries-and-page-size

(defthm xlate-equiv-entries-and-page-size
  (implies (xlate-equiv-entries e-1 e-2)
           (equal (page-size e-1) (page-size e-2)))
  :rule-classes :congruence)

Theorem: xlate-equiv-entries-and-page-execute-disable

(defthm xlate-equiv-entries-and-page-execute-disable
  (implies (xlate-equiv-entries e-1 e-2)
           (equal (page-execute-disable e-1)
                  (page-execute-disable e-2)))
  :rule-classes :congruence)

Theorem: xlate-equiv-entries-with-loghead-64-1

(defthm xlate-equiv-entries-with-loghead-64-1
  (equal (xlate-equiv-entries (loghead 64 e-1)
                              e-2)
         (xlate-equiv-entries e-1 e-2)))

Theorem: xlate-equiv-entries-with-loghead-64-2

(defthm xlate-equiv-entries-with-loghead-64-2
  (equal (xlate-equiv-entries e-1 (loghead 64 e-2))
         (xlate-equiv-entries e-1 e-2)))

Theorem: xlate-equiv-entries-with-loghead-64-cong

(defthm xlate-equiv-entries-with-loghead-64-cong
  (implies (xlate-equiv-entries e-1 e-2)
           (xlate-equiv-entries (loghead 64 e-1)
                                (loghead 64 e-2)))
  :rule-classes :congruence)

Theorem: xlate-equiv-entries-and-loghead

(defthm xlate-equiv-entries-and-loghead
  (implies (and (xlate-equiv-entries e-1 e-2)
                (syntaxp (quotep n))
                (natp n)
                (<= n 5))
           (equal (loghead n e-1)
                  (loghead n e-2))))

Theorem: xlate-equiv-entries-and-logtail

(defthm xlate-equiv-entries-and-logtail
  (implies (and (xlate-equiv-entries e-1 e-2)
                (syntaxp (quotep n))
                (natp n)
                (<= 7 n)
                (<= n 64))
           (equal (logtail n (loghead 64 e-1))
                  (logtail n (loghead 64 e-2)))))