		Search-engine friendly clone of the ACL2 documentation.

States32i

Read32i-xreg-unsigned{2}

Refine read32i-xreg-unsigned{1} to use the isomorphic states stat32i.

Definitions and Theorems

Function: read32i-xreg-unsigned{2}

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

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

(defthm read32i-xreg-unsigned{2}-to-read32i-xreg-unsigned{1}
 (implies
    (stat32ip stat)
    (equal (read32i-xreg-unsigned{2} reg stat)
           (read32i-xreg-unsigned{1} reg (stat-from-stat32i stat))))
 :rule-classes :rewrite)

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

(defthm read32i-xreg-unsigned{1}-to-read32i-xreg-unsigned{2}
 (implies
    (stat-rv32i-p stat)
    (equal (read32i-xreg-unsigned{1} reg stat)
           (read32i-xreg-unsigned{2} reg (stat32i-from-stat stat))))
 :rule-classes :rewrite)