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

• System-level-marking-view-proof-utilities

Unwind-x86-interpreter-in-marking-view

Definitions of rules to monitor in the system-level marking view

Rules about x86-run and x86-fetch-decode-execute

Theorem: x86-run-opener-not-ms-not-zp-n

(defthm x86-run-opener-not-ms-not-zp-n
  (implies (and (not (ms x86))
                (not (fault x86))
                (syntaxp (quotep n))
                (not (zp n)))
           (equal (x86-run n x86)
                  (x86-run (1- n)
                           (x86-fetch-decode-execute x86)))))

Theorem: x86-fetch-decode-execute-opener-in-marking-view

(defthm x86-fetch-decode-execute-opener-in-marking-view
 (implies
  (and
   (equal start-rip (rip x86))
   (equal four-vals-of-get-prefixes
          (get-prefixes-alt start-rip 0 0 15 x86))
   (equal flg-get-prefixes
          (mv-nth 0 four-vals-of-get-prefixes))
   (equal prefixes
          (mv-nth 1 four-vals-of-get-prefixes))
   (equal rex-byte
          (mv-nth 2 four-vals-of-get-prefixes))
   (equal x86-1
          (mv-nth 3 four-vals-of-get-prefixes))
   (equal opcode/vex/evex-byte
          (prefixes->nxt prefixes))
   (equal prefix-length (prefixes->num prefixes))
   (equal temp-rip0 (+ prefix-length start-rip 1))
   (not (equal opcode/vex/evex-byte 196))
   (not (equal opcode/vex/evex-byte 197))
   (not (equal opcode/vex/evex-byte 98))
   (equal modr/m?
          (one-byte-opcode-modr/m-p 0 opcode/vex/evex-byte))
   (equal three-vals-of-modr/m
          (if modr/m? (rml08 temp-rip0 :x x86-1)
            (mv nil 0 x86-1)))
   (equal flg-modr/m
          (mv-nth 0 three-vals-of-modr/m))
   (equal modr/m (mv-nth 1 three-vals-of-modr/m))
   (equal x86-2 (mv-nth 2 three-vals-of-modr/m))
   (equal temp-rip1
          (if modr/m? (1+ temp-rip0) temp-rip0))
   (equal sib?
          (and modr/m? (x86-decode-sib-p modr/m nil)))
   (equal three-vals-of-sib
          (if sib? (rml08 temp-rip1 :x x86-2)
            (mv nil 0 x86-2)))
   (equal flg-sib (mv-nth 0 three-vals-of-sib))
   (equal sib (mv-nth 1 three-vals-of-sib))
   (equal x86-3 (mv-nth 2 three-vals-of-sib))
   (equal temp-rip2
          (if sib? (1+ temp-rip1) temp-rip1))
   (equal
    x86-executed
    (one-byte-opcode-execute 0 start-rip temp-rip2 prefixes rex-byte
                             opcode/vex/evex-byte modr/m sib x86-3))
   (marking-view x86)
   (64-bit-modep (double-rewrite x86))
   (not (app-view x86))
   (not (ms x86))
   (not (fault x86))
   (x86p x86)
   (not (double-rewrite flg-get-prefixes))
   (canonical-address-p temp-rip0)
   (if modr/m? (and (not (double-rewrite flg-modr/m))
                    (canonical-address-p temp-rip1))
     t)
   (if sib? (and (not (double-rewrite flg-sib))
                 (canonical-address-p temp-rip2))
     t)
   (disjoint-p (mv-nth 1
                       (las-to-pas 15 (xr :rip nil x86)
                                   :x (double-rewrite x86)))
               (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                           (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas 15 (xr :rip nil x86)
                            :x (double-rewrite x86))))
   (not (enable-peripherals x86-executed))
   (or (not (fault x86-executed))
       (not (handle-exceptions x86-executed)))
   (syntaxp
     (and (not (cw "~% [ x86instr @ rip: ~p0 ~%"
                   start-rip))
          (not (cw "              op0: ~s0 ] ~%"
                   (str::hexify (unquote opcode/vex/evex-byte)))))))
  (equal (x86-fetch-decode-execute x86)
         (if (inhibit-interrupts-one-instruction x86)
             (!inhibit-interrupts-one-instruction nil x86-executed)
           x86-executed))))

