		Search-engine friendly clone of the ACL2 documentation.

States64

Memory64

Fixtype of memories [ISA:1.4].

We model the memory as a list of 2^{64} unsigned bytes, which can be interpreted in different ways (see operations on states).

This is the whole address space, although not all of it may be accessible, and parts of it may be dedicated to different purposes [ISA:1.4]. Modeling these aspects (probably via some kind of parameterization of the model) is future work.

Definitions and Theorems

Function: memory64-equiv$inline

(defun memory64-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (memory64p acl2::x)
                              (memory64p acl2::y))))
  (equal (memory64-fix acl2::x)
         (memory64-fix acl2::y)))

Theorem: memory64-equiv-is-an-equivalence

(defthm memory64-equiv-is-an-equivalence
  (and (booleanp (memory64-equiv x y))
       (memory64-equiv x x)
       (implies (memory64-equiv x y)
                (memory64-equiv y x))
       (implies (and (memory64-equiv x y)
                     (memory64-equiv y z))
                (memory64-equiv x z)))
  :rule-classes (:equivalence))

Theorem: memory64-equiv-implies-equal-memory64-fix-1

(defthm memory64-equiv-implies-equal-memory64-fix-1
  (implies (memory64-equiv acl2::x x-equiv)
           (equal (memory64-fix acl2::x)
                  (memory64-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: memory64-fix-under-memory64-equiv

(defthm memory64-fix-under-memory64-equiv
  (memory64-equiv (memory64-fix acl2::x)
                  acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-memory64-fix-1-forward-to-memory64-equiv

(defthm equal-of-memory64-fix-1-forward-to-memory64-equiv
  (implies (equal (memory64-fix acl2::x) acl2::y)
           (memory64-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-memory64-fix-2-forward-to-memory64-equiv

(defthm equal-of-memory64-fix-2-forward-to-memory64-equiv
  (implies (equal acl2::x (memory64-fix acl2::y))
           (memory64-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: memory64-equiv-of-memory64-fix-1-forward

(defthm memory64-equiv-of-memory64-fix-1-forward
  (implies (memory64-equiv (memory64-fix acl2::x)
                           acl2::y)
           (memory64-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: memory64-equiv-of-memory64-fix-2-forward

(defthm memory64-equiv-of-memory64-fix-2-forward
  (implies (memory64-equiv acl2::x (memory64-fix acl2::y))
           (memory64-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Subtopics

Memory64p: Recognizer for memory64.
Memory64-fix: Fixer for memory64.