Diana Nurbakova
email: diana.nurbakova@insa-lyon.fr

Liana Ermakova
email: liana.ermakova@univ-brest.fr

Irina Ovchinnikova
email: ovchinnikova.ig@1msmu.ru

Understanding the Personality of Contributors to Information Cascades in Social Media in Response to the COVID-19 Pandemic

Keywords: Personality traits, Sentiment analysis, Information cascades, Social media, COVID-19

Social media have become a major source of health information for lay people. It has the power to influence the public's adoption of health policies and to determine the response to the current COVID-19 pandemic. The aim of this paper is to enhance understanding of personality characteristics of users who spread information about controversial COVID-19 medical treatments on Twitter.

I. INTRODUCTION

Social media have become a major source of health information for lay people and have the power to influence the public's adoption of health policies and determine the response to the current COVID-19 pandemic. [START_REF] Vosoughi | The spread of true and false news online[END_REF] demonstrated that robots accelerate the spread of true and false news at the same rate as humans, implying that it is humans, not robots, who are responsible for spreading fake news and controversial information. Information circulation on social media has peculiar features due to message structure (length and format) and user behaviour (rules of sharing information, access to commenting on the message, etc.). Twitter users are able to share, cite short messages and add comments on them. Sharing and commenting on a hot topic tweet may result in producing an information cascade. Commenting on tweets and retweeting are two different behavioural strategies of users according to their personality and psychological type [START_REF] Marshall | Intellectual, narcissistic, or Machiavellian? How Twitter users differ from Facebook-only users, why they use Twitter, and what they tweet about[END_REF]. Although some research has been carried out in the field of microblog user profiling, research on the psychological characteristics of Twitter users is still an open challenge.

It has been shown that people with different personality characteristics show different information spreading behaviours in social media, for instance, in terms of retweets [START_REF] Lee | Who will retweet this? automatically identifying and engaging strangers on twitter to spread information[END_REF] or question answering [START_REF] Mahmud | Optimizing the selection of strangers to answer questions in social media[END_REF]. Thus, individuals with high scores on traits such as Conscientiousness, Openness, and Modesty are more likely to retweet the information [START_REF] Lee | Who will retweet this? automatically identifying and engaging strangers on twitter to spread information[END_REF]. Extraverted, agreeable individuals seeking excitement are more likely to respond to questions, unlike people scoring high on Conscientiousness [START_REF] Mahmud | Optimizing the selection of strangers to answer questions in social media[END_REF].

Moreover, the study on personality characteristics of persuasive individuals [START_REF] Oreg | Source personality and persuasiveness: Big five predispositions to being persuasive and the role of message involvement[END_REF] has demonstrated that the individuals with high scores on Extraversion and Openness are more likely to be persuasive during debates as opposed to those with a high score on Neuroticism. According to another study on persuasive argument prediction using author-reader personality characteristics [START_REF] Shmueli-Scheuer | Detecting persuasive arguments based on author-reader personality traits and their interaction[END_REF], reader Extraversion, Agreeableness, and Conscientiousness can be good indicators of persuasive arguments. Our interest in the relationship between personality characteristics and persuasion is motivated by the fact that individuals initiating cascades with their statements in tweets are more likely to be persuasive in their arguments.

We conduct a qualitative exploratory study with the objective of investigating how an individual's personality influences their participation in information cascades about controversial COVID-19 treatments on Twitter. Through the analysis of the tweets of public figures who triggered information cascades, and the reactions of other contributors to these cascades, we investigate how the personality characteristics of the participants of these cascades influence their behaviour on social media when dealing with health information. More precisely, we focus on the following research question: What are the personality characteristics of the most active contributors in information cascades about controversial COVID-19 treatments?

The remainder of the paper is organised as follows: Section II describes the background of the work carried out, Section III presents the original dataset and methodology of the study undertaken, Section IV reports and discusses the obtained results, and Section V concludes the paper.

II. BACKGROUND

In social media, information cascades appear when information flows develop hops due to comments on a comment of the initial tweet or its retweet that evokes comments [START_REF] Ribeiro | Message Distortion in Information Cascades[END_REF]. Information cascades have been studied in politics and economy because in politics and financial markets a sequence of decisions made by different agents based on the imitation of the choice of agents ahead of them may cause major societal change or a disaster [START_REF] Bikhchandani | A Theory of Fads, Fashion, Custom, and Cultural Change as Informational Cascades[END_REF]. When making a decision, the agent follows the stream regardless of their preferences and interests with no attempt to verify or reconsider information and act irrationally and impulsively [START_REF] Bikhchandani | A Theory of Fads, Fashion, Custom, and Cultural Change as Informational Cascades[END_REF]. The agents involved in an information cascade do not make one decision after another, they decide to join the activity straight after they receive a signal about the choice of those ahead of them and estimate the crowd of those who had chosen to join the activity and their experience [START_REF] Vany | Information Cascades in Multi-Agent Models[END_REF]. The cascades in social media were classified by [START_REF] Galuba | Outtweeting the Twitterers -Predicting Information Cascades in Microblogs[END_REF]. The authors distinguished two types of information cascades according to the direction of the information flow: (1) a further development of the initial tweet by followers (F-cascade); (2) a retweet that moves the information flow to another feed attracting more users to comment and share the initial information (RT-cascade) [START_REF] Galuba | Outtweeting the Twitterers -Predicting Information Cascades in Microblogs[END_REF]. As such, this makes it possible for the cascades to develop from person to person through word of mouth. When transferring information, a social network user needs to follow the rules and formatting of the platform design, and often shortens the initial tweet, paraphrases its text, includes emojis, etc. [START_REF] Boyd | Tweet, Tweet, Retweet: Conversational Aspects of Retweeting on Twitter[END_REF]. These transformations lead to information distortion; the distortion of information in cascades is extremely high due to the irrational behaviour of the cascade participants. In information cascades on social media, distortion appears when an original message is transformed from hop to hop [START_REF] Kumar | False information on web and social media: A survey[END_REF].

In studies of information distortion in social media, researchers have shown a connection between users' psychological traits and their willingness to reconsider information about COVID-19 published on the social media platform [START_REF] Bago | Fake news, fast and slow: Deliberation reduces belief in false (but not true) news headlines[END_REF], [START_REF] Pennycook | Fighting COVID-19 Misinformation on Social Media: Experimental Evidence for a Scalable Accuracy-Nudge Intervention[END_REF]. Users who skip reconsideration share unverified information even if they could recognize errors and fake news. The users -'retweeters' lack analytic cognitive style and follow their intuition in information evaluation [START_REF] Bago | Fake news, fast and slow: Deliberation reduces belief in false (but not true) news headlines[END_REF]. The information cascade participants who spread distorted information have a certain set of common psychological traits that come to light in their way of writing [START_REF] Mairesse | Using Linguistic Cues for the Automatic Recognition of Personality in Conversation and Text[END_REF].

The correlation between the linguistic features of a text or speech generated by an individual, and the individual's personality traits has been studied since Jungian experiments in the middle of the previous century. But it was only in the last quarter of the century that the standard procedures of text analysis and standard psychological tests established grounds for obtaining reliable results. However, the correlation is still unclear due to the impact of discourse and pragmatic factors on text generation. Topic, genre, recipient and communicative intention determine the text peculiarities including lexical choice and syntax structure. In social media, the effect of discourse is weakened by less restricted norms of conversation and the specific design of online communication. Studies of users' blogs and microblogs in social media show various possibilities of extracting personality characteristics from short texts aimed at searching for Big Five features through using pronouns and emotional words, auxiliary verbs and words reflecting discrepancy [START_REF] Mairesse | Using Linguistic Cues for the Automatic Recognition of Personality in Conversation and Text[END_REF]. Extraverts prefer positive emotion words and compliments showing more agreements than introverts [START_REF] Chung | Revealing dimensions of thinking in open-ended self-descriptions: An automated meaning extraction method for natural language[END_REF]. Conscientious people tend to strictly verbalise their ideas and thus avoid discrepancies, negative emotions and hesitations [START_REF] Mairesse | Using Linguistic Cues for the Automatic Recognition of Personality in Conversation and Text[END_REF]. Openness to experience reveals itself in objectivity and the disregard of first personal pronouns [START_REF] Mairesse | Using Linguistic Cues for the Automatic Recognition of Personality in Conversation and Text[END_REF]. However, the COVID-19 pandemic affects communication in social media forcing users to discuss particular topics and express mostly negative emotions on the platforms. Users show emotional involvement in conversation on research and treatment of the coronavirus. Moreover, they neglect grammatical rules and norms of syntax in short tweets. Therefore, analysis of semantic categories in the tweets provide reliable data to describe the users' personality profiles when in a stressful environment the personality traits are not seen clearly.

III. DATASET AND METHODOLOGY

In this Section, the dataset that was created and used for analysis will be presented. Second, the methodology used to reveal the psychological profiles of active contributors to the discussions about COVID-19 treatments will be described.

A. Data Description

We have collected 10 million tweets in English, including 141,866 tweets with distinct text. Twitter API1 was queried via Logstash2 with the following terms: ["science retraction", "chloroquine", "hydroxychloroquine", "Raoult", "remdesivir", "tocilizumab", "favipiravir", "Avigan", "azithromicyn", "azithromicyne", "#HCQ", "Axemal", "Dolquine", "Quensyl", "Hydroxychloroquinum", "Hydroxychloroquin", "Hidroxicloroquina", "Montagnier", "Hydroquin", "Quinoric"], in order to cover the topic of controversial medical treatment of COVID-19 [START_REF] Noel | Controverse scientifique[END_REF]. The tweets were published in the period between 30/03/2020 and 13/07/2020. In this dataset, 2,159,932 users were found to publish tweets in English.

Among these users, seven categories were selected (see statistics in Table I):

