		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-unsigned{3}

Simplify read32-xreg-unsigned{2} after the isomorphic state transformation.

We assume the guard so that we eliminate the outer if with mbt added by apt::isodata.

We simplify the guard to eliminate riscv::stat-validp from it, which is implied by stat32p.

This is the final refinement for this function, so we use the name read32-xreg-unsigned without numeric index.

Definitions and Theorems

Function: read32-xreg-unsigned{3}

(defun read32-xreg-unsigned{3} (riscv::reg riscv::stat)
  (declare (xargs :guard (and (stat32p riscv::stat)
                              (natp riscv::reg)
                              (< (nfix riscv::reg) 32))))
  (let ((riscv::reg (nfix riscv::reg)))
    (if (equal riscv::reg 0)
        0
      (nth (+ -1 riscv::reg)
           (stat32->xregs riscv::stat)))))

Theorem: read32-xreg-unsigned{2}-becomes-read32-xreg-unsigned{3}

(defthm read32-xreg-unsigned{2}-becomes-read32-xreg-unsigned{3}
 (implies (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))
          (equal (read32-xreg-unsigned{2} riscv::reg riscv::stat)
                 (read32-xreg-unsigned{3} riscv::reg riscv::stat))))

Theorem: ubyte32p-of-read32-xreg-unsigned{3}

(defthm ubyte32p-of-read32-xreg-unsigned{3}
  (implies (and (natp reg) (< reg 32))
           (ubyte32p (read32-xreg-unsigned{3} reg stat))))