		Search-engine friendly clone of the ACL2 documentation.

States32

Write32-xreg

Write a 32-bit integer to an x register.

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

The register index consists of 5 bits. If it is 0, there is no change, because x0 is always 0, and it is a no-op to write to it. If the index is not 0, we decrease it by 1, since the register file represents registers x1 to x31.

The value to write is actually any integer, signed or unsigned, of which we only write the low 32 bits into the register, as an unsigned 32-bit register.

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: write32-xreg

(defun write32-xreg (reg val stat)
  (declare (xargs :guard (and (ubyte5p reg)
                              (integerp val)
                              (state32p stat))))
  (let ((__function__ 'write32-xreg))
    (declare (ignorable __function__))
    (b* ((reg (ubyte5-fix reg)))
      (if (= reg 0)
          (state32-fix stat)
        (change-state32
             stat
             :xregfile (update-nth (1- reg)
                                   (loghead 32 val)
                                   (state32->xregfile stat)))))))

Theorem: state32p-of-write32-xreg

(defthm state32p-of-write32-xreg
  (b* ((new-stat (write32-xreg reg val stat)))
    (state32p new-stat))
  :rule-classes :rewrite)

Theorem: write32-xreg-of-ubyte5-fix-reg

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

Theorem: write32-xreg-ubyte5-equiv-congruence-on-reg

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

Theorem: write32-xreg-of-ifix-val

(defthm write32-xreg-of-ifix-val
  (equal (write32-xreg reg (ifix val) stat)
         (write32-xreg reg val stat)))

Theorem: write32-xreg-int-equiv-congruence-on-val

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

Theorem: write32-xreg-of-state32-fix-stat

(defthm write32-xreg-of-state32-fix-stat
  (equal (write32-xreg reg val (state32-fix stat))
         (write32-xreg reg val stat)))

Theorem: write32-xreg-state32-equiv-congruence-on-stat

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