Rules about get-prefixes-alt

Theorem: get-prefixes-alt-opener-lemma-no-prefix-byte

(defthm get-prefixes-alt-opener-lemma-no-prefix-byte
 (implies
  (and
    (b* (((mv flg prefix-byte &)
          (rb-alt 1 start-rip
                  :x (double-rewrite x86)))
         (prefix-byte-group-code
              (get-one-byte-prefix-array-code prefix-byte)))
      (and (not flg)
           (zp prefix-byte-group-code)
           (not (equal (ash prefix-byte -4) 4))))
    (not (zp cnt))
    (marking-view x86)
    (64-bit-modep (double-rewrite x86))
    (not (app-view x86))
    (canonical-address-p start-rip)
    (not (mv-nth 0
                 (las-to-pas cnt start-rip
                             :x (double-rewrite x86))))
    (disjoint-p (mv-nth 1
                        (las-to-pas cnt start-rip
                                    :x (double-rewrite x86)))
                (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                            (double-rewrite x86)))))
  (b* (((mv new-flg new-prefixes new-rex-byte &)
        (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
   (and
    (equal new-flg nil)
    (equal
     new-prefixes
     (let
      ((prefixes
           (!prefixes->nxt (mv-nth 1
                                   (rb-alt 1 start-rip
                                           :x (double-rewrite x86)))
                           prefixes)))
      (!prefixes->num (- 15 cnt) prefixes)))
    (equal new-rex-byte rex-byte)))))

Theorem: get-prefixes-alt-opener-lemma-group-1-prefix-in-marking-view

(defthm get-prefixes-alt-opener-lemma-group-1-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (not flg)
     (equal prefix-byte-group-code 1)
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal
        (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
        (get-prefixes-alt (+ 1 start-rip)
                          (if (equal prefix-byte 240)
                              (!prefixes->lck prefix-byte prefixes)
                            (!prefixes->rep prefix-byte prefixes))
                          0 (+ -1 cnt)
                          new-x86)))))

Theorem: get-prefixes-alt-opener-lemma-group-2-prefix-in-marking-view

(defthm get-prefixes-alt-opener-lemma-group-2-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (not flg)
     (equal prefix-byte-group-code 2)
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal
        (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
        (if (or (equal prefix-byte 100)
                (equal prefix-byte 101))
            (get-prefixes-alt (1+ start-rip)
                              (!prefixes->seg prefix-byte prefixes)
                              0 (1- cnt)
                              new-x86)
          (get-prefixes-alt (1+ start-rip)
                            prefixes 0 (1- cnt)
                            new-x86))))))

Theorem: get-prefixes-alt-opener-lemma-group-3-prefix-in-marking-view

(defthm get-prefixes-alt-opener-lemma-group-3-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (not flg)
     (equal prefix-byte-group-code 3)
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
          (get-prefixes-alt (+ 1 start-rip)
                            (!prefixes->opr prefix-byte prefixes)
                            0 (+ -1 cnt)
                            new-x86)))))

Theorem: get-prefixes-alt-opener-lemma-group-4-prefix-in-marking-view

(defthm get-prefixes-alt-opener-lemma-group-4-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (not flg)
     (equal prefix-byte-group-code 4)
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
          (get-prefixes-alt (+ 1 start-rip)
                            (!prefixes->adr prefix-byte prefixes)
                            0 (+ -1 cnt)
                            new-x86)))))

Theorem: get-prefixes-alt-and-wb-in-system-level-marking-view-disjoint-from-paging-structures

