• 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
            • 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
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Reasoning-about-page-tables

Mult-8-qword-paddr-listp

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

Signature

(mult-8-qword-paddr-listp xs) → *

Definitions and Theorems

Function: mult-8-qword-paddr-listp

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

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

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

Theorem: mult-8-qword-paddr-listp-and-append

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

Theorem: mult-8-qword-paddr-listp-remove-duplicates-equal

(defthm mult-8-qword-paddr-listp-remove-duplicates-equal
  (implies
       (mult-8-qword-paddr-listp addrs)
       (mult-8-qword-paddr-listp (remove-duplicates-equal addrs))))

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

(defthm qword-paddrp-element-of-mult-8-qword-paddr-listp
 (implies (and (mult-8-qword-paddr-listp xs)
               (natp m)
               (< m (len xs)))
          (unsigned-byte-p 52 (nth m xs)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (and (mult-8-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 (mult-8-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-mult-8-qword-paddr-listp

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

Theorem: member-p-and-mult-8-qword-paddr-listp

(defthm member-p-and-mult-8-qword-paddr-listp
  (implies (and (member-p index addrs)
                (mult-8-qword-paddr-listp addrs))
           (and (physical-address-p index)
                (equal (loghead 3 index) 0)))
  :rule-classes (:rewrite :forward-chaining))