11institutetext:  Department of Computer Science, Reykjavik University,
Iceland
11email<EMAIL_ADDRESS>22institutetext: Gran Sasso Science Institute,
L’Aquila, Italy 33institutetext: Sapienza, Università di Roma, Rome, Italy
33email<EMAIL_ADDRESS>44institutetext: Polytechnique Montreal,
Montreal, Quebec, Canada
44email<EMAIL_ADDRESS>
# Preventing Out-of-Gas Exceptions by Typing††thanks: The work of Luca Aceto,
Mohammad Hamdaqa and Stian Lybech was supported by the Icelandic Research Fund
Grant No. 218202-05(1-3).

Luca Aceto 1122 0000-0002-2197-3018 Daniele Gorla 33 0000-0001-8859-9844 Stian
Lybech 11 0000-0001-8219-2285 Mohammad Hamdaqa 1144 0000-0003-4927-2755

###### Abstract

We continue the development of TinySol, a minimal object-oriented language
based on Solidity, the standard smart-contract language used for the Ethereum
platform. We first extend TinySol with exceptions and a gas mechanism, and
equip it with a small-step operational semantics. Introducing the gas
mechanism is fundamental for modelling real-life smart contracts in TinySol,
since this is the way in which termination of Ethereum smart contracts is
usually ensured. We then devise a type system for smart contracts guaranteeing
that such programs never run out of gas at runtime. This is a desirable
property for smart contracts, since a transaction that runs out of gas is
aborted, but the price paid to run the code is not returned to the invoker.

###### Keywords:

Smart-contract language Type system Static analysis Semantics of programming
languages.

##  1 Introduction

Smart contracts running on a blockchain can be viewed as a collective system:
they are typically deployed in large numbers and interact in an adversarial
environment, each pursuing its own individual goal, without specific
centralised control. Many languages have been deployed to program them, with
the Ethereum Virtual Machine language [15] (EVM) as one of the most successful
proposals. It is a Turing-complete language and, thus, it is in principle
undecidable whether a given EVM smart contract will halt or not. This is
problematic in a blockchain setting, since smart contracts may be called in
transactions, which are executed by miners as part of their attempts to find
the next block, as well as when validating existing blocks. If a transaction
were to run forever, it would therefore in effect block the miner from making
progress, which for instance could be used to cause a denial of service for
the entire network.

To limit such undesirable scenarios, EVM introduced the concept of _gas_ ,
which effectively ensures termination of all transactions. This mechanism
works as follows (see [11] for details): The gas represents a unit of
computation, and thus also a unit of work for the miner. Each EVM instruction
has an associated _gas cost_ 111Usually 3–5 units, although some complex
operations such as CREATE have a much higher cost. An overview of the EVM
instructions and their gas costs can be found at https://evm.codes., and the
total gas cost of a transaction is thus proportional to the amount of
computational work required by the miner to execute the transaction. Whenever
a user schedules a transaction, two additional parameters have to be
specified: the _gas limit_ and the _gas price_. The gas limit is an upper
bound on the gas cost of the transaction. If this limit is exceeded, an out-
of-gas exception is thrown, the transaction aborts and its effects are rolled
back. The gas price is the amount of currency that the user is willing to pay
to the miner for each unit of gas consumed in the transaction. This ensures
that users will not schedule long-running transactions and just pick an
arbitrarily high gas limit, since the gas price will still be paid for each
unit of gas consumed in a transaction, even if the transaction aborts with an
out-of-gas exception.

The concept of gas is, of course, also inherent in Solidity, since this
language compiles to EVM. However, the original presentation of TinySol [4], a
minimal object-oriented language based on Solidity, does not include such a
mechanism. This limits its ability to realistically model, e.g., aborting
transactions and rollback. In particular, the latter phenomenon is modelled in
the operational semantics of that language through a rule with an undecidable
premise. In our previous work on TinySol [1], we simply decided to omit this
rule, thus in effect allowing non-terminating transactions and also leaving
transactions stuck, if an exception-raising command were ever to be reached.

In the present paper, we therefore add a gas mechanism to our version of
TinySol and present a first attempt at a type system ensuring that
transactions never run of out gas at runtime. The syntax of the language is
provided in Section 2 and is essentially the one we used in [1], where we gave
a big-step operational semantics for TinySol. However, handling exceptions in
a big-step semantics is rather unnatural, as exceptions can be raised at any
intermediate point of a computation. For this reason, a first contribution of
this work is to provide a small-step operational semantics for TinySol; this
is done in Section 3.

We then move to the core contribution of this paper: a type system for
guaranteeing that a transaction never runs out-of-gas, that is, an out-of-gas
exception is never raised at runtime. The type system is defined in Section
4.1 and its properties are stated in Section 4.2. Never running out-of-gas is
essentially a problem of checking termination of a program, a well-known
undecidable problem in its general formulation. To make it decidable, and
efficiently checkable, we have to reduce the set of programs that the type
system accepts; this is discussed thoroughly in Section 4.3. We conclude the
paper in Section 5, where we also hint at possible directions for future
enhancements of this work. Due to space limitations, proofs and supplementary
material are relegated to the appendices.

#### Related work

The literature on methods for proving that programs terminate is vast and we
cannot do justice to related work fully in this paper. We therefore limit
ourselves to mentioning the survey of program termination proof techniques for
sequential programs given in [7] and the textbook [14], which offers an
introduction to Hoare-style methods to prove total correctness and to give
bounds on the execution time of imperative programs [13].

In the setting of smart-contract languages, as observed in [9], proofs of
termination are non-trivial even in the presence of a gas mechanism. That
article presents the first mechanised proof of termination of contracts
written in EVM bytecode using minimal assumptions on the gas cost of
operations. Efficient static-analysis techniques for detecting gas-focused
vulnerabilities in smart contracts and their implementation in the tool MadMax
have been presented in [10].

Among the plethora of studies on type systems for ensuring program termination
in several settings, we mention the work by Boudol on typing termination in a
higher-order concurrent imperative language; see [5] and the references
therein. Our contribution is inspired by the work by Deng and Sangiorgi in [8]
for the $\pi$-calculus. In particular, we build on their type system 1, which
imposes limitations similar to those for our type system, e.g. it prohibits
(the $\pi$-calculus equivalent of) recursive function calls.

##  2 TinySol with Gas and Exceptions

$\begin{array}[]{r @{~} c @{~} l @{\qquad}
l}DF\in\text{Dec}_{F}~{}&::=\hfil~{}&\epsilon~{}~{}\big{|}~{}~{}~{}\texttt{field
$p$ := $v$;}DF\cr
DM\in\text{Dec}_{M}~{}&::=\hfil~{}&\epsilon~{}~{}\big{|}~{}~{}~{}\texttt{$f(\widetilde{x})$
\\{ $S$ \\} }DM\cr
DC\in\text{Dec}_{C}~{}&::=\hfil~{}&\epsilon~{}~{}\big{|}~{}~{}~{}\texttt{contract
$X$ \\{ }\cr~{}&\hfil~{}&\qquad\ \ \ \texttt{field balance := $n$;
$DF$}\cr~{}&\hfil~{}&\qquad\ \ \ \texttt{send() \\{ skip \\}
$DM$}\cr~{}&\hfil~{}&\qquad\ \texttt{\\} $DC$}\cr
m\in\text{MVar}~{}&::=\hfil~{}&\texttt{this}~{}~{}\big{|}~{}~{}~{}\texttt{sender}~{}~{}\big{|}~{}~{}~{}\texttt{value}\cr
L\in\text{LVal}~{}&::=\hfil~{}&x~{}~{}\big{|}~{}~{}~{}\texttt{this.$p$}\cr
e\in\text{Exp}~{}&::=\hfil~{}&v~{}~{}\big{|}~{}~{}~{}x~{}~{}\big{|}~{}~{}~{}m\quad|\quad\texttt{$e$.balance}~{}~{}\big{|}~{}~{}~{}\texttt{
$e$.$p$ }~{}~{}\big{|}~{}~{}~{}\operatorname{op}(\widetilde{e})\cr
S\in\text{Stm}~{}&::=\hfil~{}&\texttt{skip}~{}~{}\big{|}~{}~{}~{}\texttt{throw}~{}~{}\big{|}~{}~{}~{}\texttt{var
$x$ := $e$ in $S$}~{}~{}\big{|}~{}~{}~{}\texttt{$L$ :=
$e$}~{}~{}\big{|}~{}~{}~{}\texttt{$S_{1}$;$S_{2}$}\cr~{}&~{}~{}\big{|}{}{}{}\hfil~{}&\texttt{if
$e$ then $S_{\text{T}}$ else $S_{\text{F}}$ }~{}~{}\big{|}~{}~{}~{}\texttt{for
$e$ do
$S$}~{}~{}\big{|}~{}~{}~{}\texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$}\cr
v\in\text{Val}~{}&::=\hfil~{}&\mathbb{Z}\cup\mathbb{B}\cup\text{ANames}\cr~{}\cr\end{array}$

where $x,y\in\text{VNames}$ (variable names), $p,q\in\text{FNames}$ (field
names),
$X,Y\in\text{ANames}$ (address names), $f,g\in\text{MNames}$ (method names).

Figure 1: The syntax of TinySol.

The syntax of TinySol is given in Figure 1, where we use the notation
$\mathop{\widetilde{\cdot}}$ to denote (possibly empty) sequences of items.
The set of _values_ , ranged over by $v$, is formed by the sets of integers
$\mathbb{Z}$, ranged over by $n$, booleans
$\mathbb{B}=\left\\{\,\text{T},\text{F}\,\right\\}$, ranged over by $b$, and
address names ANames, ranged over by $X,Y$.

We introduce explicit declarations for fields $DF$, methods $DM$, and
contracts $DC$. The latter also encompasses declarations of accounts: an
_account_ is a contract that contains only the declarations of a special field
balance and of a single special method send(), which does nothing and is used
only for transferring funds to the account. By contrast, a contract usually
contains other declarations of fields and methods. For the sake of simplicity,
we make no syntactic distinction between an account and a contract but, to
distinguish them, we can assume that the set ANames is split into contract
addresses and account addresses.

We have four ‘magic’ keywords in our syntax. The keyword balance (type int)
stands for a special field recording the current balance of the contract (or
account). It can be read from, but not directly assigned to, except through
method calls. This ensures that the total amount of currency ‘on-chain’
remains constant during execution. The keyword value (type int) denotes a
special variable that is bound to the currency amount transferred with a
method call. The special variable sender (type address) is always bound to the
address of the caller of a method. Finally, this (type address) is a special
variable that is always bound to the address of the contract containing the
currently executing method. The last three of these are local variables, and
we collectively refer to them as ‘magic variables’ $m\in\text{MVar}$.

The declaration of variables and fields ($DV$ and $DF$) are very alike: the
main difference is that variable bindings will be created at runtime (and with
scoped visibility), hence we can let the initial assignment be an expression
$e$; by contrast, the initial assignment to fields must be a value $v$.

The core part of the language is the declaration of expressions $e$ and
statements $S$, which are almost the same as in [4]. The main differences are:
(1) we introduce fields $p$ in expressions, instead of keys; (2) we explicitly
distinguish between (global) fields and (local) variables, where the latter
are declared with a scope limited to a statement $S$; (3) we introduce
explicit _lvalues_ $L$, to restrict what can appear on the left-hand side of
an assignment (which, in particular, ensures that the special field balance
can never be assigned to directly); and (4) we have a for loop, instead of the
more general (and less controllable) while loop. This last difference is only
introduced for the sake of the type system we are going to present and,
indeed, in [1] the while loop is present.

We now use TinySol to describe transactions and blockchains. A _transaction_
is simply a call, where the caller is an account $A$, rather than a contract,
together with some gas quantity, used to specify how much computational cost
the transaction can consume. We denote this by writing
$A$->$X$.$f(\widetilde{v})$:$(n,g)$, which expresses that the account $A$
calls the method $f$ on the contract (residing at address) $X$, with actual
parameters $\widetilde{v}$, transferring the amount of currency $n$ with the
call, and with an upper bound on the computational cost of the call given by
the gas amount $g$ (a positive integer). Hence, blockchains can be defined as
follows:

######  Definition 1 (Syntax of blockchains)

A _blockchain_ $B\in\mathcal{B}$ is a list of initial contract declarations
$DC$, followed by a sequence of transactions $T\in\text{Tr}$:

