		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Write1-memory-unsigned8

Refine write-memory-unsigned8 to use the stobj states.

Definitions and Theorems

Function: write1-memory-unsigned8

(defun write1-memory-unsigned8 (addr val stat feat)
 (declare (xargs :non-executable t))
 (declare
    (xargs :guard (non-exec (and (stat1p stat)
                                 (integerp addr)
                                 (ubyte8p val)
                                 (statp (stat-from-stat1 stat))
                                 (featp feat)
                                 (stat-validp (stat-from-stat1 stat)
                                              feat)))))
 (prog2$
      (acl2::throw-nonexec-error 'write1-memory-unsigned8
                                 (list addr val stat feat))
      (if (acl2::mbt$ (stat1p stat))
          (let ((addr (loghead (feat->xlen feat) addr))
                (stat (stat-from-stat1 stat)))
            (let ((change-stat stat)
                  (stat->memory (update-nth addr (ubyte8-fix val)
                                            (stat->memory stat))))
              (stat (stat->xregs change-stat)
                    (stat->pc change-stat)
                    stat->memory
                    (stat->error change-stat))))
        0)))

Theorem: write1-memory-unsigned8-to-write-memory-unsigned8

(defthm write1-memory-unsigned8-to-write-memory-unsigned8
 (implies
      (stat1p stat)
      (equal (write1-memory-unsigned8 addr val stat feat)
             (write-memory-unsigned8 addr val (stat-from-stat1 stat)
                                     feat)))
 :rule-classes :rewrite)

Theorem: write-memory-unsigned8-to-write1-memory-unsigned8

(defthm write-memory-unsigned8-to-write1-memory-unsigned8
 (implies
     (statp stat)
     (equal (write-memory-unsigned8 addr val stat feat)
            (write1-memory-unsigned8 addr val (stat1-from-stat stat)
                                     feat)))
 :rule-classes :rewrite)