Dead-code-eliminator-execution
Proof that the DeadCodeEliminator transformation preserves
the execution behavior.
We prove that the elimination of dead code performed by the transformation
does not affect the dynamic semantics of the code,
i.e. the code calculates the same outputs for the same inputs
(essentially; more on this below).
In the Yul context, inputs must be understood as
(parts of) the computation state,
and outputs must be understood as
expression results as well as (parts of) the computation state.
We prove correctness theorems
for all the execution functions in the dynamic semantics:
a theorem for executing expressions,
a theorem for executing statements,
and so on.
This is natural, given that the proof is by mutual induction.
These execution functions
have slightly different argument and result types,
but they all take an initial computation state as argument,
and they all return a possibly modified computation state as result,
along with values for expressions (see eoutcome)
and modes for statements (see soutcome).
Roughly speaking, we prove theorems of the form
(exec (xform ast) cstate) = (exec ast cstate)
where exec is one of the execution functions
(e.g. exec-statement),
ast is an AST of Yul abstract syntax
(e.g. a value of type statement),
xform is the function that transforms ast
(e.g. statement-dead),
and cstate is a computation state.
But the actual formal assertion we prove is slightly different,
for two reasons explained below.
The first reason is that the execution functions
also take function environments as arguments,
which contain function bodies that must be transformed.
Thus, we define transformation functions on function environments,
and we refine the formulation of our theorems to
(exec (xform ast) cstate (xform funenv)) = (exec ast state funenv)
The second reason, and refinement of the theorems,
has to do with error results,
which may be returned by the defensive execution functions.
The error values include information about AST pieces
and the ACL2 call stack (see fty::defresult),
which causes a dependency of error values
on more than just the input/output behavior of ACL2 functions,
but also on the ASTs executed and the specific calls.
Since the DeadCodeEliminator transformation
removes certain pieces of ASTs,
some functions may return slightly different error values
when run on (xform ast) vs. ast.
The difference is inessential from a semantic point of view.
Thus, we define equivalence relations on execution results,
which weaken equality to accommodate slightly different errors.
The equivalence holds when two execution results are
either not errors and equal, or both errors;
that is, we consider all errors equivalent,
but we consider non-errors non-equivalent unless equal.
The theorem formulation is thus further refined to
(exec (xform ast) cstate (xform funenv)) ~=~ (exec ast cstate funenv)
where ~=~ denotes the equivalence
(we use this symbol just here, for readability).
The description above has left out the limit input of exec.
For this DeadCodeEliminator transformation,
that input is unchanged between the left side and right side,
because this transformation does not affect
the values taken by the limit during execution:
this transformation just removes code
that would never be executed anyways.
The theorems above are simultaneously proved
by mutual induction on the execution functions.
Since the execution functions make use of auxiliary semantic functions,
e.g. to read and write variables,
we first prove theorems about these functions.
These theorems also have essentially the form discussed above,
with the necessary adaptations.
It should be clear that the approach explained above
is more general than the DeadCodeEliminator transformation,
and should be applicable to other Yul transformations as well.
To summarize, the approach is:
- Extend the transformation from syntactic to semantic entities.
- Define equivalence relations over execution results.
- Prove equivalence theorems for the auxiliary semantic functions.
- Prove equivalence theorems for the execution functions.
Some theorems about the auxiliary semantic semantics
can be proved as equalities rather than equivalences.
In the proofs, we generally enable
functions ...-result-dead that transform result values.
This exposes the error and non-error cases in the proof.
Perhaps there is a way to avoid enabling these functions,
and using suitable rules instead.
In the proofs, we generally enable
the equivalence relations ...-result-okeq.
This, together with the enabling of the ...-result-dead functions,
exposes the error and non-error cases.
Perhaps there is a way to avoid enabling these functions,
and using suitable rules instead.
Subtopics
- Exec-of-dead
- Correctness theorems of the execution functions.
- Soutcome-result-okeq
- Equality of statement outcome results modulo errors.
- Eoutcome-result-okeq
- Equality of expression outcome results modulo errors.
- Funscope-dead
- Eliminate dead code in function scopes.
- Funinfo+funenv-result-dead
- Eliminate dead code in errors
and pairs consisting of
function information and a function environment.
- Funinfo+funenv-dead
- Eliminate dead code in pairs consisting of
function information and a function environment.
- Funinfo-dead
- Eliminate dead code in function information.
- Funscope-result-dead
- Eliminate dead code in errors and function scopes.
- Funenv-result-dead
- Eliminate dead code in errors and function environments.
- Funenv-dead
- Eliminate dead code in function environments.
- Add-funs-of-dead
- Correctness theorem for add-funs.
- Funscope-for-fundefs-of-dead
- Correctness theorem for funscope-for-fundefs.
- Funinfo-for-fundef-of-dead
- Correctness theorem for funinfo-for-fundef.
- Ensure-funscope-disjoint-of-dead
- Correctness theorem for ensure-funscope-disjoint.
- Find-fun-of-dead
- Correctness theorem for find-fun.
