		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

Msri-alistp

Recognizer for pairs of model-specific register indices and values

Signature
(msri-alistp alst) → *

Note that the register values are required to be n64p

Definitions and Theorems

Function: msri-alistp

(defun msri-alistp (alst)
  (declare (xargs :guard t))
  (let ((__function__ 'msri-alistp))
    (declare (ignorable __function__))
    (if (atom alst)
        (equal alst nil)
      (if (atom (car alst))
          nil
        (let ((index (caar alst))
              (value (cdar alst))
              (rest (cdr alst)))
          (and (natp index)
               (< index
                  *model-specific-register-names-len*)
               (unsigned-byte-p 64 value)
               (msri-alistp rest)))))))