(defthm
 get-prefixes-alt-and-wb-in-system-level-marking-view-disjoint-from-paging-structures
 (implies
  (and
    (disjoint-p$ (mv-nth 1
                         (las-to-pas n-w write-addr
                                     :w (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
    (disjoint-p (mv-nth 1
                        (las-to-pas n-w write-addr
                                    :w (double-rewrite x86)))
                (mv-nth 1
                        (las-to-pas cnt start-rip
                                    :x (double-rewrite x86))))
    (posp cnt)
    (canonical-address-p (+ -1 cnt start-rip))
    (64-bit-modep (double-rewrite x86))
    (not (app-view x86))
    (x86p x86))
  (and
   (equal
    (mv-nth
      0
      (get-prefixes-alt start-rip prefixes rex-byte cnt
                        (mv-nth 1 (wb n-w write-addr w value x86))))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth
      1
      (get-prefixes-alt start-rip prefixes rex-byte cnt
                        (mv-nth 1 (wb n-w write-addr w value x86))))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth
      2
      (get-prefixes-alt start-rip prefixes rex-byte cnt
                        (mv-nth 1 (wb n-w write-addr w value x86))))
    (mv-nth
         2
         (get-prefixes-alt start-rip prefixes
                           rex-byte cnt (double-rewrite x86)))))))

Theorem: mv-nth-3-get-prefixes-alt-no-prefix-byte

(defthm mv-nth-3-get-prefixes-alt-no-prefix-byte
 (b* (((mv flg prefix-byte &)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (marking-view x86)
     (not flg)
     (zp prefix-byte-group-code)
     (not (equal (ash prefix-byte -4) 4))
     (not (zp cnt))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86))))
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (64-bit-modep (double-rewrite x86)))
   (equal
     (mv-nth 3
             (get-prefixes-alt start-rip prefixes rex-byte cnt x86))
     (mv-nth 2 (las-to-pas 1 start-rip :x x86))))))

Rules related to instruction fetches and program location

Theorem: one-read-with-rb-alt-from-program-at-alt-in-marking-view

(defthm one-read-with-rb-alt-from-program-at-alt-in-marking-view
 (implies (and (bind-free (find-program-at-info 'prog-addr
                                                'bytes
                                                mfc state)
                          (prog-addr bytes))
               (program-at-alt prog-addr bytes (double-rewrite x86))
               (<= prog-addr lin-addr)
               (< lin-addr (+ (len bytes) prog-addr))
               (integerp lin-addr)
               (byte-listp bytes)
               (64-bit-modep (double-rewrite x86))
               (tlb-consistent-n (len bytes)
                                 prog-addr
                                 :x x86)
               (x86p x86))
          (equal (mv-nth 1 (rb-alt 1 lin-addr :x x86))
                 (nth (- lin-addr prog-addr) bytes))))

Theorem: program-at-alt-wb-disjoint-in-sys-view

