		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-unsigned{1}

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

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

Definitions and Theorems

Function: read32-xreg-unsigned{1}

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

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

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