|
|
|---|
|
|
|
|---|
Abstract syntax of Yul.
We introduce an abstract syntax of Yul based on its concrete syntax.
The abstract syntax defined here is fairly close to the concrete syntax. The reason for this closeness is to reduce incidental differences between the code before and after a transformation, to facilitate inspection and debugging. (Although our formalization of Yul stands on its own, a major motivation for it is to formalize and verify Yul transformations.) In some cases our abstract syntax may be broader than the concrete syntax, to keep the definition of the abstract syntax slightly simpler; the important thing is that all the concrete syntax is representable in abstract syntax.
We plan to formalize a syntax abstraction mapping from the concrete syntax to the abstract syntax. For the time being, our parser can be regarded as proving a low-level version of that mapping, since it generates abstract syntax directly.