(defthm program-at-alt-wb-disjoint-in-sys-view
 (implies
  (and
    (disjoint-p$ (mv-nth 1
                         (las-to-pas n-w write-addr
                                     :w (double-rewrite x86)))
                 (mv-nth 1
                         (las-to-pas (len bytes)
                                     prog-addr
                                     :x (double-rewrite x86))))
    (disjoint-p$ (mv-nth 1
                         (las-to-pas n-w write-addr
                                     :w (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
    (canonical-address-p (+ -1 n-w write-addr))
    (canonical-address-p write-addr)
    (tlb-consistent-n (len bytes)
                      prog-addr
                      :x x86))
  (equal (program-at-alt prog-addr bytes
                         (mv-nth 1 (wb n-w write-addr w value x86)))
         (program-at-alt prog-addr bytes (double-rewrite x86)))))

Rules related to canonical linear addresses

Theorem: member-p-canonical-address-listp

(defthm member-p-canonical-address-listp
  (implies
       (and (<= prog-addr addr)
            (< addr (+ n prog-addr))
            (canonical-address-p prog-addr)
            (canonical-address-p (+ -1 n prog-addr))
            (integerp addr))
       (equal (member-p addr
                        (create-canonical-address-list n prog-addr))
              t)))

Rules related to disjointness/overlap of memory regions

Theorem: rb-alt-wb-equal-in-sys-view

(defthm rb-alt-wb-equal-in-sys-view
 (implies
  (and
   (equal
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (mv-nth 1
                (las-to-pas n-w write-addr
                            :w (double-rewrite x86))))
   (disjoint-p$ (mv-nth 1
                        (las-to-pas n-w write-addr
                                    :w (double-rewrite x86)))
                (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                            (double-rewrite x86))))
   (no-duplicates-p (mv-nth 1
                            (las-to-pas n-w write-addr
                                        :w (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n-w write-addr
                            :w (double-rewrite x86))))
   (canonical-address-p (+ -1 n lin-addr))
   (canonical-address-p lin-addr)
   (unsigned-byte-p (ash n-w 3) value)
   (natp n-w)
   (64-bit-modep (double-rewrite x86))
   (not (app-view x86))
   (marking-view x86)
   (tlb-consistent-n n lin-addr r-w-x x86)
   (x86p x86))
  (and
   (equal
        (mv-nth 0
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        nil)
   (equal
        (mv-nth 1
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        value))))

Theorem: rb-alt-wb-disjoint-in-sys-view

(defthm rb-alt-wb-disjoint-in-sys-view
 (implies
  (and
   (disjoint-p
        (mv-nth 1
                (las-to-pas n-w write-addr
                            :w (double-rewrite x86)))
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86))))
   (disjoint-p$ (mv-nth 1
                        (las-to-pas n-w write-addr
                                    :w (double-rewrite x86)))
                (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                            (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (canonical-address-p (+ -1 n lin-addr))
   (canonical-address-p lin-addr)
   (canonical-address-p (+ -1 n-w write-addr))
   (canonical-address-p write-addr)
   (marking-view x86)
   (64-bit-modep (double-rewrite x86))
   (tlb-consistent-n n lin-addr r-w-x x86)
   (not (app-view x86)))
  (and
   (equal
        (mv-nth 0
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        (mv-nth 0
                (rb-alt n lin-addr r-w-x (double-rewrite x86))))
   (equal
        (mv-nth 1
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        (mv-nth 1
                (rb-alt n lin-addr
                        r-w-x (double-rewrite x86)))))))

Theorem: rb-alt-and-wb-to-paging-structures-disjoint

(defthm rb-alt-and-wb-to-paging-structures-disjoint
 (implies
  (and
   (direct-map-p 8 entry-addr
                 :w (double-rewrite x86))
   (equal (page-size (double-rewrite value))
          1)
   (disjoint-p
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86))))
   (disjoint-p (mv-nth 1
                       (las-to-pas 8 entry-addr
                                   :w (double-rewrite x86)))
               (all-xlation-governing-entries-paddrs
                    n lin-addr (double-rewrite x86)))
   (disjoint-p
        (mv-nth 1
                (las-to-pas 8 entry-addr
                            :w (double-rewrite x86)))
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (physical-address-p entry-addr)
   (equal (loghead 3 entry-addr) 0)
   (unsigned-byte-p 64 value)
   (canonical-address-p entry-addr)
   (tlb-consistent-n n lin-addr r-w-x x86))
  (and
   (equal (mv-nth 0
                  (rb-alt n lin-addr r-w-x
                          (mv-nth 1 (wb 8 entry-addr w value x86))))
          (mv-nth 0
                  (rb-alt n lin-addr r-w-x (double-rewrite x86))))
   (equal (mv-nth 1
                  (rb-alt n lin-addr r-w-x
                          (mv-nth 1 (wb 8 entry-addr w value x86))))
          (mv-nth 1
                  (rb-alt n lin-addr
                          r-w-x (double-rewrite x86)))))))

Theorem: rb-wb-disjoint-in-sys-view

(defthm rb-wb-disjoint-in-sys-view
 (implies
  (and
   (disjoint-p
        (mv-nth 1
                (las-to-pas n-w write-addr
                            :w (double-rewrite x86)))
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (all-xlation-governing-entries-paddrs
             n-w write-addr (double-rewrite x86)))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (all-xlation-governing-entries-paddrs
             n lin-addr (double-rewrite x86)))
   (disjoint-p (mv-nth 1
                       (las-to-pas n-w write-addr
                                   :w (double-rewrite x86)))
               (all-xlation-governing-entries-paddrs
                    n lin-addr (double-rewrite x86)))
   (tlb-consistent-n n lin-addr r-w-x x86)
   (not (app-view x86))
   (64-bit-modep (double-rewrite x86)))
  (and
     (equal (mv-nth 0
                    (rb n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
            (mv-nth 0
                    (rb n lin-addr r-w-x (double-rewrite x86))))
     (equal (mv-nth 1
                    (rb n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
            (mv-nth 1
                    (rb n lin-addr
                        r-w-x (double-rewrite x86)))))))

Theorem: rb-wb-equal-in-sys-view

(defthm rb-wb-equal-in-sys-view
 (implies
  (and
   (equal
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (mv-nth 1
                (las-to-pas n-w write-addr
                            :w (double-rewrite x86))))
   (disjoint-p (mv-nth 1
                       (las-to-pas n-w write-addr
                                   :w (double-rewrite x86)))
               (all-xlation-governing-entries-paddrs
                    n lin-addr (double-rewrite x86)))
   (no-duplicates-p (mv-nth 1
                            (las-to-pas n-w write-addr
                                        :w (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n-w write-addr
                            :w (double-rewrite x86))))
   (unsigned-byte-p (ash n-w 3) value)
   (natp n-w)
   (tlb-consistent-n n lin-addr r-w-x x86)
   (64-bit-modep (double-rewrite x86))
   (x86p x86))
  (equal (mv-nth 1
                 (rb n lin-addr r-w-x
                     (mv-nth 1 (wb n-w write-addr w value x86))))
         value)))

Theorem: all-xlation-governing-entries-paddrs-and-mv-nth-1-wb-disjoint

(defthm
      all-xlation-governing-entries-paddrs-and-mv-nth-1-wb-disjoint
 (implies
      (and (disjoint-p (mv-nth 1
                               (las-to-pas n-2 addr-2
                                           :w (double-rewrite x86)))
                       (all-xlation-governing-entries-paddrs
                            n-1 addr-1 (double-rewrite x86)))
           (64-bit-modep (double-rewrite x86)))
      (equal (all-xlation-governing-entries-paddrs
                  n-1 addr-1
                  (mv-nth 1 (wb n-2 addr-2 w value x86)))
             (all-xlation-governing-entries-paddrs
                  n-1 addr-1 (double-rewrite x86)))))

Theorem: la-to-pas-values-and-mv-nth-1-wb-disjoint-from-xlation-gov-addrs

(defthm
   la-to-pas-values-and-mv-nth-1-wb-disjoint-from-xlation-gov-addrs
 (implies
  (and (disjoint-p (mv-nth 1
                           (las-to-pas n-w write-addr
                                       :w (double-rewrite x86)))
                   (all-xlation-governing-entries-paddrs
                        n lin-addr (double-rewrite x86)))
       (tlb-consistent-n n lin-addr r-w-x x86)
       (64-bit-modep (double-rewrite x86)))
  (and
   (equal
    (mv-nth 0
            (las-to-pas n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w 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
                        (mv-nth 1 (wb n-w write-addr w value x86))))
    (mv-nth 1
            (las-to-pas n lin-addr
                        r-w-x (double-rewrite x86)))))))

.