		Search-engine friendly clone of the ACL2 documentation.

States

Read-memory-unsigned8

Read an unsigned 8-bit integer from memory.

Signature
(read-memory-unsigned8 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-memory-unsigned8

(defun read-memory-unsigned8 (addr stat feat)
  (declare (xargs :guard (and (integerp addr)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (let ((__function__ 'read-memory-unsigned8))
    (declare (ignorable __function__))
    (b* ((addr (loghead (feat->xlen feat)
                        (lifix addr))))
      (ubyte8-fix (nth addr (stat->memory stat))))))

Theorem: ubyte8p-of-read-memory-unsigned8

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

Theorem: natp-of-read-memory-unsigned8

(defthm natp-of-read-memory-unsigned8
  (b* ((val (read-memory-unsigned8 addr stat feat)))
    (natp val))
  :rule-classes :type-prescription)

Theorem: read-memory-unsigned8-upper-bound

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

Theorem: read-memory-unsigned8-of-ifix-addr

(defthm read-memory-unsigned8-of-ifix-addr
  (equal (read-memory-unsigned8 (ifix addr)
                                stat feat)
         (read-memory-unsigned8 addr stat feat)))

Theorem: read-memory-unsigned8-int-equiv-congruence-on-addr

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

Theorem: read-memory-unsigned8-of-stat-fix-stat

(defthm read-memory-unsigned8-of-stat-fix-stat
  (equal (read-memory-unsigned8 addr (stat-fix stat)
                                feat)
         (read-memory-unsigned8 addr stat feat)))

Theorem: read-memory-unsigned8-stat-equiv-congruence-on-stat

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

Theorem: read-memory-unsigned8-of-feat-fix-feat

(defthm read-memory-unsigned8-of-feat-fix-feat
  (equal (read-memory-unsigned8 addr stat (feat-fix feat))
         (read-memory-unsigned8 addr stat feat)))

Theorem: read-memory-unsigned8-feat-equiv-congruence-on-feat

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