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