		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. 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: 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__))
    (b* ((reg (ubyte5-fix reg)))
      (if (= reg 0)
          0
        (nth (1- 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)