Rules about read-object.
The theorems about read-object skip over all the functions that represent the computation states, except for possibly update-object: this is similar to the interaction between read-var and update-var.
The last theorem is a bit different. It lets us replace read-object with the more specific read-static-var when the object designator is for a static variable.
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).
Theorem:
(defthm read-object-of-add-frame (implies (or (equal (objdesign-kind objdes) :alloc) (equal (objdesign-kind objdes) :static)) (equal (read-object objdes (add-frame fun compst)) (read-object objdes compst))))
Theorem:
(defthm read-object-of-enter-scope (implies (equal (objdesign-kind objdes) :alloc) (equal (read-object objdes (enter-scope compst)) (read-object objdes compst))))
Theorem:
(defthm read-object-of-add-var (implies (equal (objdesign-kind objdes) :alloc) (equal (read-object objdes (add-var var val compst)) (read-object objdes compst))))
Theorem:
(defthm read-object-of-update-var (implies (equal (objdesign-kind objdes) :alloc) (equal (read-object objdes (update-var var val compst)) (read-object objdes compst))))
Theorem:
(defthm read-object-of-update-object-same (implies (equal (objdesign-kind objdes) :alloc) (equal (read-object objdes (update-object objdes val compst)) (value-fix val))))
Theorem:
(defthm read-object-of-update-object-disjoint (implies (object-disjointp objdes objdes2) (equal (read-object objdes (update-object objdes2 val compst)) (read-object objdes compst))))
Theorem:
(defthm read-object-of-objdesign-static (equal (read-object (objdesign-static var) compst) (read-static-var var compst)))
Theorem:
(defthm read-object-of-value-pointer->designator-of-if* (equal (read-object (value-pointer->designator ptr) (if* a b c)) (if* a (read-object (value-pointer->designator ptr) b) (read-object (value-pointer->designator ptr) c))))