Theorems about cstate-to-vars and execution.
We prove theorems saying how the execution functions, and the auxiliary functions they use, operate on the variable tables obtained from the computation states. Many functions leave the variable table unchanged; some extend it, which we express via subset. In the case of restrict-vars, the theorem provides the exact result.
For the subset cases, we could prove more precise results, in terms of set operations; we had that during the development of the static soundness proof, but at some point it seemed that the subset formulation was more convenient. This is somewhat undesirable though: it seems more principled and clear to calculate the exact variable tables, rather than just constraining them to be superset. We will revisit this, seeing if we can keep the proof working with the theorems reformulated (perhaps this may actually make the overall proof simpler).
Note the use of the
Theorem:
(defthm cstate-to-vars-of-write-var-value (b* ((cstate1 (write-var-value var val cstate))) (implies (not (reserrp cstate1)) (equal (cstate-to-vars cstate1) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-write-vars-values (b* ((cstate1 (write-vars-values vars vals cstate))) (implies (not (reserrp cstate1)) (equal (cstate-to-vars cstate1) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-restrict-vars (equal (cstate-to-vars (restrict-vars vars cstate)) (intersect (identifier-set-fix vars) (cstate-to-vars cstate))))
Theorem:
(defthm cstate-to-vars-of-add-var-value (b* ((cstate1 (add-var-value var val cstate))) (implies (not (reserrp cstate1)) (equal (cstate-to-vars cstate1) (insert (identifier-fix var) (cstate-to-vars cstate))))))
Theorem:
(defthm cstate-to-vars-of-add-vars-values (b* ((cstate1 (add-vars-values vars vals cstate))) (implies (not (reserrp cstate1)) (equal (cstate-to-vars cstate1) (set::list-insert (identifier-list-fix vars) (cstate-to-vars cstate))))))
Theorem:
(defthm cstate-to-vars-of-exec-literal (b* ((outcome (exec-literal lit cstate))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-path (b* ((outcome (exec-path path cstate))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-expression (b* ((outcome (exec-expression expr cstate funenv limit))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-expression-list (b* ((outcome (exec-expression-list exprs cstate funenv limit))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-funcall (b* ((outcome (exec-funcall call cstate funenv limit))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-function (b* ((outcome (exec-function fun args cstate funenv limit))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-statement (b* ((outcome (exec-statement stmt cstate funenv limit))) (implies (not (reserrp outcome)) (subset (cstate-to-vars cstate) (cstate-to-vars (soutcome->cstate outcome))))))
Theorem:
(defthm cstate-to-vars-of-exec-statement-list (b* ((outcome (exec-statement-list stmts cstate funenv limit))) (implies (not (reserrp outcome)) (subset (cstate-to-vars cstate) (cstate-to-vars (soutcome->cstate outcome))))))
Theorem:
(defthm cstate-to-vars-of-exec-block (b* ((outcome (exec-block block cstate funenv limit))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (soutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-for-iterations (b* ((outcome (exec-for-iterations test update body cstate funenv limit))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (soutcome->cstate outcome)) (cstate-to-vars cstate)))))
Theorem:
(defthm cstate-to-vars-of-exec-switch-rest (b* ((outcome (exec-switch-rest cases default target cstate funenv limit))) (implies (not (reserrp outcome)) (equal (cstate-to-vars (soutcome->cstate outcome)) (cstate-to-vars cstate)))))