Theorems about the static soundness of variable addition.
If add-var and add-vars succeed, also add-var-value and add-vars-values do. Furthermore, the variable table for the resulting computation states is the same returned by the safety checks.
Theorem:
(defthm add-var-value-when-add-var (b* ((varset1 (add-var var (cstate-to-vars cstate))) (cstate1 (add-var-value var val cstate))) (implies (not (reserrp varset1)) (and (not (reserrp cstate1)) (equal (cstate-to-vars cstate1) varset1)))))
Theorem:
(defthm add-vars-values-when-add-vars (b* ((varset1 (add-vars vars (cstate-to-vars cstate))) (cstate1 (add-vars-values vars vals cstate))) (implies (and (not (reserrp varset1)) (equal (len vals) (len vars))) (and (not (reserrp cstate1)) (equal (cstate-to-vars cstate1) varset1)))))