		Search-engine friendly clone of the ACL2 documentation.

States

Read-mem8

Read an unsigned 8-bit integer from memory.

Signature
(read-mem8 addr stat feat) → val
Arguments: addr — Guard (integerp addr).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: val — Type (ubyte8p val).

The address is an integer of arbitrary size, of which we consider only the low XLEN bits, as an unsigned address. Allowing any integer is convenient for callers. We return the byte at that address.

Since we read a single byte, there is no difference between little and big endian.

Definitions and Theorems

Function: read-mem8

(defun read-mem8 (addr stat feat)
  (declare (xargs :guard (and (integerp addr)
                              (statp stat)
                              (featp feat))))
  (declare
       (xargs :type-prescription (natp (read-mem8 addr stat feat))
              :guard (stat-validp stat feat)))
  (b* ((addr (loghead (feat->xlen feat) addr)))
    (ubyte8-fix (nth addr (stat->memory stat)))))

Theorem: ubyte8p-of-read-mem8

(defthm ubyte8p-of-read-mem8
  (b* ((val (read-mem8 addr stat feat)))
    (ubyte8p val))
  :rule-classes :rewrite)

Theorem: read-mem8-upper-bound

(defthm read-mem8-upper-bound
  (b* ((?val (read-mem8 addr stat feat)))
    (<= val 255))
  :rule-classes :linear)

Theorem: read-mem8-of-loghead-xlen

(defthm read-mem8-of-loghead-xlen
  (implies (equal n (feat->xlen feat))
           (equal (read-mem8 (loghead n addr) stat feat)
                  (read-mem8 addr stat feat))))

Theorem: read-mem8-of-ifix-addr

(defthm read-mem8-of-ifix-addr
  (equal (read-mem8 (ifix addr) stat feat)
         (read-mem8 addr stat feat)))

Theorem: read-mem8-int-equiv-congruence-on-addr

(defthm read-mem8-int-equiv-congruence-on-addr
  (implies (acl2::int-equiv addr addr-equiv)
           (equal (read-mem8 addr stat feat)
                  (read-mem8 addr-equiv stat feat)))
  :rule-classes :congruence)

Theorem: read-mem8-of-stat-fix-stat

(defthm read-mem8-of-stat-fix-stat
  (equal (read-mem8 addr (stat-fix stat) feat)
         (read-mem8 addr stat feat)))

Theorem: read-mem8-stat-equiv-congruence-on-stat

(defthm read-mem8-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (read-mem8 addr stat feat)
                  (read-mem8 addr stat-equiv feat)))
  :rule-classes :congruence)

Theorem: read-mem8-of-feat-fix-feat

(defthm read-mem8-of-feat-fix-feat
  (equal (read-mem8 addr stat (feat-fix feat))
         (read-mem8 addr stat feat)))

Theorem: read-mem8-feat-equiv-congruence-on-feat

(defthm read-mem8-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (read-mem8 addr stat feat)
                  (read-mem8 addr stat feat-equiv)))
  :rule-classes :congruence)