		Search-engine friendly clone of the ACL2 documentation.

X86-decoder

X86-run-steps

An alternative to x86-run

Signature
(x86-run-steps n x86) → (mv * x86)

x86-run-steps returns two values --- number of steps taken by the machine before it comes to a halt and the x86 state. Note that the number of steps will always be less than or equal to n.

Definitions and Theorems

Function: x86-run-steps

(defun x86-run-steps (n x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 59) n))
  (let ((__function__ 'x86-run-steps))
    (declare (ignorable __function__))
    (x86-run-steps1 n n x86)))

Theorem: x86-run-steps1-is-x86-run-ms

(defthm x86-run-steps1-is-x86-run-ms
  (implies (ms x86)
           (equal (mv-nth 1 (x86-run-steps1 n n0 x86))
                  (x86-run n x86))))

Theorem: x86-run-steps1-is-x86-run-zp-n

(defthm x86-run-steps1-is-x86-run-zp-n
  (implies (and (not (ms x86))
                (not (fault x86))
                (zp n))
           (equal (mv-nth 1 (x86-run-steps1 n n0 x86))
                  (!ms (list (list* 'x86-run
                                    :rip (rip x86)
                                    '(:timeout t)))
                       (x86-run n x86)))))

Theorem: x86-run-steps1-open

(defthm x86-run-steps1-open
 (implies
  (and (not (ms x86))
       (not (fault x86))
       (not (zp n)))
  (equal
      (mv-nth 1 (x86-run-steps1 n n0 x86))
      (mv-nth 1
              (x86-run-steps1 (1- n)
                              n0 (x86-fetch-decode-execute x86))))))