		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Update-object

Update an object in a canonical representation of computation states.

Signature
(update-object objdes val compst) → new-compst
Arguments: objdes — Guard (objdesignp objdes).; val — Guard (valuep val).; compst — Guard (compustatep compst).
Returns: new-compst — Type (compustatep new-compst).

This is like write-object, but it does not return an error, and it only really handles top-level object designators, by taking the base address of the object designators, which is what we need for now. We update the heap with the new object regardless of whether an old object at that address exists or not, and whether, if it exists, its type matches the new object. This way, update-object always guarantees that the object goes into the heap, thus simplifying rules about it. When we replace write-object with update-object, we ensure that all the conditions mentioned above hold, so in a way update-object caches the fact that those conditions are satisfied.

Definitions and Theorems

Function: update-object

(defun update-object (objdes val compst)
  (declare (xargs :guard (and (objdesignp objdes)
                              (valuep val)
                              (compustatep compst))))
  (let ((__function__ 'update-object))
    (declare (ignorable __function__))
    (b* ((addr (objdesign->base-address objdes))
         (heap (compustate->heap compst))
         (new-heap (omap::update addr (value-fix val)
                                 heap))
         (new-compst (change-compustate compst
                                        :heap new-heap)))
      new-compst)))

Theorem: compustatep-of-update-object

(defthm compustatep-of-update-object
  (b* ((new-compst (update-object objdes val compst)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: update-object-of-objdesign-fix-objdes

(defthm update-object-of-objdesign-fix-objdes
  (equal (update-object (objdesign-fix objdes)
                        val compst)
         (update-object objdes val compst)))

Theorem: update-object-objdesign-equiv-congruence-on-objdes

(defthm update-object-objdesign-equiv-congruence-on-objdes
  (implies (objdesign-equiv objdes objdes-equiv)
           (equal (update-object objdes val compst)
                  (update-object objdes-equiv val compst)))
  :rule-classes :congruence)

Theorem: update-object-of-value-fix-val

(defthm update-object-of-value-fix-val
  (equal (update-object objdes (value-fix val)
                        compst)
         (update-object objdes val compst)))

Theorem: update-object-value-equiv-congruence-on-val

(defthm update-object-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (update-object objdes val compst)
                  (update-object objdes val-equiv compst)))
  :rule-classes :congruence)

Theorem: update-object-of-compustate-fix-compst

(defthm update-object-of-compustate-fix-compst
  (equal (update-object objdes val (compustate-fix compst))
         (update-object objdes val compst)))

Theorem: update-object-compustate-equiv-congruence-on-compst

(defthm update-object-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (update-object objdes val compst)
                  (update-object objdes val compst-equiv)))
  :rule-classes :congruence)