		Search-engine friendly clone of the ACL2 documentation.

Language

Static-soundness

Proof of static soundness of Yul.

We show that if the safety checks in the static semantics are satisfied, no dynamic semantics errors can occur during execution, except for running out of the artificial limit counter (since the static semantics clearly does not check for termination). This is a soundness property, because the safety checks in the static semantics are designed exactly to prevent the occurrence of those errors, which the dynamic semantics defensively checks.

Subtopics

Static-soundess-of-execution: Main static soundness theorems.
Theorems-about-cstate-to-vars-and-execution: Theorems about cstate-to-vars and execution.
Static-soundness-theorems-about-add-funs: Theorems about add-funs for the static soundness proof.
Static-soundness-theorems-about-modes: Theorems about modes for the static soundness proof.
Static-soundness-theorems-about-init-local: Theorems about init-local for the static soundness proof.
Check-var-list: Check if the variables in a list are all in a variable table.
Funinfo-safep: Check the safety of function information.
Static-soundness-theorems-about-find-fun: Theorems about find-fun for the static soundness proof.
Funenv-to-funtable: Turn a function environment into a function table.
Theorems-about-checking-expression-lists-in-reverse: Theorems about check-safe-expression-list and rev.
Static-soundness-of-variable-writing: Theorems about the static soundness of variable writing.
Funscope-to-funtable: Turn a function scope into a function table.
Funenv-safep: Check the safey of a function environment.
Funscope-safep: Check the safety of a function scope.
Cstate-to-vars: Turn a computation state into a variable table.
Funinfo-to-funtype: Turn function information into a function type.
Static-soundness-of-variable-addition: Theorems about the static soundness of variable addition.
Static-soundness-of-variable-reading: Theorems about the static soundness of variable reading.
Static-soundness-of-literal-execution: Theorem about the static soundness of literal execution.
Exec-top-block-static-soundness: Top-level static soundness theorem.
Static-soundness-of-path-execution: Theorem about the static soundness of path execution.