		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-unsigned{2}

Refine read32-xreg-unsigned{1} to use the isomorphic states stat32.

Definitions and Theorems

Function: read32-xreg-unsigned{2}

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

Theorem: read32-xreg-unsigned{2}-to-read32-xreg-unsigned{1}

(defthm read32-xreg-unsigned{2}-to-read32-xreg-unsigned{1}
 (implies
   (stat32p riscv::stat)
   (equal (read32-xreg-unsigned{2} riscv::reg riscv::stat)
          (read32-xreg-unsigned{1} riscv::reg
                                   (stat-from-stat32 riscv::stat))))
 :rule-classes :rewrite)

Theorem: read32-xreg-unsigned{1}-to-read32-xreg-unsigned{2}

(defthm read32-xreg-unsigned{1}-to-read32-xreg-unsigned{2}
 (implies
   (stat-rv32im-le-p riscv::stat)
   (equal (read32-xreg-unsigned{1} riscv::reg riscv::stat)
          (read32-xreg-unsigned{2} riscv::reg
                                   (stat32-from-stat riscv::stat))))
 :rule-classes :rewrite)