		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Atc-write-object-rules

Rules about write-object.

The theorem about write-object turns it into update-object, similarly to how write-var is turned into update-var. The condition for the replacement is captured by write-object-okp, for which we supply rules to go through all the computation state layers. When the computation state (meta) variable is reached, it must be the case that there are hypotheses available saying that reading the object yields a value of appropriate type and length. The rule is used as last resort, only if the computation state is an ACL2 variable (as enforced by the syntaxp hypothesis).

For now we only support top-level object designators, but we plan to extend things to other object designators.

Since update-object takes the base address, the rules write-object-okp-of-update-object-same and write-object-okp-when-valuep-of-read-object need the hypothesis that the object designator is a top-level one.

We include the rule for commutativity of object-disjointp, so it does not matter the order of the disjoint objects in the hypotheses of the rules vs. the available hypothesis during the symbolic execution (i.e. commutativity normalizes them, via its loop stopper).

Definitions and Theorems

Function: write-object-okp

(defun write-object-okp (objdes val compst)
  (declare (xargs :guard (and (objdesignp objdes)
                              (valuep val)
                              (compustatep compst))))
  (let ((__function__ 'write-object-okp))
    (declare (ignorable __function__))
    (b* (((unless (objdesign-case objdes :alloc))
          nil)
         (addr (objdesign-alloc->get objdes))
         (heap (compustate->heap compst))
         (addr+obj (omap::assoc addr heap))
         ((unless (consp addr+obj)) nil)
         (obj (cdr addr+obj))
         ((unless (equal (type-of-value val)
                         (type-of-value obj)))
          nil))
      t)))

Theorem: booleanp-of-write-object-okp

(defthm booleanp-of-write-object-okp
  (b* ((yes/no (write-object-okp objdes val compst)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: write-object-okp-of-objdesign-fix-objdes

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

Theorem: write-object-okp-objdesign-equiv-congruence-on-objdes

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

Theorem: write-object-okp-of-value-fix-val

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

Theorem: write-object-okp-value-equiv-congruence-on-val

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

Theorem: write-object-okp-of-compustate-fix-compst

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

Theorem: write-object-okp-compustate-equiv-congruence-on-compst

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

Theorem: write-object-okp-of-add-frame

(defthm write-object-okp-of-add-frame
  (equal (write-object-okp objdes val (add-frame fun compst))
         (write-object-okp objdes val compst)))

Theorem: write-object-okp-of-enter-scope

(defthm write-object-okp-of-enter-scope
  (equal (write-object-okp objdes val (enter-scope compst))
         (write-object-okp objdes val compst)))

Theorem: write-object-okp-of-add-var

(defthm write-object-okp-of-add-var
  (equal (write-object-okp objdes val (add-var var val2 compst))
         (write-object-okp objdes val compst)))

Theorem: write-object-okp-of-update-var

(defthm write-object-okp-of-update-var
  (equal (write-object-okp objdes val (update-var var val2 compst))
         (write-object-okp objdes val compst)))

Theorem: write-object-okp-of-update-object-same

(defthm write-object-okp-of-update-object-same
 (implies
    (equal (objdesign-kind objdes) :alloc)
    (equal (write-object-okp objdes
                             val (update-object objdes val2 compst))
           (equal (type-of-value val)
                  (type-of-value val2)))))

Theorem: write-object-okp-of-update-object-disjoint

(defthm write-object-okp-of-update-object-disjoint
 (implies
   (object-disjointp objdes objdes2)
   (equal (write-object-okp objdes
                            val (update-object objdes2 val2 compst))
          (write-object-okp objdes val compst))))

Theorem: write-object-okp-when-valuep-of-read-object

(defthm write-object-okp-when-valuep-of-read-object
  (implies (and (syntaxp (symbolp compst))
                (equal (objdesign-kind objdes) :alloc)
                (equal old-val (read-object objdes compst))
                (valuep old-val))
           (equal (write-object-okp objdes val compst)
                  (equal (type-of-value val)
                         (type-of-value old-val)))))

Theorem: write-object-okp-of-if*-val

(defthm write-object-okp-of-if*-val
  (implies (and (write-object-okp objdes b compst)
                (write-object-okp objdes c compst))
           (write-object-okp objdes (if* a b c)
                             compst)))

Theorem: write-object-okp-when-valuep-of-read-object-no-syntaxp

(defthm write-object-okp-when-valuep-of-read-object-no-syntaxp
  (implies (and (equal (objdesign-kind objdes) :alloc)
                (equal old-val (read-object objdes compst))
                (valuep old-val))
           (equal (write-object-okp objdes val compst)
                  (equal (type-of-value val)
                         (type-of-value old-val)))))

Theorem: write-object-to-update-object

(defthm write-object-to-update-object
  (implies (write-object-okp objdes val compst)
           (equal (write-object objdes val compst)
                  (update-object objdes val compst))))

Theorem: write-object-of-objdesign-static

(defthm write-object-of-objdesign-static
  (equal (write-object (objdesign-static var)
                       val compst)
         (write-static-var var val compst)))