		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Reasoning-about-memory-reads-and-writes

Definitions of rb and wb

The functions rb (read bytes) and wb (write bytes) are used in reasoning about memory reads and writes. Functions like rml08, rml16, rml32, and rml64 are reduced to rb, and wml08, wml16, wml32, and wml64 to wb during reasoning.

Definitions and Theorems

Function: canonical-address-listp

(defun canonical-address-listp (lst)
  (declare (xargs :guard t))
  (let ((__function__ 'canonical-address-listp))
    (declare (ignorable __function__))
    (if (equal lst nil)
        t
      (and (consp lst)
           (canonical-address-p (car lst))
           (canonical-address-listp (cdr lst))))))

Theorem: cdr-canonical-address-listp

(defthm cdr-canonical-address-listp
  (implies (canonical-address-listp x)
           (canonical-address-listp (cdr x))))

Function: create-canonical-address-list

(defun create-canonical-address-list (count addr)
  (declare (xargs :guard (natp count)))
  (let ((__function__ 'create-canonical-address-list))
    (declare (ignorable __function__))
    (if (or (zp count)
            (not (canonical-address-p addr)))
        nil
      (cons addr
            (create-canonical-address-list (1- count)
                                           (1+ addr))))))

Theorem: true-listp-create-canonical-address-list

(defthm true-listp-create-canonical-address-list
  (true-listp (create-canonical-address-list cnt lin-addr))
  :rule-classes (:rewrite :type-prescription))

Theorem: canonical-address-listp-create-canonical-address-list

(defthm canonical-address-listp-create-canonical-address-list
  (canonical-address-listp
       (create-canonical-address-list count addr))
  :rule-classes (:rewrite :type-prescription))

Theorem: create-canonical-address-list-1

(defthm create-canonical-address-list-1
  (implies (canonical-address-p x)
           (equal (create-canonical-address-list 1 x)
                  (list x))))

Theorem: len-of-create-canonical-address-list

(defthm len-of-create-canonical-address-list
  (implies (and (canonical-address-p (+ -1 addr count))
                (canonical-address-p addr)
                (natp count))
           (equal (len (create-canonical-address-list count addr))
                  count)))

Theorem: car-create-canonical-address-list

(defthm car-create-canonical-address-list
  (implies (and (canonical-address-p addr)
                (posp count))
           (equal (car (create-canonical-address-list count addr))
                  addr)))

Theorem: cdr-create-canonical-address-list

(defthm cdr-create-canonical-address-list
  (implies (and (canonical-address-p addr)
                (posp count))
           (equal (cdr (create-canonical-address-list count addr))
                  (create-canonical-address-list (1- count)
                                                 (1+ addr)))))

Theorem: consp-of-create-canonical-address-list

(defthm consp-of-create-canonical-address-list
  (implies (and (canonical-address-p addr)
                (natp count)
                (< 0 count))
           (consp (create-canonical-address-list count addr))))

Theorem: create-canonical-address-list-split

(defthm create-canonical-address-list-split
 (implies
     (and (canonical-address-p addr)
          (canonical-address-p (+ k addr))
          (natp j)
          (natp k))
     (equal (create-canonical-address-list (+ k j)
                                           addr)
            (append (create-canonical-address-list k addr)
                    (create-canonical-address-list j (+ k addr))))))

Function: rb-1

(defun rb-1 (n addr r-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :r :x) r-x))
  (declare (xargs :guard (and (natp n) (integerp addr))))
  (declare (xargs :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'rb-1))
    (declare (ignorable __function__))
    (if (zp n)
        (mv nil 0 x86)
      (b* (((unless (canonical-address-p addr))
            (mv 'rb-1 0 x86))
           ((mv flg0 byte0 x86) (rvm08 addr x86))
           ((when flg0) (mv flg0 0 x86))
           ((mv rest-flg rest-bytes x86)
            (rb-1 (1- n) (1+ addr) r-x x86)))
        (mv rest-flg
            (logior byte0 (ash rest-bytes 8))
            x86)))))

Theorem: natp-of-rb-1.val

(defthm natp-of-rb-1.val
  (b* (((mv ?flg ?val ?new-x86)
        (rb-1 n addr r-x x86)))
    (natp val))
  :rule-classes :type-prescription)

Theorem: x86p-of-rb-1.new-x86

(defthm x86p-of-rb-1.new-x86
  (implies (x86p x86)
           (b* (((mv ?flg ?val ?new-x86)
                 (rb-1 n addr r-x x86)))
             (x86p new-x86)))
  :rule-classes :rewrite)

Theorem: integerp-of-mv-nth-1-rb-1

(defthm integerp-of-mv-nth-1-rb-1
  (b* (((mv ?flg ?val ?new-x86)
        (rb-1 n addr r-x x86)))
    (integerp val))
  :rule-classes :type-prescription)

Theorem: rb-1-returns-x86

(defthm rb-1-returns-x86
  (b* (((mv ?flg ?val ?new-x86)
        (rb-1 n addr r-x x86)))
    (implies t (equal new-x86 x86))))

Theorem: rb-1-returns-no-error

(defthm rb-1-returns-no-error
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr)))
           (equal (mv-nth 0 (rb-1 n addr r-x x86))
                  nil)))

Theorem: size-of-rb-1

(defthm size-of-rb-1
 (implies (and (equal m (ash n 3)) (natp n))
          (unsigned-byte-p m (mv-nth 1 (rb-1 n addr r-x x86))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary (implies (and (equal m (ash n 3)) (natp n))
                       (and (<= 0 (mv-nth 1 (rb-1 n addr r-x x86)))
                            (< (mv-nth 1 (rb-1 n addr r-x x86))
                               (expt 2 m))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: las-to-pas

(defun las-to-pas (n lin-addr r-w-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :r :w :x) r-w-x))
  (declare (xargs :guard (and (natp n) (integerp lin-addr))))
  (declare (xargs :guard (not (app-view x86))))
  (let ((__function__ 'las-to-pas))
    (declare (ignorable __function__))
    (if (zp n)
        (mv nil nil x86)
      (b* (((unless (canonical-address-p lin-addr))
            (mv t nil x86))
           ((mv flg p-addr x86)
            (ia32e-la-to-pa lin-addr r-w-x x86))
           ((when flg) (mv flg nil x86))
           ((mv flg p-addrs x86)
            (las-to-pas (1- n)
                        (1+ lin-addr)
                        r-w-x x86)))
        (mv flg (if flg nil (cons p-addr p-addrs))
            x86)))))

Theorem: true-listp-of-las-to-pas.p-addrs

(defthm true-listp-of-las-to-pas.p-addrs
  (b* (((mv ?flg ?p-addrs ?x86)
        (las-to-pas n lin-addr r-w-x x86)))
    (true-listp p-addrs))
  :rule-classes (:rewrite :type-prescription))

Theorem: x86p-of-las-to-pas.x86

(defthm x86p-of-las-to-pas.x86
  (implies (x86p x86)
           (b* (((mv ?flg ?p-addrs ?x86)
                 (las-to-pas n lin-addr r-w-x x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Theorem: consp-mv-nth-1-las-to-pas

(defthm consp-mv-nth-1-las-to-pas
  (implies (and (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
                (not (zp n)))
           (consp (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))
  :rule-classes (:rewrite :type-prescription))

Theorem: car-mv-nth-1-las-to-pas

(defthm car-mv-nth-1-las-to-pas
  (implies (and (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
                (not (zp n)))
           (equal (car (mv-nth 1 (las-to-pas n lin-addr r-w-x x86)))
                  (mv-nth 1
                          (ia32e-la-to-pa lin-addr r-w-x x86)))))

Theorem: physical-address-listp-mv-nth-1-las-to-pas

(defthm physical-address-listp-mv-nth-1-las-to-pas
  (physical-address-listp
       (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: las-to-pas-n=0

(defthm las-to-pas-n=0
  (and (equal (mv-nth 0 (las-to-pas 0 lin-addr r-w-x x86))
              nil)
       (equal (mv-nth 1 (las-to-pas 0 lin-addr r-w-x x86))
              nil)
       (equal (mv-nth 2 (las-to-pas 0 lin-addr r-w-x x86))
              x86)))

Theorem: xr-las-to-pas

(defthm xr-las-to-pas
  (implies (and (not (equal fld :tlb))
                (not (equal fld :mem))
                (not (equal fld :fault)))
           (equal (xr fld index
                      (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
                  (xr fld index x86))))

Theorem: xr-rflags-las-to-pas

(defthm xr-rflags-las-to-pas
 (implies
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (equal (xr :rflags nil
              (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
          (xr :rflags nil (double-rewrite x86)))))

Theorem: xr-fault-las-to-pas

(defthm xr-fault-las-to-pas
 (implies
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (equal (xr :fault nil
              (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
          (xr :fault nil (double-rewrite x86)))))

Theorem: las-to-pas-xw-values

(defthm las-to-pas-xw-values
 (implies
  (and (not (equal fld :mem))
       (not (equal fld :rflags))
       (not (equal fld :fault))
       (not (equal fld :ctr))
       (not (equal fld :msr))
       (not (equal fld :app-view))
       (not (equal fld :marking-view))
       (not (equal fld :seg-visible))
       (not (equal fld :tlb))
       (not (equal fld :implicit-supervisor-access)))
  (and
    (equal
         (mv-nth 0
                 (las-to-pas n
                             lin-addr r-w-x (xw fld index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
    (equal
         (mv-nth 1
                 (las-to-pas n
                             lin-addr r-w-x (xw fld index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))))

Theorem: 64-bit-modep-of-las-to-pas

(defthm 64-bit-modep-of-las-to-pas
  (equal (64-bit-modep (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-las-to-pas

(defthm x86-operation-mode-of-las-to-pas
 (equal
   (x86-operation-mode (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
   (x86-operation-mode x86)))

Theorem: las-to-pas-xw-state

(defthm las-to-pas-xw-state
 (implies
  (and (not (equal fld :mem))
       (not (equal fld :rflags))
       (not (equal fld :fault))
       (not (equal fld :ctr))
       (not (equal fld :msr))
       (not (equal fld :app-view))
       (not (equal fld :marking-view))
       (not (equal fld :seg-visible))
       (not (equal fld :tlb))
       (not (equal fld :implicit-supervisor-access)))
  (equal (mv-nth 2
                 (las-to-pas n
                             lin-addr r-w-x (xw fld index val x86)))
         (xw fld index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86))))))

Theorem: las-to-pas-xw-rflags-not-ac

(defthm las-to-pas-xw-rflags-not-ac
 (implies
  (equal (rflagsbits->ac value)
         (rflagsbits->ac (rflags (double-rewrite x86))))
  (and
   (equal
        (mv-nth 0
                (las-to-pas n lin-addr
                            r-w-x (xw :rflags nil value x86)))
        (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (equal (mv-nth 1
                  (las-to-pas n lin-addr
                              r-w-x (xw :rflags nil value x86)))
          (mv-nth 1
                  (las-to-pas n lin-addr
                              r-w-x (double-rewrite x86)))))))

Theorem: las-to-pas-xw-rflags-state-not-ac

(defthm las-to-pas-xw-rflags-state-not-ac
  (implies
       (equal (rflagsbits->ac value)
              (rflagsbits->ac (rflags x86)))
       (equal (mv-nth 2
                      (las-to-pas n lin-addr
                                  r-w-x (xw :rflags nil value x86)))
              (xw :rflags nil value
                  (mv-nth 2 (las-to-pas n lin-addr r-w-x x86))))))

Theorem: len-of-mv-nth-1-las-to-pas

(defthm len-of-mv-nth-1-las-to-pas
  (implies (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
           (equal (len (mv-nth 1 (las-to-pas n lin-addr r-w-x x86)))
                  (nfix n))))

Function: read-from-physical-memory

(defun read-from-physical-memory (p-addrs x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (physical-address-listp p-addrs)))
  (declare (xargs :guard (not (app-view x86))))
  (let ((__function__ 'read-from-physical-memory))
    (declare (ignorable __function__))
    (if (endp p-addrs)
        0
      (b* ((addr0 (car p-addrs))
           (byte0 (memi addr0 x86))
           (rest-bytes (read-from-physical-memory (cdr p-addrs)
                                                  x86)))
        (logior byte0 (ash rest-bytes 8))))))

Theorem: integerp-of-read-from-physical-memory

(defthm integerp-of-read-from-physical-memory
  (b* ((value (read-from-physical-memory p-addrs x86)))
    (integerp value))
  :rule-classes :type-prescription)

Theorem: size-of-read-from-physical-memory

(defthm size-of-read-from-physical-memory
 (implies (equal n (ash (len p-addrs) 3))
          (unsigned-byte-p n
                           (read-from-physical-memory p-addrs x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (implies (equal n (ash (len p-addrs) 3))
               (natp (read-from-physical-memory p-addrs x86)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies (equal n (ash (len p-addrs) 3))
            (and (<= 0
                     (read-from-physical-memory p-addrs x86))
                 (< (read-from-physical-memory p-addrs x86)
                    (expt 2 n))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: read-from-physical-memory-xw-rflags

(defthm read-from-physical-memory-xw-rflags
 (equal (read-from-physical-memory p-addrs (xw :rflags nil val x86))
        (read-from-physical-memory p-addrs x86)))

Theorem: read-from-physical-memory-xw-not-mem

(defthm read-from-physical-memory-xw-not-mem
 (implies
   (not (equal fld :mem))
   (equal (read-from-physical-memory p-addrs (xw fld index val x86))
          (read-from-physical-memory p-addrs x86))))

Function: rb

(defun rb (n addr r-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :r :x) r-x))
  (declare (xargs :guard (and (natp n) (integerp addr))))
  (declare (xargs :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'rb))
    (declare (ignorable __function__))
    (if (app-view x86)
        (rb-1 n addr r-x x86)
      (b* (((mv flg p-addrs x86)
            (las-to-pas n addr r-x x86))
           ((when flg) (mv flg 0 x86))
           (val (read-from-physical-memory p-addrs x86)))
        (mv nil val x86)))))

Theorem: integerp-of-rb.val

(defthm integerp-of-rb.val
  (b* (((mv ?flg ?val ?new-x86)
        (rb n addr r-x x86)))
    (integerp val))
  :rule-classes :type-prescription)

Theorem: x86p-of-rb.new-x86

(defthm x86p-of-rb.new-x86
  (implies (x86p x86)
           (b* (((mv ?flg ?val ?new-x86)
                 (rb n addr r-x x86)))
             (x86p new-x86)))
  :rule-classes :rewrite)

Theorem: natp-of-mv-nth-1-rb

(defthm natp-of-mv-nth-1-rb
  (b* (((mv ?flg ?val ?new-x86)
        (rb n addr r-x x86)))
    (natp val))
  :rule-classes :type-prescription)

Theorem: rb-no-reads-when-zp-n

(defthm rb-no-reads-when-zp-n
  (b* (((mv ?flg ?val ?new-x86)
        (rb n addr r-x x86)))
    (implies (zp n) (equal val 0))))

Theorem: rb-is-rb-1-for-app-view

(defthm rb-is-rb-1-for-app-view
  (implies (app-view x86)
           (equal (rb n addr r-x x86)
                  (rb-1 n addr r-x x86))))

Theorem: rb-returns-no-error-app-view

(defthm rb-returns-no-error-app-view
  (implies (and (app-view x86)
                (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr)))
           (equal (mv-nth 0 (rb n addr r-x x86))
                  nil)))

Theorem: rb-returns-x86-app-view

(defthm rb-returns-x86-app-view
  (implies (app-view x86)
           (equal (mv-nth 2 (rb n addr r-x x86))
                  x86)))

Theorem: size-of-rb

(defthm size-of-rb
 (implies (and (equal m (ash n 3)) (natp n))
          (unsigned-byte-p m (mv-nth 1 (rb n addr r-x x86))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary (implies (and (equal m (ash n 3)) (natp n))
                       (and (<= 0 (mv-nth 1 (rb n addr r-x x86)))
                            (< (mv-nth 1 (rb n addr r-x x86))
                               (expt 2 m))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: size-of-rb-in-app-view

(defthm size-of-rb-in-app-view
 (implies (and (app-view x86) (natp n))
          (unsigned-byte-p (ash n 3)
                           (mv-nth 1 (rb n addr r-x x86))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary (implies (and (app-view x86) (natp n))
                       (and (<= 0 (mv-nth 1 (rb n addr r-x x86)))
                            (< (mv-nth 1 (rb n addr r-x x86))
                               (expt 2 (ash n 3)))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: rb-values-and-xw-rflags-in-sys-view

(defthm rb-values-and-xw-rflags-in-sys-view
 (implies
     (and (equal (rflagsbits->ac (double-rewrite value))
                 (rflagsbits->ac (rflags x86)))
          (not (app-view x86))
          (x86p x86))
     (and (equal (mv-nth 0
                         (rb n addr r-x (xw :rflags nil value x86)))
                 (mv-nth 0 (rb n addr r-x (double-rewrite x86))))
          (equal (mv-nth 1
                         (rb n addr r-x (xw :rflags nil value x86)))
                 (mv-nth 1
                         (rb n addr r-x (double-rewrite x86)))))))

Theorem: 64-bit-modep-of-rb

(defthm 64-bit-modep-of-rb
  (equal (64-bit-modep (mv-nth 2 (rb n addr r-x x86)))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-rb

(defthm x86-operation-mode-of-rb
  (equal (x86-operation-mode (mv-nth 2 (rb n addr r-x x86)))
         (x86-operation-mode x86)))

Function: wb-1

(defun wb-1 (n addr w value x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :w) w))
  (declare (xargs :guard (and (natp n)
                              (integerp addr)
                              (natp value))))
  (declare (xargs :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'wb-1))
    (declare (ignorable __function__))
    (if (zp n)
        (mv nil x86)
      (b* (((unless (canonical-address-p addr))
            (mv t x86))
           ((mv flg0 x86)
            (wvm08 addr (loghead 8 value) x86))
           ((when flg0) (mv flg0 x86))
           ((mv rest-flg x86)
            (wb-1 (1- n)
                  (1+ addr)
                  w (logtail 8 value)
                  x86)))
        (mv rest-flg x86)))))

Theorem: wb-1-returns-x86p

(defthm wb-1-returns-x86p
  (implies (x86p x86)
           (x86p (mv-nth 1 (wb-1 n addr w value x86)))))

Theorem: wb-1-returns-no-error

(defthm wb-1-returns-no-error
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr)))
           (equal (mv-nth 0 (wb-1 n addr w value x86))
                  nil)))

Function: write-to-physical-memory

(defun write-to-physical-memory (p-addrs value x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (and (physical-address-listp p-addrs)
                              (natp value))))
  (declare (xargs :guard (not (app-view x86))))
  (let ((__function__ 'write-to-physical-memory))
    (declare (ignorable __function__))
    (if (endp p-addrs)
        x86
      (b* ((addr0 (car p-addrs))
           (byte0 (loghead 8 value))
           (x86 (!memi addr0 byte0 x86)))
        (write-to-physical-memory (cdr p-addrs)
                                  (logtail 8 value)
                                  x86)))))

Theorem: x86p-write-to-physical-memory

(defthm x86p-write-to-physical-memory
  (implies (and (x86p x86)
                (physical-address-listp p-addrs))
           (x86p (write-to-physical-memory p-addrs value x86))))

Theorem: xr-not-mem-write-to-physical-memory

(defthm xr-not-mem-write-to-physical-memory
  (implies (not (equal fld :mem))
           (equal (xr fld index
                      (write-to-physical-memory p-addrs bytes x86))
                  (xr fld index x86))))

Theorem: write-to-physical-memory-xw-in-sys-view

(defthm write-to-physical-memory-xw-in-sys-view
 (implies
  (not (equal fld :mem))
  (equal
   (write-to-physical-memory p-addrs bytes (xw fld index value x86))
   (xw fld index value
       (write-to-physical-memory p-addrs bytes x86)))))

Theorem: 64-bit-modep-of-write-to-physical-memory

(defthm 64-bit-modep-of-write-to-physical-memory
  (equal (64-bit-modep (write-to-physical-memory p-addrs value x86))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-write-to-physical-memory

(defthm x86-operation-mode-of-write-to-physical-memory
 (equal
   (x86-operation-mode (write-to-physical-memory p-addrs value x86))
   (x86-operation-mode x86)))

Function: wb

(defun wb (n addr w value x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :w) w))
  (declare (xargs :guard (and (natp n)
                              (integerp addr)
                              (natp value))))
  (declare (xargs :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'wb))
    (declare (ignorable __function__))
    (if (app-view x86)
        (wb-1 n addr w value x86)
      (b* (((mv flg p-addrs x86)
            (las-to-pas n addr :w x86))
           ((when flg) (mv flg x86))
           (x86 (write-to-physical-memory p-addrs value x86)))
        (mv nil x86)))))

Theorem: wb-no-writes-when-zp-n

(defthm wb-no-writes-when-zp-n
  (equal (mv-nth 1 (wb 0 addr val w x86))
         x86))

Theorem: wb-is-wb-1-for-app-view

(defthm wb-is-wb-1-for-app-view
  (implies (app-view x86)
           (equal (wb n addr w value x86)
                  (wb-1 n addr w value x86))))

Theorem: x86p-of-wb

(defthm x86p-of-wb
  (implies (x86p x86)
           (x86p (mv-nth 1 (wb n addr w value x86)))))

Theorem: wb-returns-no-error-app-view

(defthm wb-returns-no-error-app-view
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr))
                (app-view x86))
           (equal (mv-nth 0 (wb n addr w value x86))
                  nil)))

Theorem: wb-by-wb-1-for-app-view-induction-rule

(defthm wb-by-wb-1-for-app-view-induction-rule
  t
  :rule-classes ((:induction :pattern (wb n addr w value x86)
                             :condition (app-view x86)
                             :scheme (wb-1 n addr w value x86))))

Theorem: xr-rb-state-in-app-view

(defthm xr-rb-state-in-app-view
  (implies (app-view x86)
           (equal (xr fld
                      index (mv-nth 2 (rb n addr r-x x86)))
                  (xr fld index x86))))

Theorem: rb-xw-values-in-app-view

(defthm rb-xw-values-in-app-view
  (implies
       (and (app-view x86)
            (not (equal fld :mem))
            (not (equal fld :app-view)))
       (and (equal (mv-nth 0
                           (rb n addr r-x (xw fld index value x86)))
                   (mv-nth 0 (rb n addr r-x x86)))
            (equal (mv-nth 1
                           (rb n addr r-x (xw fld index value x86)))
                   (mv-nth 1 (rb n addr r-x x86))))))

Theorem: rb-xw-state-in-app-view

(defthm rb-xw-state-in-app-view
  (implies (and (app-view x86)
                (not (equal fld :app-view)))
           (equal (mv-nth 2
                          (rb n addr r-x (xw fld index value x86)))
                  (xw fld index
                      value (mv-nth 2 (rb n addr r-x x86))))))

Theorem: xr-rb-1-state-in-sys-view

(defthm xr-rb-1-state-in-sys-view
  (implies (and (not (app-view x86))
                (not (equal fld :mem))
                (not (equal fld :fault)))
           (equal (xr fld
                      index (mv-nth 2 (rb-1 n addr r-x x86)))
                  (xr fld index x86))))

Theorem: xr-rb

(defthm xr-rb
  (implies (and (not (equal fld :mem))
                (not (equal fld :fault))
                (not (equal fld :tlb)))
           (equal (xr fld
                      index (mv-nth 2 (rb n addr r-x x86)))
                  (xr fld index x86))))

Theorem: rb-1-xw-values-in-sys-view

(defthm rb-1-xw-values-in-sys-view
 (implies
     (and (not (equal fld :mem))
          (not (equal fld :rflags))
          (not (equal fld :ctr))
          (not (equal fld :seg-visible))
          (not (equal fld :msr))
          (not (equal fld :fault))
          (not (equal fld :app-view))
          (not (equal fld :marking-view)))
     (and (equal (mv-nth 0
                         (rb-1 n addr r-x (xw fld index value x86)))
                 (mv-nth 0 (rb-1 n addr r-x x86)))
          (equal (mv-nth 1
                         (rb-1 n addr r-x (xw fld index value x86)))
                 (mv-nth 1 (rb-1 n addr r-x x86))))))

Theorem: rb-xw-values

(defthm rb-xw-values
  (implies
       (and (not (equal fld :mem))
            (not (equal fld :rflags))
            (not (equal fld :ctr))
            (not (equal fld :seg-visible))
            (not (equal fld :msr))
            (not (equal fld :fault))
            (not (equal fld :app-view))
            (not (equal fld :marking-view))
            (not (equal fld :tlb))
            (not (equal fld :implicit-supervisor-access)))
       (and (equal (mv-nth 0
                           (rb n addr r-x (xw fld index value x86)))
                   (mv-nth 0 (rb n addr r-x x86)))
            (equal (mv-nth 1
                           (rb n addr r-x (xw fld index value x86)))
                   (mv-nth 1 (rb n addr r-x x86))))))

Theorem: rb-1-xw-rflags-not-ac-values-in-sys-view

(defthm rb-1-xw-rflags-not-ac-values-in-sys-view
 (implies
   (and (not (app-view x86))
        (equal (rflagsbits->ac value)
               (rflagsbits->ac (rflags x86))))
   (and (equal (mv-nth 0
                       (rb-1 n addr r-x (xw :rflags nil value x86)))
               (mv-nth 0 (rb-1 n addr r-x x86)))
        (equal (mv-nth 1
                       (rb-1 n addr r-x (xw :rflags nil value x86)))
               (mv-nth 1 (rb-1 n addr r-x x86))))))

Theorem: rb-xw-rflags-not-ac-values-in-sys-view

(defthm rb-xw-rflags-not-ac-values-in-sys-view
 (implies
     (and (not (app-view x86))
          (equal (rflagsbits->ac value)
                 (rflagsbits->ac (rflags x86))))
     (and (equal (mv-nth 0
                         (rb n addr r-x (xw :rflags nil value x86)))
                 (mv-nth 0 (rb n addr r-x x86)))
          (equal (mv-nth 1
                         (rb n addr r-x (xw :rflags nil value x86)))
                 (mv-nth 1 (rb n addr r-x x86))))))

Theorem: rb-1-xw-state-in-sys-view

(defthm rb-1-xw-state-in-sys-view
 (implies (and (not (equal fld :mem))
               (not (equal fld :rflags))
               (not (equal fld :ctr))
               (not (equal fld :seg-visible))
               (not (equal fld :msr))
               (not (equal fld :fault))
               (not (equal fld :app-view))
               (not (equal fld :marking-view)))
          (equal (mv-nth 2
                         (rb-1 n addr r-x (xw fld index value x86)))
                 (xw fld index value
                     (mv-nth 2 (rb-1 n addr r-x x86))))))

Theorem: rb-xw-state

(defthm rb-xw-state
  (implies (and (not (equal fld :mem))
                (not (equal fld :rflags))
                (not (equal fld :ctr))
                (not (equal fld :seg-visible))
                (not (equal fld :msr))
                (not (equal fld :fault))
                (not (equal fld :app-view))
                (not (equal fld :marking-view))
                (not (equal fld :tlb))
                (not (equal fld :implicit-supervisor-access)))
           (equal (mv-nth 2
                          (rb n addr r-x (xw fld index value x86)))
                  (xw fld index
                      value (mv-nth 2 (rb n addr r-x x86))))))

Theorem: rb-1-xw-rflags-not-ac-state-in-sys-view

(defthm rb-1-xw-rflags-not-ac-state-in-sys-view
  (implies
       (and (not (app-view x86))
            (equal (rflagsbits->ac value)
                   (rflagsbits->ac (rflags x86))))
       (equal (mv-nth 2
                      (rb-1 n addr r-x (xw :rflags nil value x86)))
              (xw :rflags nil value
                  (mv-nth 2 (rb-1 n addr r-x x86))))))

Theorem: rb-xw-rflags-not-ac-state-in-sys-view

(defthm rb-xw-rflags-not-ac-state-in-sys-view
 (implies (and (not (app-view x86))
               (equal (rflagsbits->ac value)
                      (rflagsbits->ac (rflags x86))))
          (equal (mv-nth 2
                         (rb n addr r-x (xw :rflags nil value x86)))
                 (xw :rflags nil
                     value (mv-nth 2 (rb n addr r-x x86))))))

Theorem: xr-wb-1-in-app-view

(defthm xr-wb-1-in-app-view
  (implies (and (app-view x86)
                (not (equal fld :mem)))
           (equal (xr fld index
                      (mv-nth 1 (wb-1 n addr w value x86)))
                  (xr fld index x86))))

Theorem: xr-wb-in-app-view

(defthm xr-wb-in-app-view
  (implies (and (app-view x86)
                (not (equal fld :mem)))
           (equal (xr fld index
                      (mv-nth 1 (wb n addr w value x86)))
                  (xr fld index x86))))

Theorem: wb-1-xw-in-app-view

(defthm wb-1-xw-in-app-view
 (implies
   (and (app-view x86)
        (not (equal fld :mem))
        (not (equal fld :app-view)))
   (and (equal (mv-nth 0
                       (wb-1 n addr w val (xw fld index value x86)))
               (mv-nth 0 (wb-1 n addr w val x86)))
        (equal (mv-nth 1
                       (wb-1 n addr w val (xw fld index value x86)))
               (xw fld index value
                   (mv-nth 1 (wb-1 n addr w val x86)))))))

Theorem: wb-xw-in-app-view

(defthm wb-xw-in-app-view
 (implies
     (and (app-view x86)
          (not (equal fld :mem))
          (not (equal fld :app-view)))
     (and (equal (mv-nth 0
                         (wb n addr w val (xw fld index value x86)))
                 (mv-nth 0 (wb n addr w val x86)))
          (equal (mv-nth 1
                         (wb n addr w val (xw fld index value x86)))
                 (xw fld index value
                     (mv-nth 1 (wb n addr w val x86)))))))

Theorem: xr-wb

(defthm xr-wb
  (implies (and (not (equal fld :mem))
                (not (equal fld :fault))
                (not (equal fld :tlb)))
           (equal (xr fld index
                      (mv-nth 1 (wb n addr w value x86)))
                  (xr fld index x86))))

Theorem: xr-fault-wb-in-system-level-marking-view

(defthm xr-fault-wb-in-system-level-marking-view
  (implies (not (mv-nth 0
                        (las-to-pas n addr
                                    :w (double-rewrite x86))))
           (equal (xr :fault
                      nil (mv-nth 1 (wb n addr w val x86)))
                  (xr :fault nil x86))))

Theorem: 64-bit-modep-of-mv-nth-1-of-wb

(defthm 64-bit-modep-of-mv-nth-1-of-wb
  (equal (64-bit-modep (mv-nth 1 (wb n addr w value x86)))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-mv-nth-1-of-wb

(defthm x86-operation-mode-of-mv-nth-1-of-wb
  (equal (x86-operation-mode (mv-nth 1 (wb n addr w value x86)))
         (x86-operation-mode x86)))

Theorem: wb-xw-values

(defthm wb-xw-values
 (implies (and (not (equal fld :mem))
               (not (equal fld :rflags))
               (not (equal fld :ctr))
               (not (equal fld :seg-visible))
               (not (equal fld :msr))
               (not (equal fld :fault))
               (not (equal fld :app-view))
               (not (equal fld :marking-view))
               (not (equal fld :tlb))
               (not (equal fld :implicit-supervisor-access)))
          (equal (mv-nth 0
                         (wb n addr w value (xw fld index val x86)))
                 (mv-nth 0 (wb n addr w value x86)))))

Theorem: wb-xw-state

(defthm wb-xw-state
 (implies (and (not (equal fld :mem))
               (not (equal fld :rflags))
               (not (equal fld :ctr))
               (not (equal fld :seg-visible))
               (not (equal fld :msr))
               (not (equal fld :fault))
               (not (equal fld :app-view))
               (not (equal fld :marking-view))
               (not (equal fld :tlb))
               (not (equal fld :implicit-supervisor-access)))
          (equal (mv-nth 1
                         (wb n addr w value (xw fld index val x86)))
                 (xw fld index val
                     (mv-nth 1 (wb n addr w value x86))))))

Theorem: wb-xw-rflags-not-ac-in-sys-view

(defthm wb-xw-rflags-not-ac-in-sys-view
 (implies
     (equal (rflagsbits->ac value)
            (rflagsbits->ac (rflags x86)))
     (and (equal (mv-nth 0
                         (wb n
                             addr w val (xw :rflags nil value x86)))
                 (mv-nth 0
                         (wb n addr w val (double-rewrite x86))))
          (equal (mv-nth 1
                         (wb n
                             addr w val (xw :rflags nil value x86)))
                 (xw :rflags nil value
                     (mv-nth 1 (wb n addr w val x86)))))))

Theorem: xr-fault-wb-in-sys-view

(defthm xr-fault-wb-in-sys-view
  (implies (and (not (mv-nth 0 (las-to-pas n addr :w x86)))
                (not (marking-view x86)))
           (equal (xr :fault
                      nil (mv-nth 1 (wb n addr w val x86)))
                  (xr :fault nil x86))))

Theorem: split-rb-in-app-view

(defthm split-rb-in-app-view
  (implies
       (and (canonical-address-p (+ -1 i j lin-addr))
            (canonical-address-p lin-addr)
            (app-view x86)
            (natp i)
            (natp j))
       (equal (mv-nth 1 (rb (+ i j) lin-addr r-x x86))
              (b* ((low (mv-nth 1 (rb i lin-addr r-x x86)))
                   (high (mv-nth 1 (rb j (+ i lin-addr) r-x x86))))
                (logior low (ash high (ash i 3)))))))

Function: split-wb-induction-scheme

(defun split-wb-induction-scheme (i j lin-addr val x86)
 (declare (xargs :non-executable t))
 (prog2$ (acl2::throw-nonexec-error 'split-wb-induction-scheme
                                    (list i j lin-addr val x86))
         (cond ((or (not (natp i))
                    (not (natp j))
                    (zp (+ i j))
                    (zp i)
                    (not (canonical-address-p lin-addr))
                    (not (canonical-address-p (+ -1 i j lin-addr))))
                (mv i j lin-addr val x86))
               (t (split-wb-induction-scheme
                       (1- i)
                       j (1+ lin-addr)
                       (logtail 8 val)
                       (mv-nth 1
                               (wvm08 lin-addr (loghead 8 val)
                                      x86)))))))

Theorem: split-wb-in-app-view

(defthm split-wb-in-app-view
 (implies
  (and (canonical-address-p lin-addr)
       (canonical-address-p (+ -1 i j lin-addr))
       (unsigned-byte-p (ash (+ i j) 3) val)
       (app-view x86)
       (posp i)
       (natp j))
  (equal
    (mv-nth 1 (wb-1 (+ i j) lin-addr w val x86))
    (mv-nth 1
            (wb-1 j (+ i lin-addr)
                  w
                  (loghead (ash j 3)
                           (logtail (ash i 3) val))
                  (mv-nth 1
                          (wb-1 i lin-addr w (loghead (ash i 3) val)
                                x86)))))))

Subtopics

Las-to-pas
Rb
Create-canonical-address-list
Rb-1
Read-from-physical-memory
Write-to-physical-memory
Wb
Wb-1
Canonical-address-listp: Recognizer of a list of canonical addresses