		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Read-object-of-write-object

How read-object changes under write-object.

We provide a read-over-write theorem, limited to top-level object designators. Handling other kinds of object designators is more complicated, due to the possibility of partial overlap of objects; we plan to tackle these eventually.

We also provide an object type preservation theorem, saying that if a computation state includes an object with a certain type, the computation state after a write-object still contains that object with the same type (although the value may have been changed). This theorem is also limited to top-level object designators, for the object whose preservation the theorem asserts; the object designator for write-object is arbitrary.

Definitions and Theorems

Theorem: read-object-of-write-object-when-auto/static/alloc

(defthm read-object-of-write-object-when-auto/static/alloc
  (implies (and (member-equal (objdesign-kind objdes)
                              '(:auto :static :alloc))
                (member-equal (objdesign-kind objdes1)
                              '(:auto :static :alloc))
                (not (errorp (write-object objdes val compst))))
           (equal (read-object objdes1
                               (write-object objdes val compst))
                  (if (equal (objdesign-fix objdes1)
                             (objdesign-fix objdes))
                      (if (equal (objdesign-kind objdes) :alloc)
                          (value-fix val)
                        (remove-flexible-array-member val))
                    (read-object objdes1 compst)))))

Theorem: read-object-of-write-object-when-auto/static/alloc-existing

(defthm read-object-of-write-object-when-auto/static/alloc-existing
 (b* ((compst1 (write-object objdes1 val compst)))
   (implies
        (and (not (errorp compst1))
             (member-equal (objdesign-kind objdes)
                           '(:auto :static :alloc))
             (not (errorp (read-object objdes compst))))
        (and (not (errorp (read-object objdes compst1)))
             (equal (type-of-value (read-object objdes compst1))
                    (type-of-value (read-object objdes compst)))))))