1) 192 users with the highest number of tweets about controversial treatments from our dataset (top); 2) 431 users with the most quoted tweets about controversial treatments (most_quoted); 3) 339 users with the most retweeted tweets about controversial treatments (most_rt); 4) 247 verified3 users with the highest number of tweets about controversial treatments (verified); 5) 196 users randomly selected from a set of users who published between 1 and 50 tweets about controversial treatments in our dataset (rnd_1_50); 6) 183 users randomly selected from a set of users who published between 50 and 500 tweets about controversial treatments in our dataset (rnd_50_500); 7) 292 users who published tweets in the cascades with a depth of at least four hops (cascade_depth_4). The majority of users have only one tweet about controversial treatments in the dataset (see Fig. 1a). However, many users published more than 500 tweets (Fig. 1b). After a closer look at these tweets, it could be seen that in many cases the text is the same but a short link to an external web page is different even though it points to the same external resource. These tweets are published within a short interval (a few seconds), therefore, it is supposed that they are generated automatically. That is why users who published less than 500 tweets were also analysed. Verified users often published between 1-10 tweets about controversial treatments. Twitter verifies the authenticity of public interest accounts, e.g. accounts maintained by public figures (music, acting, government, politics, religion, journalism, media, etc.). In general public figures published less than 50 tweets about controversial treatments (Fig. 1c). Therefore, it was decided to analyse users who tweeted with the same frequency as public figures considering that it is a normal tweeting rate (not bots). Information cascades appear on social media when a number of users choose the same option while sharing information by retweeting or quoting an initial tweet [START_REF] Galuba | Outtweeting the Twitterers -Predicting Information Cascades in Microblogs[END_REF]. Information cascades were created based on tweet replies and quotations, and cascades with a depth of at least four tweets were selected in order to have balanced categories. The users who participated in these cascades were added to the set of users under analysis, making the total number of selected users 1,880. The choice was limited by the number of free queries in IBM Personality Insights service that we used to predict users personality traits. For each user, the Tweepy 4 module was used to retrieve the last 200 tweets. To extract the personality traits of the users under consideration, the concatenated texts of tweets for each user were passed to IBM Personality Insights service.

B. Personality Traits

Personality traits were extracted by analysing the textual content of the last tweets of the participants of information cascades. From each of the seven aforementioned user categories, we selected those who had at least 10 user-generated tweets (i.e. retweets were excluded), in order to ensure the minimum text length for analysis. Such user generated content then constitutes the user profile for this study (see Table I for statistics per category).

To predict users' personality traits, the publicly available IBM Personality Insights 5 service was used, similar to the works of [START_REF] Shmueli-Scheuer | Detecting persuasive arguments based on author-reader personality traits and their interaction[END_REF], [START_REF] Herzig | Predicting customer satisfaction in customer support conversations in social media using affective features[END_REF]. This service infers psychological character-4 http://docs.tweepy.org/en/latest/api.html 5 https://cloud.ibm.com/apidocs/personality-insights istics of an individual based on the analysis of the input text they generated. It was trained mainly on social media datasets, such as Reddit and Twitter (e.g. see [START_REF] Chen | Understanding individuals' personal values from social media word use[END_REF]). The inference is performed with respect to three personality models:

• Big Five personality traits (agreeableness, conscientiousness, extraversion, emotional range, openness) each coupled with six facets detailing the corresponding trait: general dimensions characterising an individual's engagement with the world [START_REF] Costa | The revised neo personality inventory (neo-pir)[END_REF]. See Table II for lower level facets of the personality traits (as provided in [START_REF] Mahmud | Optimizing the selection of strangers to answer questions in social media[END_REF]). • Person's Needs (excitement, harmony, curiosity, ideal, closeness, self-expression, liberty, love, practicality, stability, challenge, structure): universal aspects of human behaviour reflecting the desires that people aim to satisfy via the consumption of a certain product or a service [START_REF] Kotler | Principles of Marketing[END_REF]. • Personal Values (Self-transcendence / Helping others; Conservation / Tradition; Hedonism / Taking pleasure in life; Self-enhancement / Achieving success; Open to change / Excitement): motivating factors and principles of people's lives [START_REF] Schwartz | Basic human values: Theory, measurement, and applications[END_REF]. Fifty-two personality characteristics can be obtained using this classifier. The results for this study are reported based on the percentile scores for all these characteristics.

C. Case Study Methodology

For expert study, five users per category were selected (5 users × 7 categories = 35 in total) among popular users who have original content about controversial treatment of COVID-19. The number of retweets were considered as a popularity measure. Among these 35 users, there were 14 verified accounts. A psycho-linguist manually analysed 200 recent tweets per user along with 100 the most frequent words from the concatenated tweets of each user.

For the psychological descriptions, a reliable set of linguistic units (mostly words) associated with a particular trait were used. The sets are represented as dictionaries or lexicons received in experimental studies and through content analysis of texts produced by those who filled in questionnaires to define the personality profile [START_REF] Seegmiller | Distinguishing Thinking-Feeling Preferences Through the Content Analysis of Natural Language[END_REF]. The dictionaries and lexicons were worked out for Jungian psychological types, which psychologists and psychotherapists have been applying in their studies and practical work [START_REF] Li | Learning Styles: A Review of Validity and Usefulness[END_REF]. In typology, Jung constructed four oppositions to distinguish psychological types based on the preferences in activity, information processing, reasoning and planning [START_REF] Jung | Psychological Types, ser[END_REF]. For the purpose of this study, the opposition of 'Thinking -Feeling' matches the criteria for expertise personality profiles of the Twitter users who participated in the The lower level facets of Big Five personality traits [START_REF] Mahmud | Optimizing the selection of strangers to answer questions in social media[END_REF] Big Five Trait Lower Level Facets Openness Imagination, Artistic interests, Emotionality, Adventurousness, Intellect, Liberalism Conscientiousness Self-efficacy, Orderliness, Dutifulness, Achievement-striving, Self-discipline, Cautiousness Extraversion Friendliness, Gregariousness, Assertiveness, Activity level, Excitement-seeking, Cheerfulness Agreeableness Trust, Morality, Altruism, Cooperation, Modesty, Sympathy Neuroticism Anxiety, Anger, Depression, Self-consciousness, Immoderation, Vulnerability information cascade generation. The opposition describes the difference between logical thinking and consideration based on social norms and attitudes. The first one is associated with analytic cognitive style, which is needed for critical analysis of information from unreliable sources [START_REF] Pennycook | Fighting COVID-19 Misinformation on Social Media: Experimental Evidence for a Scalable Accuracy-Nudge Intervention[END_REF]. Based on Seegmiller's dictionary (1987), where the sets of verbs for thinking and feeling types were included, the frequent verbs in tweets were analysed grouped into three semantic classes:

(1) acts of perception; (2) mental processes and actions; (3) emotions and feelings. The latter group corresponds to Feeling type. To strengthen the reliability of the expertise, adjectives and nouns with emotional connotations were extracted. Thus, for each user, a list of verbs and other words with emotional connotations was received. In each tweet, the analysis procedure included a comparison of frequent words denoting emotions and feelings with those referring to mental and perception activity in the tweets of each user. We evaluated the personality profile as Thinking, Feeling or Neutral according to the prevalence of a certain group of words. A user's personality was characterised as Thinking when verbs referring to mental and perception activity prevailed over the words with emotional connotations and verbs denoting feelings and emotions. When the prevalence was not essential, characterisation of the personality was avoided. The Thinking type is correlated with Conscientiousness and Emotional stability since the use of verbs of cognitive processes and insight shows significant negative correlation with the Dark Triad traits [START_REF] Sumner | Predicting Dark Triad Personality Traits from Twitter Usage and a Linguistic Analysis of Tweets[END_REF].

IV. RESULTS

This section will present the results of the study.

A. Users' Personality Profiles

First, the results of classification of users were studied w.r.t. three personality models, as described above. Fig. 4 depicts the averaged users' profiles in terms of personality models and categories depicted.

It can be seen that all considered categories share the same general tendency for most of the dimensions. Thus, the active contributors to information cascades have a tendency to score high 6 on Openness, Extraversion, and Neuroticism. While Extraversion and Openness traits align well with previous studies on the relation between user's engagement in social media and personality [START_REF] Lee | Who will retweet this? automatically identifying and engaging strangers on twitter to spread information[END_REF], [START_REF] Mahmud | Optimizing the selection of strangers to answer questions in social media[END_REF], Neuroticism may at first seem more surprising, but this could be explained by the context of COVID-19 pandemic that engenders messages of fear, loneliness, depression, anger, uncertainty, and grief, among others. Thus, it is reflected in terms of the facets of Neuroticism, where users score extremely high on Anger, and slightly less on Anxiety, Depression, Vulnerability, and Self consciousness. Mind that the individuals we are dealing with have actively taken part in the discussions of treatments. Note however, that people who score low on emotional stability are less likely to be considered credible or persuasive [START_REF] Shmueli-Scheuer | Detecting persuasive arguments based on author-reader personality traits and their interaction[END_REF], [START_REF] Falcione | The factor structure of source credibility scales for immediate superiors in the organizational context[END_REF], and therefore, effective in arguments. In contrast, the same context gives rise to the expression of Sympathy (facets of Agreeableness), Selfefficacy and Orderliness (facets of Conscientiousness), and an increase in Activity level (facets of Extraversion). Moreover, the users tend to score very high on the majority of facets of Openness. There is also a tendency for Openness to change in terms of Values.

Interestingly, the need for Curiosity stands apart. At the same time, the given context of pandemic and isolation influences such facets as Stability, Structure, Excitement, Harmony, Love, and Closeness, on which the users score extremely low.

