Rules about read-static-var.
These are somewhat similar to the ones about read-var. We go through the frame, the scopes, and the added (automatic) variables. We also go through the updated variables, provided that the names are distinct; this will have to be refined soon. We also go through object updates, which currently are only for objects in the heap (see update-object).
Theorem:
(defthm read-static-var-of-add-frame (equal (read-static-var var (add-frame fun compst)) (read-static-var var compst)))
Theorem:
(defthm read-static-var-of-enter-scope (equal (read-static-var var (enter-scope compst)) (read-static-var var compst)))
Theorem:
(defthm read-static-var-of-add-var (equal (read-static-var var (add-var var2 val compst)) (read-static-var var compst)))
Theorem:
(defthm read-static-var-of-update-var (implies (not (equal (ident-fix var) (ident-fix var2))) (equal (read-static-var var (update-var var2 val compst)) (read-static-var var compst))))
Theorem:
(defthm read-static-var-of-update-static-var (equal (read-static-var var (update-static-var var2 val compst)) (if (equal (ident-fix var) (ident-fix var2)) (remove-flexible-array-member val) (read-static-var var compst))))
Theorem:
(defthm read-static-var-of-update-object (equal (read-static-var var (update-object objdes val compst)) (read-static-var var compst)))