• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
        • System-level-marking-view-proof-utilities
        • Non-marking-view-proof-utilities
          • Unwind-x86-interpreter-in-non-marking-view
        • 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
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Testing-utilities
  • Math

• Non-marking-view-proof-utilities

Unwind-x86-interpreter-in-non-marking-view

Definitions of rules to monitor in the system-level non-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

(defthm x86-fetch-decode-execute-opener
 (implies
  (and
   (not (ms x86))
   (not (fault x86))
   (equal proc-mode (x86-operation-mode x86))
   (equal start-rip (read-*ip proc-mode x86))
   (not (mv-nth 0
                (get-prefixes proc-mode start-rip 0 0 15 x86)))
   (equal prefixes
          (mv-nth 1
                  (get-prefixes proc-mode start-rip 0 0 15 x86)))
   (equal rex-byte
          (mv-nth 2
                  (get-prefixes proc-mode start-rip 0 0 15 x86)))
   (equal opcode/vex/evex-byte
          (prefixes->nxt prefixes))
   (equal prefix-length (prefixes->num prefixes))
   (equal temp-rip0
          (mv-nth 1
                  (add-to-*ip proc-mode start-rip (1+ prefix-length)
                              x86)))
   (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 proc-mode opcode/vex/evex-byte))
   (equal
        modr/m
        (if modr/m? (mv-nth 1 (rme08 proc-mode temp-rip0 1 :x x86))
          0))
   (equal
        temp-rip1
        (if modr/m? (mv-nth 1
                            (add-to-*ip proc-mode temp-rip0 1 x86))
          temp-rip0))
   (equal p4?
          (equal 103 (prefixes->adr prefixes)))
   (equal 16-bit-addressp
          (equal 2
                 (select-address-size proc-mode p4? x86)))
   (equal sib?
          (and modr/m?
               (x86-decode-sib-p modr/m 16-bit-addressp)))
   (equal sib
          (if sib? (mv-nth 1 (rme08 proc-mode temp-rip1 1 :x x86))
            0))
   (equal temp-rip2
          (if sib? (mv-nth 1
                           (add-to-*ip proc-mode temp-rip1 1 x86))
            temp-rip1))
   (or (app-view x86)
       (not (marking-view x86)))
   (not (mv-nth 0
                (add-to-*ip proc-mode start-rip (1+ prefix-length)
                            x86)))
   (if modr/m?
       (and (not (mv-nth 0
                         (add-to-*ip proc-mode temp-rip0 1 x86)))
            (not (mv-nth 0
                         (rme08 proc-mode temp-rip0 1 :x x86))))
     t)
   (if sib?
       (and (not (mv-nth 0
                         (add-to-*ip proc-mode temp-rip1 1 x86)))
            (not (mv-nth 0
                         (rme08 proc-mode temp-rip1 1 :x x86))))
     t)
   (x86p x86)
   (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)
    (one-byte-opcode-execute proc-mode
                             start-rip temp-rip2 prefixes rex-byte
                             opcode/vex/evex-byte modr/m sib x86))))

Rules about get-prefixes

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

