, Ok (g,pc,p,e))#l) = (case p.(pc) of, smallstep

, Call (gcall,ccall,name) ? if ((gcall>0)?(ccall>0)? (((length l)+1)<stack_lim)? ((gcall+ccall)?g)) then (case e(name) of None ?

#. Ok,

, execute

, As explained in the introduction, implementations generally use a slightly different semantics for the call: g is retracted to c 1 at the calling point for c 2 and g ref und is added when the control flow returns from c 2 . This is the case for (pevm, 2017) (see class BaseCall and class Call(BaseCall, The corresponding call stack will thus be

O. ,

O. ,

, Note that the ordering used for the previous semantics does not satisfy those constraints

. However, The termination ordering is a lexicographic combination of an order comparing the sum of all gas in the frames, an order comparing the size of the call stack, and finally an order comparing the type of the frame (where Ok > Halt > Exception). See (EFSimplem, 2020) for the complete formalization and Isabelle/HOL proof. The Isabelle/HOL development is around 900 lines. The proof of soundness is very similar to the previous one, p.20

S. Amani, M. Bégel, M. Bortin, and M. Staples, Towards verifying ethereum smart contract bytecode in isabelle/hol, CPP'18, pp.66-77, 2018.

V. Buterin, Ethereum: A Next-Generation SmartContract and Decentralized Application Platform, 2013.

. Efsimplem, Ethereum Formal Semantics for Gas Consumption Analysis -Implementations semantics, 2020.

. Efsyellow, Ethereum Formal Semantics for Gas Consumption Analysis -Yellow paper semantics, 2017.

, Formalization of Ethereum Virtual Machine in Lem, ETS, 2015.

W. Gavin, Ethereum: A secure decentralised generalised transaction ledger, 2014.

W. Gavin, Ethereum: A secure decentralised generalised transaction ledger, 2019.

, Official Go implementation of the Ethereum protocol, 2014.

N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz et al., Madmax: surviving out-of-gas conditions in Ethereum smart contracts, PACMPL, vol.2, p.27, 2018.

I. Grishchenko, M. Maffei, and C. Schneidewind, Foundations and Tools for the Static Analysis of Ethereum Smart Contracts, CAV'18, vol.10981, pp.51-78, 2018.

I. Grishchenko, M. Maffei, and C. Schneidewind, A Semantic Framework for the Security Analysis of Ethereum Smart Contracts, POST'18, vol.10804, pp.243-269, 2018.

E. Hildenbrandt, M. Saxena, N. Rodrigues, X. Zhu, P. Daian et al., KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine, CSF'18, pp.204-217, 2018.

Y. Hirai, Defining the Ethereum Virtual Machine for Interactive Theorem Provers, FC'17, vol.10323, pp.520-535, 2017.

J. Hudson, Upcoming Ethereum Hard Fork, vol.18, 2016.

J. Hudson, Upcoming Ethereum Hard Fork, 2016.

, A Python implementation of the Ethereum Virtual Machine, 2017.

, Pythonic Smart Contract Language for the evm, 2014.

R. Yang, T. Murray, P. Rimba, and U. Parampalli, Empirically Analyzing Ethereum's Gas Mechanism, 2019 IEEE European Symposium on Security and Privacy Workshops, pp.310-319, 2019.