		Search-engine friendly clone of the ACL2 documentation.

States32i

Read32i-xreg-unsigned{1}

Simplify read32i-xreg-unsigned{0} after partial evaluation.

We assume the guard so that we can eliminate the fixers.

Definitions and Theorems

Function: read32i-xreg-unsigned{1}

(defun read32i-xreg-unsigned{1} (reg stat)
 (declare
  (xargs
     :guard (and (natp reg)
                 (statp stat)
                 (stat-validp stat
                              '((base :rv32i) (endian :little) (m)))
                 (< reg 32))))
 (if (= reg 0)
     0
   (nth (+ -1 reg) (stat->xregs stat))))

Theorem: read32i-xreg-unsigned{0}-becomes-read32i-xreg-unsigned{1}

(defthm read32i-xreg-unsigned{0}-becomes-read32i-xreg-unsigned{1}
  (implies (and (natp reg)
                (statp stat)
                (featp (feat-rv32i-le))
                (stat-validp stat (feat-rv32i-le))
                (< (lnfix reg)
                   (feat->xnum (feat-rv32i-le))))
           (equal (read32i-xreg-unsigned{0} reg stat)
                  (read32i-xreg-unsigned{1} reg stat))))