		Search-engine friendly clone of the ACL2 documentation.

States32

Memory32

Fixtype of memories [ISA:1.4].

We model the memory as a list of 2^{32} 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: memory32-equiv$inline

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

Theorem: memory32-equiv-is-an-equivalence

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

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

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

Theorem: memory32-fix-under-memory32-equiv

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

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

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

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

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

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

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

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

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

Subtopics

Memory32p: Recognizer for memory32.
Memory32-fix: Fixer for memory32.