• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • 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
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • Program-at-alt
          • 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
        • 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
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • 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-xlate-equiv-memory-cong

(defthm mv-nth-0-rb-and-xlate-equiv-memory-cong
  (implies (xlate-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

(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-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: 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-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
   (marking-view (double-rewrite x86))
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (not (app-view (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: xlate-equiv-memory-and-two-mv-nth-2-rb

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

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))))))