		Search-engine friendly clone of the ACL2 documentation.

X86-decoder

X86-run

Top-level specification function for the x86 ISA model

Signature
(x86-run n x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

x86-run returns the x86 state obtained by executing n instructions or until it halts, whatever comes first. It simply called the step function x86-fetch-decode-execute recursively.

Definitions and Theorems

Function: x86-run

(defun x86-run (n x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 59) n))
  (let ((__function__ 'x86-run))
    (declare (ignorable __function__))
    (cond ((fault x86) x86)
          ((ms x86) x86)
          ((mbe :logic (zp n) :exec (equal 0 n))
           x86)
          (t (let* ((x86 (x86-fetch-decode-execute x86))
                    (n (the (unsigned-byte 59) (1- n))))
               (x86-run n x86))))))

Theorem: x86p-of-x86-run

(defthm x86p-of-x86-run
  (implies (x86p x86)
           (b* ((x86 (x86-run n x86))) (x86p x86)))
  :rule-classes :rewrite)

Theorem: x86-run-and-x86-fetch-decode-and-execute-commutative

(defthm x86-run-and-x86-fetch-decode-and-execute-commutative
  (implies (and (natp k)
                (x86p x86)
                (not (ms x86))
                (not (fault x86)))
           (equal (x86-run k (x86-fetch-decode-execute x86))
                  (x86-fetch-decode-execute (x86-run k x86)))))

Theorem: x86-run-halted

(defthm x86-run-halted
  (implies (or (ms x86) (fault x86))
           (equal (x86-run n x86) x86)))

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

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

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-run-plus

(defthm x86-run-plus
  (implies (and (natp n1)
                (natp n2)
                (syntaxp (quotep n1)))
           (equal (x86-run (clk+ n1 n2) x86)
                  (x86-run n2 (x86-run n1 x86)))))

Theorem: x86-run-plus-1

(defthm x86-run-plus-1
  (implies (and (natp n1)
                (natp n2)
                (syntaxp (quotep n1)))
           (equal (x86-run (clk+ n1 n2) x86)
                  (x86-run n1 (x86-run n2 x86)))))