Ethereum Formal Semantics for Gas Consumption Analysis

This is a formal semantics of Ethereum Virtual Machine (EVM) specialized for gas consumption analysis. This formal model is used for proving termination of any contract on EVM. The model is defined and property are proved using the Isabelle/HOL proof assistant, more precisely Isabelle/HOL 2018. The only assumptions made on EVM are:

Other technical assumptions and abstractions are explained in the theory files. There are two theory files. The two theories differs on a very particular point: how gas is consumed when a contract is called from another one.

The subtle differences between the two are explained in the comments at the beginning of the files.