Theorems about the static soundness of variable writing.
If check-safe-path and check-safe-path-list succeeds, also write-var-value and write-vars-values do. These are proved by showing that path checking ensures the success of path-to-var and paths-to-vars, and also the success of check-var and check-var-list. Then we show that check-var and check-var-list ensure that write-var-value and write-vars-values succeed, and finally we put things together.
Theorem:
(defthm path-to-var-when-check-safe-path (implies (not (reserrp (check-safe-path path varset))) (not (reserrp (path-to-var path)))))
Theorem:
(defthm check-var-when-check-safe-path (implies (not (reserrp (check-safe-path path varset))) (check-var (path-to-var path) varset)))
Theorem:
(defthm paths-to-vars-when-check-safe-path-list (implies (not (reserrp (check-safe-path-list paths varset))) (not (reserrp (paths-to-vars paths)))))
Theorem:
(defthm check-var-list-when-check-safe-path-list (implies (not (reserrp (check-safe-path-list paths varset))) (check-var-list (paths-to-vars paths) varset)))
Theorem:
(defthm write-var-value-when-check-var (implies (check-var var (cstate-to-vars cstate)) (not (reserrp (write-var-value var val cstate)))))
Theorem:
(defthm write-var-value-when-check-safe-path (implies (not (reserrp (check-safe-path path (cstate-to-vars cstate)))) (not (reserrp (write-var-value (path-to-var path) val cstate)))))
Theorem:
(defthm write-vars-values-when-check-var-list (implies (and (check-var-list vars (cstate-to-vars cstate)) (equal (len vals) (len vars))) (not (reserrp (write-vars-values vars vals cstate)))))
Theorem:
(defthm write-vars-values-when-check-safe-path-list (implies (and (not (reserrp (check-safe-path-list paths (cstate-to-vars cstate)))) (equal (len vals) (len paths))) (not (reserrp (write-vars-values (paths-to-vars paths) vals cstate)))))