		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Static-soundness-of-path-execution

Theorem about the static soundness of path execution.

This is fairly easy, and relies on the theorem about read-var-value and check-var.

Definitions and Theorems

Theorem: exec-path-when-check-safe-path

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