Rules about read-var.
The theorems below about read-var are a bit different because read-var does not return a state, but a value instead.
The first theorem turns read-var into read-static-var when we encounter add-frame: since add-frame adds no variables in automatic storage, the variable must be in static storage.
The second theorem skips over enter-scope.
The third theorem either returns the value of the encountered variable or skips over it, based on whether the names coincide or not.
The fourth theorem serves for variables read in loops that are declared outside the scope of the loop, i.e. that are represented as update-vars: if the two variables are the same, the value is returned; otherwise, we skip over the update-var in search for the variable.
The fifth and sixth theorem describe the effect of read-var when it encounters update-static-var, which happens with C loops (not with C functions, because an add-frame would have been encountered first, turning read-var into read-static-var). If the variable names differ, we skip over the update-static-var. If the variable names are the same, the two functions cancel and we return the value, but only if the variable is not found in automatic storage.
The seventh theorem serves to move past object updates.
The eight theorem turns read-var into read-static-var
when the variable is not found in automatic storage.
This is used in the proofs for loops,
which do not use the rule
Theorem:
(defthm read-var-of-add-frame (equal (read-var var (add-frame fun compst)) (read-static-var var compst)))
Theorem:
(defthm read-var-of-enter-scope (implies (> (compustate-frames-number compst) 0) (equal (read-var var (enter-scope compst)) (read-var var compst))))
Theorem:
(defthm read-var-of-add-var (equal (read-var var (add-var var2 val compst)) (if (equal (ident-fix var) (ident-fix var2)) (remove-flexible-array-member val) (read-var var compst))))
Theorem:
(defthm read-var-of-update-var (equal (read-var var (update-var var2 val2 compst)) (if (equal (ident-fix var) (ident-fix var2)) (remove-flexible-array-member val2) (read-var var compst))))
Theorem:
(defthm read-var-of-update-static-var-different (implies (not (equal (ident-fix var) (ident-fix var2))) (equal (read-var var (update-static-var var2 val compst)) (read-var var compst))))
Theorem:
(defthm read-var-of-update-static-var-same (implies (not (var-autop var compst)) (equal (read-var var (update-static-var var val compst)) (remove-flexible-array-member val))))
Theorem:
(defthm read-var-of-update-object (implies (> (compustate-frames-number compst) 0) (equal (read-var var (update-object objdes obj compst)) (read-var var compst))))
Theorem:
(defthm read-var-to-read-static-var (implies (not (var-autop var compst)) (equal (read-var var compst) (read-static-var var compst))))
Theorem:
(defthm read-var-of-if* (equal (read-var var (if* a b c)) (if* a (read-var var b) (read-var var c))))