		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Write1-xreg

Refine write-xreg to use the stobj states.

Definitions and Theorems

Function: write1-xreg

(defun write1-xreg (reg val stat feat)
 (declare (xargs :non-executable t))
 (declare
  (xargs :guard (non-exec (and (stat1p stat)
                               (natp reg)
                               (integerp val)
                               (statp (stat-from-stat1 stat))
                               (featp feat)
                               (stat-validp (stat-from-stat1 stat)
                                            feat)
                               (< (lnfix reg) (feat->xnum feat))))))
 (prog2$
  (acl2::throw-nonexec-error 'write1-xreg
                             (list reg val stat feat))
  (if
   (acl2::mbt$ (stat1p stat))
   (let ((reg (lnfix reg))
         (stat (stat-from-stat1 stat)))
    (if (= reg 0)
        (stat-fix stat)
      (let ((change-stat stat)
            (stat->xregs (update-nth (+ -1 reg)
                                     (loghead (feat->xlen feat) val)
                                     (stat->xregs stat))))
        (stat stat->xregs (stat->pc change-stat)
              (stat->memory change-stat)
              (stat->error change-stat)))))
   0)))

Theorem: write1-xreg-to-write-xreg

(defthm write1-xreg-to-write-xreg
  (implies (stat1p stat)
           (equal (write1-xreg reg val stat feat)
                  (write-xreg reg val (stat-from-stat1 stat)
                              feat)))
  :rule-classes :rewrite)

Theorem: write-xreg-to-write1-xreg

(defthm write-xreg-to-write1-xreg
  (implies (statp stat)
           (equal (write-xreg reg val stat feat)
                  (write1-xreg reg val (stat1-from-stat stat)
                               feat)))
  :rule-classes :rewrite)