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

• System-level-marking-view-proof-utilities

Rb-in-system-level-marking-view

Definitions and Theorems

Theorem: xr-fault-rb-state-in-sys-view

(defthm xr-fault-rb-state-in-sys-view
 (implies
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (equal (xr :fault index
              (mv-nth 2 (rb n lin-addr r-w-x x86)))
          (xr :fault index x86))))

Theorem: rb-and-xw-flags-state-in-sys-view

(defthm rb-and-xw-flags-state-in-sys-view
  (implies (and (equal (rflagsbits->ac (double-rewrite value))
                       (rflagsbits->ac (rflags x86)))
                (x86p x86))
           (equal (mv-nth 2
                          (rb n lin-addr
                              r-w-x (xw :rflags nil value x86)))
                  (xw :rflags nil value
                      (mv-nth 2 (rb n lin-addr r-w-x x86))))))

Theorem: mv-nth-0-rb-and-paging-equiv-memory-cong

(defthm mv-nth-0-rb-and-paging-equiv-memory-cong
  (implies (paging-equiv-memory x86-1 x86-2)
           (equal (mv-nth 0 (rb n lin-addr r-w-x x86-1))
                  (mv-nth 0 (rb n lin-addr r-w-x x86-2))))
  :rule-classes :congruence)

Theorem: read-from-physical-memory-and-xlate-equiv-memory-disjoint-from-paging-structures-0

(defthm
 read-from-physical-memory-and-xlate-equiv-memory-disjoint-from-paging-structures-0
 (implies
  (and
   (bind-free (find-an-xlate-equiv-x86
                   'read-from-physical-memory-and-xlate-equiv-memory
                   x86-1 'x86-2
                   mfc state)
              (x86-2))
   (syntaxp (and (not (eq x86-2 x86-1))
                 (term-order x86-2 x86-1)))
   (xlate-equiv-memory (double-rewrite x86-1)
                       x86-2)
   (physical-address-listp p-addrs)
   (disjoint-p
        p-addrs
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-1)))))
  (equal (read-from-physical-memory p-addrs x86-1)
         (read-from-physical-memory p-addrs x86-2))))

Theorem: read-from-physical-memory-and-paging-equiv-memory-disjoint-from-paging-structures-0

(defthm
 read-from-physical-memory-and-paging-equiv-memory-disjoint-from-paging-structures-0
 (implies
   (and (bind-free
             (find-an-paging-equiv-x86
                  'read-from-physical-memory-and-paging-equiv-memory
                  x86-1 'x86-2
                  mfc state)
             (x86-2))
        (syntaxp (and (not (eq x86-2 x86-1))
                      (term-order x86-2 x86-1)))
        (paging-equiv-memory (double-rewrite x86-1)
                             x86-2)
        (physical-address-listp p-addrs)
        (disjoint-p
             p-addrs
             (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                         (double-rewrite x86-1)))))
   (equal (read-from-physical-memory p-addrs x86-1)
          (read-from-physical-memory p-addrs x86-2))))

Theorem: read-from-physical-memory-and-xlate-equiv-memory-disjoint-from-paging-structures

(defthm
 read-from-physical-memory-and-xlate-equiv-memory-disjoint-from-paging-structures
 (implies
  (and
   (bind-free (find-an-xlate-equiv-x86
                   'read-from-physical-memory-and-xlate-equiv-memory
                   x86-1 'x86-2
                   mfc state)
              (x86-2))
   (syntaxp (and (not (eq x86-2 x86-1))
                 (term-order x86-2 x86-1)))
   (xlate-equiv-memory (double-rewrite x86-1)
                       x86-2)
   (disjoint-p
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-2)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-2))))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-1)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-1)))))
  (equal (read-from-physical-memory
              (mv-nth 1 (las-to-pas n lin-addr r-w-x x86-1))
              x86-1)
         (read-from-physical-memory
              (mv-nth 1 (las-to-pas n lin-addr r-w-x x86-1))
              x86-2))))

Theorem: read-from-physical-memory-and-paging-equiv-memory-disjoint-from-paging-structures

(defthm
 read-from-physical-memory-and-paging-equiv-memory-disjoint-from-paging-structures
 (implies
  (and
    (bind-free
         (find-an-paging-equiv-x86
              'read-from-physical-memory-and-paging-equiv-memory
              x86-1 'x86-2
              mfc state)
         (x86-2))
    (syntaxp (and (not (eq x86-2 x86-1))
                  (term-order x86-2 x86-1)))
    (paging-equiv-memory (double-rewrite x86-1)
                         x86-2)
    (disjoint-p
         (mv-nth 1
                 (las-to-pas n
                             lin-addr r-w-x (double-rewrite x86-2)))
         (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                     (double-rewrite x86-2))))
    (disjoint-p
         (mv-nth 1
                 (las-to-pas n
                             lin-addr r-w-x (double-rewrite x86-1)))
         (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                     (double-rewrite x86-1)))))
  (equal (read-from-physical-memory
              (mv-nth 1 (las-to-pas n lin-addr r-w-x x86-1))
              x86-1)
         (read-from-physical-memory
              (mv-nth 1 (las-to-pas n lin-addr r-w-x x86-1))
              x86-2))))

Theorem: xlate-equiv-memory-tlb-consistent-n-implies-equal-las-to-pas

