|
|
|---|
|
|
|
|---|
Static safety checking of Yul.
This is (the main) part of the Yul static semantics. It consists of checks that ensure the safety of execution, i.e. that certain situations never happen during execution, such as reading or writing a non-existent variable. Our formal dynamic semantics of Yul defensively checks these conditions, returning error values when the conditions are not satisfied. The static safety checks formalized here ensure that those error values are never returned by the dynamic semantics, as proved in static-soundness.
The static safety of the Yul constructs is checked with respect to (i) a set of variable names (identifiers) and (ii) an omap from function names (identifiers) to function input/output information. These are essentially symbol tables for variables and functions: they describe the variables and functions in scope.
These symbol tables for variables consists of the variables that are not only visible, but also accessible, according to [Yul: Specification of Yul: Scoping Rules]: a variable is visible in the rest of the block in which it is declared, including sub-blocks, but it is not accessible in function definitions in the block or sub-blocks. Variables that are visible but inaccessible are not represented in these symbol tables for variables.
The Yul static semantics requires that visible but inaccessible variables are not shadowed [Yul: Specification of Yul: Scoping Rules]. However, this requirement is not needed for safety, as evidenced by the fact that the static soundness proof in static-soundness does not make use of that requirement. In fact, we do not include that requirement in the static safety checks formalized here. This requirement is formalized separately in static-shadowing-checking.