No-function-definitions
The condition in which function definitions are elsewhere.
The FunctionHoister transformation, described in
[Solidity: Internals: The Optimizer: Yul-Based Optimizer Module:
Preprocessing: FunctionHoister],
moves all the function definitions to the top-level block.
The FunctionGrouper transformation, described in
[Solidity: Internals: The Optimizer: Yul-Based Optimizer Module:
Preprocessing: FunctionGrouper],
further moves them to the end of the top-level block,
putting the rest of the top-level block into a nested block
at the beginning of the top-level block.
An important property that these transformations establish
is that, aside from the top-level block,
there are no function definitions in statements and blocks.
Here we capture this property,
which is used as precondition for certain transformations.
Subtopics
- Statements/blocks/cases/fundefs-nofunp
- Mutually recursive functions that check
the absence of function definitions in
statements, blocks, cases, and function definitions.
- No-function-definitions-in-dynamic-semantics
- The condition in which function definitions are elsewhere,
applied to entities in the dynamic semantics.
- Fundef-list-nofunp
- Check that a list of function definitions
has no nested function definitions.
- Statements-to-fundefs-when-nofunp
- Theorem that statements-to-fundefs is nil
under statement-list-nofunp.
