		Search-engine friendly clone of the ACL2 documentation.

States

Read-memory-unsigned16

Read an unsigned 16-bit integer from memory.

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

The memory address is the one of the first byte; we read that, and the subsequent byte. 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 twice. Note that if addr is 2^XLEN - 1, then addr + 1 wraps around to address 0.

Definitions and Theorems

Function: read-memory-unsigned16

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

Theorem: ubyte16p-of-read-memory-unsigned16

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

Theorem: natp-of-read-memory-unsigned16

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

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

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

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

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

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

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

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

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

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

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

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

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