Proof that the

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-statement`),
`statement`),
`statement-dead`),
and

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

(exec (xform ast) cstate (xform funenv)) ~=~ (exec ast cstate funenv)

where

The description above has left out the

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

- 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

In the proofs, we generally enable
the equivalence relations

- 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`.