|
|
|---|
|
|
|
|---|
Top-level static soundness theorem.
This applies to the top-level block. If the block is safe, then its execution can only return either a final state or a limit error, never any other kind of error.
Theorem:
(defthm exec-top-block-static-soundness (implies (not (reserrp (check-safe-top-block block))) (b* ((cstate (exec-top-block block limit))) (implies (not (reserr-limitp cstate)) (not (reserrp cstate))))))