Evm Models Equivalence
▶
Overall Approach
▶
Code generation
Reasoning Interfaces
EvmYul Summaries
State Mapping
Proving Equivalence
Axioms and sorries
1
K generated code
▶
1.1
Structure of the Code
1.2
Prelude
▶
1.2.1
Type Abbreviations
1.2.2
Builtin Inductives
1.2.3
Inj
type class
1.2.4
Function Implementations
1.3
Generated Functions
▶
1.3.1
Modifications to the Generated Code
1.4
Rewrite
2
Interfaces
▶
2.1
EvmYul Interface
▶
2.1.1
Compatibility Axioms
2.1.2
Opcode Semantics
2.2
KEVM Interface
2.3
Gas Interface
3
State Map
▶
3.1
Type Mapping
3.2
State Mapping
3.3
Axiomatic Mapping
▶
3.3.1
Axioms as pre-theorems
4
EvmYul Summaries
▶
4.1
EVM.step
and
EVM.X
summary
5
Equivalences
▶
5.1
Defining Equivalence
▶
Clarifications on \(\rightarrow \)
5.2
Proof Outline
5.3
Case Study: Stack Operations
▶
5.3.1
Opcode Bundling
5.3.2
\(\forall p, p'\in S_{\text{KEVM}}\, \, \texttt{Rewrites}\, \, p \, \, p'\)
5.3.3
\(f\bigl(\text{stateMap}(p)\bigr) = \text{stateMap}(p')\)
5.4
Future Work
6
Axioms
▶
6.1
Generated code instances
6.2
Uninterpreted functions
6.3
Pre-theorems and theorem sorries
6.4
Subgoal sorries
Dependency graph
EVM Equivalence
Runtime Verification
Evm Models Equivalence
Overall Approach
Code generation
Reasoning Interfaces
EvmYul Summaries
State Mapping
Proving Equivalence
Axioms and sorries
1
K generated code
1.1
Structure of the Code
1.2
Prelude
1.2.1
Type Abbreviations
1.2.2
Builtin Inductives
1.2.3
Inj
type class
1.2.4
Function Implementations
1.3
Generated Functions
1.3.1
Modifications to the Generated Code
1.4
Rewrite
2
Interfaces
2.1
EvmYul Interface
2.1.1
Compatibility Axioms
2.1.2
Opcode Semantics
2.2
KEVM Interface
2.3
Gas Interface
3
State Map
3.1
Type Mapping
3.2
State Mapping
3.3
Axiomatic Mapping
3.3.1
Axioms as pre-theorems
4
EvmYul Summaries
4.1
EVM.step
and
EVM.X
summary
5
Equivalences
5.1
Defining Equivalence
Clarifications on \(\rightarrow \)
5.2
Proof Outline
5.3
Case Study: Stack Operations
5.3.1
Opcode Bundling
5.3.2
\(\forall p, p'\in S_{\text{KEVM}}\, \, \texttt{Rewrites}\, \, p \, \, p'\)
5.3.3
\(f\bigl(\text{stateMap}(p)\bigr) = \text{stateMap}(p')\)
5.4
Future Work
6
Axioms
6.1
Generated code instances
6.2
Uninterpreted functions
6.3
Pre-theorems and theorem sorries
6.4
Subgoal sorries