• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Prime-field-constraint-systems
    • Proof-checker-array
    • Soft
    • Rp-rewriter
    • Farray
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Bigmem
      • Bigmem-concrete-stobj
      • Get-mem-aux
      • Get-mem
      • Write-mem$a
      • Read-mem$a
    • Regex
    • ACL2-programming-language
    • Java
    • C
    • Jfkr
    • X86isa
    • Equational
    • Cryptography
    • Where-do-i-place-my-book
    • Json
    • Built-ins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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)))))