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.

- 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.