		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Static-soundness-theorems-about-init-local

Theorems about init-local for the static soundness proof.

Some of these are actually more general and could be moved. These more general theorems are about adding variables, which is what init-local does for the local state of course.

First, we show that add-var-value fails iff add-var does (the value put into the variable entails no constraints), and the same holds for add-vars-values and add-vars provided that the number of values matches the number of variables.

We prove a theorem that characterizes the effect of init-local on the variable table of the computation state. This should belong to the theorems in theorems-about-cstate-to-vars-and-execution, and it can probably put there, but currently it needs some other theorems, but it may be possible to streamline and simplify its proof.

The theorem check-var-list-when-add-vars-not-error serves to establish that the output variables of a function are readable given that they have been added via init-local. This is not really a theorem about init-local, but it is related; nonetheless, we may move this theorem at some point.

We finally show that init-local fails iff the addition of the variables to the variable table fails, or the number of values does not match the number of variables.

Definitions and Theorems

Theorem: error-add-var-value-iff-error-add-var

(defthm error-add-var-value-iff-error-add-var
        (equal (reserrp (add-var-value var val cstate))
               (reserrp (add-var var (cstate-to-vars cstate)))))

Theorem: error-add-vars-values-iff-error-add-vars

(defthm
    error-add-vars-values-iff-error-add-vars
    (implies
         (equal (len vals) (len vars))
         (equal (reserrp (add-vars-values vars vals cstate))
                (reserrp (add-vars vars (cstate-to-vars cstate))))))

Theorem: cstate-to-vars-of-init-local

(defthm
 cstate-to-vars-of-init-local
 (implies
  (and (equal (len in-vals) (len in-vars))
       (not (reserrp (init-local in-vars in-vals out-vars cstate))))
  (equal
       (cstate-to-vars (init-local in-vars in-vals out-vars cstate))
       (add-vars out-vars (add-vars in-vars nil)))))

Theorem: check-var-list-when-add-vars-not-error

(defthm check-var-list-when-add-vars-not-error
        (implies (and (identifier-listp vars)
                      (identifier-setp varset)
                      (not (reserrp (add-vars vars varset))))
                 (check-var-list vars (add-vars vars varset))))

Theorem: reserrp-of-init-local

(defthm
     reserrp-of-init-local
     (equal (reserrp (init-local in-vars in-vals out-vars cstate))
            (or (reserrp (add-vars in-vars nil))
                (reserrp (add-vars out-vars (add-vars in-vars nil)))
                (not (equal (len in-vals) (len in-vars))))))