Get a unique unknown to be used when reasoning about undefined values in the processor
(undef-read x86) → (mv unknown x86)
See characterizing-undefined-behavior for more details.
The accessor and updater functions of the
Function:
(defun undef-read$notinline (x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard t)) (let ((__function__ 'undef-read)) (declare (ignorable __function__)) (undef-read-logic x86)))
Theorem:
(defthm natp-of-undef-read.unknown (b* (((mv ?unknown ?x86) (undef-read$notinline x86))) (natp unknown)) :rule-classes :type-prescription)
Theorem:
(defthm x86p-of-undef-read.x86 (implies (x86p x86) (b* (((mv ?unknown ?x86) (undef-read$notinline x86))) (x86p x86))) :rule-classes :rewrite)