		Search-engine friendly clone of the ACL2 documentation.

States64

Read64-xreg-unsigned

Read an unsigned 64-bit integer from an x register.

Signature
(read64-xreg-unsigned reg stat) → val
Arguments: reg — Guard (ubyte5p reg).; stat — Guard (state64p stat).
Returns: val — Type (ubyte64p val).

The register index consists of 5 bits. We read the whole register, which is unsigned.

Definitions and Theorems

Function: read64-xreg-unsigned

(defun read64-xreg-unsigned (reg stat)
  (declare (xargs :guard (and (ubyte5p reg) (state64p stat))))
  (let ((__function__ 'read64-xreg-unsigned))
    (declare (ignorable __function__))
    (nth (ubyte5-fix reg)
         (state64->xregfile stat))))

Theorem: ubyte64p-of-read64-xreg-unsigned

(defthm ubyte64p-of-read64-xreg-unsigned
  (b* ((val (read64-xreg-unsigned reg stat)))
    (ubyte64p val))
  :rule-classes :rewrite)

Theorem: read64-xreg-unsigned-of-ubyte5-fix-reg

(defthm read64-xreg-unsigned-of-ubyte5-fix-reg
  (equal (read64-xreg-unsigned (ubyte5-fix reg)
                               stat)
         (read64-xreg-unsigned reg stat)))

Theorem: read64-xreg-unsigned-ubyte5-equiv-congruence-on-reg

(defthm read64-xreg-unsigned-ubyte5-equiv-congruence-on-reg
  (implies (ubyte5-equiv reg reg-equiv)
           (equal (read64-xreg-unsigned reg stat)
                  (read64-xreg-unsigned reg-equiv stat)))
  :rule-classes :congruence)

Theorem: read64-xreg-unsigned-of-state64-fix-stat

(defthm read64-xreg-unsigned-of-state64-fix-stat
  (equal (read64-xreg-unsigned reg (state64-fix stat))
         (read64-xreg-unsigned reg stat)))

Theorem: read64-xreg-unsigned-state64-equiv-congruence-on-stat

(defthm read64-xreg-unsigned-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (read64-xreg-unsigned reg stat)
                  (read64-xreg-unsigned reg stat-equiv)))
  :rule-classes :congruence)