		Search-engine friendly clone of the ACL2 documentation.

States32i

Read32i-xreg-unsigned

Simplify read32i-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 stat-validp from it, which is implied by stat32ip.

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

Definitions and Theorems

Function: read32i-xreg-unsigned

(defun read32i-xreg-unsigned (reg stat)
  (declare (xargs :guard (and (stat32ip stat)
                              (natp reg)
                              (< reg 32))))
  (if (equal reg 0)
      0
    (nth (+ -1 reg) (stat32i->xregs stat))))

Theorem: read32i-xreg-unsigned{2}-becomes-read32i-xreg-unsigned

(defthm read32i-xreg-unsigned{2}-becomes-read32i-xreg-unsigned
  (implies (and (stat32ip stat)
                (natp reg)
                (statp (stat-from-stat32i stat))
                (stat-validp (stat-from-stat32i stat)
                             '((base :rv32i) (endian :little) (m)))
                (< reg 32))
           (equal (read32i-xreg-unsigned{2} reg stat)
                  (read32i-xreg-unsigned reg stat))))

Theorem: ubyte32p-of-read32i-xreg-unsigned

(defthm ubyte32p-of-read32i-xreg-unsigned
  (implies (and (natp reg) (< reg 32))
           (ubyte32p (read32i-xreg-unsigned reg stat))))