Theorem about the static soundness of path execution.
This is fairly easy, and relies on the theorem about read-var-value and check-var.
Theorem:
(defthm exec-path-when-check-safe-path (implies (not (reserrp (check-safe-path path (cstate-to-vars cstate)))) (b* ((outcome (exec-path path cstate))) (and (not (reserrp outcome)) (equal (eoutcome->cstate outcome) (cstate-fix cstate)) (equal (len (eoutcome->values outcome)) 1)))))