• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
          • Separate-mapped-mem
        • Debugging-code-proofs
        • General-memory-utils
        • X86-row-wow-thms
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Common-system-level-utils

Separate-mapped-mem

Signature

(separate-mapped-mem r-w-x-1 n-1 
                     lin-addr-1 r-w-x-2 n-2 lin-addr-2 x86) 
 
  → 
separatep

Arguments

n-1 — Guard (posp n-1).

lin-addr-1 — Guard (canonical-address-p lin-addr-1).

n-2 — Guard (posp n-2).

lin-addr-2 — Guard (canonical-address-p lin-addr-2).

Returns

separatep — Type (booleanp separatep).

Two memory regions are truly separate if:

• the linear memory regions are separate, as defined by separate
• their corresponding physical memory regions are separate.

Note that this predicate ignores whether the translation of the memory regions results in an error.

Definitions and Theorems

Function: separate-mapped-mem

(defun
 separate-mapped-mem
 (r-w-x-1 n-1
          lin-addr-1 r-w-x-2 n-2 lin-addr-2 x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (member :r :w :x) r-w-x-1)
          (type (member :r :w :x) r-w-x-2))
 (declare (xargs :guard (and (posp n-1)
                             (canonical-address-p lin-addr-1)
                             (posp n-2)
                             (canonical-address-p lin-addr-2))))
 (declare
   (xargs :non-executable t
          :guard (and (not (app-view x86))
                      (canonical-address-p (+ -1 n-1 lin-addr-1))
                      (canonical-address-p (+ -1 n-2 lin-addr-2)))))
 (prog2$ (acl2::throw-nonexec-error
              'separate-mapped-mem
              (list r-w-x-1 n-1
                    lin-addr-1 r-w-x-2 n-2 lin-addr-2 x86))
         (let ((__function__ 'separate-mapped-mem))
              (declare (ignorable __function__))
              (and (separate r-w-x-1
                             n-1 lin-addr-1 r-w-x-2 n-2 lin-addr-2)
                   (b* (((mv ?r-1-err r-1-paddrs)
                         (las-to-pas n-1 lin-addr-1 r-w-x-1 x86))
                        ((mv ?r-2-err r-2-paddrs)
                         (las-to-pas n-2 lin-addr-2 r-w-x-2 x86)))
                       (and (disjoint-p r-1-paddrs r-2-paddrs)))))))

Theorem: booleanp-of-separate-mapped-mem

(defthm
 booleanp-of-separate-mapped-mem
 (b*
  ((separatep
       (separate-mapped-mem r-w-x-1 n-1
                            lin-addr-1 r-w-x-2 n-2 lin-addr-2 x86)))
  (booleanp separatep))
 :rule-classes :type-prescription)

Theorem: separate-mapped-mem-is-commutative

(defthm
    separate-mapped-mem-is-commutative
    (implies
         (separate-mapped-mem r-w-x-1 n-1 a-1 r-w-x-2 n-2 a-2 x86)
         (separate-mapped-mem r-w-x-2 n-2 a-2 r-w-x-1 n-1 a-1 x86)))