We set the FPU tag and TOS field to 00B (valid) and 000B respectively. This function accounts for the effects of all MMX instructions except EMMS.
(mmx-instruction-updates x86) → x86
Function:
(defun mmx-instruction-updates$inline (x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard t)) (b* ((x86 (!fp-tag 0 x86)) (fp-status (fp-status x86)) (x86 (!fp-status (!fp-statusbits->top 0 fp-status) x86))) x86))
Theorem:
(defthm x86p-mmx-instruction-updates (implies (x86p x86) (x86p (mmx-instruction-updates x86))))