• 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

Create-qword-address-list

Signature

(create-qword-address-list count addr) → *

Arguments

count — Guard (natp count).

Definitions and Theorems

Theorem: n52p-left-shifting-a-40-bit-natp-by-12

(defthm n52p-left-shifting-a-40-bit-natp-by-12
  (implies (unsigned-byte-p 40 x)
           (unsigned-byte-p 52 (+ 4095 (ash x 12))))
  :rule-classes (:rewrite))

Theorem: n52p-left-shifting-a-40-bit-natp-by-12-+-7

(defthm n52p-left-shifting-a-40-bit-natp-by-12-+-7
  (implies (unsigned-byte-p 40 x)
           (unsigned-byte-p 52 (+ 7 (ash x 12))))
  :rule-classes (:rewrite))

Theorem: loghead-3-+8-addr

(defthm loghead-3-+8-addr
  (implies (equal (loghead 3 addr) 0)
           (equal (loghead 3 (+ 8 addr)) 0)))

Function: create-qword-address-list

(defun create-qword-address-list (count addr)
 (declare (type (unsigned-byte 52) addr))
 (declare (xargs :guard (natp count)))
 (declare
      (xargs :guard (physical-address-p (+ -1 (ash count 3) addr))))
 (let ((__function__ 'create-qword-address-list))
   (declare (ignorable __function__))
   (if (or (zp count)
           (not (physical-address-p addr))
           (not (physical-address-p (+ 7 addr))))
       nil
     (if (equal count 1)
         (list addr)
       (cons addr
             (create-qword-address-list (1- count)
                                        (+ 8 addr)))))))

Theorem: nat-listp-create-qword-address-list

(defthm nat-listp-create-qword-address-list
  (nat-listp (create-qword-address-list count addr))
  :rule-classes :type-prescription)

Theorem: qword-paddr-listp-create-qword-address-list

(defthm qword-paddr-listp-create-qword-address-list
  (qword-paddr-listp (create-qword-address-list count addr)))

Theorem: mult-8-qword-paddr-listp-create-qword-address-list

(defthm mult-8-qword-paddr-listp-create-qword-address-list
  (implies (equal (loghead 3 addr) 0)
           (mult-8-qword-paddr-listp
                (create-qword-address-list count addr))))

Theorem: create-qword-address-list-1

(defthm create-qword-address-list-1
  (implies (and (physical-address-p (+ 7 addr))
                (physical-address-p addr))
           (equal (create-qword-address-list 1 addr)
                  (list addr))))

Theorem: non-nil-create-qword-address-list

(defthm non-nil-create-qword-address-list
  (implies (and (posp count)
                (physical-address-p addr)
                (physical-address-p (+ 7 addr)))
           (create-qword-address-list count addr)))

Theorem: consp-create-qword-address-list

(defthm consp-create-qword-address-list
  (implies (and (physical-address-p addr)
                (physical-address-p (+ 7 addr))
                (posp count))
           (consp (create-qword-address-list count addr)))
  :rule-classes (:type-prescription :rewrite))

Theorem: car-of-create-qword-address-list

(defthm car-of-create-qword-address-list
  (implies (and (posp count)
                (physical-address-p addr)
                (physical-address-p (+ 7 addr)))
           (equal (car (create-qword-address-list count addr))
                  addr)))

Theorem: member-p-create-qword-address-list

(defthm member-p-create-qword-address-list
  (implies (and (<= addr x)
                (< x (+ (ash count 3) addr))
                (equal (loghead 3 addr) 0)
                (equal (loghead 3 x) 0)
                (physical-address-p x)
                (physical-address-p addr))
           (equal (member-p x
                            (create-qword-address-list count addr))
                  t)))

Theorem: not-member-p-create-qword-address-list

(defthm not-member-p-create-qword-address-list
  (implies (or (not (<= addr x))
               (not (< x (+ (ash count 3) addr))))
           (equal (member-p x
                            (create-qword-address-list count addr))
                  nil)))

Theorem: no-duplicates-p-create-qword-address-list

(defthm no-duplicates-p-create-qword-address-list
  (no-duplicates-p (create-qword-address-list count addr)))