As for individual tendencies considered category-wise, it was noted that two categories, namely verified (yellow) and Fig. 2: Correlation between Jung categories and personality traits rnd 1 50 (cyan), to some extent exhibit opposite tendencies, while still following the same general trends. For instance, verified gets the highest scores among other categories on Conscientiousness and Extraversion, and the lowest on Neuroticism, while rnd 1 50 is the opposite. The same tendencies can be found in terms of the facets of Conscientiousness, such as Cautiousness, Self-efficacy, Self-discipline, Achievement striving; Assertiveness and Activity level (facets of Extraversion), Trust and Sympathy (facets of Agreeableness). On the other hand, rnd 1 50 score the highest on all facets of Neuroticism, Values such as Hedonism, Openness to change, Self-transcendence, and Needs, such as Liberty, Ideal, and Self-expression. This duality is not surprising, as most of the verified accounts belong to public figures, while the majority of users constituting rnd 1 50 category are lay people.

B. Psycholinguistic Case Study

The results of the annotation of the users' tweets with Jung categories can be seen in Table III. To respect privacy, user IDs are not provided, nor is the text of tweets due to the paper limit.

The results of this analysis are summarised in Fig. 3. It shows the proportion of original texts in 200 recent tweets of 35 users. It can be seen that the Thinking class tends to have more original tweets than Feeling users or users we could not categorize (Neutral).

In order to align these results with the personality traits of the same users, we estimated the correlation between Jung categories and the personality traits (see Fig 2). It can be seen that Thinking positively correlated with Openness to change, Neuroticism, and Curiosity, while being negatively correlated with Agreeableness, Extraversion, and Conscientiousness. The latter is a rather surprising finding, which is due to the fact that the users in our dataset score low on Conscientiousness. In contrast, Feeling is positively correlated with Conscientiousness, Agreeableness, Stability, and Closeness. We consider that the opposition 'Thinking -Feeling' can provide additional nuances of a user's personality, which may be especially enriching when dealing with discussions that result in information cascades. In this paper, we investigated the personality characteristics of users who were spreading information about controversial COVID-19 medical treatments on Twitter. It was noted that the context of the pandemic accentuates the expression of emotional instability. Thus, the recent tweets of the active users who contributed to the information cascades about COVID-19 treatments tend to exhibit a user tendency to score high on Neuroticism. The differences in personalities of public figures versus lay people when tweeting were also highlighted. Moreover, the psycholinguistic analysis on a sample of popular and active users showed the prevailing tendency of the original content when the users belong to the class of Thinking.

Future work will consider user personality traits and use sentiment analysis to predict information distortion within cascades.

ACKNOWLEDGMENT

We would like to thank Bilel Benbouzid and Marianne Noël for the idea of studying controversial treatments of COVID-19 and for their participation in building the initial Twitter query.

Fig. 1 :

 1 Fig. 1: Number of tweets per user

Fig. 3 :

 3 Fig. 3: Proportion of original texts in 200 recent tweets

Fig. 4 :

 4 Fig. 4: Averaged personality traits of user categories regarding various dimensions of personality models

TABLE I :

 I Number of users and tweets in the overall dataset and in its subset with only original content

			top	most quoted most rt verified rnd 1 50 rnd 50 500 cascade depth 4	TOTAL
	All tweets	# users	192	431	339	247	196	183	292	1,880
		# tweets	38,357 85,450	67,150	49,236	37,094	36,488	57,344	371,119
	Original content	# users	127	429	338	234	180	124	286	1,718
	(min 10 per user) # tweets	9,898	61,064	47,514	28,154	15,995	7,329	35,378	205,332

TABLE II :

 II

https://developer.twitter.com/en/docs/twitter-api

https://www.elastic.co/fr/logstash

https://help.twitter.com/en/managing-your-account/ about-twitter-verified-accounts

Covering the latest news in all fields of science. Tweets by @wwrfd, @ThatMikeDenison and @Kate Travis. Publisher @soci-ety4science. See also @SNStudents.


Thomas Genet
email: thomas.genet@irisa.fr

Thomas Jensen
email: thomas.jensen@irisa.fr

Justine Sauvage
email: justine.sauvage@ens-lyon.fr

Termination of Ethereum's Smart Contracts a

Keywords: Formal Methods for Security, Ethereum, Smart Contracts, Security in Distributed Systems

Ethereum is a decentralized blockchain technology equipped with so-called Smart Contracts. A contract is a program whose code is public, which can be triggered by any user, and whose actual execution is performed by miners participating in Ethereum. Miners execute the contract on the Ethereum Virtual Machine (EVM) and apply its effect by adding new blocks to the blockchain. A contract that takes too much time to be processed by the miners of the network may result into delays or a denial of service in the Ethereum system. To prevent this scenario, termination of Ethereum's Smart Contracts is ensured using a gas mechanism. Roughly, the EVM consumes gas to process each instruction of a contract and the gas provided to run a contract is limited. This technique could make termination of contracts easy to prove but the way the official definition of the EVM specifies gas usage makes the proof of this property non-trivial. EVM implementations and formal analysis techniques of EVM's Smart Contracts use termination of contracts as an assumption, so having a formal proof of termination of contracts is crucial. This paper presents a mechanized, formal, and general proof of termination of Smart Contracts based on a measure of EVM call stacks.

A blockchain is a decentralized ledger, shared over a network, on which all users agree. Users can submit new elements to be added to this ledger. To add new elements in the ledger, one needs to add a new block (containing the new elements) to the blockchain. A block will be added to the blockchain if most of the participants agree on it. In Bitcoin, to add a new block to the chain, one has to solve a cryptographic puzzle on this new block in a limited amount of time (around 10 minutes in Bitcoin). This is called mining a block. Since the puzzle is computationally difficult it requires that most users participate in its resolution. Users contributing to the resolution are called miners. The fact that most miners try to solve the same puzzle entails that they all agree on the block itself and on all the added elements.

Bitcoin is equipped with a programming language, called Script (script, 2014), that is used to define programs reading inputs in the blockchain and proposing outputs (new elements) to be added to the blockchain. It is the role of the a This work was partially supported by Laboratoire d'excellence CominLabs miners to execute the Script programs and to build the new blocks containing the outputs of those programs. If one Script program is nonterminating, this prevents miners from building new blocks and adding them to the blockchain within the 10 minutes time limit. If many Script programs are non terminating, this could cause a denial of service in the Bitcoin system. This is the reason why the Script language is not Turingcomplete, in particular it has no loops.

Ethereum extends Bitcoin's blockchain with a Turing-complete programming language and the ability to store those programs (called contracts) in the blockchain itself. Contracts are programmed into dedicated high-level languages like [START_REF] Solidity | The Solidity Language[END_REF] or Vyper (vyper, 2017) and compiled to a bytecode format executed by the so-called Ethereum Virtual Machine (EVM). Since the programming language is Turing-complete, Ethereum needs to prevent looping contracts. In addition, Ethereum also targets to accelerate the pace of block additions w.r.t. Bitcoin. Thus, a terminating contract that takes too long to complete is another source of denial of service for Ethereum. Ethereum protects its system from non terminating programs and too complex programs with a single mechanism: the gas [START_REF] Buterin | Ethereum Formal Semantics for Gas Consumption Analysis -Implementations semantics[END_REF]. Intuitively, the EVM consumes gas to process each instruction of a contract and the gas provided to run a contract is limited.

Though this mechanism looks simple and robust, the protection it offers against denial of service is fragile. For instance, in 2016, badly chosen gas values for some EVM instructions resulted into several denial of service of Ethereum. This had to be fixed by two consecutive hard forks of the system (Hudson, 2016a;[START_REF] Hudson | Upcoming Ethereum Hard Fork[END_REF]. Independently of choosing for the best gas cost for each instruction, a general question to ask is whether the gas mechanism is sufficient to prove termination of any contract? Surprisingly, proving formally that this is true is not trivial because of the complexity of the EVM semantics (see Section 4).

The goal of this paper is twofold: to prove that no program can execute indefinitely without consuming gas in the EVM execution model, and to prove it in a way that can be used in a mechanized proof. More precisely, we present two termination proofs on two slightly different EVM semantics. The first model is the formal semantics of the (foundational) Ethereum Yellow Paper [START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF], the Isabelle/HOL EVM semantics [START_REF] Hirai | Defining the Ethereum Virtual Machine for Interactive Theorem Provers[END_REF][START_REF] References Amani | Towards verifying ethereum smart contract bytecode in isabelle/hol[END_REF] and the small-step formal semantics of [START_REF] Grishchenko | A Semantic Framework for the Security Analysis of Ethereum Smart Contracts[END_REF]. The second model is the semantics of the reference implementations of EVM such as (pevm, 2017; gevm, 2014). Noteworthy, the implementations and the Yellow Paper disagree on the gas consumption when calling a contract from another contract. In the Yellow Paper, when a contract c 1 calls another contract c 2 with, say, g units of gas, the gas associated to c 1 is not charged immediately. In implementations, this gas is immediately consumed. This little difference in the semantics makes a big difference when we are interested in proving the termination of contracts. Indeed, with the Yellow Paper semantics, a contract c 1 calling itself can loop without consuming gas, until it exhausts the call stack. This paper provides a termination proof of contracts for the two semantics. Proving termination of contracts when gas is charged immediately is natural and will be briefly discussed in Section 6. Proving termination of the contracts for the Yellow Paper semantics is more difficult and requires a complex termination measure on call stacks. Though the Yellow Paper semantics differs from the reference implementations, having a termination proof for this semantics is important. First, this termination proof contributes evidence that the Yellow Paper semantic model is indeed coherent. Second, this semantics serves as a base for formal verification tools, such as [START_REF] Grishchenko | A Semantic Framework for the Security Analysis of Ethereum Smart Contracts[END_REF]Grishchenko et al., 2018a), or for formal semantics such as [START_REF] Hirai | Defining the Ethereum Virtual Machine for Interactive Theorem Provers[END_REF][START_REF] References Amani | Towards verifying ethereum smart contract bytecode in isabelle/hol[END_REF]. In those tools and semantics, the termination of contracts is used as an assumption. In particular, in the Isabelle/HOL formalization of [START_REF] Hirai | Defining the Ethereum Virtual Machine for Interactive Theorem Provers[END_REF][START_REF] References Amani | Towards verifying ethereum smart contract bytecode in isabelle/hol[END_REF] the termination of the contract evaluation is proven using an internal step counter, which is not related to the gas, and simplifies the proofs. 1 Our proof complement their work by showing how the gas itself ensures termination of contracts, and thus assuming termination of contracts in the Yellow Paper semantics was indeed correct.

