|
|
|---|
|
|
|
|---|
An ACL2 library for Yul.
Yul is a programming language that is being used as an intermediate language in the compilation of Ethereum smart contracts written in in the Solidity language. However, Yul is designed to be more general than Solidity, and may find additional uses soon.
This ACL2 library for Yul is being developed to provide a formalization of Yul in ACL2, as well as tools related to Yul and ACL2. This library is work in progress.
Yul is currently documented as part of the Solidity documentation, precisely in the `Yul' section of the Solidity documentation. However, since Yul is designed to be more general than Solidity, it is possible that eventually it may have its own documentation.
In the documentation of this ACL2 library, the Yul documentation (part of the Solidity documentation) is referenced as `[Yul]`; subsections of it are referenced by appending their titles separated by colons, e.g. `[Yul: Specification of Yul: Scoping Rules]`. These square-bracketed references may be used as nouns or parenthetically.
Since some aspects of Yul are described in part of the Solidity documentation that is not [Yul], we also reference (the rest of) the Solidity documentation, which we do as `[Solidity]' and `[Solidity: ...]', similarly to how we reference the Yul documentation proper.