		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Stat1-validp

Signature
(stat1-validp stat1 feat) → *

Definitions and Theorems

Function: stat1-validp

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