		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-signed{4}

Simplify the guard of read32-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: read32-xreg-signed{4}

(defun read32-xreg-signed{4} (riscv::reg riscv::stat)
  (declare (xargs :guard (and (stat32p riscv::stat)
                              (natp riscv::reg)
                              (< (nfix riscv::reg) 32))))
  (logext 32
          (riscv::read-xreg-unsigned riscv::reg
                                     (stat-from-stat32 riscv::stat)
                                     '((riscv::base :rv32i)
                                       (riscv::endian :little)
                                       (riscv::m . t)))))

Theorem: read32-xreg-signed{3}-becomes-read32-xreg-signed{4}

(defthm read32-xreg-signed{3}-becomes-read32-xreg-signed{4}
  (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)))
                (< (nfix riscv::reg) 32))
           (equal (read32-xreg-signed{3} riscv::reg riscv::stat)
                  (read32-xreg-signed{4} riscv::reg riscv::stat))))