		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

!rgfi-from-alist

Update general-purpose registers as dictated by rgf-alist, which is required to be a rgfi-alistp.

Signature
(!rgfi-from-alist rgf-alist x86) → x86

Definitions and Theorems

Function: !rgfi-from-alist

(defun !rgfi-from-alist (rgf-alist x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (rgfi-alistp rgf-alist)))
  (let ((__function__ '!rgfi-from-alist))
    (declare (ignorable __function__))
    (cond ((endp rgf-alist) x86)
          (t (let ((x86 (!rgfi (caar rgf-alist)
                               (n64-to-i64 (cdar rgf-alist))
                               x86)))
               (!rgfi-from-alist (cdr rgf-alist)
                                 x86))))))

Theorem: x86p-!rgfi-from-alist

(defthm x86p-!rgfi-from-alist
  (implies (and (rgfi-alistp rgf-alist) (x86p x86))
           (x86p (!rgfi-from-alist rgf-alist x86))))