		Search-engine friendly clone of the ACL2 documentation.

States

Stat-validp

Check if a state is valid with respect to given features.

Signature
(stat-validp stat feat) → yes/no
Arguments: stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: yes/no — Type (booleanp yes/no).

As explained in stat, that fixtype models all possible machine states for all possible features. Here we define restrictions based on features.

For now, the only features we model are whether the base is RV32I or RV64I. This dictates the size XLEN of the registers, either 32 or 64 bits; so we use contrain them to form a list of 32-bit or 64-bit unsigned values. The number of registers is feat->xnum. However, since x0 is hardwired to 0 [ISA:2.1], we do not model that register explicitly: we only model x1, x2, etc.; so we constrain the length of the list to be one less than the number of registers.

Based on XLEN, we constrain the program counter to be either 32 or 64 bits.

The size of the memory is 2^XLEN, so we constrain the length of the list to be that.

Definitions and Theorems

Function: stat-validp

(defun stat-validp (stat feat)
  (declare (xargs :guard (and (statp stat) (featp feat))))
  (let ((__function__ 'stat-validp))
    (declare (ignorable __function__))
    (b* (((stat stat) stat)
         (xlen (feat->xlen feat))
         (xnum (feat->xnum feat)))
      (and (unsigned-byte-listp xlen stat.xregs)
           (equal (len stat.xregs) xnum)
           (unsigned-byte-p xlen stat.pc)
           (equal (len stat.memory)
                  (expt 2 xlen))))))

Theorem: booleanp-of-stat-validp

(defthm booleanp-of-stat-validp
  (b* ((yes/no (stat-validp stat feat)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: unsigned-byte-listp-of-stat->xregs

(defthm unsigned-byte-listp-of-stat->xregs
  (implies (stat-validp stat feat)
           (unsigned-byte-listp (feat->xlen feat)
                                (stat->xregs stat))))

Theorem: true-listp-of-stat->xregs

(defthm true-listp-of-stat->xregs
  (implies (stat-validp stat feat)
           (true-listp (stat->xregs stat)))
  :rule-classes :type-prescription)

Theorem: ubyte32-listp-of-stat->xregs

(defthm ubyte32-listp-of-stat->xregs
  (implies (and (stat-validp stat feat)
                (feat-bits-case (feat->bits feat)
                                :|32|))
           (ubyte32-listp (stat->xregs stat))))

Theorem: ubyte64-listp-of-stat->xregs

(defthm ubyte64-listp-of-stat->xregs
  (implies (and (stat-validp stat feat)
                (feat-bits-case (feat->bits feat)
                                :|64|))
           (ubyte64-listp (stat->xregs stat))))

Theorem: len-of-stat->xregs

(defthm len-of-stat->xregs
  (implies (stat-validp stat feat)
           (equal (len (stat->xregs stat))
                  (feat->xnum feat))))

Theorem: unsigned-byte-p-of-stat->pc

(defthm unsigned-byte-p-of-stat->pc
  (implies (stat-validp stat feat)
           (unsigned-byte-p (feat->xlen feat)
                            (stat->pc stat))))

Theorem: ubyte32p-of-stat->pc

(defthm ubyte32p-of-stat->pc
  (implies (and (stat-validp stat feat)
                (feat-bits-case (feat->bits feat)
                                :|32|))
           (ubyte32p (stat->pc stat))))

Theorem: ubyte64p-of-stat->pc

(defthm ubyte64p-of-stat->pc
  (implies (and (stat-validp stat feat)
                (feat-bits-case (feat->bits feat)
                                :|64|))
           (ubyte64p (stat->pc stat))))

Theorem: len-of-stat->memory

(defthm len-of-stat->memory
  (implies (stat-validp stat feat)
           (equal (len (stat->memory stat))
                  (expt 2 (feat->xlen feat)))))

Theorem: stat-validp-of-stat-fix-stat

(defthm stat-validp-of-stat-fix-stat
  (equal (stat-validp (stat-fix stat) feat)
         (stat-validp stat feat)))

Theorem: stat-validp-stat-equiv-congruence-on-stat

(defthm stat-validp-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (stat-validp stat feat)
                  (stat-validp stat-equiv feat)))
  :rule-classes :congruence)

Theorem: stat-validp-of-feat-fix-feat

(defthm stat-validp-of-feat-fix-feat
  (equal (stat-validp stat (feat-fix feat))
         (stat-validp stat feat)))

Theorem: stat-validp-feat-equiv-congruence-on-feat

(defthm stat-validp-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (stat-validp stat feat)
                  (stat-validp stat feat-equiv)))
  :rule-classes :congruence)