• 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

Xlate-equiv-memory-and-rml08

Definitions and Theorems

Theorem: paging-equiv-memory-and-rvm08

(defthm paging-equiv-memory-and-rvm08
  (implies (and (xr :app-view nil (double-rewrite x86-1))
                (paging-equiv-memory (double-rewrite x86-1)
                                     x86-2))
           (and (equal (mv-nth 0 (rvm08 lin-addr x86-1))
                       (mv-nth 0 (rvm08 lin-addr x86-2)))
                (equal (mv-nth 1 (rvm08 lin-addr x86-1))
                       (mv-nth 1 (rvm08 lin-addr x86-2))))))

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

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

Theorem: xlate-equiv-memory-and-xr-mem-from-rest-of-memory

(defthm xlate-equiv-memory-and-xr-mem-from-rest-of-memory
 (implies
  (and
   (bind-free
        (find-an-xlate-equiv-x86
             'xlate-equiv-memory-and-xr-mem-from-rest-of-memory
             x86-1 'x86-2
             mfc state)
        (x86-2))
   (xlate-equiv-memory (double-rewrite x86-1)
                       x86-2)
   (syntaxp (not (equal x86-1 x86-2)))
   (disjoint-p (list j)
               (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                           (double-rewrite x86-1))))
   (natp j)
   (< j *mem-size-in-bytes*))
  (equal (xr :mem j x86-1)
         (xr :mem j x86-2))))

Theorem: paging-equiv-memory-and-xr-mem-from-rest-of-memory

(defthm paging-equiv-memory-and-xr-mem-from-rest-of-memory
 (implies
  (and
   (bind-free
        (find-an-paging-equiv-x86
             'paging-equiv-memory-and-xr-mem-from-rest-of-memory
             x86-1 'x86-2
             mfc state)
        (x86-2))
   (paging-equiv-memory (double-rewrite x86-1)
                        x86-2)
   (syntaxp (not (equal x86-1 x86-2)))
   (disjoint-p (list j)
               (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                           (double-rewrite x86-1))))
   (natp j)
   (< j *mem-size-in-bytes*))
  (equal (xr :mem j x86-1)
         (xr :mem j x86-2))))

Theorem: paging-equiv-memory-and-mv-nth-1-rml08

(defthm paging-equiv-memory-and-mv-nth-1-rml08
 (implies
  (and
   (bind-free (find-an-paging-equiv-x86
                   'paging-equiv-memory-and-mv-nth-1-rml08
                   x86-1 'x86-2
                   mfc state)
              (x86-2))
   (syntaxp (not (equal x86-1 x86-2)))
   (paging-equiv-memory (double-rewrite x86-1)
                        x86-2)
   (disjoint-p
    (list
       (mv-nth
            1
            (ia32e-la-to-pa lin-addr r-w-x (double-rewrite x86-1))))
    (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                (double-rewrite x86-1)))))
  (equal (mv-nth 1 (rml08 lin-addr r-w-x x86-1))
         (mv-nth 1 (rml08 lin-addr r-w-x x86-2)))))

Theorem: xlate-equiv-memory-and-two-mv-nth-2-rml08-cong

(defthm xlate-equiv-memory-and-two-mv-nth-2-rml08-cong
 (implies
      (xlate-equiv-memory x86-1 x86-2)
      (xlate-equiv-memory (mv-nth 2 (rml08 lin-addr r-w-x x86-1))
                          (mv-nth 2 (rml08 lin-addr r-w-x x86-2)))))

Theorem: paging-equiv-memory-and-two-mv-nth-2-rml08-cong

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

Theorem: paging-equiv-memory-mv-nth-2-rml08

(defthm paging-equiv-memory-mv-nth-2-rml08
  (implies
       (64-bit-modep (double-rewrite x86))
       (paging-equiv-memory x86
                            (mv-nth 2 (rml08 lin-addr r-w-x x86)))))

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

(defthm xlate-equiv-memory-and-mv-nth-2-rml08
  (implies (64-bit-modep (double-rewrite x86))
           (xlate-equiv-memory (mv-nth 2 (rml08 lin-addr r-w-x x86))
                               x86)))