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

• Reasoning-about-page-tables

Qword-paddr-listp

Recognizer for a list of physical addresses that can accommodate a quadword

Signature

(qword-paddr-listp xs) → *

Definitions and Theorems

Function: qword-paddr-listp

(defun qword-paddr-listp (xs)
  (declare (xargs :guard t))
  (let ((__function__ 'qword-paddr-listp))
    (declare (ignorable __function__))
    (if (consp xs)
        (and (physical-address-p (car xs))
             (physical-address-p (+ 7 (car xs)))
             (qword-paddr-listp (cdr xs)))
      (equal xs nil))))

Theorem: qword-paddr-listp-implies-true-listp

(defthm qword-paddr-listp-implies-true-listp
  (implies (qword-paddr-listp xs)
           (true-listp xs))
  :rule-classes :forward-chaining)

Theorem: qword-paddr-listp-and-append

(defthm qword-paddr-listp-and-append
  (implies (and (qword-paddr-listp a)
                (qword-paddr-listp b))
           (qword-paddr-listp (append a b))))

Theorem: qword-paddr-listp-and-remove-duplicates-equal

(defthm qword-paddr-listp-and-remove-duplicates-equal
  (implies (qword-paddr-listp a)
           (qword-paddr-listp (remove-duplicates-equal a))))

Theorem: qword-paddrp-element-of-qword-paddr-listp

(defthm qword-paddrp-element-of-qword-paddr-listp
 (implies (and (qword-paddr-listp xs)
               (natp m)
               (< m (len xs)))
          (unsigned-byte-p 52 (nth m xs)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (and (qword-paddr-listp xs)
                               (natp m)
                               (< m (len xs)))
                          (natp (nth m xs)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (implies (and (qword-paddr-listp xs)
                            (natp m)
                            (< m (len xs)))
                       (and (<= 0 (nth m xs))
                            (< (nth m xs) 4503599627370496)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: nthcdr-qword-paddr-listp

(defthm nthcdr-qword-paddr-listp
  (implies (qword-paddr-listp xs)
           (qword-paddr-listp (nthcdr n xs)))
  :rule-classes (:rewrite :type-prescription))