Read an unsigned 8-bit integer from memory.
The address is an integer of arbitrary size,
of which we consider only the low
Since we read a single byte, there is no difference between little and big endian.
Function:
(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:
(defthm ubyte8p-of-read-memory-unsigned8 (b* ((val (read-memory-unsigned8 addr stat feat))) (ubyte8p val)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-read-memory-unsigned8 (b* ((val (read-memory-unsigned8 addr stat feat))) (natp val)) :rule-classes :type-prescription)
Theorem:
(defthm read-memory-unsigned8-upper-bound (b* ((?val (read-memory-unsigned8 addr stat feat))) (<= val 255)) :rule-classes :linear)
Theorem:
(defthm read-memory-unsigned8-of-ifix-addr (equal (read-memory-unsigned8 (ifix addr) stat feat) (read-memory-unsigned8 addr stat feat)))
Theorem:
(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:
(defthm read-memory-unsigned8-of-stat-fix-stat (equal (read-memory-unsigned8 addr (stat-fix stat) feat) (read-memory-unsigned8 addr stat feat)))
Theorem:
(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:
(defthm read-memory-unsigned8-of-feat-fix-feat (equal (read-memory-unsigned8 addr stat (feat-fix feat)) (read-memory-unsigned8 addr stat feat)))
Theorem:
(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)