		Search-engine friendly clone of the ACL2 documentation.

States

Read-memory-unsigned32

Read an unsigned 32-bit integer from memory.

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

The memory address is the one of the first byte; we read that, and the subsequent bytes. For now we only support little endian memory, so the first byte is the lowest one.

As in read-memory-unsigned8, we let the address be any integer. We use read-memory-unsigned8 four times. Note that if addr is close to 2^XLEN - 1, then the subsequent addresses may wrap around to addres 0.

Definitions and Theorems

Function: read-memory-unsigned32

(defun read-memory-unsigned32 (addr stat feat)
  (declare (xargs :guard (and (integerp addr)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (let ((__function__ 'read-memory-unsigned32))
    (declare (ignorable __function__))
    (b* ((addr (lifix addr))
         (b0 (read-memory-unsigned8 addr stat feat))
         (b1 (read-memory-unsigned8 (+ addr 1)
                                    stat feat))
         (b2 (read-memory-unsigned8 (+ addr 2)
                                    stat feat))
         (b3 (read-memory-unsigned8 (+ addr 3)
                                    stat feat)))
      (+ b0 (ash b1 8)
         (ash b2 16)
         (ash b3 24)))))

Theorem: ubyte32p-of-read-memory-unsigned32

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

Theorem: natp-of-read-memory-unsigned32

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

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

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

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

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

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

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

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

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

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

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

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

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