		Search-engine friendly clone of the ACL2 documentation.

States

Read-xreg-unsigned

Read an unsigned integer from an x register.

Signature
(read-xreg-unsigned reg stat feat) → val
Arguments: reg — Guard (natp reg).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: val — Type (unsigned-byte-p (feat->xlen feat) val).

The index must be less than the number n of registers, so that the registers x0 to x<n-1> can be indexed. The result is a natural number in general; additionally, based on XLEN, it consists of either 32 or 64 bits.

As explained in stat, x0 is not modeled explicitly, since it is hardwired to 0. Thus, the 0 index is treated separately; the other cases are handled by decrementing the index by 1.

Definitions and Theorems

Function: read-xreg-unsigned

(defun read-xreg-unsigned (reg stat feat)
 (declare (xargs :guard (and (natp reg)
                             (statp stat)
                             (featp feat))))
 (declare
   (xargs
        :type-prescription (natp (read-xreg-unsigned reg stat feat))
        :guard (and (stat-validp stat feat)
                    (< (lnfix reg) (feat->xnum feat)))))
 (let ((__function__ 'read-xreg-unsigned))
   (declare (ignorable __function__))
   (b* ((reg (lnfix reg)))
     (if (= reg 0)
         0
       (unsigned-byte-fix (feat->xlen feat)
                          (nth (1- reg) (stat->xregs stat)))))))

Theorem: return-type-of-read-xreg-unsigned

(defthm return-type-of-read-xreg-unsigned
  (b* ((val (read-xreg-unsigned reg stat feat)))
    (unsigned-byte-p (feat->xlen feat) val))
  :rule-classes :rewrite)

Theorem: ubyte32p-of-read-xreg-unsigned-when-32p

(defthm ubyte32p-of-read-xreg-unsigned-when-32p
  (implies (feat-32p feat)
           (b* ((?val (read-xreg-unsigned reg stat feat)))
             (ubyte32p val))))

Theorem: ubyte64p-of-read-xreg-unsigned-when-64p

(defthm ubyte64p-of-read-xreg-unsigned-when-64p
  (implies (feat-64p feat)
           (b* ((?val (read-xreg-unsigned reg stat feat)))
             (ubyte64p val))))

Theorem: read-xreg-unsigned-of-x0

(defthm read-xreg-unsigned-of-x0
  (equal (read-xreg-unsigned 0 stat feat)
         0))

Theorem: read-xreg-unsigned-of-nfix-reg

(defthm read-xreg-unsigned-of-nfix-reg
  (equal (read-xreg-unsigned (nfix reg)
                             stat feat)
         (read-xreg-unsigned reg stat feat)))

Theorem: read-xreg-unsigned-nat-equiv-congruence-on-reg

(defthm read-xreg-unsigned-nat-equiv-congruence-on-reg
  (implies (acl2::nat-equiv reg reg-equiv)
           (equal (read-xreg-unsigned reg stat feat)
                  (read-xreg-unsigned reg-equiv stat feat)))
  :rule-classes :congruence)

Theorem: read-xreg-unsigned-of-stat-fix-stat

(defthm read-xreg-unsigned-of-stat-fix-stat
  (equal (read-xreg-unsigned reg (stat-fix stat)
                             feat)
         (read-xreg-unsigned reg stat feat)))

Theorem: read-xreg-unsigned-stat-equiv-congruence-on-stat

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

Theorem: read-xreg-unsigned-of-feat-fix-feat

(defthm read-xreg-unsigned-of-feat-fix-feat
  (equal (read-xreg-unsigned reg stat (feat-fix feat))
         (read-xreg-unsigned reg stat feat)))

Theorem: read-xreg-unsigned-feat-equiv-congruence-on-feat

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