		Search-engine friendly clone of the ACL2 documentation.

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