Functions to read/write into the MSRs
Function:
(defun valid-msr-addr-p (msr-addr) (declare (xargs :guard t)) (member msr-addr '(372 373 374 3221225600 3221225728 3221225729 3221225730 3221225601 3221225602 3221225604 416)))
Function:
(defun msr-addr-to-index (msr-addr) (declare (xargs :guard (valid-msr-addr-p msr-addr))) (case msr-addr (372 8) (373 9) (374 10) (3221225600 0) (3221225728 1) (3221225729 2) (3221225730 3) (3221225601 4) (3221225602 5) (3221225604 6) (416 7) (t -1)))
Function:
(defun msra (msr-addr x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard (valid-msr-addr-p msr-addr))) (let ((__function__ 'msra)) (declare (ignorable __function__)) (b* ((msr-index (msr-addr-to-index msr-addr))) (msri msr-index x86))))
Theorem:
(defthm n64p-of-msra (b* ((msr-val (msra msr-addr x86))) (n64p msr-val)) :rule-classes :rewrite)
Function:
(defun !msra (msr-addr val x86) (declare (xargs :stobjs (x86))) (declare (type (unsigned-byte 64) val)) (declare (xargs :guard (valid-msr-addr-p msr-addr))) (let ((__function__ '!msra)) (declare (ignorable __function__)) (b* ((msr-index (msr-addr-to-index msr-addr))) (!msri msr-index val x86))))
Theorem:
(defthm x86p-of-!msra (implies (x86p x86) (b* ((x86 (!msra msr-addr val x86))) (x86p x86))) :rule-classes :rewrite)