		Search-engine friendly clone of the ACL2 documentation.

Features

Feat->xnum

The number of x registers.

Signature
(feat->xnum feat) → xnum
Arguments: feat — Guard (featp feat).
Returns: xnum — Type (posp xnum).

This is 32 for the RV32I and RV64I bases, but it is reduced to 16 for the RV32E and RV64E bases [ISA:3].

Definitions and Theorems

Function: feat->xnum

(defun feat->xnum (feat)
  (declare (xargs :guard (featp feat)))
  (let ((__function__ 'feat->xnum))
    (declare (ignorable __function__))
    (b* (((feat feat) feat))
      (feat-base-case feat.base
                      :rv32i 32
                      :rv64i 32
                      :rv32e 16
                      :rv64e 16))))

Theorem: posp-of-feat->xnum

(defthm posp-of-feat->xnum
  (b* ((xnum (feat->xnum feat)))
    (posp xnum))
  :rule-classes :rewrite)

Theorem: feat->xnum-when-embedp

(defthm feat->xnum-when-embedp
  (implies (feat-embedp feat)
           (b* ((?xnum (feat->xnum feat)))
             (equal xnum 16))))

Theorem: feat->xnum-when-not-embedp

(defthm feat->xnum-when-not-embedp
  (implies (not (feat-embedp feat))
           (b* ((?xnum (feat->xnum feat)))
             (equal xnum 32))))

Theorem: feat->xnum-of-feat-fix-feat

(defthm feat->xnum-of-feat-fix-feat
  (equal (feat->xnum (feat-fix feat))
         (feat->xnum feat)))

Theorem: feat->xnum-feat-equiv-congruence-on-feat

(defthm feat->xnum-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (feat->xnum feat)
                  (feat->xnum feat-equiv)))
  :rule-classes :congruence)