		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Stat1-validp

Refine stat-validp to use the stobj states.

Definitions and Theorems

Function: stat1-validp

(defun stat1-validp (stat feat)
 (declare (xargs :non-executable t))
 (declare
      (xargs :guard (non-exec (and (stat1p stat)
                                   (statp (stat-from-stat1 stat))
                                   (featp feat)))))
 (prog2$
  (acl2::throw-nonexec-error 'stat1-validp
                             (list stat feat))
  (let nil
   (let nil
    (let nil
      (let nil
        (and (acl2::mbt$ (stat1p stat))
             (let ((stat.xregs (stat->xregs (stat-from-stat1 stat)))
                   (stat (stat-from-stat1 stat)))
               (let* ((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))))))))))))

Theorem: stat1-validp-to-stat-validp

(defthm stat1-validp-to-stat-validp
  (implies (stat1p stat)
           (equal (stat1-validp stat feat)
                  (stat-validp (stat-from-stat1 stat)
                               feat)))
  :rule-classes :rewrite)

Theorem: stat-validp-to-stat1-validp

(defthm stat-validp-to-stat1-validp
  (implies (statp stat)
           (equal (stat-validp stat feat)
                  (stat1-validp (stat1-from-stat stat)
                                feat)))
  :rule-classes :rewrite)