Static semantics of Yul.
We define the static semantics of Yul via ACL2 functions that check that the abstract syntax of Yul satisfies a number of constraints, described in [Yul]. We formalize different kinds of constraints separately.
