		Search-engine friendly clone of the ACL2 documentation.

States32i

Read32i-xreg-signed

Simplify the guard of read32i-xreg-signed{3} to eliminate the isomorphic conversion.

We had to do this simplication separately from the previous one because the rules needed to do the rewritings interfere.

Definitions and Theorems

Function: read32i-xreg-signed

(defun read32i-xreg-signed (reg stat)
  (declare (xargs :guard (and (stat32ip stat)
                              (natp reg)
                              (< reg 32))))
  (logext 32 (read32i-xreg-unsigned reg stat)))

Theorem: read32i-xreg-signed{3}-becomes-read32i-xreg-signed

(defthm read32i-xreg-signed{3}-becomes-read32i-xreg-signed
  (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-signed{3} reg stat)
                  (read32i-xreg-signed reg stat))))