|
|
|---|
|
|
|
|---|
A formalization of the Yul language in ACL2.
This formalization covers a generic form of Yul that supports the types of the EVM dialect. The formalization consists of a concrete syntax, an abstract syntax, a static semantics, and a dynamic semantics. We plan to make this formalization more generic, and in particular to also support types in other Yul dialects.