(defthm xlate-equiv-memory-tlb-consistent-n-implies-equal-las-to-pas
  (implies
       (and (xlate-equiv-memory x86-1 x86-2)
            (syntaxp (and (not (eq x86-2 x86-1))
                          (term-order x86-2 x86-1)))
            (tlb-consistent-n n lin-addr r-w-x x86-1)
            (tlb-consistent-n n lin-addr r-w-x x86-2))
       (and (equal (mv-nth 0 (las-to-pas n lin-addr r-w-x x86-1))
                   (mv-nth 0 (las-to-pas n lin-addr r-w-x x86-2)))
            (equal (mv-nth 1 (las-to-pas n lin-addr r-w-x x86-1))
                   (mv-nth 1
                           (las-to-pas n lin-addr r-w-x x86-2))))))

Theorem: mv-nth-1-rb-and-xlate-equiv-memory-disjoint-from-paging-structures

(defthm
 mv-nth-1-rb-and-xlate-equiv-memory-disjoint-from-paging-structures
 (implies
  (and
   (bind-free
    (find-an-xlate-equiv-x86
     'mv-nth-1-rb-and-xlate-equiv-memory-disjoint-from-paging-structures
     x86-1 'x86-2
     mfc state)
    (x86-2))
   (syntaxp (and (not (eq x86-2 x86-1))
                 (term-order x86-2 x86-1)))
   (xlate-equiv-memory (double-rewrite x86-1)
                       x86-2)
   (disjoint-p
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-2)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-2))))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-1)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-1))))
   (tlb-consistent-n n lin-addr r-w-x x86-1)
   (tlb-consistent-n n lin-addr r-w-x x86-2)
   (64-bit-modep (double-rewrite x86-1)))
  (equal (mv-nth 1 (rb n lin-addr r-w-x x86-1))
         (mv-nth 1 (rb n lin-addr r-w-x x86-2)))))

Theorem: mv-nth-1-rb-and-paging-equiv-memory-disjoint-from-paging-structures

(defthm
 mv-nth-1-rb-and-paging-equiv-memory-disjoint-from-paging-structures
 (implies
  (and
   (bind-free
    (find-an-paging-equiv-x86
     'mv-nth-1-rb-and-paging-equiv-memory-disjoint-from-paging-structures
     x86-1 'x86-2
     mfc state)
    (x86-2))
   (syntaxp (and (not (eq x86-2 x86-1))
                 (term-order x86-2 x86-1)))
   (paging-equiv-memory (double-rewrite x86-1)
                        x86-2)
   (disjoint-p
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-2)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-2))))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-1)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-1))))
   (64-bit-modep (double-rewrite x86-1)))
  (equal (mv-nth 1 (rb n lin-addr r-w-x x86-1))
         (mv-nth 1 (rb n lin-addr r-w-x x86-2)))))

Theorem: mv-nth-2-rb-and-xlate-equiv-memory

(defthm mv-nth-2-rb-and-xlate-equiv-memory
 (implies
  (and
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (64-bit-modep (double-rewrite x86)))
  (xlate-equiv-memory (mv-nth 2 (rb n lin-addr r-w-x x86))
                      (double-rewrite x86))))

Theorem: mv-nth-2-rb-and-paging-equiv-memory

(defthm mv-nth-2-rb-and-paging-equiv-memory
 (implies
  (and
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (64-bit-modep (double-rewrite x86)))
  (paging-equiv-memory (mv-nth 2 (rb n lin-addr r-w-x x86))
                       (double-rewrite x86))))

Theorem: mv-nth-1-rb-after-mv-nth-2-rb

(defthm mv-nth-1-rb-after-mv-nth-2-rb
 (implies
  (and
     (disjoint-p$ (mv-nth 1
                          (las-to-pas n-1 lin-addr-1
                                      r-w-x-1 (double-rewrite x86)))
                  (all-xlation-governing-entries-paddrs
                       n-2 lin-addr-2 (double-rewrite x86)))
     (disjoint-p$ (mv-nth 1
                          (las-to-pas n-1 lin-addr-1
                                      r-w-x-1 (double-rewrite x86)))
                  (all-xlation-governing-entries-paddrs
                       n-1 lin-addr-1 (double-rewrite x86)))
     (64-bit-modep (double-rewrite x86)))
  (equal (mv-nth 1
                 (rb n-1 lin-addr-1 r-w-x-1
                     (mv-nth 2 (rb n-2 lin-addr-2 r-w-x-2 x86))))
         (mv-nth 1 (rb n-1 lin-addr-1 r-w-x-1 x86)))))

Theorem: mv-nth-1-rb-after-mv-nth-2-las-to-pas

(defthm mv-nth-1-rb-after-mv-nth-2-las-to-pas
 (implies
  (and
      (disjoint-p (mv-nth 1
                          (las-to-pas n-1 lin-addr-1
                                      r-w-x-1 (double-rewrite x86)))
                  (all-xlation-governing-entries-paddrs
                       n-2 lin-addr-2 (double-rewrite x86)))
      (disjoint-p (mv-nth 1
                          (las-to-pas n-1 lin-addr-1
                                      r-w-x-1 (double-rewrite x86)))
                  (all-xlation-governing-entries-paddrs
                       n-1 lin-addr-1 (double-rewrite x86)))
      (not (app-view x86))
      (64-bit-modep (double-rewrite x86)))
  (equal
      (mv-nth 1
              (rb n-1 lin-addr-1 r-w-x-1
                  (mv-nth 2
                          (las-to-pas n-2 lin-addr-2 r-w-x-2 x86))))
      (mv-nth 1
              (rb n-1 lin-addr-1
                  r-w-x-1 (double-rewrite x86))))))