$\begin{array}[]{r @{~} c @{~} l @{\qquad} l}B\in\mathcal{B}::=\texttt{$DC$
$T$}\qquad\qquad
T\in\text{Tr}::=\epsilon~{}~{}\big{|}~{}~{}~{}A\texttt{->}X\texttt{.}f\texttt{(}\widetilde{v}\texttt{):}(n,g),\,T~{}\end{array}$

where $g>0$ is the _gas limit_ of the transaction. Notationally, a blockchain
with an empty $DC$ will be simply written as the sequence of transactions.

##  3 A Small-step Semantics with Exceptions and Gas

The semantics given in [1] describes the execution of a complex statement as
one single computational step. This is sensible from the point of view of a
user, since a transaction is a method call and transactions are atomic.
However, we can also create a small-step semantics for statements in TinySol
to describe the individual computational steps involved; this form of
semantics is more suitable than a big-step one when exception handling is
introduced.

To define the semantics, we need some environments to record the bindings of
variables (including the three magic variable names this, sender and value),
fields, methods, and contracts. We define them as sets of partial functions:

######  Definition 2 (Binding model)

The binding model consists of the following:

$\displaystyle\text{env}_{V}\in\text{Env}_{V}$
$\displaystyle:\text{VNames}\cup\text{MVar}\rightharpoonup\text{Val}$
$\displaystyle\text{env}_{S}\in\text{Env}_{S}$
$\displaystyle:\text{ANames}\rightharpoonup\text{Env}_{F}$
$\displaystyle\text{env}_{F}\in\text{Env}_{F}$
$\displaystyle:\text{FNames}\cup\left\\{\,\texttt{balance}\,\right\\}\rightharpoonup\text{Val}$
$\displaystyle\text{env}_{T}\in\text{Env}_{T}$
$\displaystyle:\text{ANames}\rightharpoonup\text{Env}_{M}$
$\displaystyle\text{env}_{M}\in\text{Env}_{M}$
$\displaystyle:\text{MNames}\rightharpoonup\text{VNames}^{*}\times\text{Stm}$

We write each environment $\text{env}_{X}$, for
$X\in\left\\{\,V,F,M,S,T\,\right\\}$, as an unordered sequence of pairs
$(d,c)$ where $d\in\operatorname{dom}\left(\text{env}_{X}\right)$ and
$c\in\operatorname{codom}\left(\text{env}_{X}\right)$. The notation
$\text{env}_{X}\kern-2.0pt\left[d\mapsto c\right]$ denotes the update of
$\text{env}_{X}$ mapping $d$ to $c$. We write $\text{env}_{X}^{\emptyset}$ for
the empty $X$-environment.

To simplify the notation, when two or more environments appear together, we
shall use the convention of writing the subscripts together; e.g., we write
$\text{env}_{MF}$ instead of $\text{env}_{M},\text{env}_{F}$, and
$\text{env}_{SV}^{\prime}$ instead of
$\text{env}_{S}^{\prime},\text{env}_{V}^{\prime}$.

Statements are executed in the context of the following environments: a
_method table_ $\text{env}_{T}$, which maps addresses to method environments,
and a _state_ $\text{env}_{SV}$, which maps addresses to lists of fields and
their values, and local variables to their values. Thus, for each contract, we
have the list of methods it declares and its current state. Of course, the
method table is constant, once all declarations are performed, whereas the
state will change during the evaluation of a program.

The semantics relies on the concept of a _stack_ $Q$ that holds the code that
has not yet been executed and the variable environments needed to switch
execution frames during a call.

######  Definition 3 (Syntax of stacks)

The syntax of a _stack_ $Q$ is given as follows:

$\begin{array}[]{r @{~} c @{~} l @{\qquad}
l}Q~{}&::=\hfil~{}&\bot~{}~{}\big{|}~{}~{}~{}S::Q~{}~{}\big{|}~{}~{}~{}\text{env}_{V}::Q~{}~{}\big{|}~{}~{}~{}\text{del}(x)::Q~{}~{}\big{|}~{}~{}~{}\text{exc}(l)::Q\cr
l~{}&::=\hfil~{}&\texttt{rte}~{}~{}\big{|}~{}~{}~{}\texttt{neg}~{}~{}\big{|}~{}~{}~{}\texttt{oog}~{}~{}\big{|}~{}~{}~{}\texttt{pge}\end{array}$

In the above definition, $\bot$ denotes the bottom of the stack, $S$ is a
statement, $\text{env}_{V}$ is a variable environment, $\text{del}(x)$ marks
the end of the scope of a locally declared variable $x$, and $\text{exc}(l)$
denotes raising of an exception of kind $l$, whose possibilities are as
follows: rte denotes an exception raised at runtime because of ill-formed code
(e.g., when attempting to access a field not present in a contract or when
invoking a method not provided by a contract); neg denotes an exception raised
when a contract’s balance becomes negative; oog denotes an exception raised
when a transaction consumes all its gas; and pge denotes an exception raised
by a throw command.

In the small-step semantics, we always execute the element at the top of the
stack. Transitions have the form
$\text{env}_{T}\vdash\left<Q,\text{env}_{SV},g\right>\rightarrow\left<Q^{\prime},\text{env}_{SV}^{\prime},g^{\prime}\right>$,
where $g\geq g^{\prime}\geq 0$, and are defined by the rules in Figure 3,
which rely on the (standard) semantics for expression evaluation (written
$\rightarrow_{e}$) taken from [1] and whose rules are in Appendix 0.A. To keep
the language and the semantics easy, we make a few simplifying assumptions:

  1. 1.

We assume a unitary gas cost for all TinySol commands, rather than having
different prices for different instructions.

  2. 2.

We only let commands consume gas; this is in contrast to EVM, which also has
gas costs for expression operations such as ADD, MUL etc.

  3. 3.

We omit the _gas price_ , since the TinySol model of blockchains does not
include the concept of miners and blocks. Instead, we shall simply say that
the actual amount of gas consumed in a transaction is subtracted from the
user’s account balance.

[ss-skip] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<\texttt{skip}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{SV},g-1\right>}\;\left(g\geq 1\right)\par$
---|---
[ss-seq] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<\texttt{$S_{1}$;$S_{2}$}::Q,\text{env}_{SV},g\right>\rightarrow\left<S_{1}::S_{2}::Q,\text{env}_{SV},g\right>}\;\left(g\geq 1\right)\par$
[ss-if] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow_{e}b\in\left\\{\,\text{T},\text{F}\,\right\\}}{\begin{array}[]{r @{~} l}\text{env}_{T}\vdash~{}&\left<\texttt{if $e$ then $S_{\text{T}}$ else $S_{\text{F}}$}::Q,\text{env}_{SV},g\right>\\\ ~{}&\qquad\rightarrow\left<S_{b}::Q,\text{env}_{SV},g-1\right>\end{array}}\;\left(g\geq 1\right)\par$
[ss-for${}_{\text{T}}$] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow v\quad v\geq 1\quad v^{\prime}=v-1}{\begin{array}[]{r @{~} l}\text{env}_{T}\vdash~{}&\left<\texttt{for $e$ do $S$}::Q,\text{env}_{SV},g\right>\\\ ~{}&\qquad\rightarrow\left<S::\texttt{for $v^{\prime}$ do $S$}::Q,\text{env}_{SV},g-1\right>\end{array}}\;\left(g\geq 1\right)\par$
[ss-for${}_{\text{F}}$] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow v\quad v<1}{\text{env}_{T}\vdash\left<\texttt{for $e$ do $S$}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{SV},g-1\right>}\;\left(g\geq 1\right)\par$
[ss-decv] | $\dfrac{x\notin\operatorname{dom}\left(\text{env}_{V}\right)\quad\text{env}_{SV}\vdash e\rightarrow_{e}v}{\begin{array}[]{r @{~} l}\text{env}_{T}\vdash~{}&\left<\texttt{var $x$ := $e$ in $S$}::Q,\text{env}_{SV},g\right>\\\ ~{}&\qquad\rightarrow\left<S::\text{del}(x)::Q,\text{env}_{S},((x,v),\text{env}_{V}),g-1\right>\end{array}}\;\left(g\geq 1\right)\par$
[ss-assv] | $\dfrac{x\in\operatorname{dom}\left(\text{env}_{V}\right)\quad\text{env}_{SV}\vdash e\rightarrow_{e}v}{\begin{array}[]{r @{~} l}\text{env}_{T}\vdash~{}&\left<\texttt{$x$ := $e$}::Q,\text{env}_{SV},g\right>\\\ ~{}&\qquad\rightarrow\left<Q,\text{env}_{S},\text{env}_{V}\kern-2.0pt\left[x\mapsto v\right],g-1\right>\end{array}}\;\left(g\geq 1\right)\par$
[ss-assf] | $\dfrac{\begin{array}[]{l}\text{env}_{V}(\texttt{this})=X\quad\text{env}_{S}(X)=\text{env}_{P}\\\ p\in\operatorname{dom}\left(\text{env}_{P}\right)\quad\text{env}_{SV}\vdash e\rightarrow_{e}v\end{array}}{\begin{array}[]{r @{~} l}\text{env}_{T}\vdash~{}&\left<\texttt{this.$p$ := $e$}::Q,\text{env}_{SV},g\right>\\\ ~{}&\qquad\rightarrow\left<Q,\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{P}\kern-2.0pt\left[p\mapsto v\right]\right],\text{env}_{V},g-1\right>\end{array}}\;\left(g\geq 1\right)\par$
[ss-call] |
[ss-throw] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<\texttt{throw}::Q,\text{env}_{SV},g\right>\rightarrow\left<\text{exc}(\texttt{pge})::Q,\text{env}_{SV},g\right>}\;\left(g\geq 1\right)\par$
[ss-oog] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<S::Q,\text{env}_{SV},0\right>\rightarrow\left<\text{exc}(\texttt{oog})::S::Q,\text{env}_{SV},0\right>}\par$
[ss-delv] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<\text{del}(x)::Q,\text{env}_{S},((x,v),\text{env}_{V}),g\right>\rightarrow\left<Q,\text{env}_{SV},g\right>}\par$
[ss-return] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<\text{env}_{V}^{\prime}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{S},\text{env}_{V}^{\prime},g\right>}\par\par$

Figure 2: Small-step semantics transition rules for statements with gas.

With these assumptions, gas consumption is modelled by introducing the side
condition $g\geq 1$ in most of the rules, since $g$ is decremented by $1$ in
the reduct of these rules.222It is conceptually easy, albeit notationally
cumbersome, to provide each operation and command with its own cost $c(\cdot)$
and modify the semantics to take such costs into account in the side
conditions and conclusions of each rule. This would relax the simplifying
assumptions 1 and 2 given above.  The only rules that do not consume gas are
LABEL:ts2_sss_seq, since this rule does not describe the execution of an
operation but merely transforms the top element of the stack, and
LABEL:ts2_sss_throw. Notice, however, that those two rules have the side
condition $g\geq 1$ to ensure determinism of the operational semantics: in
this way, when the gas becomes 0, only rule LABEL:ts2_sss_oog can be used.
Finally, the only rules that do not check the remaining amount of gas are
LABEL:ts2_sss_delv and LABEL:ts2_sss_return, since these rules do not
correspond to commands, but are only used to restore a previous state of the
variable environment.

Rule LABEL:ts2_sss_throw says that a throw command is simply converted into an
exception $\text{exc}(\texttt{pge})$, denoting that the exception was thrown
from within the program. The remaining exception labels are used if one of the
side conditions fails; so, the execution of most of the statements can lead to
an exception in several different ways:

  * •

An out-of-gas exception oog is thrown if we have a command on top of the stack
but no gas is left, see rule LABEL:ts2_sss_oog.

  * •

A negative balance exception neg is thrown if executing the statement would
lead to a negative balance. Hence, this exception can only be thrown from the
rule LABEL:ts2_sss_call, if the side condition
$n\leq\text{env}_{P}^{X}(\texttt{balance})$ does not hold.

  * •

Finally, a runtime exception rte is thrown if any of the other side conditions
does not hold. We omit the rules for generating these exceptions, since they
are heavy and do not add anything to our presentation. Furthermore, by using a
very standard type system, such exceptions can be easily prevented at compile
time.

Notice that, when an exception appears on top of the stack, the execution
halts as there are no rules to conclude a transition in such a case.
Furthermore, the exception label $l$ has no meaning in the semantics, and the
different labels are used only to distinguish between different situations
that raise an exception. We could have added a command catch to handle
exceptions according to their label (like in many programming languages).
However, since the purpose of this paper is to develop techniques that prevent
out-of-gas exceptions through static checks, for the sake of simplicity we
preferred to omit such a command.

