• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-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
          • Addr-range
          • Read-from-physical-memory
          • Write-to-physical-memory
          • Rm-low-32
          • Wm-low-32
          • Rm-low-64
          • Create-physical-address-list
          • Wm-low-64
          • Physical-address-listp
          • Physical-address-p
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Physical-memory

Addr-range

Signature

(addr-range count addr) → *

Definitions and Theorems

Function: addr-range

(defun addr-range (count addr)
  (declare (xargs :guard (natp count)))
  (let ((__function__ 'addr-range))
    (declare (ignorable __function__))
    (if (zp count)
        nil
      (cons (ifix addr)
            (addr-range (1- count)
                        (1+ (ifix addr)))))))

Theorem: neg-addr-range=nil

(defthm neg-addr-range=nil
  (implies (negp i)
           (equal (addr-range i n) nil)))

Theorem: true-listp-addr-range

(defthm true-listp-addr-range
  (true-listp (addr-range count addr))
  :rule-classes :type-prescription)

Theorem: addr-range-1

(defthm addr-range-1
  (equal (addr-range 1 x)
         (list (ifix x))))

Theorem: len-of-addr-range

(defthm len-of-addr-range
  (implies (natp n)
           (equal (len (addr-range n val)) n)))

Theorem: physical-address-listp-addr-range

(defthm physical-address-listp-addr-range
  (implies (and (physical-address-p lin-addr)
                (physical-address-p (+ -1 n lin-addr)))
           (physical-address-listp (addr-range n lin-addr))))

Theorem: member-p-addr-range

(defthm member-p-addr-range
  (implies (and (<= prog-addr addr)
                (< addr (+ n prog-addr))
                (integerp n)
                (integerp addr)
                (integerp prog-addr))
           (equal (member-p addr (addr-range n prog-addr))
                  t)))

Theorem: member-p-addr-range-from-member-p-addr-range

(defthm member-p-addr-range-from-member-p-addr-range
  (implies (and (member-p x (addr-range j y))
                (integerp l)
                (< j l))
           (equal (member-p x (addr-range l y))
                  t)))

Theorem: not-member-p-addr-range

(defthm not-member-p-addr-range
  (implies (and (or (< addr prog-addr)
                    (<= (+ n prog-addr) addr))
                (integerp prog-addr))
           (equal (member-p addr (addr-range n prog-addr))
                  nil)))

Theorem: not-member-p-addr-range-from-not-member-p-addr-range

(defthm not-member-p-addr-range-from-not-member-p-addr-range
  (implies (and (not (member-p x (addr-range j y)))
                (integerp j)
                (<= l j))
           (equal (member-p x (addr-range l y))
                  nil)))

Theorem: subset-p-two-addr-ranges

(defthm subset-p-two-addr-ranges
  (implies (and (integerp x)
                (integerp y)
                (<= y x)
                (<= (+ i x) (+ j y))
                (integerp j))
           (subset-p (addr-range i x)
                     (addr-range j y))))

Theorem: not-disjoint-p-two-addr-ranges-thm

(defthm not-disjoint-p-two-addr-ranges-thm
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j)
                (<= x y)
                (< y (+ i x))
                (<= (+ i x) (+ j y)))
           (equal (disjoint-p (addr-range i x)
                              (addr-range j y))
                  nil)))

Theorem: disjoint-p-two-addr-ranges-thm-0

(defthm disjoint-p-two-addr-ranges-thm-0
  (implies (and (integerp x)
                (integerp y)
                (integerp j)
                (< 0 j)
                (<= (+ i x) y))
           (disjoint-p (addr-range i x)
                       (addr-range j y))))

Theorem: disjoint-p-two-addr-ranges-thm-1

(defthm disjoint-p-two-addr-ranges-thm-1
  (implies (and (integerp x)
                (integerp y)
                (integerp j)
                (< 0 j)
                (<= (+ j y) x))
           (disjoint-p (addr-range i x)
                       (addr-range j y))))

Theorem: disjoint-p-two-addr-ranges-thm-2

(defthm disjoint-p-two-addr-ranges-thm-2
  (implies (and (disjoint-p (addr-range i x)
                            (addr-range j y))
                (subset-p (addr-range ia a)
                          (addr-range i x))
                (subset-p (addr-range jb b)
                          (addr-range j y)))
           (disjoint-p (addr-range ia a)
                       (addr-range jb b))))

Theorem: disjoint-p-two-addr-ranges-thm-3

(defthm disjoint-p-two-addr-ranges-thm-3
  (implies (and (disjoint-p (addr-range j y)
                            (addr-range i x))
                (subset-p (addr-range ia a)
                          (addr-range i x))
                (subset-p (addr-range jb b)
                          (addr-range j y)))
           (disjoint-p (addr-range ia a)
                       (addr-range jb b))))

Theorem: consp-addr-range

(defthm consp-addr-range
  (implies (posp n)
           (consp (addr-range n val)))
  :rule-classes (:type-prescription :rewrite))

Theorem: car-addr-range

(defthm car-addr-range
  (implies (posp n)
           (equal (car (addr-range n val))
                  (ifix val))))

Theorem: cdr-addr-range

(defthm cdr-addr-range
  (implies (and (posp n) (integerp val))
           (equal (cdr (addr-range n val))
                  (addr-range (1- n) (1+ val)))))

Theorem: no-duplicates-p-and-addr-range

(defthm no-duplicates-p-and-addr-range
  (no-duplicates-p (addr-range n x)))

Theorem: instance-of-pos-1-accumulator-thm

(defthm instance-of-pos-1-accumulator-thm
  (implies (and (member-p e x) (natp acc))
           (equal (pos-1 e x (+ 1 acc))
                  (+ 1 (pos-1 e x acc)))))

Theorem: nth-pos-of-addr-range

(defthm nth-pos-of-addr-range
  (implies (and (<= index i)
                (< i (+ n index))
                (integerp index)
                (integerp i)
                (posp n))
           (equal (pos i (addr-range n index))
                  (- i index))))

Theorem: addr-range-ifix

(defthm addr-range-ifix
  (equal (addr-range n (ifix x))
         (addr-range n x)))

Theorem: integerp-addr-range-member

(defthm integerp-addr-range-member
  (implies (member-p x (addr-range n m))
           (integerp x)))

Theorem: addr-range-not-member-out-of-range

(defthm addr-range-not-member-out-of-range
  (implies (and (natp n)
                (integerp addr)
                (< el addr)
                (>= el (+ addr n)))
           (not (member-p el (addr-range n addr)))))