		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Static-soundness-of-literal-execution

Theorem about the static soundness of literal execution.

This is very simple, because both static and dynamic semantics evaluate the literal.

We also show that it returns one value.

Definitions and Theorems

Theorem: exec-literal-when-check-safe-literal

(defthm exec-literal-when-check-safe-literal
        (implies (not (reserrp (check-safe-literal lit)))
                 (b* ((outcome (exec-literal lit cstate)))
                     (and (not (reserrp outcome))
                          (equal (eoutcome->cstate outcome)
                                 (cstate-fix cstate))
                          (equal (len (eoutcome->values outcome))
                                 1)))))