		Search-engine friendly clone of the ACL2 documentation.

States32

Read32-mem-ubyte8

Read an unsigned 8-bit integer from memory.

Signature
(read32-mem-ubyte8 addr stat) → val
Arguments: addr — Guard (integerp addr).; stat — Guard (state32p stat).
Returns: val — Type (ubyte8p val).

The address is any integer, which we turn into a 32-bit unsigned address. We return the byte at that memory address, directly.

Definitions and Theorems

Function: read32-mem-ubyte8

(defun read32-mem-ubyte8 (addr stat)
  (declare (xargs :guard (and (integerp addr) (state32p stat))))
  (let ((__function__ 'read32-mem-ubyte8))
    (declare (ignorable __function__))
    (b* ((addr (loghead 32 addr)))
      (nth addr (state32->mem stat)))))

Theorem: ubyte8p-of-read32-mem-ubyte8

(defthm ubyte8p-of-read32-mem-ubyte8
  (b* ((val (read32-mem-ubyte8 addr stat)))
    (ubyte8p val))
  :rule-classes :rewrite)

Theorem: natp-of-read32-mem-ubyte8

(defthm natp-of-read32-mem-ubyte8
  (b* ((val (read32-mem-ubyte8 addr stat)))
    (natp val))
  :rule-classes :type-prescription)

Theorem: read32-mem-ubyte8-upper-bound

(defthm read32-mem-ubyte8-upper-bound
  (b* ((?val (read32-mem-ubyte8 addr stat)))
    (< val 256))
  :rule-classes :linear)

Theorem: read32-mem-ubyte8-of-ifix-addr

(defthm read32-mem-ubyte8-of-ifix-addr
  (equal (read32-mem-ubyte8 (ifix addr) stat)
         (read32-mem-ubyte8 addr stat)))

Theorem: read32-mem-ubyte8-int-equiv-congruence-on-addr

(defthm read32-mem-ubyte8-int-equiv-congruence-on-addr
  (implies (acl2::int-equiv addr addr-equiv)
           (equal (read32-mem-ubyte8 addr stat)
                  (read32-mem-ubyte8 addr-equiv stat)))
  :rule-classes :congruence)

Theorem: read32-mem-ubyte8-of-state32-fix-stat

(defthm read32-mem-ubyte8-of-state32-fix-stat
  (equal (read32-mem-ubyte8 addr (state32-fix stat))
         (read32-mem-ubyte8 addr stat)))

Theorem: read32-mem-ubyte8-state32-equiv-congruence-on-stat

(defthm read32-mem-ubyte8-state32-equiv-congruence-on-stat
  (implies (state32-equiv stat stat-equiv)
           (equal (read32-mem-ubyte8 addr stat)
                  (read32-mem-ubyte8 addr stat-equiv)))
  :rule-classes :congruence)