		Search-engine friendly clone of the ACL2 documentation.

States64

Write64-xreg-32

Write an integer to the low 32 bits of an x register, sign-extending it to the high 32 bits of the register.

Signature
(write64-xreg-32 reg val stat) → new-stat
Arguments: reg — Guard (ubyte5p reg).; val — Guard (integerp val).; stat — Guard (state64p stat).
Returns: new-stat — Type (state64p new-stat).

The register index consists of 5 bits.

The value to write is actually any integer, signed or unsigned, of which we only write the low 32 bits into the register, by converting it to a signed 32-bit integer, and then writing that to the register, which sign-extends it.

The fact that the value to write is any integer is handy for callers, who can just pass the integer (e.g. the exact result of an operation) and let this writer function convert the integer for the register.

Definitions and Theorems

Function: write64-xreg-32

(defun write64-xreg-32 (reg val stat)
  (declare (xargs :guard (and (ubyte5p reg)
                              (integerp val)
                              (state64p stat))))
  (let ((__function__ 'write64-xreg-32))
    (declare (ignorable __function__))
    (write64-xreg reg (logext 32 val)
                  stat)))

Theorem: state64p-of-write64-xreg-32

(defthm state64p-of-write64-xreg-32
  (b* ((new-stat (write64-xreg-32 reg val stat)))
    (state64p new-stat))
  :rule-classes :rewrite)

Theorem: write64-xreg-32-of-ubyte5-fix-reg

(defthm write64-xreg-32-of-ubyte5-fix-reg
  (equal (write64-xreg-32 (ubyte5-fix reg)
                          val stat)
         (write64-xreg-32 reg val stat)))

Theorem: write64-xreg-32-ubyte5-equiv-congruence-on-reg

(defthm write64-xreg-32-ubyte5-equiv-congruence-on-reg
  (implies (ubyte5-equiv reg reg-equiv)
           (equal (write64-xreg-32 reg val stat)
                  (write64-xreg-32 reg-equiv val stat)))
  :rule-classes :congruence)

Theorem: write64-xreg-32-of-ifix-val

(defthm write64-xreg-32-of-ifix-val
  (equal (write64-xreg-32 reg (ifix val) stat)
         (write64-xreg-32 reg val stat)))

Theorem: write64-xreg-32-int-equiv-congruence-on-val

(defthm write64-xreg-32-int-equiv-congruence-on-val
  (implies (acl2::int-equiv val val-equiv)
           (equal (write64-xreg-32 reg val stat)
                  (write64-xreg-32 reg val-equiv stat)))
  :rule-classes :congruence)

Theorem: write64-xreg-32-of-state64-fix-stat

(defthm write64-xreg-32-of-state64-fix-stat
  (equal (write64-xreg-32 reg val (state64-fix stat))
         (write64-xreg-32 reg val stat)))

Theorem: write64-xreg-32-state64-equiv-congruence-on-stat

(defthm write64-xreg-32-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (write64-xreg-32 reg val stat)
                  (write64-xreg-32 reg val stat-equiv)))
  :rule-classes :congruence)