		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-xreg-unsigned

Refine read-xreg-unsigned to use the stobj states.

Definitions and Theorems

Function: read1-xreg-unsigned

(defun read1-xreg-unsigned (reg stat feat)
 (declare (xargs :non-executable t))
 (declare
  (xargs :guard (non-exec (and (stat1p stat)
                               (natp reg)
                               (statp (stat-from-stat1 stat))
                               (featp feat)
                               (stat-validp (stat-from-stat1 stat)
                                            feat)
                               (< (lnfix reg) (feat->xnum feat))))))
 (prog2$
   (acl2::throw-nonexec-error 'read1-xreg-unsigned
                              (list reg stat feat))
   (if (acl2::mbt$ (stat1p stat))
       (let ((reg (lnfix reg))
             (stat (stat-from-stat1 stat)))
         (if (= reg 0)
             0
           (unsigned-byte-fix (feat->xlen feat)
                              (nth (+ -1 reg) (stat->xregs stat)))))
     0)))

Theorem: read1-xreg-unsigned-to-read-xreg-unsigned

(defthm read1-xreg-unsigned-to-read-xreg-unsigned
  (implies (stat1p stat)
           (equal (read1-xreg-unsigned reg stat feat)
                  (read-xreg-unsigned reg (stat-from-stat1 stat)
                                      feat)))
  :rule-classes :rewrite)

Theorem: read-xreg-unsigned-to-read1-xreg-unsigned

(defthm read-xreg-unsigned-to-read1-xreg-unsigned
  (implies (statp stat)
           (equal (read-xreg-unsigned reg stat feat)
                  (read1-xreg-unsigned reg (stat1-from-stat stat)
                                       feat)))
  :rule-classes :rewrite)