		Search-engine friendly clone of the ACL2 documentation.

States64

Read64-xreg-signed

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

Signature
(read64-xreg-signed reg stat) → val
Arguments: reg — Guard (ubyte5p reg).; stat — Guard (state64p stat).
Returns: val — Type (sbyte64p val).

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

Definitions and Theorems

Function: read64-xreg-signed

(defun read64-xreg-signed (reg stat)
  (declare (xargs :guard (and (ubyte5p reg) (state64p stat))))
  (let ((__function__ 'read64-xreg-signed))
    (declare (ignorable __function__))
    (logext 64 (read64-xreg-unsigned reg stat))))

Theorem: sbyte64p-of-read64-xreg-signed

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

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

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

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

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

Theorem: read64-xreg-signed-of-state64-fix-stat

(defthm read64-xreg-signed-of-state64-fix-stat
  (equal (read64-xreg-signed reg (state64-fix stat))
         (read64-xreg-signed reg stat)))

Theorem: read64-xreg-signed-state64-equiv-congruence-on-stat

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