Dynamic-semantics
Dynamic semantics of Yul.
We define the dynamic semantics of Yul
by formalizing the Yul computation state
and by defining ACL2 functions that manipulate the computation state
via execution of the Yul abstract syntax.
The formalization also involves a function environment
that includes the Yul functions in scope,
and that is manipulated along with the computation state.
This is based on the formal specification in
[Yul: Specification of Yul: Formal Specification],
which defines an interpreter for Yul.
We formalize a big-step interpretive semantics,
which consists of mutually recursive execution functions.
To ensure their termination, as required by ACL2,
these functions take a limit argument
that is decremented at each recursive call.
This is an artificial limit,
that has no counterpart in the run-time data of an executing Yul program.
Formal proofs need to deal with this limit,
e.g. the termination of a Yul program is proved
by showing that there is a suitable limit that does not run out.
Subtopics
- Exec
- Mutually recursive execution functions.
- Init-local
- Initialize the local state of a computation state.
- Find-fun
- Find a function in the function environment by name.
- Mode
- Fixtype of modes.
- Write-vars-values
- Lift write-var-value to lists.
- Add-vars-values
- Lift add-var-value to lists.
- Add-funs
- Add functions to the function environment.
- Eoutcome
- Fixtype of expression outcomes.
- Ensure-funscope-disjoint
- Ensure that a function scope is disjoint from a function environment.
- Write-var-value
- Write a variable value to the computation state.
- Soutcome
- Fixtype of statement outcomes.
- Restrict-vars
- Restrict the variables in the local state to a specified set.
- Add-var-value
- Add a variable with a value to the computation state.
- Exec-top-block
- Execute the top block.
- Funinfo
- Fixtype of function information.
- Values
- Yul values.
- Cstate
- Fixtype of computation states.
- Read-vars-values
- Lift read-var-value to lists.
- Funinfo+funenv
- Fixtype of pairs consisting of
function information and a function environment.
- Read-var-value
- Read a variable value from the computation state.
- Funenv
- Fixtype of function environments.
- Funscope-for-fundefs
- Function scope for a list of function definitions.
- Exec-path
- Execute a path.
- Path-to-var
- Extract a variable from a path.
- Exec-literal
- Execute a literal.
- Funinfo+funenv-result
- Fixtype of errors and
pairs consisting of
function information and a function environment.
- Soutcome-result
- Fixtype of errors and statement outcomes.
- Paths-to-vars
- Extract variables from paths.
- Mode-set-result
- Fixtype of errors and osets of modes.
- Funscope-result
- Fixtype of errors and function scopes.
- Funinfo-result
- Fixtype of errors and function information.
- Funenv-result
- Fixtype of errors and function environments.
- Eoutcome-result
- Fixtype of errors and expression outcomes.
- Cstate-result
- Fixtype of errors and computation states.
- Funinfo-for-fundef
- Function information for a function definition.
- Literal-evaluation
- Evaluation of Yul literals.
- Lstate
- Fixtype of local states.
- Funscope
- Fixtype of function scopes.
- Mode-set
- Fixtype of osets of modes.
