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.
This ACL2 library for Yul is being developed to provide a formalization of Yul in ACL2, verified Yul code transformations, and 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. However, since Yul is designed to be more general than Solidity.
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.