		Search-engine friendly clone of the ACL2 documentation.

States64

Read64-xreg-unsigned32

Read an unsigned 32-bit integer from the low bits of an x register.

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

The register index consists of 5 bits. We read an unsigned 64-bit integer from the register, and we keep the low 32 bits, stil unsigned.

Definitions and Theorems

Function: read64-xreg-unsigned32

(defun read64-xreg-unsigned32 (reg stat)
  (declare (xargs :guard (and (ubyte5p reg) (state64p stat))))
  (let ((__function__ 'read64-xreg-unsigned32))
    (declare (ignorable __function__))
    (loghead 32 (read64-xreg-unsigned reg stat))))

Theorem: ubyte32p-of-read64-xreg-unsigned32

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

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

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

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

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

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

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

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

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