		Search-engine friendly clone of the ACL2 documentation.

Bigmem

Get-mem-aux

Signature
(get-mem-aux i 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-aux

(defun get-mem-aux (i mem)
  (declare (xargs :stobjs (mem)))
  (declare (type (unsigned-byte 64) i))
  (declare (xargs :guard (memp mem)))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'get-mem-aux
                                     (list i mem))
          (let ((__function__ 'get-mem-aux))
            (declare (ignorable __function__))
            (if (zp i)
                (list (read-mem i mem))
              (cons (read-mem i mem)
                    (get-mem-aux (1- i) mem))))))

Theorem: return-type-of-get-mem-aux

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

Theorem: len-of-get-mem-aux

(defthm len-of-get-mem-aux
  (implies (and (memp mem) (natp i))
           (equal (len (get-mem-aux i mem))
                  (+ 1 i))))

Theorem: read-mem-and-get-mem-aux

(defthm read-mem-and-get-mem-aux
  (implies (and (memp mem)
                (<= i j)
                (natp i)
                (natp j))
           (equal (nth i (acl2::rev (get-mem-aux j mem)))
                  (read-mem i mem))))

Theorem: get-mem-aux-beyond-write-mem

(defthm get-mem-aux-beyond-write-mem
  (implies (< j i)
           (equal (get-mem-aux j (write-mem i v mem))
                  (get-mem-aux j mem))))

Theorem: get-mem-aux-after-write-mem

(defthm get-mem-aux-after-write-mem
  (implies (and (<= i j) (natp i) (natp j))
           (equal (get-mem-aux j (write-mem i v mem))
                  (update-nth (- j i)
                              (loghead 8 v)
                              (get-mem-aux j mem)))))