		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-memory-unsigned8

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

Definitions and Theorems

Function: read1-memory-unsigned8

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

Theorem: read1-memory-unsigned8-to-read-memory-unsigned8

(defthm read1-memory-unsigned8-to-read-memory-unsigned8
  (implies (stat1p stat)
           (equal (read1-memory-unsigned8 addr stat feat)
                  (read-memory-unsigned8 addr (stat-from-stat1 stat)
                                         feat)))
  :rule-classes :rewrite)

Theorem: read-memory-unsigned8-to-read1-memory-unsigned8

(defthm read-memory-unsigned8-to-read1-memory-unsigned8
 (implies (statp stat)
          (equal (read-memory-unsigned8 addr stat feat)
                 (read1-memory-unsigned8 addr (stat1-from-stat stat)
                                         feat)))
 :rule-classes :rewrite)