		Search-engine friendly clone of the ACL2 documentation.

States

Read-memory-unsigned64

Read an unsigned 64-bit integer from memory.

Signature
(read-memory-unsigned64 addr stat feat) → val
Arguments: addr — Guard (integerp addr).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: val — Type (ubyte64p 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 address 0.

Definitions and Theorems

Function: read-memory-unsigned64

(defun read-memory-unsigned64 (addr stat feat)
  (declare (xargs :guard (and (integerp addr)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (let ((__function__ 'read-memory-unsigned64))
    (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))
         (b4 (read-memory-unsigned8 (+ addr 4)
                                    stat feat))
         (b5 (read-memory-unsigned8 (+ addr 5)
                                    stat feat))
         (b6 (read-memory-unsigned8 (+ addr 6)
                                    stat feat))
         (b7 (read-memory-unsigned8 (+ addr 7)
                                    stat feat)))
      (+ b0 (ash b1 8)
         (ash b2 16)
         (ash b3 24)
         (ash b4 32)
         (ash b5 40)
         (ash b6 48)
         (ash b7 56)))))

Theorem: ubyte64p-of-read-memory-unsigned64

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

Theorem: natp-of-read-memory-unsigned64

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

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

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

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

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

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

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

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

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

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

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

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

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