		Search-engine friendly clone of the ACL2 documentation.

States

Write-xreg

Write an integer to an x register.

Signature
(write-xreg reg val stat feat) → new-stat
Arguments: reg — Guard (natp reg).; val — Guard (integerp val).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: new-stat — Type (statp new-stat).

The integer may have any size: we only keep its low XLEN bits, and write those to the register.

The index must be less than the number n of registers, so that the registers x0 to x<n> can be indexed.

As explained in stat, x0 is not modeled explicitly, since it is hardwired to 0. Thus, the 0 index is treated separately; the other cases are handled by decrementing the index by 1.

Definitions and Theorems

Function: write-xreg

(defun write-xreg (reg val stat feat)
 (declare (xargs :guard (and (natp reg)
                             (integerp val)
                             (statp stat)
                             (featp feat))))
 (declare (xargs :guard (and (stat-validp stat feat)
                             (< (lnfix reg) (feat->xnum feat)))))
 (let ((__function__ 'write-xreg))
  (declare (ignorable __function__))
  (b* ((reg (lnfix reg)))
   (if (= reg 0)
       (stat-fix stat)
     (change-stat
          stat
          :xregs (update-nth (1- reg)
                             (loghead (feat->xlen feat) (lifix val))
                             (stat->xregs stat)))))))

Theorem: statp-of-write-xreg

(defthm statp-of-write-xreg
  (b* ((new-stat (write-xreg reg val stat feat)))
    (statp new-stat))
  :rule-classes :rewrite)

Theorem: stat-validp-of-write-xreg

(defthm stat-validp-of-write-xreg
  (implies (and (stat-validp stat feat)
                (< (lnfix reg) (feat->xnum feat)))
           (b* ((?new-stat (write-xreg reg val stat feat)))
             (stat-validp new-stat feat))))

Theorem: write-xreg-of-nfix-reg

(defthm write-xreg-of-nfix-reg
  (equal (write-xreg (nfix reg) val stat feat)
         (write-xreg reg val stat feat)))

Theorem: write-xreg-nat-equiv-congruence-on-reg

(defthm write-xreg-nat-equiv-congruence-on-reg
  (implies (acl2::nat-equiv reg reg-equiv)
           (equal (write-xreg reg val stat feat)
                  (write-xreg reg-equiv val stat feat)))
  :rule-classes :congruence)

Theorem: write-xreg-of-ifix-val

(defthm write-xreg-of-ifix-val
  (equal (write-xreg reg (ifix val) stat feat)
         (write-xreg reg val stat feat)))

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

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

Theorem: write-xreg-of-stat-fix-stat

(defthm write-xreg-of-stat-fix-stat
  (equal (write-xreg reg val (stat-fix stat)
                     feat)
         (write-xreg reg val stat feat)))

Theorem: write-xreg-stat-equiv-congruence-on-stat

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

Theorem: write-xreg-of-feat-fix-feat

(defthm write-xreg-of-feat-fix-feat
  (equal (write-xreg reg val stat (feat-fix feat))
         (write-xreg reg val stat feat)))

Theorem: write-xreg-feat-equiv-congruence-on-feat

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