Contributions: This paper gives the first formal and mechanized proof of termination of EVM contracts, written in EVM bytecode. The central part is a measure that can be used for the proof of termination in a proof assistant (in our case Isabelle/HOL). We prove termination for:

• the two variants of the semantics of the contract call described above;

• a formal model where contracts can add and run arbitrary new contracts;

• a formal model that safely over-approximates the EVM semantics with minimal assumptions. In particular, for non-zero cost byte code operations (i.e. all operations except STOP, RETURN, REVERT), we only require that they have any strictly positive cost. Similarly, we only require the call stack size is upper-bounded by any natural number greater than 0.

Note that having minimal assumptions on the concrete gas costs for each operation is valuable because the gas cost has already changed several times during the EVM's lifetime 2 and is likely to evolve again since gas pricing of operations is still not fully satisfactory [START_REF] Yang | Empirically Analyzing Ethereum's Gas Mechanism[END_REF].

RELATED WORK

The Ethereum system has been formalized in the so-called Yellow Paper [START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF] which has been updated recently [START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF]. This update does not impact gas consumption but provides some new instructions which are taken into account in our formal proof. A nice complementary reading is the White Paper [START_REF] Buterin | Ethereum Formal Semantics for Gas Consumption Analysis -Implementations semantics[END_REF] which provides useful intuitions about the system. There are several available reference implementations of EVM such as (pevm, 2017; gevm, 2014). Grishchenko et al. have proposed EtherTrust (ethertrust, 2017) a verification framework for the static analysis of contracts code (Grishchenko et al., 2018a). The static analysis tools focus on proving some security properties on contracts, such as singleentrancy [START_REF] Grishchenko | A Semantic Framework for the Security Analysis of Ethereum Smart Contracts[END_REF]. EtherTrust comes with a complete small-step semantics for EVM [START_REF] Grishchenko | A Semantic Framework for the Security Analysis of Ethereum Smart Contracts[END_REF]) that uses the Yellow Paper semantics for the contract call.

