		Search-engine friendly clone of the ACL2 documentation.

States32

Read32-xreg-signed

Read a signed 32-bit integer from an x register.

Signature
(read32-xreg-signed reg stat) → val
Arguments: reg — Guard (ubyte5p reg).; stat — Guard (state32p stat).
Returns: val — Type (sbyte32p val).

The register index consists of 5 bits. We read an unsigned 32-bit integer from the register, and convert it to signed.

Definitions and Theorems

Function: read32-xreg-signed

(defun read32-xreg-signed (reg stat)
  (declare (xargs :guard (and (ubyte5p reg) (state32p stat))))
  (let ((__function__ 'read32-xreg-signed))
    (declare (ignorable __function__))
    (logext 32 (read32-xreg-unsigned reg stat))))

Theorem: sbyte32p-of-read32-xreg-signed

(defthm sbyte32p-of-read32-xreg-signed
  (b* ((val (read32-xreg-signed reg stat)))
    (sbyte32p val))
  :rule-classes :rewrite)

Theorem: read32-xreg-signed-of-ubyte5-fix-reg

(defthm read32-xreg-signed-of-ubyte5-fix-reg
  (equal (read32-xreg-signed (ubyte5-fix reg)
                             stat)
         (read32-xreg-signed reg stat)))

Theorem: read32-xreg-signed-ubyte5-equiv-congruence-on-reg

(defthm read32-xreg-signed-ubyte5-equiv-congruence-on-reg
  (implies (ubyte5-equiv reg reg-equiv)
           (equal (read32-xreg-signed reg stat)
                  (read32-xreg-signed reg-equiv stat)))
  :rule-classes :congruence)

Theorem: read32-xreg-signed-of-state32-fix-stat

(defthm read32-xreg-signed-of-state32-fix-stat
  (equal (read32-xreg-signed reg (state32-fix stat))
         (read32-xreg-signed reg stat)))

Theorem: read32-xreg-signed-state32-equiv-congruence-on-stat

(defthm read32-xreg-signed-state32-equiv-congruence-on-stat
  (implies (state32-equiv stat stat-equiv)
           (equal (read32-xreg-signed reg stat)
                  (read32-xreg-signed reg stat-equiv)))
  :rule-classes :congruence)