		Search-engine friendly clone of the ACL2 documentation.

Transformations

Yul transformations in ACL2.

We formalize and verify some of the Yul transformations used in the Solidity compiler, which are documented at [Yul: Yul Optimizer].

Renaming-variables: Renaming of variables.
Dead-code-eliminator: The DeadCodeEliminator transformation.
Renamings: Renamings of variables and functions.
Disambiguator: The Disambiguator transformation.
Unique-variables: The condition in which all the variable names are distinct.
Dead-code-eliminator-static-safety: Proof that the DeadCodeEliminator transformation preserves the static safety checks.
No-function-definitions: The condition in which function definitions are elsewhere.
Unique-functions: The condition in which all the function names are distinct.
Renaming-functions: Renaming of functions.
Dead-code-eliminator-no-loop-initializers: Proof that the DeadCodeEliminator transformation preserves the condition in which loop initialization blocks are empty.
Dead-code-eliminator-no-function-definitions: Proof that the DeadCodeEliminator transformation preserves the condition in which functions are defined elsewhere.
No-loop-initializers: The condition in which loop initialization blocks are empty.
For-loop-init-rewriter: The ForLoopInitRewriter transformation.