There are several attempts to define a mechanized and formal semantics of EVM. The first one was defined in Lem by Yoichi Hirai [START_REF] Hirai | Defining the Ethereum Virtual Machine for Interactive Theorem Provers[END_REF]. This semantics was defined to prove safety and security properties on specific contracts. It is partially executable and can be used to export Isabelle/HOL theories. The objective here was to compile EVM bytecode to Isabelle/HOL theories so that properties on those specific contracts can be proved in Isabelle/HOL. This semantics is very precise w.r.t. specification of low level operations of EVM but it does not precisely follow the gas consumption during calls (see Section 6.2 of [START_REF] Hirai | Defining the Ethereum Virtual Machine for Interactive Theorem Provers[END_REF]). Thus, this mechanized semantics is not usable, as is, for the proof we want to carry out. Another mechanized semantics is the one by Everett Hildenbrandt et al. [START_REF] Hildenbrandt | KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine[END_REF] in the K framework. This semantics is fully executable and passes official test suite of EVM (ETS, 2015). This semantics consumes gas at the call point (see rule <k> callWithCode in https://github.com/kframework/evm-semantics/ blob/master/evm.md).

In Section 6, we will discuss termination of contracts in this specific setting.

A contract running out of gas stops without completing its task and becomes useless. Thus estimating gas consumption of contracts is an ac-tive research subject. For instance, [START_REF] Grech | Madmax: surviving out-of-gas conditions in Ethereum smart contracts[END_REF] proposes a static analysis of contract's code to detect resumable loops, loops bounded by inputs, etc. that can lead to an execution running out of gas. Our objective here is different since we aim at proving that whatever the contract code, it cannot loop forever while not spending gas.

ETHEREUM

The blockchain of Ethereum describes the global state of the system, noted σ. In Ethereum a global state σ contains accounts. An account is a structure composed of 4 elements: a nonce, a balance (an amount of money in the virtual currency called Ether), a data storage and a code. In Ethereum, there exists two types of accounts: external accounts with an empty code and contracts with a non-empty code.

Calling a contract External accounts are used to store information and Ether. Like in Bitcoin, it is possible to transfer Ether from an account to another through a transaction. When a transaction is sent to an account having a code, i.e. a contract, a part of the money is used to pay for the execution of the code3 . This is called calling a contract. When calling a contract, the sent money is not collected by the contract itself but by the miner who accepts to execute contract's code and to add the updated accounts and blocks to the blockchain. In other words, from a given global state σ, the miners produce the new global state σ resulting of the transactions (and contracts) application on σ. Since adding blocks to the blockchain costs computation power, the miner needs a way to estimate if the reward (money sent to the contract) is competitive with its own computational effort. In Ethereum, this estimation is made possible through the gas mechanism. Every basic instruction of contract's code has a fixed cost in gas and every contract claims an (estimated) maximal cost in gas to run its code. Besides, when an account calls a contract it also fixes a gas price in Ether. This is used to motivate miners to execute one particular transaction by increasing the gas price and thus their reward.

Example 1. On the left-hand side of Figure 1

(2)

(3)

Figure 1: Account aj calls contract ai and miner m process the transaction with a respective balance 130 and 20. Account a i is a contract and a j is an external account. Account a i has a storage called i whose value is 4.

The code of a i is simply i++, i.e., it increments i.

Assume that the estimated maximal cost of contract a i is g. Assume that account a j builds a transaction T towards a i , where a j calls a i with g gas. To simplify the presentation, we do not consider gas price and assume that one gas costs one Ether. Assume that a miner m processes the transaction T and then adds the new blocks encoding the new values of accounts a i and a j in the new blockchain global state σ . In σ , in the account a i , i is now 5 (1). Note that balance of a i has not evolved. Balance of a j has been decreased of g gas unit and increased by g which is a (possible) gas refund (2). Indeed, contract a i claims to need g gas units to run its code but less gas may actually be needed. Here we assume that there were g gas left after the execution of a i . This gas is refunded to a j . Finally, the miner m who adds the blocks in σ is rewarded by gg gas ( 3). Another possibility would have been that execution of a i needs more than g gas. In this case, the execution of a i runs out of gas, an exception is thrown, the value of i in a i does not change, the g gas are lost by a j , and the miner m wins g gas. Precise estimation of gas consumption for contracts is, in itself, a research subject [START_REF] Grech | Madmax: surviving out-of-gas conditions in Ethereum smart contracts[END_REF].

Creating a contract Any contract c 1 can create a (new) contract c 2 with any arbitrary code, provided that c 1 is given enough gas to store all the instructions of the bytecode of c 2 in the new global state σ . If contract creation succeeds, this makes contract c 2 publicly available in σ .

ETHEREUM VIRTUAL MACHINE : EVM

Contract code is run on the Ethereum Virtual Machine (EVM). Contracts are written in highlevel languages such as [START_REF] Solidity | The Solidity Language[END_REF] or Vyper (vyper, 2017) and compiled to a bytecode format specific to EVM. A bytecode program is a list of instructions and during the execution a program counter (pc) gives the index of the next instruction to execute. EVM is a stack machine and the effect of arithmetic instructions, test instructions, storage instructions is to read and/or modify this stack, called the execution stack.

There are more than 60 different instructions in EVM. We can split them in 5 families:

• Execution stack operations This family encompasses all arithmetic, logic and test instructions like ADD, SUB, AND, OR, EQ, LT, etc. This family also contains instructions that push, pop, swap or duplicate the elements on the execution stack.

• Memory access This family contains instructions whose effect is to transfer data between the execution stack and either the temporary local memory (MLOAD, MSTORE) or into the permanent memory (SLOAD, SSTORE). The temporary local memory is a memory where a contract can read and write during its execution and which is erased after contract's completion. The permanent memory is in accounts' storage (thus in the blockchain) and will survive after contract's completion, like variable i in contract a i of Example 1.

• Environment operations These are the operations that gather information on the current transaction and contract (who called this contract, how many gas unit are left, etc.).

• Control flow operations Those operations modify the control flow inside the same contract: JUMP, JUMPI (conditional jump), JUMPDEST (marks a jump destination), . . .

• System operations This family gathers all the operations that permit to create and destroy a contract (CREATE, SUI-CIDE in [START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF], or SELFDESTRUCT in [START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF]) and the call and exit operations on contracts (CALL, CALLCODE, DELEGATECALL, RETURN) and additional (REVERT, CALLSTATIC) in [START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF].

The differences between the four types of call (CALL, CALLCODE, DELEGATECALL, CALLSTATIC) are subtle. The differences essentially lies in the way the global state is affected by calling the contract and not about the way gas is consumed. The contract called by CALL changes the state of the callee, like in Example 1. The contract called by CALLCODE changes the state of the caller, like when calling a library code. In Example 1, assume that state of account a j has a field i, then a CALLCODE on a i , would have incremented the value of this field in the state of account a j . The DELEGATECALL acts as a CALLCODE except that the identity of the contract caller is different. In a contract c 1 , if contract c 2 is called with DELEGATECALL, the call to contract c 2 happens like with a CALLCODE except that identity of the caller is not c 1 but the identity of the caller of c 1 . See (Grishchenko et al., 2018a) for details. Finally, CALLSTATIC is similar to CALL except that no modification of the state is permitted. It can be considered as a "pure" function call without side-effects. Since there is no difference between the 4 call instructions w.r.t. to gas consumption, we will abstract them in the same way in Section 5.2.

As explained above, to implement the gas mechanism, EVM's designers have chosen to associate each operation with a cost in gas. All operations, except zero-cost operations (STOP, REVERT and RETURN), have a cost strictly greater than zero. Some instructions, like SELF-DESTRUCT or SSTORE may result into a gas refund. SELFDESTRUCT destroys the current executed contract and the Ether which may be present in the account is refunded. SSTORE writes information in the permanent storage of the account and, thus, in the blockchain. Refund with SSTORE happens when it replaces a non-zero value by a zero. This kind of erasure permits to save space in the blockchain and is, thus, rewarded. Refunds obtained using SELF-DESTRUCT or SSTORE are accumulated during the execution in a separate counter and given back after the completion of the whole contract. As a result, during the contract execution, the available gas is not increased by those specific refunds. Now, to give some intuition about EVM's behavior, we describe more precisely the semantics of some particular instructions. We present all those instructions through their EtherTrust (ethertrust, 2017) small-step semantic rules. Some examples of Yellow Paper se-mantics and their EtherTrust counterpart can be found here [START_REF] Genet | Termination of Ethereum's Smart Contracts[END_REF]. The interest of EtherTrust rules w.r.t to the Yellow Paper is that they describe in the same place the effect of the instruction on the state of the system and the gas consumption.

The ADD instruction

The rules for the ADD instruction are given Figure 2-1. In these rules, µ is the local state of the stack machine where µ.s denotes the execution stack, µ.pc the program counter, µ.gas the available gas. The other record ι represents the parameters of the transaction where ι.code denotes the program under execution. Thus ι.code[µ.pc] is the current instruction to execute. Below the line of the semantic rules, (µ, ι, σ, η) :: S is the current call stack. An element of the call stack is called a frame, e.g., (µ, ι, σ, η) is the top frame of the current call stack. The field η is a transaction effect where the only information that could be relevant for us w.r.t. gas consumption would be the refund counter. However, as explained in Section 3, this refund counter is separate from the gas available for operation execution. Finally, σ is the current state of the global state. Since, there are no side effects, every update on this global state is propagated by the semantic rules. In the first rule, for ADD, there is enough gas to execute ADD and an execution stack with at least two elements. Thus, the call stack becomes (µ , ι, σ, η) :: S where µ is µ with an updated execution stack, an increased program counter µ.pc, and a µ.gas decreased of 3 gas units. The second rule defines the execution of ADD when there are not enough elements on the execution stack or not enough gas to execute ADD. This results into stacking an exception frame (EXC) on top of the call stack.

The CALL instruction

The rule for the CALL (Figure 2-2) defines the CALL execution when everything is OK: the execution stack contains enough arguments to perform the call (µ.s has at least 7 elements), there is enough gas to perform the call µ.gas ≥ c, and there is room in the call stack to add a new frame (|A| + 1 < 1024). The cost c is the sum of the costs for calling the CALL instruction itself (700 gas units) plus a variable cost depending on the size of the input and output of the contract: this gas is paid when reading contract parameters and outputting its future result. On the lower part of 1 words in memory set to zero. Only the gas is instantiated with the gas value available for the execution.

Small-Step Rules

In the following, we will present a selection of interesting small-step rules in order to illustrate the most important features of the semantics.

For demonstrating the overall design of the semantics, we start with the example of the arithmetic expression ADD performing addition of two values on the machine stack. Note that as the word size of the stack machine is 256, all arithmetic operations are performed modulo 2 256 .

ι.code[µ.pc] = ADD µ.s = a :: b :: s µ . gas ≥ 3 µ ′ = µ[s → (a + b) :: s][pc += 1][gas -= 3] Γ (µ, ι, σ, η) :: S → (µ ′ , ι, σ, η) :: S ι.code[µ.pc] = ADD (|µ.s| < 2 ∨ µ.gas < 3)
Γ (µ, ι, σ, η) :: S → EXC :: S

We use a dot notation, in order to access components of the different state parameters. We name the components with the variable names introduced for these components in the last section written in sans-serif-style. In addition, we use the usual notation for updating components: t[c → v] denotes that the component c of tuple t is updated with value v. For expressing incremental updates in a simpler way, we additionally use the notation t[c += v] to denote that the (numerical) component of c is incremented by v and similarly t[c -= v] for decrementing a component c of t.

The execution of the arithmetic instruction ADD only performs local changes in the machine state affecting the local stack, the program counter, and the gas budget. For deciding upon the correct instruction to execute, the currently executed code (that is part of the execution environment) is accessed at the position of the current program counter. The cost of an ADD instruction is constantly three units of gas that get subtracted from the gas budget in the machine state. As every other instruction, ADD can fail due to lacking gas or due to underflows on the machine stack. In this case, the exception state is entered and the execution of the current internal transaction is terminated. For better readability, we use here the slightly sloppy ∨ notation for combining the two error cases in one inference rule.

Small-Step Rules

In the following, we will present a selection of interesting small-step rules in order to illustrate the most important features of the semantics.

For demonstrating the overall design of the semantics, we start with the example of the arithmetic expression ADD performing addition of two values on the machine stack. Note that as the word size of the stack machine is 256, all arithmetic operations are performed modulo 2 256 .

ι.code[µ.pc] = ADD µ.s = a :: b :: s µ . gas ≥ 3 µ ′ = µ[s → (a + b) :: s][pc += 1][gas -= 3] Γ (µ, ι, σ, η) :: S → (µ ′ , ι, σ, η) :: S ι.code[µ.pc] = ADD (|µ.s| < 2 ∨ µ.gas < 3)
Γ (µ, ι, σ, η) :: S → EXC :: S

We use a dot notation, in order to access components of the different state parameters. We name the components with the variable names introduced for these components in the last section written in sans-serif-style. In addition, we use the usual notation for updating components: t[c → v] denotes that the component c of tuple t is updated with value v. For expressing incremental updates in a simpler way, we additionally use the notation t[c += v] to denote that the (numerical) component of c is incremented by v and similarly t[c -= v] for decrementing a component c of t.

The execution of the arithmetic instruction ADD only performs local changes in the machine state affecting the local stack, the program counter, and the gas budget. For deciding upon the correct instruction to execute, the currently executed code (that is part of the execution environment) is accessed at the position of the current program counter. The cost of an ADD instruction is constantly three units of gas that get subtracted from the gas budget in the machine state. As every other instruction, ADD can fail due to lacking gas or due to underflows on the machine stack. In this case, the exception state is entered and the execution of the current internal transaction is terminated. For better readability, we use here the slightly sloppy ∨ notation for combining the two error cases in one inference rule. A more interesting example of a semantic rule is the one of the CALL instruction that initiates an internal call transaction. In the case of calling, several corner cases need to be treated which results in several inference rules for this case. Here, we only present one rule for illustrating the main functionality. More precisely, we present the case in that the account that should be called exists, the call stack limit of 1024 is not reached yet, and the account initiating the transaction has a sufficiently large balance for sending the specified amount of wei to the called account.

ι.code[µ.pc] = CALL

µ.s = g :: to :: va :: io :: is :: oo ::

os :: s σ(to) ̸ = ⊥ | A| + 1 < 1024 σ(ι.actor).b ≥ va aw = M (M (µ.i, io, is), oo, os) ccall = Cgascap (va, 1, g, µ.gas) c = Cbase (va, 1) + Cmem (µ.i, aw) + ccall µ.gas ≥ c σ ′ = σ to → σ(to)[b += va] ι.actor → σ(ι.actor)[b -= va] d = µ.m [io, io + is -1] µ ′ = (ccall, 0, λx. 0, 0, ϵ) ι ′ = ι[sender → ι.actor][actor → to][value → va][input → d][code → σ(to).code]
Γ (µ, ι, σ, η) :: S → (µ ′ , ι ′ , σ ′ , η) :: (µ, ι, σ, η) :: S For performing a call, the parameters to this call need to be specified on the machine stack. These are the amount of gas g that should be given as budget to the call, the recipient to of the call and the amount va of wei to be transferred with the call. In addition, the caller needs to specify the input data that should be given to the transaction and the place in memory where the return data of the call should be written after successful execution. To this end, the remaining arguments specify the offset and size of the memory fragment that input data should be read from (determined by io and is) and return data should be written to (determined by oo and os).

Calculating the cost in terms of gas for the execution is quite complicated in the case of CALL as it is influenced by several factors including the arguments given to the call and the current machine state. First of all, the gas that should be given to the call (here denoted by c call ) needs to be determined. This value is not necessarily equal to the value g specified on the stack, but also depends on the value va transferred by the call and the currently available gas. In addition, as the memory needs to be accessed for reading the input value and writing the return value, the number of active words in memory might be increased. This effect is captured by the memory extension function M . As accessing additional words in memory costs gas, this cost needs to be taken into account in the overall cost. The costs resulting from an increase in the number of active words is calculated by the function C mem . Finally, there is also a base cost charged for the call that depends on the value va. As the cost also depends on the specific case for calling that is considered, the cost calculation functions receive a flag (here 1) as arguments. These technical details are spelled out in the full version [22].

The call itself then has several effects: First, it transfers the balance from the executing state (actor in the execution environment) to the recipient (to). To this end, the global state is updated. Here we use a special notation for the functional update on the global state using ⟨⟩ instead of []. Second, for initializing the execution of the initiated internal transaction, a new regular execution state 3 executing account, up to for 'topics' (specified on stack) and a fraction of the memory. There are four logging instructions, but as seen before we describe their effects using common rules parameterising the instruction by the amount of log information read from the stack.

!µ,◆ = LOGn µ . s = pos m :: size ::

(s1 + +s2) |s1| = n aw = M (µ.i, pos m , size) c = Cmem (µ.i, aw) + 375 + 8 • size + n • 375 valid (µ.gas, c, |µ.s|) µ 0 = µ[s ! s][pc += 1][gas = c][i ! aw] d = µ.m[pos m , pos m + size 1] ⌘ 0 = ⌘[L ! ⌘.L + +[(◆.actor, s1, d)]] ✏ (µ,

Halting instructions

The execution of a RETURN command requires to read data from the local memory. Consequently the cost for memory consumption is charged. Additionally the read data is recorded in the halting state in order to potentially propagate it to the caller.

!µ,◆ = RETURN µ.s = io :: is :: s aw = M (µ.i, io, is) c = Cmem (µ.i, aw) valid (µ.gas, c, |s|) d = µ.m[io, io + is + 1] g = µ.gas c ✏ (µ, ◆, , ⌘) :: S ! HALT( , g, d, ⌘) :: S !µ,◆ = RETURN µ.s = io :: is :: s aw = M (µ.i, io, is) c = Cmem (µ.i, aw) ¬valid (µ.gas, c, |s|) ✏ (µ, ◆, , ⌘) :: S ! EXC :: S !µ,◆ = RETURN |µ.s| < 2 ✏ (µ, ◆, , ⌘) :: S ! EXC :: S
The execution of a STOP command halts execution without propagating any data to the caller.

3. The execution of the called code ends with an exception. In this case the remaining arguments are removed from the caller's stack and instead 0 is written to the caller's stack. The caller does not get the remaining gas refunded

As the first two cases can be treated analogously, we just need two rules for returning from a call. !µ,◆ = CALL µ.s = g :: to :: va :: io :: is :: oo :: os :: s toa = to mod 2 160 flag = .toa = ? ? 0 : 1 aw = M (M (µ.i, io, is), oo, os) ccall = Cgascap (va, flag, g, µ.gas) c = Cbase (va, flag) + Cmem (µ.i, aw)

+ ccall µ 0 = µ[i ! aw][s ! 1 :: s][pc += 1][gas += gas c][m ! µ.m[[oo, oo + s 1] ! d]]
✏ HALT( 0 , ⌘ 0 , gas, d) :: (µ, ◆, , ⌘) :: S ! (µ 0 , ◆, 0 , ⌘ 0 ) :: S !µ,◆ = CALL µ.s = g :: to :: va :: io :: is :: oo :: os :: s toa = to mod 2 160 flag = (toa) = ? ? 0 : 1 aw = M (M (µ.i, io, is), oo, os) ccall = Cgascap (va, flag, g, µ.gas) c = Cbase (va, flag) + Cmem (µ.i, aw)

+ ccall µ 0 = µ[i ! aw][s ! 0 :: s][pc += 1][gas = c]
✏ EXC :: (µ, ◆, , ⌘) :: S ! (µ 0 , ◆, , ⌘) :: S

The two other instructions for calling (CALLCODE and DELEGATECALL) are similar to CALL.

The CALLCODE instruction only differs in the fact that the control flow is not handed over to the called contract, but only its code is executed in the environment of the calling account. This means in particular that the amount of money transferred is only relevant as a guard for the call, but does not need to be actually transferred. In addition, in case that the account whose code should be executed does not exists, this account is not created, but only the empty code is run. However, still the amount of Ether specified on the stack influences the execution cost. this rule, the call stack (µ, ι, σ, η) :: S becomes (µ , ι , σ , η ) :: (µ, ι, σ, η) :: S where (µ , ι , σ , η ) is a new frame stack which has been added on top of the call stack, where µ is a new record, where µ .gas = c call is the gas transferred to the new frame stack by the old one and µ .pc is set to 0. The code to execute in this new frame is ι .code = σ(to).code where σ(to) is the account receiving the call. Note that, like it was stated in the above sections, the new call stack is (µ , ι , σ , η ) :: (µ, ι, σ, η) :: S where the gas sent to the new frame (µ .gas) has not been subtracted from the frame (µ, ι, σ, η) (µ is the same, thus so is µ.gas). The gas is retracted when the contracts returns. Note also that this is compatible with the Yellow Paper semantics where, to update the gas w.r.t. the execution of the CALL, one has to know how much gas g will be refunded after the execution of the called contract, see [START_REF] Genet | Termination of Ethereum's Smart Contracts[END_REF].

The RETURN instruction

Contract returning is performed by two rules (Figure 2-3). The first rule processes the RE-TURN operation, where the current instruction to execute ι.code[µ.pc] is abbreviated by ω µ,ι . The effect of this rule is to replace the frame by an HALT frame with the information that should be provided to the caller, i.e., the possible updates on the global state σ, the remaining gas g, a result d and transaction effects η. Finally, the HALT frame is popped by the second rule of (Figure 2- 3). We only present the rule for the standard case, i.e., in the frame below the HALT frame, the current instruction is a CALL and the execution stack contains all the information that were necessary to perform the call. Then, we retract the gas units necessary to perform the call (noted c) and refund gas units of gas coming from the HALT frame. The global store σ coming from the HALT frame replaces σ in the current frame.

For the semantics of the CREATE instruction, see [START_REF] Genet | Termination of Ethereum's Smart Contracts[END_REF].

AN EVM MODEL SPECIALIZED FOR GAS ANALYSIS

The gas mechanism ensures that a contract can only run a finite number of "local" instructions, i.e., instructions whose effect is local to the current contract (no call, return, etc.). As mentioned above, when a contract c 1 calls another contract c 2 with, say, g units of gas, the gas associated to c 1 is not charged immediately. Thus, using Yellow Paper semantics, a contract c 1 calling itself is indefinitely looping. The Yellow Paper prevents this by fixing a call stack size limit. If a contract exhausts the stack limit then its execution ends by an exception. However, unlike other virtual machines, EVM has no exception catching mechanism. When an exception is raised in a contract c, the execution of c stops, the information of the contract c is popped from the stack and the control flow goes back to the previous contract in the stack if it exists, otherwise the execution stops.

To sum up, termination of contracts in the formal semantics of the Yellow Paper is enforced by the gas mechanism and the fact that the call stack is finite. In the following, to formally prove termination we prove that, whatever the contracts may be, the call stacks decrease w.r.t. a well founded-ordering. First, we define the call stacks and the frames composing the call stacks based on the formal small-step semantics of [START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF][START_REF] Gavin | Ethereum: A secure decentralised generalised transaction ledger[END_REF] and [START_REF] Grishchenko | A Semantic Framework for the Security Analysis of Ethereum Smart Contracts[END_REF]Grishchenko et al., 2018a).

The maximal call stack size The maximal call stack size is denoted by stack lim. We assume that stack lim is a natural number strictly greater to 0.

Abstraction of the frames For running a contract c 1 , the EVM stores information in the call stack. In the following, we call this information a frame. Following [START_REF] Grishchenko | A Semantic Framework for the Security Analysis of Ethereum Smart Contracts[END_REF], our frames can denote standard program execution frames, HALT frames and EXC frames. In our EVM model specialized for gas analysis, we can abstract frames by three different frame forms: either Ok(g, pc, p, e), Halt(g, e) or Exception, where g is a gas value, pc is a program counter, p is a program code, and e is an environment. Like in [START_REF] Grishchenko | A Semantic Framework for the Security Analysis of Ethereum Smart Contracts[END_REF], this environment is an abstraction of the global state of the system σ. In our model, this environment maps contract names to the associated codes. An Ok(g, pc, p, e) frame represents a standard execution frame (µ, ι, σ, η), where we abstract away η and most parts of µ (including the execution stack and the local memory). In µ, we only keep track of µ.pc the program counter and µ.gas the available gas. Similarly, we forget everything about ι except ι.code the current program to execute. In σ, we only follow the contract names associated to code and forget about all other type of information. A Halt(g, e) frame represents a contract that successfully reaches a RETURN instruction, where g is the gas remaining after the execution of the contract (the refund) and e is the (possibly) modified environment. In particular, e may contain new contract names and their associated code. On the opposite, the result value d and the effect η are not stored in our abstract version of the semantics, because they have no impact on the control flow nor on gas consumption. In particular, if a conditional jump depends on the result d then this will be modeled in our abstract semantics by the fact that the abstract Jump instruction can jump to any valid position in the current contract. Finally an Exception frame represents a contract whose execution has failed because it exhausted the available gas, overflowed the call stack, jumped to an invalid pc or tried to execute an undefined instruction.

The call stacks Call stacks will be represented by lists of frames, where the top of the stack is the left-most element of the list. Example 2. (1) Assume that we are running a unique contract c 1 having 18 gas units left, a program counter pc, a program p and an environment e. The corresponding call stack will thus be [Ok(18,pc,p,e)]. (2) Assume that the instruction at position pc in p is a CALL to contract c 2 with a calling gas value of 10, then the call stack becomes [Ok(10, 0, p2, e2), Ok(18, pc, p, e)], where p2 and e2 are the program and environment associated to c 2 . ( 3) Now assume that the instruction at position 0 in p2 consumes 2 gas units, the call stack is now [Ok(8,1,p2,e3),Ok(18,pc,p,e)] where e2 may have been transformed into e3. (4) Then, assume that contract c 2 reaches program point pc2 with 4 gas units left and the environment e4: [Ok (4,pc2,p2,e4),Ok(18,pc,p,e)]. (5) At pc2 in p2 there is a RETURN instruction so that c 2 halts on a valid state. The call stack becomes: [Halt (4,e4),Ok(18,pc,p,e)]. (6) Then, the frame of contract c 2 is popped and control is returned back to c 1 that called c 2 . When returning back to c 1 , we have to consume all the gas used for the call: the cost of the call instruction itself with the cost of calling c 2 . Assume that the call instruction costs 3 gas. Thus, we need to consume 3 gas plus the gas that was planned at step ( 2) for calling contract c 2 : 10. Besides, we refund the 4 gas returned by Halt and place the environment e4 into c 1 frame. Thus, the call stack becomes [Ok(9,pc+1,p,e4)]. (7) Now we assume that, the execution of contract c 1 ends with an exceptional state. The resulting stack is thus [Exception].

TERMINATION PROOF FOR THE YELLOW PAPER SEMANTICS IN ISABELLE/HOL

The Termination measure

A usual technique to prove termination of a recursive function f mapping values of type A to values of type B is to define a well-founded strict ordering on elements of type A. This ordering has to be defined such that for all x ∈ A if f (x) evaluates to f (y), noted f (x) f (y), then we have x y. If such a well-founded ordering exists then it proves termination of f . Indeed, for any infinite derivation f (t 1 ) f (t 2 ) . . .,

we have an infinite chain t 1 t 2 . . ., which contradicts the fact that is well-founded.

To prove termination of the EVM semantics, we need to show that when executing one EVM bytecode on a stack s 1 we obtain a stack s 2 which is strictly smaller to s 1 w.r.t. a well-founded ordering . Finding such an order is not straightforward as we show on the following example. For instance, to prove termination on the execution of Example 2, we need a well-founded ordering such that

(1) [Ok(18, pc, p, e)] (2)
[Ok(10, 0, p2, e2), Ok(18, pc, p, e)]

[Ok(8, 1, p2, e3), Ok(18, pc, p, e)] (4) [Ok (4, pc2, p2, e4), Ok(18, pc, p, e)] (5)

[Halt(4, e4), Ok(18, pc, p, e)] (6)

[Ok(9, pc + 1, p, e4)] (7) [Exception] Since we may have loops in a frame, we may have two consecutive frames with the same pc or ascending pc. Thus, the program counter is not relevant for the ordering. In the same way, since environments e, e2, e3, e4 and programs p, p2 may not evolve between two frames, they are hardly usable for a strict ordering. Hence, the ordering can only depend on the gas value of the frames. If we abstract away anything but gas from the previous example, we obtain: Note that, using a simple ordering for does not satisfy the above ordering chain. For instance, the following orderings fail:

• comparing the size of the list:

[Ok( 18)] [Ok(10), Ok(18)]

• comparing the gas value of the topmost frame: [Halt(4), Ok( 18)] [Ok(9)]

• comparing the gas value of frames from bottom to top: [Ok( 18)] [Ok(10), Ok(18)]

• comparing the sum of the gas values: [Ok( 18)] [Ok(10), Ok(18)]

• or, lexicographic combinations of them starting from the leftmost part of the list: [Halt(4), Ok( 18)] [Ok(9)]

• or, lexicographic combinations of them starting from the rightmost part of the list: [Ok( 18)] [Ok(10), Ok( 18)]

The order we define to prove termination of EVM semantics is based on measure functions, i.e., functions mapping frames to natural numbers. Thus, stacks can be evaluated into lists of natural numbers and lists of natural numbers are compared using a lexicographic combination of the order > on natural numbers. Before defining our measure functions, we complete the call stacks by dummy frames up to the frame stack's maximal size stack lim. These dummy frames (noted D) have a gas value depending on the type of the topmost frame and on its gas value if there is one (for Ok and Halt) and 0 otherwise (for Exception). If the topmost frame is Ok(i) then the dummy frames will be D(i+3), if the topmost frame is Halt(i) then the dummy frames will be D(i + 2). If the topmost frame is Exception then the dummy frames will be D(0). Assuming that the maximal stack size is 4, the frame stacks of our previous example will be completed up to size 4 in the following way: Using this completion of call stacks, the order becomes straightforward: we compare frame's measures lexicographically, starting from the rightmost part of the list, i.e., from the bottom of the stack. We use the following measure function for frames: measure(Ok(i)

[ D(21), D(21), D (21), Ok(18)
) = i + 3, measure(Halt(i)) = i + 2, measure(D(i)) = i and measure(Exception) = 1.
Thus, on the above example, we have [D(13), D(13), Halt(4), Ok(18)] because measure(Ok( 4)) = 7 and measure(Halt( 4)) = 6.

The values for the measure of frames, measure(Ok(i)) = i + 3, measure(Halt(i)) = i + 2, measure(D(i)) = i and measure(Exception) = 1, have been chosen so that an Ok frame halting (correctly) with a gas i and moving to a Halt with the same gas value i can be ordered. With this measure, we have [Ok(i), f 1 , ..., f n ]

[Halt(i), f 1 , ..., f n ], for all i ≥ 0 and all frames f 1 , . . . , f n . This is crucial since this sequence of frame stacks is possible with the EVM semantics.

Definition 1 (Stack measure). Let Es be the maximal height of the EVM call stack. Let s be an EVM call stack represented by a list of frames of the form Ok(i), Halt(j), or Exception where i, j are strictly positive natural numbers. Let s(k) be the k-th element of the stack s for 0 ≤ k < |s|, thus s(0) is the topmost frame. For 0 ≤ k < |s|, let

m k =    i + 3 if s(k) = Ok(i) i + 2 if s(k) = Halt(i) 1 if s(k) = Exception d =    i + 3 if s(0) = Ok(i) i + 2 if s(0) = Halt(i) 0 if s(0) = Exception
The stack measure of s is a list of natural numbers, of length Es, defined by:

measure(s) = [d, . . . , d] Es-|s| @[m 0 , . . . , m |s|-1 ]
where @ denotes list concatenation.

With this measure, we can prove the following termination theorem.

Theorem 1. The execution of any contract on the EVM terminates.

The proof amounts to showing that each EVM execution step results in a decrease of the measure on call stacks defined in Definition 1. To prove this formally, we need to define an abstract version of the EVM semantics specialized for gas analysis. This will be done in the next section where we propose an Isabelle/HOL formalization of this specialized semantics.

Implementation in

Isabelle/HOL The abstraction of frames defined in Section 5.1 only keeps track of the gas, the current program to execute, the program counter, and the environment. With this abstraction, many EVM instructions have a similar behavior and can be abstracted by a general Local instruction whose only parameter is its gas cost. The Local(g) instruction represents any instruction whose effect is local to the current frame, does not affect the control flow, and whose cost in gas is the natural number g. This instruction represents all instructions of the families Execution stack operations, Memory access and Environment operations of Section 3, i.e., instructions such as ADD, SSTORE, MSTORE, LT, AND, PUSHi, POP, DUPi, SWAPi, . . . The Nil instruction stands for undefined instruction (an undefined opcode) that may appear in a program or the INVALID instruction. The Jump(g) instruction represents the JUMP and JUMPI instructions where g is the cost of executing the jump. There is no destination associated with the Jump instruction because the abstract semantics will arbitrarily chose the destination when executing the Jump. This is an over-approximation of all the possible JUMP and JUMPI behaviors with any position in the contract tagged by a JUMPDEST instruction. Thus, we cover all the instructions of the Control flow operations family of Section 3. The family of System operations is represented by two different abstract instructions. The (Call gcall ccall cname) instruction represent EVM's CREATE, CALL, CALL-CODE, DELEGATECALL, and CALLSTATIC where gcall is the cost in gas of executing the call instruction itself, ccall is the gas transferred to the called contract, and cname is the contract name to be called. Having CREATE and CALL abstracted by the same Call instruction is coherent with EVM semantics, where the difference between the two is small. In the case of a CALL, the contract name exists in the environment and is associated to a program. In the case of a CRE-ATE the contract name does not exist and the association is added in the environment of the new frame, see [START_REF] Genet | Termination of Ethereum's Smart Contracts[END_REF] for details. The last abstract instruction for the family System operations is the Stop instruction which represents STOP, RETURN, REVERT and SELF-DESTRUCT EVM's instructions. Finally, a program p is a list of such instructions and a program counter pc of p is a position between 0 and length(p) -1 in this list.

Note that, in EVM, all instructions (except STOP, REVERT and RETURN) have a gas cost which is strictly greater than zero. However, the above Isabelle/HOL datatype only imposes that gas costs are of type nat, i.e., that they are greater or equal to zero. Thus, we complement this datatype with a valid_prog(p) predicate stating that, in a program p, every instruction with a cost g is such that g > 0.

The function defining the EVM semantics is smallstep and its Isabelle/HOL type is call_stack ⇒ call_stack. Starting from a call stack, whose top frame is Ok(g, pc, p, e) this function executes the instruction at position pc in p with environment e and returns the resulting call stack. Recall that there are three kinds of frames: Ok, Halt or Exception. The Isabelle/HOL type call_stack is simply a list of frames. Thus, this type includes invalid call stacks, i.e., stacks that contain frames whose program is invalid, and stacks that cannot be produced by a correct execution of the EVM semantics (such as [Exception, Exception]). Since functions in Isabelle/HOL have to be total, we need to define the smallstep function for all stacks including the invalid ones. To ensure totality of smallstep, while preserving its soundness w.r.t. EVM, we map any invalid call stacks to the result stack [Invalid f rame], where Invalid f rame is an additional kind of frame. Here is the corresponding Isabelle/HOL datatype. We define a predicate valid_stack checking that a call stack is valid: it contains only valid programs, valid environments and valid sequence of frames.

A valid sequence does not contain Invalid f rame, and Exception or Halt cannot be below other frames. We now present the smallstep function of type smallstep::"call_stack ⇒ call_stack" and whose role is to execute the abstract instructions on a call stack. The complete Isabelle/HOL code can be found here [START_REF] Efsyellow | Ethereum Formal Semantics for Gas Consumption Analysis -Yellow paper semantics[END_REF]. Note that this semantics is executable and some examples can be found and run at the end of the theory file. We here only give some excerpts of the smallstep function.

Semantics for Stop, Nil and Local instructions

The first one illustrates the execution of Stop, Nil and Local instructions. Recall that the Local instruction covers the Execution stack, Memory access and Environment families of operations of Section 3. This code has to be compared with the semantic rules of Section 3.1.

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

) of Stop ⇒ ((Halt (g,e))#l) | Nil ⇒ (Exception#l)| Local(n) ⇒(if (n>0) then ( if (n≤g) then ((Ok ((g-n),pc+1,p,e))#l) else (Exception#l)) else [Invalid_frame] )| [...]
In the case of a Local(n) instruction, if n = 0 this results into a [Invalid f rame]. Otherwise if n is lesser or equal to the available gas g then instruction is executed, gas is updated and pc is incremented. Otherwise, an exception is stacked on the call stack.

Semantics for the Jump instuction

Now, we present the semantics of the Jump instruction which covers the operations of the Control flow family of Section 3.

" Like above, for Local(n) if n = 0 this results into a [Invalid f rame]. Otherwise we compute an arbitrary value for the destination of the jump, named pj, using the function any_jump. This function is left unspecified, we only known its type any_jump::'a ⇒ nat. Thus, pj= (any_jump 0) associates any natural number to pj. This models the fact that the jump can be conditional and JUMPDEST labels can be attached to any part of the current contract. Then, if there is enough gas to execute the jump (n≤g) and the jump destination is in the range of the current contract (pj<(length p)) then the program counter is updated with pj and the top frame becomes (Ok(g-n,pj,p,e). Otherwise, an exception is stacked on the call stack.

Semantics for the CALL return

The semantics of the contract call is straightforward, see [START_REF] Efsyellow | Ethereum Formal Semantics for Gas Consumption Analysis -Yellow paper semantics[END_REF]. Thus, the third excerpt, illustrates the return of a contract call. This has to be compared with the second rule of Section 3.3.

,p,ef))#l) |_ ⇒ [Invalid_frame] )"| [...] (pc+1)
When a contract halts correctly (frame (Halt (gend,ef)) on top of the stack, with gas refund gend and environment ef) then if the frame below is a frame (Ok (g,pc,p,e)) such that the instruction at position pc in p is a call, and such that all calling conditions were satisfied before the call, then we pop the Halt frame and continue in the Ok frame, with gas (g+gend-gcall-ccall), at position pc+1 and with (possibly) modified environment ef. Any other behavior results into an [Invalid f rame].

