		Search-engine friendly clone of the ACL2 documentation.

X86-decoder

X86-run-halt

Alternative version of x86-run that uses x86-fetch-decode-execute-halt instead of x86-fetch-decode-execute

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

Definitions and Theorems

Function: x86-run-halt

(defun x86-run-halt (halt-address n x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (signed-byte 48) halt-address)
          (type (unsigned-byte 59) n))
 (let ((__function__ 'x86-run-halt))
  (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-halt halt-address x86))
              (n (the (unsigned-byte 59) (1- n))))
         (x86-run-halt halt-address n x86))))))

Theorem: x86p-of-x86-run-halt

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