		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Theorems-about-cstate-to-vars-and-execution

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 cstate-to-vars-fold-def rule in the mutual induction proof below. This rule, and its undesirability, is discussed in cstate-to-vars. This might be actually related to the issue discussed in the paragraph just above.

Definitions and Theorems

Theorem: cstate-to-vars-of-write-var-value

(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: cstate-to-vars-of-write-vars-values

(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: cstate-to-vars-of-restrict-vars

(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: cstate-to-vars-of-add-var-value

(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: cstate-to-vars-of-add-vars-values

(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: cstate-to-vars-of-exec-literal

(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: cstate-to-vars-of-exec-path

(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: cstate-to-vars-of-exec-expression

(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: cstate-to-vars-of-exec-expression-list

(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: cstate-to-vars-of-exec-funcall

(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: cstate-to-vars-of-exec-function

(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: cstate-to-vars-of-exec-statement

(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: cstate-to-vars-of-exec-statement-list

(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: cstate-to-vars-of-exec-block

(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: cstate-to-vars-of-exec-for-iterations

(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: cstate-to-vars-of-exec-switch-rest

(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)))))