Soundness and termination proof

Since we completed the EVM semantics with a new type of frames (Invalid f rame) to have a total function smallstep, we first need to verify that this modification does not break the EVM semantics encoded in the smallstep function. This can be checked using the following Isabelle/HOL theorem stating that validity of stacks is preserved by smallstep. Again, we can lift the previous theorem to prove that adding Invalid f rame does not break the semantics, i.e. executing a valid stack always result into a valid stack, where stack lim is an arbitrary constant (greater than 0) which defines the maximal stack size.

TERMINATION PROOF FOR THE EVM REFERENCE IMPLEMENTATIONS SEMANTICS

As explained in the introduction, implementations generally use a slightly different semantics Note that the ordering used for the previous semantics does not satisfy those constraints. If we complete our stacks up to size 4, we obtain: However, with this second semantics, finding a satisfying termination order is easier. 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. The proof of termination is composed of 14 intermediate lemmas and is around 130 lines.

CONCLUSION

Termination is an important property of any smart contract. To this end, the Ethereum platform (EVM) has introduced a mechanism based on gas which gets consumed as the execution progresses. This paper presents an abstract model of EVM execution that focuses on gas consumption. On this model, we prove that for any EVM execution, gas is used in such a way that it is impossible to construct an infinite loop that does not consume any gas. This property is not immediate to establish for the specification in the EVM Yellow Paper, because of the decidedly nontrivial semantics of contract calls and the fact that cashing-in of the cost of the call is delayed until after the return (whether regular or exceptional).

