|
|
|---|
|
|
|
|---|
Errors used in the formalization of Yul.
When we formalize static and dynamic semantics of Yul, our ACL2 functions return error values in certain circumstances. An example is when a variable is referenced that is not accessible.
We use fty::defresult and companion utilities to handle errors in our Yul formalization.