Theorems about the static soundness of variable reading.
If check-var and check-var-list succeed, also read-var-value and read-vars-values do.
Theorem:
(defthm read-var-value-when-check-var (implies (check-var var (cstate-to-vars cstate)) (not (reserrp (read-var-value var cstate)))))
Theorem:
(defthm read-vars-values-when-check-var-list (implies (check-var-list vars (cstate-to-vars cstate)) (not (reserrp (read-vars-values vars cstate)))))