The proof relies on a non-trivial measure on contract call stacks and has the salient feature that it is independent of the specific costing of instructions, as long as they are greater than 0. This latter point is important as the costs of certain instructions of the EVM has evolved over its rather short life.

The mechanized proof is based on an abstract model of the EVM and fills a gap in current formal developments on verification of contracts with proof assistants [START_REF] Hirai | Defining the Ethereum Virtual Machine for Interactive Theorem Provers[END_REF][START_REF] References Amani | Towards verifying ethereum smart contract bytecode in isabelle/hol[END_REF]. There are a number of steps for further work related to this mechanization. First, it would be worthwhile formalizing the relation to the complete semantic formalization by Grishchenko (Grishchenko et al., 2018a) or even the Isabelle/HOL formalization [START_REF] Hirai | Defining the Ethereum Virtual Machine for Interactive Theorem Provers[END_REF][START_REF] References Amani | Towards verifying ethereum smart contract bytecode in isabelle/hol[END_REF]. This can likely be done by setting up a simulation relation between the concrete and the abstract semantics. Second, it would be useful to show that the gas consumption in the two semantics are similar or, at least, that the consumption of one is bounded by a polynomial function of the consumption of the other. Another possible extension stems from the fact that this proof is only for one transaction. It does not take into account several transaction rounds.

  ◆, , ⌘) :: S ! (µ 0 , ◆, , ⌘ 0 ) :: S !µ,◆ = LOGn µ.s = pos m :: size :: (s1 + +s2) |s1| = n aw = M (µ.i, pos m , size) c = Cmem (µ.i, aw) + 375 + 8 • size + n • 375 ¬valid (µ.gas, c, |µ.s|) ✏ (µ, ◆, , ⌘) :: S ! EXC :: S !µ,◆ = LOGn |µ.s| < n + 2 ✏ (µ, ◆, , ⌘) :: S ! EXC :: S

