• 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
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
          • Unwind-x86-interpreter-in-app-view
        • 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

• App-view-proof-utilities

Unwind-x86-interpreter-in-app-view

Definitions of rules to monitor in the application-level 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
   (app-view x86)
   (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 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)
                                byte-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
 (b*
   (((mv flg byte x862)
     (rme08 proc-mode start-rip 1 :x x86))
    (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
   (implies
        (and (not flg)
             (equal prefix-byte-group-code 3)
             (not (zp cnt))
             (not (mv-nth 0
                          (add-to-*ip proc-mode start-rip 1 x862))))
        (equal (get-prefixes proc-mode
                             start-rip prefixes rex-byte cnt x86)
               (get-prefixes proc-mode (1+ start-rip)
                             (!prefixes->opr byte prefixes)
                             0 (1- cnt)
                             x862)))))

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

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

Rules related to instruction fetches and program location

Theorem: one-read-with-rb-from-program-at

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

Theorem: program-at-wb-disjoint

(defthm program-at-wb-disjoint
 (implies (and (separate :x (len bytes)
                         prog-addr w n addr)
               (app-view x86))
          (equal (program-at prog-addr
                             bytes (mv-nth 1 (wb n addr w val x86)))
                 (program-at prog-addr bytes x86))))

Rules related to disjointness/overlap of memory regions

Theorem: rb-wb-disjoint

(defthm rb-wb-disjoint
 (implies
      (and (separate r-x n-1 addr-1 w n-2 addr-2)
           (app-view x86))
      (and (equal (mv-nth 0
                          (rb n-1 addr-1 r-x
                              (mv-nth 1 (wb n-2 addr-2 w val x86))))
                  (mv-nth 0 (rb n-1 addr-1 r-x x86)))
           (equal (mv-nth 1
                          (rb n-1 addr-1 r-x
                              (mv-nth 1 (wb n-2 addr-2 w val x86))))
                  (mv-nth 1 (rb n-1 addr-1 r-x x86))))))

Theorem: rb-wb-subset

(defthm rb-wb-subset
  (implies (and (app-view x86)
                (< (+ addr-1 n-1) (+ addr-2 n-2))
                (<= addr-2 addr-1)
                (canonical-address-p addr-1)
                (canonical-address-p (+ -1 n-1 addr-1))
                (canonical-address-p addr-2)
                (canonical-address-p (+ -1 n-2 addr-2))
                (unsigned-byte-p (ash n-2 3) val)
                (posp n-1)
                (posp n-2)
                (x86p x86))
           (equal (mv-nth 1
                          (rb n-1 addr-1 r-x
                              (mv-nth 1 (wb n-2 addr-2 w val x86))))
                  (part-select val
                               :low (ash (- addr-1 addr-2) 3)
                               :width (ash n-1 3)))))

Theorem: rb-wb-equal

(defthm rb-wb-equal
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr))
                (posp n)
                (app-view x86))
           (equal (mv-nth 1
                          (rb n addr
                              r-x (mv-nth 1 (wb n addr w val x86))))
                  (loghead (ash n 3) val))))

Theorem: separate-smaller-regions

(defthm separate-smaller-regions
  (implies
       (and (bind-free (separate-bindings 'separate-smaller-regions
                                          r-w-x-1 r-w-x-2 mfc state)
                       (n-1 a-1 n-2 a-2))
            (<= a-2 a-2-bigger)
            (<= (+ n-2-smaller a-2-bigger)
                (+ n-2 a-2))
            (<= a-1 a-1-bigger)
            (<= (+ n-1-smaller a-1-bigger)
                (+ n-1 a-1))
            (separate r-w-x-1 n-1 a-1 r-w-x-2 n-2 a-2))
       (separate r-w-x-1 n-1-smaller a-1-bigger
                 r-w-x-2 n-2-smaller a-2-bigger))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: separate-contiguous-regions

(defthm separate-contiguous-regions
  (and (separate r-w-x-1 i (+ (- i) x)
                 r-w-x-2 j x)
       (implies (<= j i)
                (separate r-w-x-1 i x r-w-x-2 j (+ (- i) x)))
       (separate r-w-x-1 i x r-w-x-2 j (+ i x))
       (implies (or (<= (+ j k2) k1) (<= (+ i k1) k2))
                (separate r-w-x-1 i (+ k1 x)
                          r-w-x-2 j (+ k2 x)))))