		Search-engine friendly clone of the ACL2 documentation.

Language

Abstract-syntax

Abstract syntax of Yul.

We introduce an abstract syntax of Yul based on its concrete syntax; more precisely, on the new grammar (see description there).

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.

It is not yet clear whether the proper handling of Yul dialects will require extending this abstract syntax with types (which are not present in the new grammar). For now we omit types, but we may revisit this at some point.

Subtopics

Escape: Fixtype of escapes.
Swcase-list->value-list: Lift swcase->value to lists.
Hex-digit-list->chars: Extract the characters from a list of hex digits.
Fundef-list->name-list: Lift fundef->name to lists.
Literal: Fixtype of literals.
Path: Fixtype of paths.
Hex-string-rest-element: Fixtype of elements of hex strings after the first one.
Plain-string: Fixtype of plain strings.
String-element: Fixtype of string elements.
Hex-string-content-option: Fixtype of optional contents of hex strings.
Hex-string-content: Fixtype of contents of hex strings.
Identifier: Fixtype of identifiers.
Funcall-option: Fixtype of optional function calls.
Expression-option: Fixtype of optional expressions.
Statement-option: Fixtype of optional statements.
Literal-option: Fixtype of optional literals.
Identifier-option: Fixtype of optional identifiers.
Hex-string: Fixtype of hex strings.
Hex-quad: Fixtype of quadruples of hex digits.
Hex-digit: Fixtype of hex digits.
Hex-pair: Fixtype of pairs of hex digits.
Data-value: Fixtype of data values in Yul objects.
Data-item: Fixtype of data items in Yul objects.
Statements-to-fundefs: Filter function definitions out of a list of statements.
String-element-list-result: Fixtype of errors and lists of string elements.
Identifier-identifier-map-result: Fixtype of errors and maps from identifiers to identifiers.
Swcase-result: Fixtype of errors and swcase clauses (for switch statements).
String-element-result: Fixtype of errors and string elements.
Statement-result: Fixtype of errors and statements.
Literal-result: Fixtype of errors and literals.
Identifier-set-result: Fixtype of errors and sets of identifiers.
Identifier-result: Fixtype of errors and identifiers.
Identifier-list-result: Fixtype of errors and lists of identifiers.
Fundef-result: Fixtype of errors and function definitions.
Funcall-result: Fixtype of errors and function calls.
Expression-result: Fixtype of errors and expressions.
Escape-result: Fixtype of errors and escapes.
Path-result: Fixtype of errors and paths.
Block-result: Fixtype of errors and blocks.
Objects: Fixtypes of Yul objects and related entities.
Statements/blocks/cases/fundefs: Fixtypes of statements, blocks, cases, and function definitions.
Identifier-list: Fixtype of lists of identifiers.
Identifier-set: Fixtype of sets of identifiers.
Identifier-identifier-map: Fixtype of maps from identifiers to identifiers.
Identifier-identifier-alist: Fixtype of alists from identifiers to identifiers.
Hex-string-rest-element-list: Fixtype of lists of elements of hex strings after the first one.
String-element-list: Fixtype of string elements.
Path-list: Fixtype of lists of paths.
Hex-digit-list: Fixtype of lists of hex digits.
Literal-list: Fixtype of lists of literals.
Fundef-list: Fixtype of lists of function definitions.
Expressions/funcalls: Fixtypes of expressions and function calls.
Abstract-syntax-induction-schemas: Some induction schemas based on the Yul abstract syntax.