		Search-engine friendly clone of the ACL2 documentation.

States32

Read32-xreg-unsigned

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

Signature
(read32-xreg-unsigned reg stat) → val
Arguments: reg — Guard (ubyte5p reg).; stat — Guard (state32p stat).
Returns: val — Type (ubyte32p val).

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

Definitions and Theorems

Function: read32-xreg-unsigned

(defun read32-xreg-unsigned (reg stat)
  (declare (xargs :guard (and (ubyte5p reg) (state32p stat))))
  (let ((__function__ 'read32-xreg-unsigned))
    (declare (ignorable __function__))
    (nth (ubyte5-fix reg)
         (state32->xregfile stat))))

Theorem: ubyte32p-of-read32-xreg-unsigned

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

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

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

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

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

Theorem: read32-xreg-unsigned-of-state32-fix-stat

(defthm read32-xreg-unsigned-of-state32-fix-stat
  (equal (read32-xreg-unsigned reg (state32-fix stat))
         (read32-xreg-unsigned reg stat)))

Theorem: read32-xreg-unsigned-state32-equiv-congruence-on-stat

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