		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Write1-pc

Refine write-pc to use the stobj states.

Definitions and Theorems

Function: write1-pc

(defun write1-pc (pc stat feat)
 (declare (xargs :non-executable t))
 (declare
    (xargs :guard (non-exec (and (stat1p stat)
                                 (natp pc)
                                 (statp (stat-from-stat1 stat))
                                 (featp feat)
                                 (stat-validp (stat-from-stat1 stat)
                                              feat)))))
 (prog2$ (acl2::throw-nonexec-error 'write1-pc
                                    (list pc stat feat))
         (let ((change-stat stat)
               (stat->pc (loghead (feat->xlen feat) (lnfix pc))))
           (if (acl2::mbt$ (stat1p change-stat))
               (let ((change-stat (stat-from-stat1 change-stat)))
                 (stat (stat->xregs change-stat)
                       stat->pc (stat->memory change-stat)
                       (stat->error change-stat)))
             0))))

Theorem: write1-pc-to-write-pc

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

Theorem: write-pc-to-write1-pc

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