		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. If the index is 0, we return 0, because x0 is always (implicitly) 0. Otherwise, we read the whole register (decreasing the index by 1), 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__))
    (b* ((reg (ubyte5-fix reg)))
      (if (= reg 0)
          0
        (nth (1- 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)