Figure 2 :

 2 Figure 2: The EtherTrust definitions for ADD, CALL and RETURN.

  [D(21), D(21), D(21), Ok(18)] [D(13), D(13), Ok(10), Ok(18)] because the 4 th element of the two stacks are equal (Ok(18)) but the 3 rd element of the first stack has a measure of 21 where the 3 rd element of the second stack has a measure of 13. Similarly, we have [D(21), D(21), Ok(4), Ok(18)]

  In other words, when running smallstep on a valid stack, then Invalid f rame will never show up. The (complete) execution of a contract starts from a call stack, applies the smallstep function until a Halt, Exception or Invalid_frame is reached. The result of a complete execution is a single frame. It is defined in Isabelle/HOL in the execute function as follows: function (sequential) execute :: "call_stack ⇒ frame" where "execute ([]) = Invalid_frame"| "execute ([Halt (g,e)]) = (Halt (g,e))"| "execute ([Exception]) = (Exception)"| "execute ([Invalid_frame]) = Invalid_frame"| "execute l = (if (length l > stack_lim) then Invalid_frame else execute (smallstep l))"

  l ∧ (length l ≤ stack_lim)) -→ (valid_stack [(execute l)])"Now, we can state and prove in Isabelle/HOL the termination theorem (Theorem 1) which corresponds to the termination proof of the execute function. The proof of this property relies on the measure technique described in section 5.1 extended with measure(Invalid_frame) = 1 and encoded into Isabelle/HOL. Note that this final termination theorem is valid for any stack size (stack lim), where the termination measure is the one defined in Section 5.1 and formalized by the list order Isabelle/HOL function. termination execute apply (relation "measures (list_order stack_lim)") The Isabelle/HOL development is around 1200 lines. Excluding definitions, the proof of soundness is composed of 18 intermediate lemmas and of 300 lines of Isabelle/HOL. The proof of termination is composed of 57 intermediate lemmas and of 400 lines of Isabelle/HOL.

  , in the state σ, there are two accounts a i and a j

		Ethereum
	State σ			State σ 0
	Account a i			Account a i
	Balance	130		Balance	130
	Storage	[i : 4]		Storage	[i : 5]
	Code	i++		Code	i++
	Account a j			Account a j
	Balance	20		Balance	20-g+g 0
	Storage Code	/ /	Transaction T a j g a i	Storage Code	/ /
				Account m ( miner of T)
				Balance += g-g'

In the comments of the lem/evm.lem specification file, it becomes evident that the termination proof uses an artificial step counter and not the gas mechanism. This choice was made to simplify the proof as stated line 1859 of lem/evm.lem (FEL

, 2018).2 There was a cost increase for 8 EVM instructions on 2016/10/18(Hudson, 2016a) and a cost increase for one EVM instruction on 2016/11/18[START_REF] Hudson | Upcoming Ethereum Hard Fork[END_REF]

In addition, it is possible to transfer money to a contract, but this part is not important for our termination proof and will not be modeled here.

ACKNOWLEDGEMENTS

Many thanks to Emmanuelle Anceaume, Vincent Laporte, Romaric Ludinard, and Clara Schneidewind for valuable discusions about Ethereum and SmartContracts.

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) in https://github.com/ethereum/py-evm/blob/ master/eth/vm/logic/call.py).

Executing Example 2 with this other semantics yields the following sequence of call stacks. Example 3. (1) Assume that we are running a unique contract c 1 having 18 gas units left, a program counter pc, a program p and an environment e. The corresponding call stack will thus be [Ok(18,pc,p,e)]. (2) Assume that the instruction at position pc in p is a CALL to contract c 2 with a calling gas value of 10, and the cost of a CALL is 3. Then the call stack becomes [Ok(10, 0, p2, e2), Ok (5, pc, p, e)],

where p2 and e2 are the program and environment associated to c 2 . ( 3) Now assume that the instruction at position 0 in p2 consumes 2 gas units, the call stack is now [Ok(8, 1, p2, e3), Ok (5, pc, p, e)] where e2 may have been transformed into e3. (4) Then, assume that contract c 2 reaches program point pc2 with 4 gas units left and the environment e4:

[Ok (4, pc2, p2, e4), Ok (5, pc, p, e)].

(5) At pc2 in p2 there is a RETURN instruction so that c 2 halts on a valid state. The call stack becomes:

[Halt(4, e4), Ok (5, pc, p, e)].

(6) Then, the frame of contract c 2 is popped and control is returned back to c 1 that called c 2 , the 4 gas are refunded to c 1 and we place the environment e4 into c 1 frame. Thus, the call stack becomes [Ok(9, pc + 1, p, e4)]. (7) Now we assume that, the execution of contract c 1 ends with an exceptional state. The resulting stack is thus [Exception].

To prove termination we now need a wellfounded strict ordering that satisfy the following ordering constraints: