		Search-engine friendly clone of the ACL2 documentation.

States64

Write64-xreg

Write a 64-bit integer to an x register.

Signature
(write64-xreg 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. If it is 0, there is no change, because x0 is always 0, and it is a no-op to write to it.

The value to write is actually any integer, signed or unsigned, of which we only write the low 64 bits into the register, as an unsigned 64-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: write64-xreg

(defun write64-xreg (reg val stat)
  (declare (xargs :guard (and (ubyte5p reg)
                              (integerp val)
                              (state64p stat))))
  (let ((__function__ 'write64-xreg))
    (declare (ignorable __function__))
    (if (ubyte5-equiv reg 0)
        (state64-fix stat)
      (change-state64
           stat
           :xregfile (update-nth (ubyte5-fix reg)
                                 (loghead 64 val)
                                 (state64->xregfile stat))))))

Theorem: state64p-of-write64-xreg

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

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

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

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

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

Theorem: write64-xreg-of-ifix-val

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

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

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

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

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

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

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