		Search-engine friendly clone of the ACL2 documentation.

Bigmem-asymmetric

Get-mem

Get the entire contents of the memory in the form of a linear list

Signature
(get-mem mem) → memlist
Arguments: mem — Guard (memp mem).
Returns: memlist — Type (acl2::unsigned-byte-listp 8 memlist), given (memp mem).

Definitions and Theorems

Function: get-mem

(defun get-mem (mem)
  (declare (xargs :stobjs (mem)))
  (declare (xargs :guard (memp mem)))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'get-mem
                                     (list mem))
          (let ((__function__ 'get-mem))
            (declare (ignorable __function__))
            (acl2::rev (get-mem-aux (1- (expt 2 64)) mem)))))

Theorem: return-type-of-get-mem

(defthm return-type-of-get-mem
  (implies (memp mem)
           (b* ((memlist (get-mem mem)))
             (acl2::unsigned-byte-listp 8 memlist)))
  :rule-classes :rewrite)

Theorem: rewrite-read-mem-to-nth-of-get-mem

(defthm rewrite-read-mem-to-nth-of-get-mem
  (implies (and (unsigned-byte-p 64 i) (memp mem))
           (equal (read-mem i mem)
                  (nth i (get-mem mem)))))

Theorem: get-mem-after-write-mem

(defthm get-mem-after-write-mem
  (implies (unsigned-byte-p 64 i)
           (equal (get-mem (write-mem i v mem))
                  (update-nth i (loghead 8 v)
                              (get-mem mem)))))