[Gen] | $\dfrac{\left<DC,\text{env}_{ST}^{\emptyset}\right>\rightarrow_{DC}\text{env}_{ST}}{\left<\texttt{$DC$ $T$},\text{env}_{ST}^{\emptyset}\right>\rightarrow_{B}\left<T,\text{env}_{ST}\right>}$
---|---

[Rev] | $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{ST}\right>\rightarrow_{B}\text{env}_{ST}}$
---|---

[Tx1] | $\dfrac{\begin{array}[]{l}\text{env}_{S}(A)=\text{env}_{P}^{A}\qquad g\leq\text{env}_{P}^{A}(\texttt{balance})-n\\\ \text{env}_{T}\vdash\left<\texttt{$X$.$f$($\widetilde{v}$):$n$}::\bot,\text{env}_{S},(\texttt{this},A),g\right>\rightarrow\left<\bot,\text{env}_{S}^{\prime},\text{env}_{V},g^{\prime}\right>\\\ \text{env}_{S}^{\prime\prime}=\text{env}_{S}^{\prime}\kern-2.0pt\left[A\mapsto\text{env}_{P}^{A}[\texttt{balance -= }(g-g^{\prime})]\right]\end{array}}{\left<A\texttt{->}X\texttt{.}f\texttt{(}\widetilde{v}\texttt{):}(n,g),T,\text{env}_{ST}\right>\rightarrow_{B}\left<T,\text{env}_{S}^{\prime\prime},\text{env}_{T}\right>}\par\par$
---|---
[Tx2] | $\dfrac{\begin{array}[]{l}\text{env}_{S}(A)=\text{env}_{P}^{A}\qquad g\leq\text{env}_{P}^{A}(\texttt{balance})-n\\\ \text{env}_{T}\vdash\left<\texttt{$X$.$f$($\widetilde{v}$):$n$}::\bot,\text{env}_{S},(\texttt{this},A),g\right>\rightarrow\left<\text{exc}(l)::Q,\text{env}_{S}^{\prime},\text{env}_{V},g^{\prime}\right>\\\ \text{env}_{S}^{\prime\prime}=\text{env}_{S}\kern-2.0pt\left[A\mapsto\text{env}_{P}^{A}[\texttt{balance -= }(g-g^{\prime})]\right]\end{array}}{\left<A\texttt{->}X\texttt{.}f\texttt{(}\widetilde{v}\texttt{):}(n,g),T,\text{env}_{ST}\right>\rightarrow_{B}\left<T,\text{env}_{S}^{\prime\prime},\text{env}_{T}\right>}\par$

Figure 3: Transition rules for blockchains.

The semantics for blockchains is given in Figure 3 and contains rules
LABEL:ts2_trans_genesis and LABEL:ts2_trans_revel, to activate and reveal the
outcome of a sequence of transactions. Notice that the first rule exploits the
semantics for declarations (written $\rightarrow_{DC}$) taken from [1] for
turning a sequence of declarations $DC$ into a proper environment; its rules
are in Appendix 0.A. The key rules for transactions are LABEL:ts2_trans_trans1
and LABEL:ts2_trans_trans2 for describing the execution of a transaction that
either succeeds or fails. Rule LABEL:ts2_trans_trans1 describes the situation
where the transaction succeeds. Having a gas limit $g$, the side condition
requires that $g$ must not be greater than the available balance of the
account $A$ initiating the transaction, _after_ any funds $n$ transferred
along with the call have been deducted from the balance (since that could
otherwise allow the balance of $A$ to become negative). After the transaction
succeeds, some amount of gas will have been consumed. The remaining gas
$g^{\prime}$ is then used to calculate how much gas was used, and then this
too is subtracted from the balance of $A$. Rule LABEL:ts2_trans_trans2
describes the situation where the transaction fails with an exception
$\text{exc}(l)$. Here, the gas difference $g-g^{\prime}$ is _still_ subtracted
from the balance of $A$, but otherwise the state $\text{env}_{S}$ is
unaltered. Thus, all other effects of the transaction that raised the
exception are rolled back, and the execution can continue with the next
transaction.

##  4 A Type System for Termination

The gas mechanism ensures that all transactions will eventually terminate,
thereby preventing denial-of-service attacks resulting from diverging method
calls. However, it does not prevent potentially diverging contracts from being
added to the blockchain. This presents a problem to the users of the smart
contracts: how to ensure that they do not inadvertently create a transaction
invoking a diverging contract, since that would consume all available gas
supplied to the transaction. Furthermore, even if a method call does not
actually diverge, it may still require many execution steps, and the user must
therefore be sure to supply sufficient gas for the transaction to allow the
execution to finish. In the present section, we shall describe a type system
for statically checking termination of transactions, whilst also providing
upper (and lower) bounds on the number of execution steps.

###  4.1 The Type System

We wish to create a type system that will allow us to derive an upper bound on
the number of execution steps required to run a statement $S$, since that is
proportional to the required amount of gas. Hence, type judgments for
statements will be of the form $\Gamma\vdash S:n$ where $n$ is an integer
denoting the maximum number of steps. This number may be affected by the
(integer) values of the loop condition expressions in $S$; thus we need the
integer type (for both variables and expressions) to provide explicit upper
and lower bounds on those values. We write this as $\text{int}^{u}_{\ell}$,
where $u$ (resp. $\ell$) is the upper (resp. lower) bound (both included).

The $\text{int}^{u}_{\ell}$ type is quite limiting; for instance, it will
disallow some common operations such as increments/decrements of a variable
(e.g., $x$ := $x$+1). Therefore, we shall also include an ordinary (unbounded)
integer type int for integer-valued variables and fields that do not in any
way contribute to the expressions that guard for loops. To allow variables of
both types to appear in operations, we shall also introduce a subtyping
relation $\mathrel{\text{{<:}}}$ to allow bounded integer types to be coerced
up to the unbounded type (see the rules in Appendix 0.B).

We also need the type of methods to have an upper bound on the number of steps
required to execute the method body. This type is written
$\text{proc}(\widetilde{B})^{u}_{\ell}:n$, to be reads as: assuming that the
formal parameters are of (base) types $\widetilde{B}$ and that the transferred
amount of currency is in the interval $[\ell..u]$, then the method body
requires at most $n$ steps to execute. The bounds on the value variable are
necessary, since the variable might be used in a loop expression333We could
also introduce an ‘unbounded’ method type (similarly to what we did for int
and $\text{int}^{u}_{\ell}$), but we shall omit this to avoid complicating the
matter further. The ‘bounded’ method type also has the added benefit of
allowing a programmer to specify a minimum amount of currency that must be
provided to call a method.. Thus, we also handle divergence resulting from
recursive method calls, since any calls within the method body would need to
have a value strictly lower than $n$ (as calling the method itself also
requires one step).

Finally, we need to give types to contract names, which must provide
information on the signatures of fields and methods implemented in the
contract. Here, we shall employ a method similar to the one used in [1] and
assume a set of _type names_ (or ‘interface names’) $\mathcal{I}$, ranged over
by $I$. We then let type environments $\Gamma$ be partial functions from names
to types, but also include $\Gamma$ in the language of types and use these as
the types of interface names. The idea is that, if $X$ is a contract name of
type $I$, then $\Gamma(X)=I$ and $\Gamma(I)=\Gamma_{I}$, where $\Gamma_{I}$
then contains the signatures of the fields and methods of contract $X$. We
shall assume that these interfaces are declared besides the contract
declarations, e.g. using an interface definition language similar to the one
described in [1], and we refer the reader to that work for further details.

######  Definition 4 (Language of types)

We use the following language of types, where $I\in\mathcal{I}$ is a _type
name_ (or ‘interface name’) and
$\mathcal{N}=\text{ANames}\cup\text{FNames}\cup\text{VNames}\cup\text{MNames}\cup\mathcal{I}$:

$\begin{array}[]{r @{~} c @{~} l @{\qquad}
l}B~{}&::=\hfil~{}&\text{bool}~{}~{}\big{|}~{}~{}~{}\text{int}~{}~{}\big{|}~{}~{}~{}\text{int}^{u}_{\ell}~{}~{}\big{|}~{}~{}~{}I\\\
T\in\mathcal{T}~{}&::=\hfil~{}&B~{}~{}\big{|}~{}~{}~{}\text{proc}(\widetilde{B})^{u}_{\ell}:n~{}~{}\big{|}~{}~{}~{}\Gamma\\\
\Gamma,\Delta~{}&::=\hfil~{}&\mathcal{N}\rightharpoonup\mathcal{T}\end{array}$

We write $\widetilde{T}$ for a tuple of types $(T_{1},\ldots,T_{n})$.

As in [1], we require that all interface declarations be _well-formed_ in the
sense that they must at least contain a declaration for the mandatory members,
i.e. the balance field (type int) and the send() method (type
$\text{proc}()^{\texttt{INT\\_MAX}}_{0}:1$). This ensures that we can define a
minimal interface declaration called $I^{\top}$, containing just the
signatures of balance and send(), such that every well-formed interface
declaration is a specialisation of $I^{\top}$; this is ensured by the
subtyping relation and it is necessary to allow us to give a type to the
‘magic’ variable sender, which is available within the body of any method.

We shall also use a _typed_ syntax of TinySol, where local variables are now
declared as $B$ $x$ := $e$ and $B$ is the type of the value of the expression
$e$. Furthermore, we assume that the type information is also stored in
$\text{env}_{V}$, along with the actual value of each variable. We write this
as a triple $(x,v,B)$ but otherwise ignore the type information in the
semantics. Interface types could also be explicitly given in the contract
definitions, i.e. as contract $X$ : $I$ { $DF$ $DM$ }, but to simplify the
presentation we shall here merely assume that interface definitions for all
contracts exist and are added to any type environment $\Gamma$ that we shall
consider in the following.

We can now give the type rules, starting with the rules for environment
agreement, given in Figure 4. The type judgments here ascertain that each
contract, field, variable and method indeed has a type in the type
environment, that these types are compatible with the values assigned to them,
and, in the case of methods, with the number of steps inferred for the method
body $S$. Note also that we write the type environment as split into two
parts: the first part, $\Gamma$, contains the types for contract addresses;
the second part, $\Delta$, records the types of local variables, including the
‘magic’ variables this, sender and value. Also, unless otherwise noted, we
shall assume in the rules that these reserved names are contained in the
respective sets of field and variables names, i.e.
$\texttt{balance}\in\text{FNames}$ and
$\texttt{this},\texttt{sender},\texttt{value}\in\text{VNames}$.

The type rules for declarations are very similar to those for environments
(environments are just an alternative representation of declarations); thus,
we omit them from the body of the paper and report them in Appendix 0.C.

[t-env-t] | $\dfrac{\Gamma,\Delta\vdash\text{env}_{M}\quad\Gamma\vdash\text{env}_{T}}{\Gamma\vdash(X,\text{env}_{M}),\text{env}_{T}}\;\left(\Delta=\texttt{this}:\Gamma(X)\right)\par$
---|---
[t-env-m] | $\dfrac{\Gamma,\Delta^{\prime}\vdash S:n\quad\Gamma,\Delta\vdash\text{env}_{M}}{\Gamma,\Delta\vdash(f,(\widetilde{x},S)),\text{env}_{M}}\;\left(\begin{array}[]{l}\Delta(\texttt{this})=I\\\ \Gamma(I)(f)=\text{proc}(\widetilde{B})^{u}_{\ell}:n\\\ \Delta^{\prime}=\Delta,\widetilde{x}:\widetilde{B},\texttt{value}:\text{int}^{u}_{\ell},\texttt{sender}:I^{\top}\end{array}\right)\par$
[t-env-s] | $\dfrac{\Gamma,\Delta\vdash\text{env}_{F}\quad\Gamma\vdash\text{env}_{S}}{\Gamma\vdash(X,\text{env}_{F}),\text{env}_{S}}\;\left(\Delta=\texttt{this}:\Gamma(X)\right)\par$
[t-env-f] | $\dfrac{\Gamma,\Delta\vdash v:B\quad\Gamma,\Delta\vdash\text{env}_{F}}{\Gamma,\Delta\vdash(p,v),\text{env}_{F}}\;\left(\begin{array}[]{l}\Delta(\texttt{this})=I\\\ \Gamma(I)(p)=B\end{array}\right)\par$
[t-env-v] | $\dfrac{\Gamma,\Delta\vdash v:B\quad\Gamma,\Delta\vdash\text{env}_{V}}{\Gamma,\Delta\vdash(x,v,B),\text{env}_{V}}\;\left(\Delta(x)=B\right)$
Figure 4: Type rules for environment agreement.

Next, we have the rules for typing expressions, which are given in Figure 5.
Type judgments are here of the form $\Gamma,\Delta\vdash e:B$. Note that in
rule LABEL:ts2_type_termination_val, when $v$ is an integer value, we set both
the upper and lower bounds in the type to be exactly the value $v$. To widen
the type of the value, e.g., when typing an assignment (such as
$\text{int}^{5}_{2}$ $x$ := $3$), we will use the subtyping relation. In the
rule LABEL:ts2_type_termination_op, we assume the existence of type rules with
judgments of the form $\vdash\operatorname{op}:\widetilde{B}\to B$ for each
operation $\operatorname{op}$. In particular, we assume that we can derive
conclusions about the upper and lower bounds on integer-valued operations from
the bounds on the expression operands. This is straightforward for standard
integer operations. As an example, consider the following rules:

$\vdash+:(\text{int}^{u_{1}}_{\ell_{1}},\text{int}^{u_{2}}_{\ell_{2}})\to\text{int}^{u_{1}+u_{2}}_{\ell_{1}+\ell_{2}}\qquad\vdash-:(\text{int}^{u_{1}}_{\ell_{1}},\text{int}^{u_{2}}_{\ell_{2}})\to\text{int}^{u_{1}-\ell_{2}}_{\ell_{1}-u_{2}}$

For example, assuming that $\Gamma,\Delta\vdash x:\text{int}^{5}_{2}$, the
type of $10-x$ is $\text{int}^{8}_{5}$.

[t-var] | $\dfrac{\phantom{P}}{\Gamma,\Delta\vdash x:B}\;\left(\Delta(x)=B\right)$
---|---

[t-field] | $\dfrac{\Gamma,\Delta\vdash e:I}{\Gamma,\Delta\vdash e.p:B}\;\left(\Gamma(I)(p)=B\right)$
---|---

[t-val] | $\dfrac{\phantom{P}}{\Gamma,\Delta\vdash v:B}\;\left(B=\begin{cases}\Gamma(v)&\text{if $v\in\text{ANames}$}\\\ \text{bool}&\text{if $v\in\mathbb{B}$}\\\ \text{int}^{v}_{v}&\text{if $v\in\mathbb{Z}$}\end{cases}\right)\par$
---|---
[t-op] | $\dfrac{\Gamma,\Delta\vdash\widetilde{e}:\widetilde{B}\quad\vdash\operatorname{op}:\widetilde{B}\to B}{\Gamma,\Delta\vdash\operatorname{op}(\widetilde{e}):B}$

Figure 5: Type rules for expressions

Finally, we have the type rules for statements, given in Figure 6. Here, type
judgments are of the form $\Gamma,\Delta\vdash S:n$, with $n$ denoting the
maximum number of steps required to execute $S$. This is mostly calculated in
an obvious way, by only using the upper bounds $u$; however, the lower bounds
$\ell$ are implicitly used when calculating the types of expressions (as
discussed above). For example, we calculate the upper bound on the number of
steps of for $e$ do $S$ by first calculating the upper bound $u$ on the value
of $e$ and the upper bound $n$ on the steps for $S$: If $u\geq 1$, we multiply
$u$ and $n+1$ (the ‘+1’ is the extra step needed for activating every
iteration of the loop, cf. LABEL:ts2_sss_fortrue) and finally we sum 1 (the
cost of the final activation of the loop; i.e., when the guard becomes < 1,
see LABEL:ts2_sss_forfalse). Otherwise the upper bound is $1$ (only the case
with a guard < 1). The max is used for covering the two cases with one single
rule.

Notice that LABEL:ts2_type_termination_decv and
LABEL:ts2_type_termination_call both have $n+2$ in their conclusion, rather
than $n+1$, because both constructs will push an extra symbol onto the stack
(viz., $\text{del}(x)$ and $\text{env}_{V}$, resp.), which will require an
extra step in the semantics when their scope ends. A similar reason justifies
the ‘+1’ in rules LABEL:ts2_type_termination_seq,
LABEL:ts2_type_termination_if, and LABEL:ts2_type_termination_loop.

[t-skip] | $\dfrac{\phantom{P}}{\Gamma,\Delta\vdash\texttt{skip}:1}\par$
---|---
[t-throw] | $\dfrac{\phantom{P}}{\Gamma,\Delta\vdash\texttt{throw}:1}$

[t-assv] | $\dfrac{\Gamma,\Delta\vdash x:B\quad\Gamma,\Delta\vdash e:B}{\Gamma,\Delta\vdash\texttt{$x$ := $e$}:1}\par$
---|---
[t-assf] | $\dfrac{\Gamma,\Delta\vdash e_{1}.p:B\quad\Gamma,\Delta\vdash e_{2}:B}{\Gamma,\Delta\vdash\texttt{$e_{1}$.$p$ := $e_{2}$}:1}$

[t-decv] | $\dfrac{\Gamma,\Delta\vdash e:B\quad\Gamma,(\Delta,x:B)\vdash S:n}{\Gamma,\Delta\vdash\texttt{$B$ $x$ := $e$ in $S$}:n+2}\par$
---|---
[t-seq] | $\dfrac{\Gamma,\Delta\vdash S_{1}:n_{1}\quad\Gamma,\Delta\vdash S_{2}:n_{2}}{\Gamma,\Delta\vdash\texttt{$S_{1}$;$S_{2}$}:n_{1}+n_{2}+1}\par$
[t-if] | $\dfrac{\Gamma,\Delta\vdash e:\text{bool}\quad\Gamma,\Delta\vdash S_{\text{T}}:n_{1}\quad\Gamma,\Delta\vdash S_{\text{F}}:n_{2}}{\Gamma,\Delta\vdash\texttt{if $e$ then $S_{\text{T}}$ else $S_{\text{F}}$}:\max(n_{1},n_{2})+1}\par$
[t-loop] | $\dfrac{\Gamma,\Delta\vdash e:\text{int}^{u}_{\ell}\quad\Gamma,\Delta\vdash S:n}{\Gamma,\Delta\vdash\texttt{for $e$ do $S$}:\max(1,u(n+1)+1)}\par$
[t-call] | $\dfrac{\Gamma,\Delta\vdash e_{1}:I\quad\Gamma,\Delta\vdash\widetilde{e}:\widetilde{B}\quad\Gamma,\Delta\vdash e_{2}:\text{int}^{u}_{\ell}}{\Gamma,\Delta\vdash\texttt{$e_{1}$.$f$($\widetilde{e}$):$e_{2}$}:n+2}\;\left(\Gamma(I)(f)=\text{proc}(\widetilde{B})^{u}_{\ell}:n\right)$

Figure 6: Type rules for statements.

We illustrate the use of the type system with a small example. Consider the
statement for $x$ do call $y$.$f$($x$):1, and assume it is to be executed in
an environment where the local variables $x$ and $y$ are declared so that
$\text{env}_{V}(x)=3$ and $\text{env}_{V}(y)=A$, for some contract $A$ of
interface type $I$ containing a method $f$. Thus, this statement will call the
method $A$.$f$ three times, each time transferring $1$ unit of currency along
with the call, and with the number $3$ as the actual parameter (since the
value of $x$ does not change, cf. rule LABEL:ts2_sss_fortrue).

To type the example, assume further that $\Delta(x)=\text{int}^{5}_{1}$,
$\Delta(y)=I$, and $\Gamma(I)(f)=\text{proc}(\text{int})^{10}_{1}:20$. Thus,
the for-loop can run at most 5 times; moreover, the method call must at least
receive 1 unit of currency to execute and will finish in at most 20 steps. The
most interesting part of the typing derivation is then as follows:

$\dfrac{\dfrac{\Delta(x)=\text{int}^{5}_{1}}{\Gamma,\Delta\vdash
x:\text{int}^{5}_{1}}\qquad\dfrac{\begin{array}[]{c}\\\
\ldots\end{array}\quad\dfrac{\dfrac{\Delta(x)=\text{int}^{5}_{1}}{\Gamma,\Delta\vdash
x:\text{int}^{5}_{1}}\qquad\begin{array}[]{c}\\\
\Gamma\vdash\text{int}^{5}_{1}\mathrel{\text{{<:}}}\text{int}\end{array}}{\Gamma,\Delta\vdash
x:\text{int}}\qquad\dfrac{\ldots}{\Gamma,\Delta\vdash
1:\text{int}^{10}_{1}}}{\Gamma,\Delta\vdash\texttt{call
$y$.$f$($x$):1}:20+2}}{\Gamma,\Delta\vdash\texttt{for $x$ do call
$y$.$f$($x$):1}:\max(1,5((20+2)+1)+1)}$

For space reasons, we have omitted the derivation of $\Gamma,\Delta\vdash
y:I$, which is concluded by LABEL:ts2_type_termination_var and of
$\Gamma,\Delta\vdash 1:\text{int}^{10}_{1}$, which is inferred using the
subtyping rules (see Appendix 0.B). The latter involves concluding
$\Gamma,\Delta\vdash 1:\text{int}^{1}_{1}$ by LABEL:ts2_type_termination_val,
and then
$\Gamma\vdash\text{int}^{1}_{1}\mathrel{\text{{<:}}}\text{int}^{10}_{1}$ can
be proved by LABEL:ts2_type_termination_subs_int1, since $1\leq 10$ for the
upper bound, and $1\leq 1$ for the lower bound. Likewise, the type of $x$,
which is $\text{int}^{5}_{1}$, is coerced up to int by the subtyping rule
LABEL:ts2_type_termination_subs_int2, when $x$ is used as a parameter for the
method call, as required by the type of $f$. Thus we conclude, by
LABEL:ts2_type_termination_call, that the method call itself will require at
most $20+2=22$ steps, and, finally, by LABEL:ts2_type_termination_loop, that
the entire for-loop will require at most $\max(1,5((20+2)+1)+1)=116$ steps.

###  4.2 Properties of the type system

Our type system ensures that a well-typed statement $S$, executing in a
configuration with well-typed environments $\text{env}_{TSV}$, will terminate
after at most $n$ steps. To prove this property, we wish to show a statement
saying that well-typedness is preserved by transitions (subject reduction),
and furthermore that the number $n$ decreases after every transition step.
However, our semantics does not describe the execution of single statements,
but rather of _stacks_ , so we shall also need the notion of well-typed stacks
and configurations.

The definition of such notions is complicated by the form of our semantic
rules (Figure 3): Atomic statements are taken from the top of the stack and
evaluated directly in the conclusion of a rule, whereas composite statements
are rewritten and then pushed back onto the stack. This feature makes
exception handling easy, since we do not need extra rules for propagating an
exception down through a derivation tree, but it does pose a problem w.r.t.
the subject reduction theorem, in particular in dealing with the rules
LABEL:ts2_sss_decv and LABEL:ts2_sss_call. Both of these rules alter the local
variable environment $\text{env}_{V}$, either by adding a new binding to it
(LABEL:ts2_sss_decv) or by replacing it with a new environment
(LABEL:ts2_sss_call), but the scope of these changes is not confined to the
premise of those rules, unlike in the corresponding type rules
(LABEL:ts2_type_termination_decv and LABEL:ts2_type_termination_call).
Instead, the syntax of stacks (Definition 3) introduces some extra symbols
($\text{del}(x)$ and $\text{env}_{V}$) to mark the end of these scopes, which
are then pushed onto the stack _before_ pushing the statement $S$ to be
executed within the scope of these new bindings. This, in turn, means that new
local variables can appear as free in the statement residing on the top of a
stack _after_ a transition step, if the previously executed statement was a
declaration or a call. Thus, to be able to type the stack after a transition
step, we need a way to update the $\Delta$ part of the type environment with
information on these new bindings. This is done as follows:

######  Definition 5 (Extraction function)

The type extraction function from stacks to type environments is given by the
following clauses:

$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}((x,v,B),\text{env}_{V}::Q)$
$\displaystyle=x:B,\ \mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}::Q)$ (1)
$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}^{\emptyset}::Q)$
$\displaystyle=\epsilon$ (2)
$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$B$ $x$ := $e$ in
$S$}::Q)$ $\displaystyle=x:B,\ \Delta$ (3)
$\displaystyle\mathcal{E}^{\Gamma}_{\Delta,x:B}(\text{del}(x)::Q)$
$\displaystyle=\Delta$ (4)
$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$e_{1}$.$f$($\widetilde{e}$):$e_{2}$}::Q)$
$\displaystyle=\texttt{this}:I,\ \texttt{sender}:I^{\top},\
\texttt{value}:\text{int}^{u}_{\ell},\ \widetilde{x}:\widetilde{B}$ (5) where
$\Gamma,\Delta\vdash e_{1}:I$ and
$\Gamma(I)(f)=\text{proc}(\widetilde{B})^{u}_{\ell}:n$.
$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}(Q)$
$\displaystyle=\Delta\qquad\text{in all other cases}$ (6)

The function ensures that the type environment for local variables $\Delta$
remains in agreement with the currently active variable environment
$\text{env}_{V}$ after a transition. This is also the reason why we needed to
store the type information of locally declared variables in $\text{env}_{V}$,
and why we use the convention of writing the type environment as split into
two segments (viz., $\Gamma$ and $\Delta$), since the $\Gamma$ segment remains
unaltered.

[t-bot] | $\dfrac{\phantom{P}}{\Gamma,\Delta\vdash\bot:0}\par$
---|---
[t-exc] | $\dfrac{\phantom{P}}{\Gamma,\Delta\vdash\text{exc}(l)::Q:0}\par$
[t-del] | $\dfrac{\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\text{del}(x)::Q)\vdash Q:n}{\Gamma,\Delta\vdash\text{del}(x)::Q:n}$

[t-stm] | $\dfrac{\Gamma,\Delta\vdash S:n_{1}\quad\Gamma,\Delta\vdash Q:n_{2}}{\Gamma,\Delta\vdash S::Q:n_{1}+n_{2}}\par$
---|---
[t-ctx] | $\dfrac{\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}::Q)\vdash Q:n}{\Gamma,\Delta\vdash\text{env}_{V}::Q:n}\par$
[t-cfg] | $\dfrac{\Gamma,\Delta\vdash Q:n\quad\Gamma\vdash\text{env}_{S}\quad\Gamma,\Delta\vdash\text{env}_{V}}{\Gamma,\Delta\vdash\left<Q,\text{env}_{SV},g\right>}\;\left(n<g\right)$

Figure 7: Type rules for stacks and configurations.

Now, we can define the notions of well-typed stacks and configurations, which
result from the rules given in Figure 7. Note that we use the extraction
function in the premises of rules LABEL:ts2_type_termination_ctx and
LABEL:ts2_type_termination_del to handle the two special cases when the top of
the stack is an end-of-scope symbol. Moreover, rule
LABEL:ts2_type_termination_cfg states that a configuration
$\left<Q,\text{env}_{SV},g\right>$ is well-typed (for some type environment
$\Gamma,\Delta$) if the environments agree, and the stack is typable as
terminating in $n$ steps, _and_ the supplied gas value $g$ is greater than
$n$; this is precisely what we want our type system to ensure.

We can now state our main theorem, whose proof is in Appendix 0.D.

######  Theorem 4.1 (Subject reduction)

Let $\Gamma\vdash\text{env}_{T}$ and
$\Gamma,\Delta\vdash\left<Q,\text{env}_{SV},g\right>$. If
$\text{env}_{T}\vdash\left<Q,\text{env}_{SV},g\right>\rightarrow\left<Q^{\prime},\text{env}_{SV}^{\prime},g^{\prime}\right>$
then
$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(Q)\vdash\left<Q^{\prime},\text{env}_{SV}^{\prime},g^{\prime}\right>$.

This theorem ensures not only that well-typedness of configurations is
preserved, but also that the number of steps always remains lower than the
provided gas value, by the side condition in rule
LABEL:ts2_type_termination_cfg.

###### Corollary 1

Let $\Gamma\vdash\text{env}_{T}$ and
$\Gamma,\Delta\vdash\left<Q,\text{env}_{SV},g\right>$. If
$\text{env}_{T}\vdash\left<Q,\text{env}_{SV},g\right>\rightarrow\left<Q^{\prime},\text{env}_{SV}^{\prime},g^{\prime}\right>$
then $Q^{\prime}\neq\text{exc}(\texttt{oog})::Q^{\prime\prime}$.

It is perhaps also worth emphasising that the type system also ensures
termination. This is another simple consequence of Theorem 4.1, since the gas
value decreases at every step, except when the transition is concluded with
one of the rules LABEL:ts2_sss_seq, LABEL:ts2_sss_delv, LABEL:ts2_sss_return,
LABEL:ts2_sss_throw and LABEL:ts2_sss_oog. Of these, the last two place an
exception on the top of the stack, which has no further transitions, so the
execution terminates. Since all stacks have a finite depth, the first three
rules can only be used finitely many times before another, gas-consuming
statement is encountered, or we reach the bottom of the stack. Thus, the
number of steps $n$ must necessarily also always eventually decrease.

Lastly, Theorem 4.1 can be generalised to transactions and blockchains in an
obvious way, since a transaction simply corresponds to a method call placed on
an empty stack (see rule LABEL:ts2_trans_trans1), from which a $\Delta$ is
derivable using the extraction function from Definition 5. Given well-typed
environments $\text{env}_{TS}$, the type system can thus be used to ensure
that a transaction is supplied with sufficient gas to allow it to finish
without invoking rule LABEL:ts2_trans_trans2.

###  4.3 Limitations of the type system

The type system ensures termination of well-typed configurations (and hence
transactions) and absence of out-of-gas exceptions, but at the cost of some
limitations. Firstly, we had to abandon while loops, in favour of the (more
controllable) for loops. This does not seem too severe, since smart contracts
are not intended to be used to create non-terminating programs.

More limiting, perhaps, is the fact that it also prohibits all forms of
recursive calls, including mutual recursions. This is a consequence of rule
LABEL:ts2_type_termination_call, which assigns a number of $n+2$ steps to a
call to a method $f$, whose number itself is $n$. By rule
LABEL:ts2_type_termination_envm, the declaration of $f$ is well-typed if the
statement $S$ in the method body is typeable as terminating in $n$ steps. As
$n$ is strictly less than $n+2$, $S$ therefore cannot contain a recursive call
to $f$, nor a call to any other method that itself calls $f$. This limitation
seems more severe, since it rules out even terminating recursive functions.

Finally, the bounded integer type needed for typing the guards of for loops
does not permit some common assignments where the assigned variable appears in
the expression (e.g., $x$ := $x$+1). This limitation is a consequence of rules
LABEL:ts2_type_termination_assv, LABEL:ts2_type_termination_decv and
LABEL:ts2_type_termination_assf, which require the assigned variable (resp.
field) to have the same base type $B$ as the expression $e$. Suppose for
example that $x$ has type $\text{int}^{u}_{\ell}$, and we have the assignment
$x$ := $x$+1. The computed bounds for the expression (which we assume in the
rule LABEL:ts2_type_termination_op) must therefore be
$\text{int}^{u+1}_{\ell+1}$, which does not match the type of $x$, nor can it
be coerced down to match it via subtyping. However, we remark that this
limitation only affects those variables that appear in the guard of for loops,
since all other ones can be typed as int.

##  5 Conclusion and Future Work

In this paper, we have further extended the TinySol model by equipping it with
a small-step semantics, exceptions and a gas mechanism. Using this refined
smart-contract model language, we presented a first step towards the
development of static analysis techniques for checking the desirable property
that a transaction never runs out-of-gas during its execution. This is done by
means of a type system whose main aim is to give an upper bound on the number
of steps needed by a transaction to complete its task.

The present type system is, in particular, inspired by Type System 1 of [8].
That paper also presents two other type systems, which e.g. allow for some
limited recursion. Thus, one avenue for future work is to extend the present
type system in a similar manner to permit some recursive method calls.

Another avenue concerns an altogether different approach to type soundness.
The present work uses the usual, inductive (subject reduction) approach of
[16]. However, one way to lift some of the restrictions on the loop construct
would be to instead use a coinductive approach, sometimes known as _semantic
typing_ [2, 3, 6]. A key difference lies in the structure of the soundness
proof, which in semantic typing allows ‘manual proofs’ to be used to guarantee
well-typedness of some ‘unsafe’ pieces of code, which cannot otherwise be
judged type-safe using the type rules. This approach has in particular been
explored by [2, 3] in a setting of proof-carrying code [12], the point being
that such proofs can be automatically verified by a proof-checker. A ‘manual
proof’ could for example be used to show that a particular usage of a while
loop in a contract in fact _will_ terminate, and it could then be published on
the blockchain along with the contract, thereby taking advantage of the
immutable nature of blockchains. This would allow users to still type check
transactions, even if they invoke methods containing unsafe code such as while
loops, because the type checker can take the accompanying ‘manual proof’ into
account. We intend to explore this possibility in future work.

An orthogonal way to evolve our type system is to let it also provide a lower
bound on the gas needed to execute a piece of code (not just an upper bound,
as it is now). This can be useful for estimating how much currency one needs
to have in the account to invoke a certain functionality.

Finally, having introduced the gas mechanism, we plan to implement real-life
smart contracts in TinySol and apply our type system to them to check its
practical applicability to meaningful case studies.

## References

  * [1] Aceto, L., Gorla, D., Lybech, S.: A sound type system for secure currency flow. In: Proc. of ECOOP 2024. LIPICS vol. 313, 19:1 – 19:27 (2024), https://arxiv.org/abs/2405.12976
  * [2] Ahmed, A.J.: Semantics of Types for Mutable State. Ph.D. thesis, Princeton University (2004), http://www.ccs.neu.edu/home/amal/ahmedsthesis.pdf
  * [3] Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (Sep 2001). https://doi.org/10.1145/504709.504712
  * [4] Bartoletti, M., Galletta, L., Murgia, M.: A minimal core calculus for Solidity contracts. In: Data Privacy Management, Cryptocurrencies and Blockchain Technology. pp. 233–243. Springer (2019). https://doi.org/10.1007/978-3-030-31500-9_15
  * [5] Boudol, G.: Typing termination in a higher-order concurrent imperative language. Information and Computation 208(6), 716–736 (2010), https://doi.org/10.1016/j.ic.2009.06.007
  * [6] Caires, L.: Logical semantics of types for concurrency. In: Proc. of CALCO. LNCS, vol. 4624, pp. 16–35. Springer (2007), https://doi.org/10.1007/978-3-540-73859-6_2
  * [7] Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011), https://doi.org/10.1145/1941487.1941509
  * [8] Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Information and Computation 204(7), 1045–1082 (2006). https://doi.org/10.1016/j.ic.2006.03.002
  * [9] Genet, T., Jensen, T.P., Sauvage, J.: Termination of Ethereum’s smart contracts. In: Proc. of the 17th International Joint Conference on e-Business and Telecommunications - Volume 2: SECRYPT. pp. 39–51. ScitePress (2020), https://doi.org/10.5220/0009564100390051
  * [10] Grech, N., Kong, M., Jurisevic, A., Brent, L., Scholz, B., Smaragdakis, Y.: MadMax: Surviving out-of-gas conditions in Ethereum smart contracts. Proc. ACM Program. Lang. 2(OOPSLA), 116:1–116:27 (2018), https://doi.org/10.1145/3276486
  * [11] Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Proc. of POST. LNCS, vol. 10804, pp. 243–269. Springer (2018), https://doi.org/10.1007/978-3-319-89722-6_10
  * [12] Necula, G.C.: Proof-carrying code. In: Proc. of POPL. p. 106–119. ACM (1997), https://doi.org/10.1145/263699.263712
  * [13] Nielson, H.R.: A Hoare-like proof system for analysing the computation time of programs. Sci. Comput. Program. 9(2), 107–136 (1987), https://doi.org/10.1016/0167-6423(87)90029-3
  * [14] Nielson, H.R., Nielson, F.: Semantics with Applications - A Formal Introduction. Wiley Professional Computing, Wiley (1992)
  * [15] Wood, G.: Ethereum: A secure decentralised generalised transaction ledger. In: Yellow Paper (2014), updated for EIP-150 in 2017
  * [16] Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)

##  Appendix 0.A Omitted Semantic Rules

The semantics of expressions is given in the following Figure 8, where we
assume an evaluation function
$\operatorname{op}(\widetilde{v})\rightarrow_{\operatorname{op}}v$ for every
basic operation $\operatorname{op}$ of the language.

[exp-val] | $\dfrac{\phantom{P}}{\text{env}_{SV}\vdash v\rightarrow_{e}v}\par$
---|---
[exp-var] | $\dfrac{x\in\operatorname{dom}\left(\text{env}_{V}\right)\quad\text{env}_{V}(x)=v}{\text{env}_{SV}\vdash x\rightarrow_{e}v}\par$
[exp-field] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow_{e}X\quad p\in\operatorname{dom}\left(\text{env}_{S}(X)\right)\quad\text{env}_{S}(X)(p)=v}{\text{env}_{SV}\vdash e.p\rightarrow_{e}v}\par$
[exp-op] | $\dfrac{\text{env}_{SV}\vdash\widetilde{e}\rightarrow_{e}\widetilde{v}\quad\operatorname{op}(\widetilde{v})\rightarrow_{\operatorname{op}}v}{\text{env}_{SV}\vdash\operatorname{op}(\widetilde{e})\rightarrow_{e}v}$
Figure 8: Semantics of expressions.

The semantics of declarations turns a field/method/contract declaration in the
appropriate environment, to be used in the semantics of transactions. The
rules are given in the following Figure 9

[dec-f1] | $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{F}\right>\rightarrow_{DF}\text{env}_{F}}\par$
---|---
[dec-f2] | $\dfrac{\left<DF,\text{env}_{F}\right>\rightarrow_{DF}\text{env}_{F}^{\prime}}{\left<\texttt{field $p$ := $v$;$DF$},\text{env}_{F}\right>\rightarrow_{DF}(p,v),\text{env}_{F}^{\prime}}\par$
[dec-m1] | $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{M}\right>\rightarrow_{DM}\text{env}_{M}}\par$
[dec-m2] | $\dfrac{\left<DM,\text{env}_{M}\right>\rightarrow_{DM}\text{env}_{M}^{\prime}}{\left<\texttt{$f$($\widetilde{x}$) \\{ $S$ \\} $DM$},\text{env}_{M}\right>\rightarrow_{DM}(f,(\widetilde{x},S)),\text{env}_{M}^{\prime}}\par$
[dec-c1] | $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{ST}\right>\rightarrow_{DC}\text{env}_{ST}}\par$
[dec-c2] | $\dfrac{\left<DF,\text{env}_{F}^{\emptyset}\right>\rightarrow_{DF}\text{env}_{F}\quad\left<DM,\text{env}_{M}^{\emptyset}\right>\rightarrow_{DM}\text{env}_{M}\quad\left<DC,\text{env}_{ST}\right>\rightarrow_{DC}\text{env}_{ST}^{\prime}}{\left<\texttt{contract $X$ \\{ $DF$ $DM$ \\} $DC$},\text{env}_{ST}\right>\rightarrow_{DC}((X,\text{env}_{F}),\text{env}_{S}^{\prime}),((X,\text{env}_{M}),\text{env}_{T}^{\prime})}$
Figure 9: Semantics of declarations.

##  Appendix 0.B Subtyping rules

The subtyping rules are only used for the right-hand side expression of
assignments and for the arguments to method calls, to allow the value of the
expression to be coerced up to a less specific type that can match the type of
the variable or field. Thus, we need the usual subsumption rule for
expressions:

[t-subs] | $\dfrac{\Gamma,\Delta\vdash e:B_{1}\quad\Gamma\vdash B_{1}\mathrel{\text{{<:}}}B_{2}}{\Gamma,\Delta\vdash e:B_{2}}$
---|---

Note that the subtyping relation is parametrised with a type environment
$\Gamma$. This is necessary for subtyping of interface names $I$. The
subtyping relation is then given by the reflexive and transitive closure of
the rules in Figure 10.

[subs-int1] | $\dfrac{\phantom{P}}{\Gamma\vdash\text{int}^{u_{1}}_{\ell_{1}}\mathrel{\text{{<:}}}\text{int}^{u_{2}}_{\ell_{2}}}\;\left(\begin{array}[]{c}u_{1}\leq u_{2}\\\ \ell_{1}\geq\ell_{2}\end{array}\right)\par$
---|---
[subs-int2] | $\dfrac{\phantom{P}}{\Gamma\vdash\text{int}^{u}_{\ell}\mathrel{\text{{<:}}}\text{int}}\par$
[subs-name] | $\dfrac{\Gamma\vdash\Gamma(I^{1})\mathrel{\text{{<:}}}\Gamma(I^{2})}{\Gamma\vdash I^{1}\mathrel{\text{{<:}}}I^{2}}\par$
[subs-env] | $\dfrac{\forall n\in\operatorname{dom}\left(\Gamma_{2}\right)\mathrel{.}\Gamma_{1}(n)\mathrel{\text{{<:}}}\Gamma_{2}(n)}{\Gamma\vdash\Gamma_{1}\mathrel{\text{{<:}}}\Gamma_{2}}\par$
[subs-proc] | $\dfrac{\Gamma\vdash\widetilde{B}_{1}\mathrel{\text{{<:}}}\widetilde{B}_{2}}{\Gamma\vdash\text{proc}(\widetilde{B}_{1})^{u_{1}}_{\ell_{1}}:n_{1}\mathrel{\text{{<:}}}\text{proc}(\widetilde{B}_{2})^{u_{2}}_{\ell_{2}}:n_{2}}\;\left(\begin{array}[]{c}n_{1}\leq n_{2}\\\ u_{1}\leq u_{2}\\\ \ell_{1}\geq\ell_{2}\end{array}\right)$
Figure 10: Subtyping rules.

Note in particular the two rules for subtyping of the two integer types. The
first rule, LABEL:ts2_type_termination_subs_int1, allows us to widen the
bounds on a bounded integer. This is necessary to make statements such as
$\text{int}^{8}_{2}$ $x$ := 5 be well-typed, since the type of 5 is
$\text{int}^{5}_{5}$ (by rule LABEL:ts2_type_termination_val). The second
rule, LABEL:ts2_type_termination_subs_int2, allows any bounded integer type to
be coerced up to an unbounded integer type. This is necessary, if e.g. both
bounded and unbounded integers appear together in an expression, or if we have
an assignment of a bounded integer type to an unbounded integer variable.

##  Appendix 0.C Omitted type rules

The type rules for declarations are given in the following Figure 11. Note
that they are almost identical to the type rules for environments (Figure 4).

[t-dec-c] | $\dfrac{\Gamma,\Delta\vdash DF\quad\Gamma,\Delta\vdash DM\quad\Gamma\vdash DC}{\Gamma\vdash\texttt{contract $X$ \\{ $DF$ $DM$ \\} $DC$}}\;\left(\Delta=\texttt{this}:\Gamma(X)\right)\par$
---|---
[t-dec-f] | $\dfrac{\Gamma,\Delta\vdash v:B\quad\Gamma,\Delta\vdash DF}{\Gamma,\Delta\vdash\texttt{field $p$ := $v$; $DF$}}\;\left(\begin{array}[]{l}\Delta(\texttt{this})=I\\\ \Gamma(I)(p)=B\end{array}\right)\par$
[t-dec-m] | $\dfrac{\Gamma,\Delta^{\prime}\vdash S:n\quad\Gamma,\Delta\vdash DM}{\Gamma,\Delta\vdash\texttt{$f(\widetilde{x})$ \\{ $S$ \\} $DM$}}\;\left(\begin{array}[]{l}\Delta(\texttt{this})=I\\\ \Gamma(I)(f)=\text{proc}(\widetilde{B})^{u}_{\ell}:n\\\ \Delta^{\prime}=\Delta,\widetilde{x}:\widetilde{B},\texttt{value}:\text{int}^{u}_{\ell},\texttt{sender}:I^{\top}\end{array}\right)$
Figure 11: Type rules for declarations.

##  Appendix 0.D Proof of Theorem 4.1 (subject reduction)

The proof relies on the following standard lemmas.

######  Lemma 1 (Strengthening)

If $\Gamma,(\Delta,x:B)\vdash\text{env}_{V}$ and
$x\notin\operatorname{dom}\left(\text{env}_{V}\right)$, then
$\Gamma,\Delta\vdash\text{env}_{V}$.

###### Proof

By induction on the structure of $\text{env}_{V}$, by using rule
LABEL:ts2_type_termination_envv.

The next two lemmas simply state that well-typedness of the variable
environment (resp. the state) is preserved, if we replace a value $v_{1}$ with
another value $v_{2}$ of the same type as $v_{1}$. Both are shown by induction
on the structure of $\text{env}_{V}$ (resp. $\text{env}_{S}$ and
$\text{env}_{P}$), by using the rules LABEL:ts2_type_termination_envv resp.
LABEL:ts2_type_termination_envs and LABEL:ts2_type_termination_envf.

######  Lemma 2 (Update for variables)

Assume that $\Gamma,\Delta\vdash\text{env}_{V}$,
$x\in\operatorname{dom}\left(\text{env}_{V}\right)$, $\Delta(x)=B$ and
$\Gamma,\Delta\vdash v:B$. Then
$\Gamma,\Delta\vdash\text{env}_{V}\kern-2.0pt\left[x\mapsto v\right]$.

######  Lemma 3 (Update for fields)

Assume that $\Gamma\vdash\text{env}_{S}$,
$X\in\operatorname{dom}\left(\text{env}_{S}\right)$, $\Gamma(X)(p)=B$ and
$\Gamma,\Delta\vdash v:B$. Then
$\Gamma\vdash\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{P}\kern-2.0pt\left[p\mapsto
v\right]\right]$.

Next, we need a lemma stating that, if $e$ has a type $B$ and $e$ evaluates to
a value $v$ relative to well-typed environments $\text{env}_{SV}$, then $v$
will indeed be a value of type $B$.

######  Lemma 4 (Safety for expressions)

Assume $\Gamma\vdash\text{env}_{S}$ and $\Gamma,\Delta\vdash\text{env}_{V}$
and $\Gamma,\Delta\vdash e:B$. If $\text{env}_{SV}\vdash e\rightarrow v$, then
$\Gamma,\Delta\vdash v:B$.

###### Proof

By induction on the structure of $e$.

We are now ready to prove subject reduction.

######  Proof (of Theorem 4.1)

$\Gamma,\Delta\vdash\left<Q,\text{env}_{SV},g\right>$ was concluded by
LABEL:ts2_type_termination_cfg; from the premises and side condition of this
rule, we know that:

  * •

$\Gamma,\Delta\vdash Q:n$,

  * •

$\Gamma\vdash\text{env}_{S}$,

  * •

$\Gamma,\Delta\vdash\text{env}_{V}$, and

  * •

$n<g$.

The transition is of the form

$\text{env}_{T}\vdash\left<Q,\text{env}_{SV},g\right>\rightarrow\left<Q^{\prime},\text{env}_{SV}^{\prime},g^{\prime}\right>$
(7)

and our goal is therefore to show that
$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(Q)\vdash\left<Q^{\prime},\text{env}_{SV}^{\prime},g^{\prime}\right>$
also holds. This must again be concluded by LABEL:ts2_type_termination_cfg;
hence, we must show that the premises of this rule, i.e.

  * •

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(Q)\vdash Q^{\prime}:n^{\prime}$,

  * •

$\Gamma\vdash\text{env}_{S}^{\prime}$,

  * •

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(Q)\vdash\text{env}_{V}^{\prime}$, and

  * •

$n^{\prime}<g^{\prime}$

are all satisfied. We therefore proceed by case analysis on how the transition
(7) has been inferred (by considering the rules in Figure 3):

  * •

Suppose the transition was concluded by LABEL:ts2_sss_skip. Then the stack is
of the form $\texttt{skip}::Q$, and (7) is of the form

$\text{env}_{T}\vdash\left<\texttt{skip}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{SV},g-1\right>$

Now, $\Gamma,\Delta\vdash\texttt{skip}::Q:n$ must have been concluded by
LABEL:ts2_type_termination_stm, since the top element on the stack is a
statement. The conclusion tells us that $n=n_{1}+n_{2}$, and from the premise
we have that

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{skip}:n_{1}$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash Q:n_{2}$

Here, $\Gamma,\Delta\vdash\texttt{skip}:n_{1}$ must have been concluded by
LABEL:ts2_type_termination_skip, which tells us that $n_{1}=1$. Thus
$n=1+n_{2}$, and therefore $n^{\prime}=n_{2}=n-1$.

Finally, $\mathcal{E}^{\Gamma}_{\Delta}(\texttt{skip}::Q)=\Delta$ by case (6)
of Definition 5. Putting this together, we thus have the following:

    * –

$\Gamma,\Delta\vdash Q:n-1$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$,

    * –

$n^{\prime}<g^{\prime}$, since $n^{\prime}=n-1$, $g^{\prime}=g-1$, and $n<g$.

  * •

Suppose that LABEL:ts2_sss_seq was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{$S_{1}$;$S_{2}$}::Q,\text{env}_{SV},g\right>\rightarrow\left<S_{1}::S_{2}::Q,\text{env}_{SV},g\right>$

Furthermore, $\Gamma,\Delta\vdash\left<\texttt{$S_{1}$;$S_{2}$}::Q\right>:n$
was concluded by LABEL:ts2_type_termination_stm, where $n=n_{1}+n_{2}$, and
with premises

$\displaystyle\Gamma,\Delta$
$\displaystyle\vdash\texttt{$S_{1}$;$S_{2}$}:n_{1}$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_seq. Thus
$n_{1}=n_{1}^{\prime}+n_{1}^{\prime\prime}+1$ from the conclusion of that
rule, and

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash S_{1}:n_{1}^{\prime}$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash S_{2}:n_{1}^{\prime\prime}$

from its premises.

As
$\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$S_{1}$;$S_{2}$}::Q^{\prime})=\Delta$
by case (6) of Definition 5, we can therefore conclude

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash
S_{2}::Q:n_{1}^{\prime\prime}+n_{2}$ $\displaystyle\Gamma,\Delta$
$\displaystyle\vdash
S_{1}::S_{2}::Q:n_{1}^{\prime}+n_{1}^{\prime\prime}+n_{2}$

by repeated application of rule LABEL:ts2_type_termination_stm. Thus we
conclude the following:

    * –

$\Gamma,\Delta\vdash
S_{1}::S_{2}::Q:n_{1}^{\prime}+n_{1}^{\prime\prime}+n_{2}$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$,

    * –

$n_{1}^{\prime}+n_{1}^{\prime\prime}+n_{2}<g$, since we know that
$n_{1}^{\prime}+n_{1}^{\prime\prime}+1+n_{2}<g$, and the transition does not
consume any gas.

  * •

Suppose that LABEL:ts2_sss_if was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{if $e$ then $S_{\text{T}}$ else
$S_{\text{F}}$}::Q,\text{env}_{SV},g\right>\rightarrow\left<S_{b}::Q,\text{env}_{SV},g-1\right>$

Furthermore, $\Gamma,\Delta\vdash\texttt{if $e$ then $S_{\text{T}}$ else
$S_{\text{F}}$}::Q:n$ was concluded by LABEL:ts2_type_termination_stm, where
$n=n_{1}+n_{2}$, and with premises

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{if $e$ then
$S_{\text{T}}$ else $S_{\text{F}}$}:n_{1}$ $\displaystyle\Gamma,\Delta$
$\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_if. Thus
$n_{1}=\max(n_{\text{T}},n_{\text{F}})+1$ from the conclusion of that rule,
and

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash S_{\text{T}}:n_{\text{T}}$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash S_{\text{F}}:n_{\text{F}}$

from its premises. Say that $n_{b}=\max(n_{\text{T}},n_{\text{F}})$, then
$n=n_{b}+1+n_{2}$.

Finally, $\mathcal{E}^{\Gamma}_{\Delta}(\texttt{if $e$ then $S_{\text{T}}$
else $S_{\text{F}}$}::Q)=\Delta$ by case (6) of Definition 5. Thus we can
conclude the following:

    * –

$\Gamma,\Delta\vdash S_{b}::Q:n_{b}+n_{2}$, which we conclude by
LABEL:ts2_type_termination_stm.

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$.

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$.

    * –

$n_{b}+n_{2}<g-1$, since we know that $n_{b}+1+n_{2}<g$.

  * •

Suppose that LABEL:ts2_sss_fortrue was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{for $e$ do
$S$}::Q,\text{env}_{SV},g\right>\rightarrow\left<S::\texttt{for $v^{\prime}$
do $S$}::Q,\text{env}_{SV},g-1\right>$

with $\text{env}_{SV}\vdash e\rightarrow v$, $v\geq 1$, and $v^{\prime}=v-1$
as premises. Then $\Gamma,\Delta\vdash\texttt{for $e$ do $S$}::Q:n$ was
concluded by LABEL:ts2_type_termination_stm, where

$n=\max(1,u(n_{1}^{\prime}+1)+1)+n_{2}$

and with premises

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{for $e$ do
$S$}:\max(1,u(n_{1}^{\prime}+1)+1)$ $\displaystyle\Gamma,\Delta$
$\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_loop. From the
premises of this rule, we get that

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash e:\text{int}^{u}_{\ell}$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash S:n_{1}^{\prime}$

As we know that $v\geq 1$, this implies that $u\geq 1$, since $v\leq u$ by
Lemma 4. Thus

$\max(1,u(n_{1}^{\prime}+1)+1)=u(n_{1}^{\prime}+1)+1$

and therefore

$n=u(n_{1}^{\prime}+1)+1+n_{2}$

We can rewrite this as

$n=(u-1)(n_{1}^{\prime}+1)+(n_{1}^{\prime}+1)+1+n_{2}$

Assume w.l.o.g. that $u=v$, since this is the worst case w.r.t. the number of
steps required. Then $u-1=v-1=v^{\prime}$, and we can therefore rewrite the
above as

$n=v^{\prime}(n_{1}^{\prime}+1)+(n_{1}^{\prime}+1)+1+n_{2}$

By case (6) of Definition 5, we have that
$\mathcal{E}^{\Gamma}_{\Delta}(\texttt{for $e$ do $S$}::Q)=\Delta$.
Furthermore, $\Gamma,\Delta\vdash
v^{\prime}:\text{int}^{v^{\prime}}_{v^{\prime}}$ by rule
LABEL:ts2_type_termination_val. We can then conclude the following:

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{for $v^{\prime}$ do
$S$}:\max(1,v^{\prime}(n_{1}^{\prime}+1)+1)$ by
LABEL:ts2_type_termination_loop $\displaystyle\Gamma,\Delta$
$\displaystyle\vdash\texttt{for $v^{\prime}$ do
$S$}::Q:\max(1,v^{\prime}(n_{1}^{\prime}+1)+1)+n_{2}$ by
LABEL:ts2_type_termination_stm $\displaystyle\Gamma,\Delta$
$\displaystyle\vdash S::\texttt{for $v^{\prime}$ do
$S$}::Q:n_{1}^{\prime}+\max(1,v^{\prime}(n_{1}^{\prime}+1)+1)+n_{2}$ by
LABEL:ts2_type_termination_stm

Say that
$n^{\prime}=n_{1}^{\prime}+\max(1,v^{\prime}(n_{1}^{\prime}+1)+1)+n_{2}$. As
we know that $v$ is positive, we also know that $v^{\prime}$ cannot be
negative. We then distinguish two cases:

    1. 1.

If $v^{\prime}=0$, then $\max(1,v^{\prime}(n_{1}^{\prime}+1)+1)=1$, and so
$n^{\prime}=n_{1}^{\prime}+1+n_{2}$. Clearly, $n^{\prime}<n-1$; as we know
that $n<g$, we therefore have that $n^{\prime}<g-1$.

    2. 2.

If $v^{\prime}>0$, then
$\max(1,v^{\prime}(n_{1}^{\prime}+1)+1)=v^{\prime}(n_{1}^{\prime}+1)+1$.
Assuming still the worst case $u=v$, we thus have that

$\displaystyle n$
$\displaystyle=v^{\prime}(n_{1}^{\prime}+1)+(n_{1}^{\prime}+1)+1+n_{2}$
$\displaystyle n^{\prime}$
$\displaystyle=v^{\prime}(n_{1}^{\prime}+1)+(n_{1}^{\prime}+1)+n_{2}$

so $n^{\prime}=n-1$. Then, as we know that $n<g$, we therefore also have that
$n^{\prime}<g-1$.

Thus we can conclude the following:

    * –

$\Gamma,\Delta\vdash S::\texttt{for $v^{\prime}$ do $S$}::Q:n^{\prime}$ as
argued above.

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$.

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$.

    * –

$n^{\prime}<g-1$ as argued above.

  * •

Suppose that LABEL:ts2_sss_forfalse was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{for $e$ do
$S$}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{SV},g-1\right>$

with $\text{env}_{SV}\vdash e\rightarrow v$ and $v<1$ as premises. Then
$\Gamma,\Delta\vdash\texttt{for $e$ do $S$}::Q:n$ was concluded by
LABEL:ts2_type_termination_stm, where $n=\max(1,u(n_{1}^{\prime}+1)+1)+n_{2}$,
and with premises

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{for $e$ do
$S$}:\max(1,u(n_{1}^{\prime}+1)+1)$ $\displaystyle\Gamma,\Delta$
$\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_loop. From the
premises of this rule, we get that

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash e:\text{int}^{u}_{\ell}$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash S:n_{1}^{\prime}$

We distinguish three cases:

    1. 1.

$e$ is just a single number $v$ (this would e.g. be the case if the loop had
previously executed at least once). In that case, $\Gamma,\Delta\vdash
v:\text{int}^{v}_{v}$ by rule LABEL:ts2_type_termination_val and, as we know
$v<1$, then $\max(1,v(n_{1}^{\prime}+1)+1)=1$, hence $n=1+n_{2}$; since $n<g$,
we therefore have that $n_{2}<g-1$.

    2. 2.

$e$ is a complex expression (containing operations and/or variables) and
$u\geq 1$ (this is possible even though $v<1$). Then
$\max(1,u(n_{1}^{\prime}+1)+1)=u(n_{1}^{\prime}+1)+1$, hence
$n=u(n_{1}^{\prime}+1)+1+n_{2}$. Clearly, $1<u(n_{1}^{\prime}+1)+1$. As we
know that $n<g$, we therefore have that $n_{2}<g-1$.

    3. 3.

$e$ is a complex expression (as in the second case), but $u<1$. In this case,
$\max(1,u(n_{1}^{\prime}+1)+1)=1$, hence $n=1+n_{2}$ as in the first case.
Thus, as we know that $n<g$, we therefore have that $n_{2}<g-1$.

By case (6) of Definition 5, we have that
$\mathcal{E}^{\Gamma}_{\Delta}(\texttt{for $e$ do $S$}::Q)=\Delta$. Thus we
can conclude the following:

    * –

$\Gamma,\Delta\vdash Q:n_{2}$ by assumption.

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$.

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$.

    * –

$n_{2}<g-1$, as argued above.

  * •

Suppose that LABEL:ts2_sss_decv was used; then (7) is

$\displaystyle\text{env}_{T}$ $\displaystyle\vdash\left<\texttt{B $x$ := $e$
in $S$}::Q,\text{env}_{SV},g\right>$
$\displaystyle\qquad\rightarrow\left<S::\text{del}(x)::Q,\text{env}_{S},((x,v,B),\text{env}_{V}),g-1\right>$

Furthermore, $\Gamma,\Delta\vdash\texttt{var $x$ := $e$ in $S$}::Q:n$ was
concluded by LABEL:ts2_type_termination_stm, where $n=n_{1}+n_{2}$, and with
premises

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{B $x$ := $e$ in
$S$}:n_{1}$ $\displaystyle\Gamma,\Delta$ $\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_decv. From the
premises of this rule, we get that

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash e:B$
$\displaystyle\Gamma,(\Delta,x:B)$ $\displaystyle\vdash S:n_{1}^{\prime}$

and from the conclusion that $n_{1}=n_{1}^{\prime}+2$. Thus
$n=n_{1}^{\prime}+2+n_{2}$.

From Definition 5, we get that

$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}(\texttt{B $x$ := $e$ in $S$}::Q)$
$\displaystyle=\Delta,x:B$ by case (3)
$\displaystyle\mathcal{E}^{\Gamma}_{\Delta,x:B}(\text{del}(x)::Q)$
$\displaystyle=\Delta$ by case (4)

We can then conclude the following:

$\displaystyle\Gamma,(\Delta,x:B)$ $\displaystyle\vdash\text{del}(x)::Q:n_{2}$
by LABEL:ts2_type_termination_del $\displaystyle\Gamma,(\Delta,x:B)$
$\displaystyle\vdash S::\text{del}(x)::Q:n_{1}^{\prime}+n_{2}$ by
LABEL:ts2_type_termination_stm $\displaystyle\Gamma,(\Delta,x:B)$
$\displaystyle\vdash(x,v,B),\text{env}_{V}$ by LABEL:ts2_type_termination_envv

where, in the last case, the premise $\Gamma,(\Delta,x:B)\vdash v:B$ holds by
Lemma 4, and is concluded by LABEL:ts2_type_termination_val (or with a
subtyping rule). In sum, we thus have the following:

    * –

$\Gamma,(\Delta,x:B)\vdash S::\text{del}(x)::Q:n_{1}+n_{2}$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,(\Delta,x:B)\vdash(x,v,B),\text{env}_{V}$ as argued above,

    * –

$n_{1}^{\prime}+n_{2}<g-1$, since we know that $n_{1}^{\prime}+2+n_{2}<g$.

  * •

Suppose that LABEL:ts2_sss_assv was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{$x$ :=
$e$}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{S},\text{env}_{V}\kern-2.0pt\left[x\mapsto
v\right],g-1\right>$

Furthermore, $\Gamma,\Delta\vdash\texttt{$x$ := $e$}::Q:n$ was concluded by
LABEL:ts2_type_termination_stm, where $n=1+n_{2}$, and with premises

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{$x$ := $e$}:1$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_assv. From the
premises of this rule, we get that $\Gamma,\Delta\vdash x:B$ and
$\Gamma,\Delta\vdash e:B$. We know that $\text{env}_{SV}\vdash e\rightarrow
v$. We can then conclude:

$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$x$ := $e$}::Q)=$
$\displaystyle\Delta$ by case (6) of Def. 5 $\displaystyle\Gamma,\Delta\vdash$
$\displaystyle v:B$ by Lemma 4 $\displaystyle\Gamma,\Delta\vdash$
$\displaystyle\text{env}_{V}\kern-2.0pt\left[x\mapsto v\right]$ by Lemma 2

In sum, we thus have the following:

    * –

$\Gamma,\Delta\vdash Q:n_{2}$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\Delta\vdash\text{env}_{V}\kern-2.0pt\left[x\mapsto v\right]$ as
argued above,

    * –

$n_{2}<g-1$, since we know that $1+n_{2}<g$.

  * •

Suppose that LABEL:ts2_sss_assf was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{this.$p$ :=
e}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{P}\kern-2.0pt\left[p\mapsto
v\right]\right],\text{env}_{V},g-1\right>$

Furthermore, $\Gamma,\Delta\vdash\texttt{this.$p$ := e}::Q:n$ was concluded by
LABEL:ts2_type_termination_stm, where $n=1+n_{2}$, and with premises

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{this.$p$ := e}:1$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_assf. From the
premises of this rule, we get that $\Gamma,\Delta\vdash\texttt{this.$p$}:B$
and $\Gamma,\Delta\vdash e:B$.

We know from the premises of LABEL:ts2_sss_assf that $\text{env}_{SV}\vdash
e\rightarrow v$ and $\text{env}_{V}(\texttt{this})=X$ and
$\text{env}_{S}(X)=\text{env}_{P}$. We can then conclude:

$\displaystyle\mathcal{E}^{\Gamma}_{\Delta}(\texttt{this.$p$ := $e$}::Q)=$
$\displaystyle\Delta$ by case (6) of Def. 5 $\displaystyle\Gamma,\Delta\vdash$
$\displaystyle v:B$ by Lemma 4 $\displaystyle\Gamma,\Delta\vdash$
$\displaystyle\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{P}\kern-2.0pt\left[p\mapsto
v\right]\right]$ by Lemma 3

In sum, we thus have the following:

    * –

$\Gamma,\Delta\vdash Q:n_{2}$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{P}\kern-2.0pt\left[p\mapsto
v\right]\right]$ as argued above,

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$,

    * –

$n_{2}<g-1$, since we know that $1+n_{2}<g$.

  * •

Suppose that LABEL:ts2_sss_call was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$}::Q,\text{env}_{SV},g\right>\rightarrow\left<S::\text{env}_{V}::Q,\text{env}_{SV}^{\prime},g-1\right>$

Furthermore,
$\Gamma,\Delta\vdash\texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$}::Q:n$ was
concluded by LABEL:ts2_type_termination_stm, where $n=n_{1}+2+n_{2}$, and with
premises

$\displaystyle\Gamma,\Delta$
$\displaystyle\vdash\texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$}:n_{1}+2$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_call. From the
premises of this rule, we get that

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash e_{1}:I$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\widetilde{e}:\widetilde{B}$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash e_{2}:\text{int}^{u}_{\ell}$

and $\Gamma(I)(f)=\text{proc}(\widetilde{B})^{u}_{\ell}:n_{1}$.

We know from the premise of LABEL:ts2_sss_call that $\text{env}_{SV}\vdash
e_{1}\rightarrow X$, and by Lemma 4 we get that $\Gamma,\Delta\vdash X:I$.

We also know by assumption that $\Gamma\vdash\text{env}_{T}$, which was
concluded by LABEL:ts2_type_termination_envt. From its premises and side
condition, we get that $\Gamma,\texttt{this}:I\vdash\text{env}_{M}$, where
$\text{env}_{T}(X)=\text{env}_{M}$ by the premise of LABEL:ts2_sss_call. This,
in turn, was concluded by LABEL:ts2_type_termination_envm; from the premise of
this rule, we get that

$\Gamma,(\texttt{this}:I,\widetilde{x}:\widetilde{B},\texttt{value}:\text{int}^{u}_{\ell},\texttt{sender}:I^{\top})\vdash
S:n_{1}$

and, from the premise of LABEL:ts2_sss_call, that
$\text{env}_{M}(f)=(f,(\widetilde{x},S))$.

Finally, by case (5) of Definition 5, we have that

$\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$e_{1}$.$f$($\widetilde{e}$):$e_{2}$}::Q)=\texttt{this}:I,\texttt{sender}:I^{\top},\texttt{value}:\text{int}^{u}_{\ell},\widetilde{x}:\widetilde{B}$

which gives us the contents of the new type environment after the transition.
We can now conclude

$\displaystyle\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$e_{1}$.$f$($\widetilde{e}$):$e_{2}$}::Q)$
$\displaystyle\vdash\text{env}_{V}::Q:n_{2}$ by LABEL:ts2_type_termination_ctx
$\displaystyle\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$e_{1}$.$f$($\widetilde{e}$):$e_{2}$}::Q)$
$\displaystyle\vdash S::\text{env}_{V}::Q:n_{1}+n_{2}$ by
LABEL:ts2_type_termination_stm

In sum, we thus have the following:

    * –

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$e_{1}$.$f$($\widetilde{e}$):$e_{2}$}::Q)\vdash
S::\text{env}_{V}::Q:n_{1}+n_{2}$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\texttt{$e_{1}$.$f$($\widetilde{e}$):$e_{2}$}::Q)\vdash\text{env}_{V}^{\prime}$
by simple inspection of the new $\text{env}_{V}^{\prime}$, which contains only
the bindings for the formal parameters of $f$,

    * –

$n_{1}+n_{2}<g-1$, since we know that $n_{1}+2+n_{2}<g$.

  * •

Suppose that LABEL:ts2_sss_throw was used; then (7) is

$\text{env}_{T}\vdash\left<\texttt{throw}::Q,\text{env}_{SV},g\right>\rightarrow\left<\text{exc}(\texttt{pge})::Q,\text{env}_{SV},g\right>$

and no further transition from the resulting configuration is then possible.
We know that $\Gamma,\Delta\vdash\texttt{throw}::Q:n$ was concluded by
LABEL:ts2_type_termination_stm, where $n=1+n_{2}$, and with premises

$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash\texttt{throw}:1$
$\displaystyle\Gamma,\Delta$ $\displaystyle\vdash Q:n_{2}$

of which the first was concluded by LABEL:ts2_type_termination_throw. By case
(6) of Definition 5, we have that
$\mathcal{E}^{\Gamma}_{\Delta}(\texttt{throw}::Q)=\Delta$. Thus we can
conclude the following:

    * –

$\Gamma,\Delta\vdash\text{exc}(\texttt{pge})::Q:0$ by rule
LABEL:ts2_type_termination_exc,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$,

    * –

$0<g$, by the side condition of LABEL:ts2_sss_throw.

  * •

Suppose that LABEL:ts2_sss_delv was used; then (7) is

$\text{env}_{T}\vdash\left<\text{del}(x)::Q,\text{env}_{S},(x,v,B):\text{env}_{V},g\right>\rightarrow\left<Q,\text{env}_{SV},g\right>$

Furthermore, $\Gamma,\Delta,x:B\vdash\text{del}(x)::Q:n$ was concluded by
LABEL:ts2_type_termination_del. From its premise, we have that

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta,x:B}(\text{del}(x)::Q)\vdash Q:n$

and by case (4) of Definition 5, we have that

$\mathcal{E}^{\Gamma}_{\Delta,x:B}(\text{del}(x)::Q)=\Delta$

so we know that $\Gamma,\Delta\vdash Q:n$. Finally, by Lemma 1 and
$\Gamma,(\Delta,x:B)\vdash(x,v,B):\text{env}_{V}$, we obtain that
$\Gamma,\Delta\vdash\text{env}_{V}$. Thus we can conclude the following:

    * –

$\Gamma,\Delta\vdash Q:n$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ as argued above,

    * –

$n<g$ by assumption, from the side condition of
LABEL:ts2_type_termination_cfg, which was used to type the initial
configuration.

  * •

Suppose that LABEL:ts2_sss_return was used; then (7) is

$\text{env}_{T}\vdash\left<\text{env}_{V}^{\prime}::Q,\text{env}_{SV},g\right>\rightarrow\left<Q,\text{env}_{S},\text{env}_{V}^{\prime},g\right>$

and $\Gamma,\Delta\vdash\text{env}_{V}^{\prime}::Q:n$ was concluded by
LABEL:ts2_type_termination_ctx. From its premise, we have that

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}^{\prime}::Q)\vdash Q:n$

and, by cases (1) and (2) of Definition 5, we have that
$\mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}^{\prime}::Q)$ yields a type
environment for local variables which is formed by the variable names and the
associated type information stored in $\text{env}_{V}^{\prime}$. Clearly,
$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}^{\prime}::Q)\vdash\text{env}_{V}^{\prime}$
for any $Q$. Thus we can conclude the following:

    * –

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}^{\prime}::Q)\vdash Q:n$
as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\mathcal{E}^{\Gamma}_{\Delta}(\text{env}_{V}^{\prime}::Q)\vdash\text{env}_{V}^{\prime}$
as argued above,

    * –

$n<g$ by assumption, from the side condition of
LABEL:ts2_type_termination_cfg, which was used to type the initial
configuration.

In all of the above cases, we have shown that we can satisfy the premises of
LABEL:ts2_type_termination_cfg after the transition step, whenever the step is
concluded by any of the ordinary transition rules for statements. What remains
now is to consider the exception rules:

  * •

Suppose the transition was concluded by LABEL:ts2_sss_oog. Then (7) is

$\text{env}_{T}\vdash\left<S::Q,\text{env}_{SV},0\right>\rightarrow\left<\text{exc}(\texttt{oog})::S::Q,\text{env}_{SV},0\right>$

This case holds vacuously, since $g=0$, but from the side condition of
LABEL:ts2_type_termination_cfg we know that $n<g$, which would imply that $n$
is negative, which is impossible. Thus $\left<S::Q,\text{env}_{SV},0\right>$
cannot be well-typed for any $\Gamma,\Delta$.

  * •

Suppose any other exception rule was used. Then (7) is

$\text{env}_{T}\vdash\left<S::Q,\text{env}_{SV},g\right>\rightarrow\left<\text{exc}(l)::S::Q,\text{env}_{SV},g\right>$

where $l$ is one of the two labels rte or neg. In either case, we have that

$\Gamma,\Delta\vdash\text{exc}(l)::S::Q:0$

for any $\Gamma,\Delta$ by rule LABEL:ts2_type_termination_exc. Thus we can
conclude the following:

    * –

$\Gamma,\Delta\vdash\text{exc}(l)::S::Q:0$ as argued above,

    * –

$\Gamma\vdash\text{env}_{S}$ by assumption, since the transition does not
alter $\text{env}_{S}$,

    * –

$\Gamma,\Delta\vdash\text{env}_{V}$ by assumption, since the transition does
not alter $\text{env}_{V}$,

    * –

$0<g$, since we know that $g$ is positive.

This concludes the proof.