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.
- Find-fun
- Find a function in the function environment by name.
- Init-local
- Initialize the local state of a computation state.
- 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.
- Soutcome
- Fixtype of statement 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.
- 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.
- Funinfo
- Fixtype of function information.
- Exec-top-block
- Execute the top block.
- Values
- Yul values.
- Cstate
- Fixtype of computation states.
- Funinfo+funenv
- Fixtype of pairs consisting of
function information and a function environment.
- Read-vars-values
- Lift read-var-value to lists.
- 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.
- Funinfo+funenv-result
- Fixtype of errors and
pairs consisting of
function information and a function environment.
- Exec-literal
- Execute a literal.
- Soutcome-result
- Fixtype of errors and statement outcomes.
- 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.
- Paths-to-vars
- Extract variables from paths.
- 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.