(defthm get-prefixes-opener-lemma-no-prefix-byte
 (implies
  (b*
   (((mv flg byte &)
     (rme08 proc-mode start-rip 1 :x x86))
    (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
   (and (not flg)
        (zp prefix-byte-group-code)
        (if (equal proc-mode 0)
            (not (equal (ash byte -4) 4))
          t)
        (not (zp cnt))))
  (equal
    (get-prefixes proc-mode
                  start-rip prefixes rex-byte cnt x86)
    (let
     ((prefixes (!prefixes->nxt
                     (mv-nth 1 (rme08 proc-mode start-rip 1 :x x86))
                     prefixes)))
     (mv nil (!prefixes->num (- 15 cnt) prefixes)
         rex-byte
         (mv-nth 2
                 (rme08 proc-mode start-rip 1
                        :x x86)))))))

Theorem: get-prefixes-opener-lemma-no-legacy-prefix-but-rex-prefix

(defthm get-prefixes-opener-lemma-no-legacy-prefix-but-rex-prefix
 (implies
   (b*
    (((mv flg byte &)
      (rme08 proc-mode start-rip 1 :x x86))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (and (equal proc-mode 0)
         (not flg)
         (zp prefix-byte-group-code)
         (equal (ash byte -4) 4)
         (not (zp cnt))))
   (equal (get-prefixes proc-mode
                        start-rip prefixes rex-byte cnt x86)
          (b* (((mv & byte byte-x86)
                (rme08 proc-mode start-rip 1 :x x86))
               ((mv flg next-rip)
                (add-to-*ip proc-mode start-rip 1 byte-x86)))
            (if flg (mv flg prefixes rex-byte byte-x86)
              (get-prefixes proc-mode
                            next-rip prefixes byte (1- cnt)
                            byte-x86))))))

Theorem: get-prefixes-opener-lemma-group-1-prefix

(defthm get-prefixes-opener-lemma-group-1-prefix
  (b*
    (((mv flg byte x86)
      (rme08 proc-mode start-rip 1 :x x86))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (or (app-view x86)
                  (not (marking-view x86)))
              (not flg)
              (equal prefix-byte-group-code 1)
              (not (zp cnt))
              (not (mv-nth 0
                           (add-to-*ip proc-mode start-rip 1 x86))))
         (equal (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)
                (let ((prefixes (if (equal byte 240)
                                    (!prefixes->lck byte prefixes)
                                  (!prefixes->rep byte prefixes))))
                  (get-prefixes proc-mode (1+ start-rip)
                                prefixes 0 (1- cnt)
                                x86))))))

Theorem: get-prefixes-opener-lemma-group-2-prefix

(defthm get-prefixes-opener-lemma-group-2-prefix
  (b*
    (((mv flg byte byte-x86)
      (rme08 proc-mode start-rip 1 :x x86))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (or (app-view x86)
                  (and (not (app-view x86))
                       (not (marking-view x86))))
              (not flg)
              (equal prefix-byte-group-code 2)
              (not (zp cnt))
              (not (mv-nth 0
                           (add-to-*ip proc-mode start-rip 1 x86))))
         (equal (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)
                (if (or (and (eql proc-mode 0)
                             (or (equal byte 100) (equal byte 101)))
                        (not (eql proc-mode 0)))
                    (get-prefixes proc-mode (1+ start-rip)
                                  (!prefixes->seg byte prefixes)
                                  0 (1- cnt)
                                  byte-x86)
                  (get-prefixes proc-mode (1+ start-rip)
                                prefixes 0 (1- cnt)
                                byte-x86))))))

Theorem: get-prefixes-opener-lemma-group-3-prefix

(defthm get-prefixes-opener-lemma-group-3-prefix
 (implies
  (and
   (or (app-view x86)
       (and (not (app-view x86))
            (not (marking-view x86))))
   (let* ((flg (mv-nth 0 (rme08 proc-mode start-rip 1 :x x86)))
          (prefix-byte-group-code
               (get-one-byte-prefix-array-code
                    (mv-nth 1
                            (rme08 proc-mode start-rip 1 :x x86)))))
     (and (not flg)
          (equal prefix-byte-group-code 3)))
   (not (zp cnt))
   (not (mv-nth 0
                (add-to-*ip proc-mode start-rip 1 x86))))
  (equal
   (get-prefixes proc-mode
                 start-rip prefixes rex-byte cnt x86)
   (get-prefixes
     proc-mode (1+ start-rip)
     (!prefixes->opr (mv-nth 1 (rme08 proc-mode start-rip 1 :x x86))
                     prefixes)
     0 (1- cnt)
     x86))))

Theorem: get-prefixes-opener-lemma-group-4-prefix

(defthm get-prefixes-opener-lemma-group-4-prefix
 (implies
  (and
   (or (app-view x86)
       (and (not (app-view x86))
            (not (marking-view x86))))
   (let* ((flg (mv-nth 0 (rme08 proc-mode start-rip 1 :x x86)))
          (prefix-byte-group-code
               (get-one-byte-prefix-array-code
                    (mv-nth 1
                            (rme08 proc-mode start-rip 1 :x x86)))))
     (and (not flg)
          (equal prefix-byte-group-code 4)))
   (not (zp cnt))
   (not (mv-nth 0
                (add-to-*ip proc-mode start-rip 1 x86))))
  (equal
   (get-prefixes proc-mode
                 start-rip prefixes rex-byte cnt x86)
   (get-prefixes
     proc-mode (1+ start-rip)
     (!prefixes->adr (mv-nth 1 (rme08 proc-mode start-rip 1 :x x86))
                     prefixes)
     0 (1- cnt)
     x86))))

Rules related to instruction fetches and program location

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

(defthm one-read-with-rb-from-program-at-in-non-marking-view
  (implies (and (bind-free (find-program-at-info 'prog-addr
                                                 'bytes
                                                 mfc state)
                           (prog-addr bytes))
                (program-at prog-addr bytes x86)
                (<= prog-addr lin-addr)
                (< lin-addr (+ (len bytes) prog-addr))
                (canonical-address-p lin-addr)
                (byte-listp bytes)
                (not (marking-view x86))
                (not (app-view x86))
                (x86p x86))
           (equal (mv-nth 1 (rb 1 lin-addr :x x86))
                  (nth (- lin-addr prog-addr) bytes))))

Theorem: program-at-wb-disjoint-in-non-marking-view

(defthm program-at-wb-disjoint-in-non-marking-view
 (implies
  (and
    (disjoint-p (mv-nth 1
                        (las-to-pas (len bytes)
                                    prog-addr
                                    :x x86))
                (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
    (disjoint-p (all-xlation-governing-entries-paddrs (len bytes)
                                                      prog-addr x86)
                (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
    (not (app-view x86))
    (not (marking-view x86))
    (not (mv-nth 0 (las-to-pas n-w write-addr :w x86))))
  (equal (program-at prog-addr bytes
                     (mv-nth 1 (wb n-w write-addr w value x86)))
         (program-at prog-addr bytes 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-wb-disjoint-in-non-marking-view

(defthm rb-wb-disjoint-in-non-marking-view
 (implies
  (and (disjoint-p (mv-nth 1 (las-to-pas n-r read-addr r-x x86))
                   (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
       (disjoint-p
            (all-xlation-governing-entries-paddrs n-r read-addr x86)
            (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
       (not (app-view x86))
       (not (marking-view x86))
       (not (mv-nth 0 (las-to-pas n-w write-addr :w x86))))
  (and
     (equal (mv-nth 0
                    (rb n-r read-addr r-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
            (mv-nth 0 (rb n-r read-addr r-x x86)))
     (equal (mv-nth 1
                    (rb n-r read-addr r-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
            (mv-nth 1 (rb n-r read-addr r-x x86))))))

Theorem: rb-wb-equal-in-non-marking-view

(defthm rb-wb-equal-in-non-marking-view
 (implies
  (and
     (equal (mv-nth 1 (las-to-pas n-r read-addr r-x x86))
            (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
     (disjoint-p
          (all-xlation-governing-entries-paddrs n-r read-addr x86)
          (mv-nth 1 (las-to-pas n-r read-addr r-x x86)))
     (no-duplicates-p (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
     (not (app-view x86))
     (not (marking-view x86))
     (not (mv-nth 0 (las-to-pas n-r read-addr r-x x86)))
     (not (mv-nth 0 (las-to-pas n-w write-addr :w x86))))
  (equal (mv-nth 1
                 (rb n-r read-addr r-x
                     (mv-nth 1 (wb n-w write-addr w value x86))))
         (loghead (ash (nfix n-w) 3) value))))

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

(defthm
 la-to-pas-values-and-mv-nth-1-wb-disjoint-from-xlation-gov-addrs-in-non-marking-view
 (implies
  (and
   (not (mv-nth 0 (las-to-pas n-w write-addr :w x86)))
   (disjoint-p (all-xlation-governing-entries-paddrs n lin-addr x86)
               (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
   (not (marking-view 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 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 x86))))))

Theorem: all-xlation-governing-entries-paddrs-and-mv-nth-1-wb-disjoint-in-non-marking-view

(defthm
 all-xlation-governing-entries-paddrs-and-mv-nth-1-wb-disjoint-in-non-marking-view
 (implies
  (and
   (not (mv-nth 0 (las-to-pas n-w write-addr :w x86)))
   (disjoint-p (all-xlation-governing-entries-paddrs n lin-addr x86)
               (mv-nth 1 (las-to-pas n-w write-addr :w x86)))
   (not (app-view x86))
   (not (marking-view x86))
   (x86p x86))
  (equal (all-xlation-governing-entries-paddrs
              n lin-addr
              (mv-nth 1 (wb n-w write-addr w value x86)))
         (all-xlation-governing-entries-paddrs n lin-addr x86))))