• 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
                • All-mem-except-paging-structures-equal-aux
              • Gather-qword-addresses-corresponding-to-1-entry
              • Xlation-governing-entries-paddrs
              • Xlate-equiv-structures
              • 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

All-mem-except-paging-structures-equal

Signature

(all-mem-except-paging-structures-equal x86-1 x86-2) → *

Definitions and Theorems

Function: all-mem-except-paging-structures-equal-aux

(defun all-mem-except-paging-structures-equal-aux
       (i paging-qword-addresses x86-1 x86-2)
 (declare
  (xargs
       :non-executable t
       :guard (and (natp i)
                   (<= i *mem-size-in-bytes*)
                   (mult-8-qword-paddr-listp paging-qword-addresses)
                   (x86p x86-1)
                   (x86p x86-2))))
 (prog2$
  (acl2::throw-nonexec-error
       'all-mem-except-paging-structures-equal-aux
       (list i paging-qword-addresses x86-1 x86-2))
  (let ((__function__ 'all-mem-except-paging-structures-equal-aux))
    (declare (ignorable __function__))
    (if
     (zp i)
     (if (disjoint-p (list i)
                     (open-qword-paddr-list paging-qword-addresses))
         (equal (xr :mem i x86-1)
                (xr :mem i x86-2))
       t)
     (if (disjoint-p (list (1- i))
                     (open-qword-paddr-list paging-qword-addresses))
         (and (equal (xr :mem (1- i) x86-1)
                     (xr :mem (1- i) x86-2))
              (all-mem-except-paging-structures-equal-aux
                   (1- i)
                   paging-qword-addresses x86-1 x86-2))
       (all-mem-except-paging-structures-equal-aux
            (1- i)
            paging-qword-addresses x86-1 x86-2))))))

Theorem: all-mem-except-paging-structures-equal-aux-and-xr-mem-from-rest-of-memory

(defthm
 all-mem-except-paging-structures-equal-aux-and-xr-mem-from-rest-of-memory
 (implies
  (and
    (all-mem-except-paging-structures-equal-aux i addrs x86-1 x86-2)
    (disjoint-p (list j)
                (open-qword-paddr-list addrs))
    (natp i)
    (natp j)
    (< j i))
  (equal (xr :mem j x86-1)
         (xr :mem j x86-2))))

Theorem: all-mem-except-paging-structures-equal-aux-and-rm-low-32-from-rest-of-memory

(defthm
 all-mem-except-paging-structures-equal-aux-and-rm-low-32-from-rest-of-memory
 (implies
  (and
    (all-mem-except-paging-structures-equal-aux i addrs x86-1 x86-2)
    (disjoint-p (addr-range 4 j)
                (open-qword-paddr-list addrs))
    (natp i)
    (natp j)
    (< (+ 3 j) i)
    (not (app-view x86-1))
    (not (app-view x86-2)))
  (equal (rm-low-32 j x86-1)
         (rm-low-32 j x86-2))))

Theorem: all-mem-except-paging-structures-equal-aux-and-rm-low-64-from-rest-of-memory

(defthm
 all-mem-except-paging-structures-equal-aux-and-rm-low-64-from-rest-of-memory
 (implies
  (and
    (all-mem-except-paging-structures-equal-aux i addrs x86-1 x86-2)
    (disjoint-p (addr-range 8 j)
                (open-qword-paddr-list addrs))
    (natp i)
    (natp j)
    (< (+ 7 j) i)
    (not (app-view x86-1))
    (not (app-view x86-2)))
  (equal (rm-low-64 j x86-1)
         (rm-low-64 j x86-2))))

Theorem: all-mem-except-paging-structures-equal-aux-is-reflexive

(defthm all-mem-except-paging-structures-equal-aux-is-reflexive
  (all-mem-except-paging-structures-equal-aux i addrs x x))

Theorem: all-mem-except-paging-structures-equal-aux-is-commutative

(defthm all-mem-except-paging-structures-equal-aux-is-commutative
 (implies (all-mem-except-paging-structures-equal-aux i addrs x y)
          (all-mem-except-paging-structures-equal-aux i addrs y x)))

Theorem: all-mem-except-paging-structures-equal-aux-is-transitive

(defthm all-mem-except-paging-structures-equal-aux-is-transitive
 (implies
      (and (all-mem-except-paging-structures-equal-aux i addrs x y)
           (all-mem-except-paging-structures-equal-aux i addrs y z))
      (all-mem-except-paging-structures-equal-aux i addrs x z)))

Theorem: all-mem-except-paging-structures-equal-aux-and-xw-1

(defthm all-mem-except-paging-structures-equal-aux-and-xw-1
 (implies
  (not (equal fld :mem))
  (equal (all-mem-except-paging-structures-equal-aux
              i addrs (xw fld index val x)
              y)
         (all-mem-except-paging-structures-equal-aux i addrs x y))))

Theorem: all-mem-except-paging-structures-equal-aux-and-xw-2

(defthm all-mem-except-paging-structures-equal-aux-and-xw-2
 (implies
  (not (equal fld :mem))
  (equal (all-mem-except-paging-structures-equal-aux
              i addrs x (xw fld index val y))
         (all-mem-except-paging-structures-equal-aux i addrs x y))))

Theorem: all-mem-except-paging-structures-equal-aux-and-xw-mem

(defthm all-mem-except-paging-structures-equal-aux-and-xw-mem
  (implies (all-mem-except-paging-structures-equal-aux i addrs x y)
           (all-mem-except-paging-structures-equal-aux
                i addrs (xw :mem index val x)
                (xw :mem index val y))))

Theorem: xr-mem-wm-low-64

(defthm xr-mem-wm-low-64
  (implies (not (member-p index (addr-range 8 addr)))
           (equal (xr :mem index (wm-low-64 addr val x86))
                  (xr :mem index x86))))

Theorem: all-mem-except-paging-structures-equal-aux-and-wm-low-64-paging-entry

(defthm
 all-mem-except-paging-structures-equal-aux-and-wm-low-64-paging-entry
 (implies
  (member-p index addrs)
  (equal (all-mem-except-paging-structures-equal-aux
              i addrs (wm-low-64 index val x)
              y)
         (all-mem-except-paging-structures-equal-aux i addrs x y))))

Theorem: all-mem-except-paging-structures-equal-aux-and-wm-low-64

(defthm all-mem-except-paging-structures-equal-aux-and-wm-low-64
  (implies
       (and (all-mem-except-paging-structures-equal-aux i addrs x y)
            (not (xr :app-view nil x))
            (not (xr :app-view nil y)))
       (all-mem-except-paging-structures-equal-aux
            i addrs (wm-low-64 index val x)
            (wm-low-64 index val y))))

Theorem: all-mem-except-paging-structures-equal-aux-and-xw-mem-commute-writes

(defthm
 all-mem-except-paging-structures-equal-aux-and-xw-mem-commute-writes
 (implies (not (equal index-1 index-2))
          (all-mem-except-paging-structures-equal-aux
               i addrs
               (xw :mem
                   index-1 val-1 (xw :mem index-2 val-2 x))
               (xw :mem index-2
                   val-2 (xw :mem index-1 val-1 x)))))

Function: all-mem-except-paging-structures-equal

(defun all-mem-except-paging-structures-equal (x86-1 x86-2)
 (declare (xargs :non-executable t
                 :guard (and (x86p x86-1) (x86p x86-2))))
 (prog2$
  (acl2::throw-nonexec-error 'all-mem-except-paging-structures-equal
                             (list x86-1 x86-2))
  (let ((__function__ 'all-mem-except-paging-structures-equal))
   (declare (ignorable __function__))
   (if
    (equal (app-view x86-1) nil)
    (if
     (equal (app-view x86-2) nil)
     (and
         (equal (gather-all-paging-structure-qword-addresses x86-1)
                (gather-all-paging-structure-qword-addresses x86-2))
         (all-mem-except-paging-structures-equal-aux
              *mem-size-in-bytes*
              (gather-all-paging-structure-qword-addresses x86-1)
              x86-1 x86-2))
     nil)
    (equal (app-view x86-2)
           (app-view x86-1))))))

Theorem: all-mem-except-paging-structures-equal-is-an-equivalence

(defthm all-mem-except-paging-structures-equal-is-an-equivalence
  (and (booleanp (all-mem-except-paging-structures-equal x y))
       (all-mem-except-paging-structures-equal x x)
       (implies (all-mem-except-paging-structures-equal x y)
                (all-mem-except-paging-structures-equal y x))
       (implies (and (all-mem-except-paging-structures-equal x y)
                     (all-mem-except-paging-structures-equal y z))
                (all-mem-except-paging-structures-equal x z)))
  :rule-classes (:equivalence))

Theorem: all-mem-except-paging-structures-equal-and-xr-mem-from-rest-of-memory

(defthm
 all-mem-except-paging-structures-equal-and-xr-mem-from-rest-of-memory
 (implies
  (and
     (all-mem-except-paging-structures-equal x86-1 x86-2)
     (disjoint-p
          (list j)
          (open-qword-paddr-list
               (gather-all-paging-structure-qword-addresses x86-1)))
     (natp j)
     (< j *mem-size-in-bytes*)
     (not (app-view x86-1)))
  (equal (xr :mem j x86-1)
         (xr :mem j x86-2))))

Theorem: all-mem-except-paging-structures-equal-and-rm-low-64-from-rest-of-memory

(defthm
 all-mem-except-paging-structures-equal-and-rm-low-64-from-rest-of-memory
 (implies
  (and
     (all-mem-except-paging-structures-equal x86-1 x86-2)
     (disjoint-p
          (addr-range 8 j)
          (open-qword-paddr-list
               (gather-all-paging-structure-qword-addresses x86-1)))
     (natp j)
     (< (+ 7 j) *mem-size-in-bytes*))
  (equal (rm-low-64 j x86-1)
         (rm-low-64 j x86-2))))

Theorem: all-mem-except-paging-structures-equal-and-xw-1

(defthm all-mem-except-paging-structures-equal-and-xw-1
 (implies
   (and (not (equal fld :mem))
        (not (equal fld :ctr))
        (not (equal fld :app-view)))
   (equal
        (all-mem-except-paging-structures-equal (xw fld index val x)
                                                y)
        (all-mem-except-paging-structures-equal (double-rewrite x)
                                                y))))

Theorem: all-mem-except-paging-structures-equal-and-xw-2

(defthm all-mem-except-paging-structures-equal-and-xw-2
 (implies
  (and (not (equal fld :mem))
       (not (equal fld :ctr))
       (not (equal fld :app-view)))
  (equal
    (all-mem-except-paging-structures-equal x (xw fld index val y))
    (all-mem-except-paging-structures-equal x (double-rewrite y)))))

Theorem: all-mem-except-paging-structures-equal-and-xw

(defthm all-mem-except-paging-structures-equal-and-xw
 (implies
  (and (not (equal fld :mem))
       (not (equal fld :ctr))
       (not (equal fld :app-view)))
  (equal
       (all-mem-except-paging-structures-equal (xw fld index val x)
                                               (xw fld index val y))
       (all-mem-except-paging-structures-equal x y))))

Theorem: all-mem-except-paging-structures-equal-and-xw-mem-except-paging-structure

(defthm
 all-mem-except-paging-structures-equal-and-xw-mem-except-paging-structure
 (implies
   (and (bind-free (find-equiv-x86-for-components y mfc state))
        (all-mem-except-paging-structures-equal x y)
        (physical-address-p index)
        (disjoint-p
             (list index)
             (open-qword-paddr-list
                  (gather-all-paging-structure-qword-addresses y))))
   (all-mem-except-paging-structures-equal (xw :mem index val x)
                                           (xw :mem index val y))))

Theorem: all-mem-except-paging-structures-equal-and-wm-low-64-paging-entry

(defthm
  all-mem-except-paging-structures-equal-and-wm-low-64-paging-entry
 (implies
  (and (member-p index
                 (gather-all-paging-structure-qword-addresses x))
       (equal (gather-all-paging-structure-qword-addresses
                   (wm-low-64 index val x))
              (gather-all-paging-structure-qword-addresses x)))
  (equal
     (all-mem-except-paging-structures-equal (wm-low-64 index val x)
                                             y)
     (all-mem-except-paging-structures-equal (double-rewrite x)
                                             y))))

Theorem: all-mem-except-paging-structures-equal-and-wm-low-64-entry-addr

(defthm
    all-mem-except-paging-structures-equal-and-wm-low-64-entry-addr
 (implies
   (and (xlate-equiv-entries (double-rewrite entry)
                             (rm-low-64 entry-addr x86))
        (member-p entry-addr
                  (gather-all-paging-structure-qword-addresses x86))
        (unsigned-byte-p 64 entry))
   (all-mem-except-paging-structures-equal
        (wm-low-64 entry-addr entry x86)
        (double-rewrite x86))))

Theorem: all-mem-except-paging-structures-equal-and-wm-low-64-except-paging-structure

(defthm
 all-mem-except-paging-structures-equal-and-wm-low-64-except-paging-structure
 (implies
  (and (bind-free (find-equiv-x86-for-components y mfc state))
       (all-mem-except-paging-structures-equal x y)
       (disjoint-p
            (addr-range 8 index)
            (open-qword-paddr-list
                 (gather-all-paging-structure-qword-addresses y))))
  (all-mem-except-paging-structures-equal (wm-low-64 index val x)
                                          (wm-low-64 index val y))))

Theorem: all-mem-except-paging-structures-equal-and-xw-mem-commute-writes

(defthm
   all-mem-except-paging-structures-equal-and-xw-mem-commute-writes
  (implies (not (equal index-1 index-2))
           (all-mem-except-paging-structures-equal
                (xw :mem
                    index-1 val-1 (xw :mem index-2 val-2 x))
                (xw :mem index-2
                    val-2 (xw :mem index-1 val-1 x)))))

Subtopics

All-mem-except-paging-structures-equal-aux