6 Axioms

We now give a full account of all the axioms / unproven results used throughout the project. We can differentiate these axioms in the following categories:

• Generated code instances: axioms that are needed for the generated code to be well behaved.

• Uninterpreted functions: axioms that pose the existence of a function without providing an implementation.

• Pre-theorems: axioms that should be turned into theorems.

• Theorem sorries: theorems with absent proofs that should hold.

• Subgoal sorries: subogals that have been sorried-out but are not the most critical part of the theorems they belong to.

6.1 Generated code instances

There are two instances that we have declared without providing any proof due to time constraints. For the SortK we have declared instances of the DecidableEq and LawfulBEq classes without providing any proofs. This has been done due to time constraints and code stability. However, these should be provable.

SortK is basically a sequence of elemts of sort SortKItem, which in turn has injections from every sort. This means that every time a new type was generated (by including more parts of the KEVM semantics in the generated code by adding more summaries) the proof should have to be adjusted.

The main application of these instances is to prove the results presents in GasInterface.lean.

6.2 Uninterpreted functions

Some functions in K are left for the backends to implement. These are called “hooked functions”. What this means is that these functions don’t have definition in the compiled K files. Instead, when such a function is encountered, K will use the implementation that the executing backend provides (the hook).

In our context, hooked functions come in two flavours: implemented or unimplemented. Implemented hooked functions are present in the Prelude.lean, and unimplemented or uninterpreted hooked functions are declared as axioms in the Func.lean file.

All axioms in Func.lean should only be unimplemented hooked functions.

6.3 Pre-theorems and theorem sorries

All axioms that are not uninterpreted functions should become a theorem at some point. We also have theorems that no proof has been attempted. All such statements are thought to hold, and not holding would imply discrepancies of some sort between the models.

6.4 Subgoal sorries

Some theorems have some subgoals sorried out. This is because we have provided the general structure of the proof, but haven’t got the time yet to close all subgoals.

All such subgoals should be provable requiring at most some small tweaking of the surrounding functions.