		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-signed{3}

Simplify the body of read32-xreg-signed{2} to call read32-xreg-unsigned{3}.

We use read-xreg-unsigned-to-read32-xreg-unsigned{3} to accomplish that rewriting. Note that this eliminates the isomorphic conversion.

Definitions and Theorems

Function: read32-xreg-signed{3}

(defun read32-xreg-signed{3} (riscv::reg riscv::stat)
 (declare
  (xargs
      :guard (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))))
 (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{2}-becomes-read32-xreg-signed{3}

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