		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Stat-rv32im-le-p

Recognizer of states for RV32IM little endian.

Signature
(stat-rv32im-le-p x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: stat-rv32im-le-p

(defun stat-rv32im-le-p (x)
  (declare (xargs :guard t))
  (and (riscv::statp x)
       (riscv::stat-validp x (feat-rv32im-le))))

Theorem: booleanp-of-stat-rv32im-le-p

(defthm booleanp-of-stat-rv32im-le-p
  (b* ((yes/no (stat-rv32im-le-p x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: unsigned-byte-p-32-of-nth-of-stat-rv32im-le->xregs

(defthm unsigned-byte-p-32-of-nth-of-stat-rv32im-le->xregs
  (implies (and (riscv::stat-validp stat (feat-rv32im-le))
                (natp reg)
                (< reg 32))
           (unsigned-byte-p 32
                            (nth (1- reg)
                                 (riscv::stat->xregs stat)))))