• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
          • Ia32e-paging
            • Paging-entry-no-page-fault-p
            • Ia32e-la-to-pa-without-tlb-internal
            • Ia32e-la-to-pa-page-directory
            • Ia32e-la-to-pa-page-dir-ptr-table
            • Ia32e-la-to-pa-page-table
            • Ia32e-la-to-pa-pml4-table
            • Ia32e-la-to-pa-without-tlb
            • Ia32e-la-to-pa
            • Same-page
            • Page-fault-exception
            • Page-dir-ptr-table-entry-addr
            • Page-directory-entry-addr
            • Page-table-entry-addr
            • Paging-entry-no-page-fault-p-did-fault?
            • Pml4-table-entry-addr
            • Same-page-offset
            • Set-dirty-bit
            • Set-accessed-bit
            • Page-user-supervisor
            • Page-read-write
            • Page-fault-err-no
            • Page-execute-disable
            • La-to-pa
            • Page-size
            • Page-present
            • Find-similar-paging-entries-from-page-present-equality-aux
            • Dirty-bit
            • Accessed-bit
            • Good-lin-addr-p
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Ia32e-paging

Same-page

Signature

(same-page lin-addr lin-addr-2) → *

Arguments

lin-addr — Guard (integerp lin-addr).

lin-addr-2 — Guard (integerp lin-addr-2).

Definitions and Theorems

Function: same-page

(defun same-page (lin-addr lin-addr-2)
  (declare (xargs :guard (and (integerp lin-addr)
                              (integerp lin-addr-2))))
  (let ((__function__ 'same-page))
    (declare (ignorable __function__))
    (or (equal lin-addr lin-addr-2)
        (and (mbt (and (integerp lin-addr)
                       (integerp lin-addr-2)))
             (equal (logtail 12 lin-addr)
                    (logtail 12 lin-addr-2))))))

Theorem: same-page-is-an-equivalence

(defthm same-page-is-an-equivalence
  (and (booleanp (same-page x y))
       (same-page x x)
       (implies (same-page x y)
                (same-page y x))
       (implies (and (same-page x y) (same-page y z))
                (same-page x z)))
  :rule-classes (:equivalence))

Theorem: same-page-implies-logtails>=12-equal

(defthm same-page-implies-logtails>=12-equal
  (implies (and (integerp i)
                (>= i 12)
                (same-page y (double-rewrite x))
                (syntaxp (not (equal x y))))
           (equal (logtail i x) (logtail i y))))

Theorem: same-page-address-construction

(defthm same-page-address-construction
  (implies (same-page x y)
           (same-page (logior (loghead i x) (ash z i))
                      (logior (loghead i y) (ash z i))))
  :rule-classes :congruence)

Theorem: same-page-implies-logapp<=12-equal

(defthm same-page-implies-logapp<=12-equal
  (implies (and (integerp n)
                (<= n 12)
                (same-page y (double-rewrite x))
                (syntaxp (not (equal x y))))
           (same-page (logapp n x z)
                      (logapp n y z))))

Theorem: same-page-implies-same-page-logheads

(defthm same-page-implies-same-page-logheads
  (implies (same-page a b)
           (same-page (loghead n a) (loghead n b)))
  :rule-classes :congruence)

Theorem: logexting-maintains-same-page

(defthm logexting-maintains-same-page
  (implies (and (integerp n)
                (> n 12)
                (same-page y (double-rewrite x))
                (syntaxp (not (equal x y))))
           (same-page (logext n x) (logext n y))))

Theorem: logtails<=12-equal-implies-same-page

(defthm logtails<=12-equal-implies-same-page
  (implies (and (integerp x)
                (integerp y)
                (natp n)
                (<= n 12)
                (equal (logtail n x) (logtail n y)))
           (same-page x y)))