# SolType: Refinement Types for Solidity

Bryan Tan  University of California, Santa BarbaraUSA<EMAIL_ADDRESS>,
Benjamin Mariano  University of Texas at AustinUSA<EMAIL_ADDRESS>,
Shuvendu Lahiri  Microsoft ResearchUSA<EMAIL_ADDRESS>,  Işıl
Dillig  University of Texas at AustinUSA<EMAIL_ADDRESS>and  Yu Feng
University of California, Santa BarbaraUSA<EMAIL_ADDRESS>
(2021)

###### Abstract.

As smart contracts gain adoption in financial transactions, it becomes
increasingly important to ensure that they are free of bugs and security
vulnerabilities. Of particular relevance in this context are arithmetic
overflow bugs, as integers are often used to represent financial assets like
account balances. Motivated by this observation, this paper presents SolType,
a refinement type system for Solidity that can be used to prevent arithmetic
over- and under-flows in smart contracts. SolType allows developers to add
refinement type annotations and uses them to prove that arithmetic operations
do not lead to over- and under-flows. SolType incorporates a rich vocabulary
of refinement terms that allow expressing relationships between integer values
and aggregate properties of complex data structures. Furthermore, our
implementation, called Solid, incorporates a type inference engine and can
automatically infer useful type annotations, including non-trivial contract
invariants.

To evaluate the usefulness of our type system, we use Solid to prove
arithmetic safety of a total of 120 smart contracts. When used in its fully
automated mode (i.e., using Solid’s type inference capabilities), Solid is
able to eliminate 86.3% of redundant runtime checks used to guard against
overflows. We also compare Solid against a state-of-the-art arithmetic safety
verifier called VeriSmart and show that Solid has a significantly lower false
positive rate, while being significantly faster in terms of verification time.

††copyright: none††journalyear: 2022††doi: 10.1145/1122445.1122456††journal:
PACMPL††journalvolume: POPL††journalnumber: 1††article: 1††publicationmonth: 1

##  1\. Introduction

Smart contracts are programs that run on top of the blockchain and perform
financial transactions in a distributed environment without intervention from
trusted third parties. In recent years, smart contracts have seen widespread
adoption, with over 45 million (eth, 2018) instances covering financial
products, online gaming, real estate (cas, 2018a), shipping, and logistics
(cas, 2018b).

Because smart contracts deployed on a blockchain are freely accessible through
their public methods, any functional bugs or vulnerabilities inside the
contracts can lead to disastrous losses, as demonstrated by recent attacks
(att, 2017b, a, 2016; Atzei et al., 2017). Therefore, unsafe smart contracts
are increasingly becoming a serious threat to the success of the blockchain
technology. For example, recent infamous attacks on the Ethereum blockchain
such as the DAO (att, 2017b) and the Parity Wallet (att, 2017a) attacks were
caused by unsafe smart contracts. To make things worse, smart contracts are
immutable once deployed, so bugs cannot be easily fixed.

One common type of security vulnerability involving smart contracts is
arithmetic overflows. In fact, according to a recent study, such bugs account
for over 96% of CVEs assigned to Ethereum smart contracts (So et al., 2020).
Furthermore, because smart contracts often use integers to represent financial
assets, arithmetic bugs, if exploited, can cause significant financial damage
(att, 2016). For this reason, smart contracts rarely _directly_ perform
arithmetic operations (e.g., addition) but instead perform arithmetic
indirectly by calling a library called SafeMath. Since this library inserts
run-time checks for over- and under-flows, this approach is effective at
preventing exploitable vulnerabilities but comes with run-time overhead.
Furthermore, because computation on the blockchain costs money (measured in a
unit called _gas_), using the SafeMath library can significantly increase the
cost of running these smart contracts.

Motivated by this observation, we are interested in _static_ techniques that
can be used to prevent integer overflows. Specifically, we propose a
refinement type system for Solidity, called SolType, that can be used to prove
that arithmetic operations do not over- or under-flow. Arithmetic operations
that are proven type-safe by SolType are guaranteed to not overflow; thus,
SolType can be used to eliminate unnecessary runtime checks.

While SolType is inspired by prior work on logically qualified types (Rondon
et al., 2008, 2010; Vekris et al., 2016), it needs to address a key challenge
that arises in Solidity programs. Because smart contracts often use non-
trivial data structures (e.g., nested mappings or mappings of structs) to
store information about accounts, it is important to reason about the
relationship between integer values and aggregate properties of such data
structures. Based on this observation, SolType allows relational-algebra-like
refinements that can be used to perform projections and aggregations over
mappings. While this design choice makes Solid expressive enough to discharge
many potential overflows, it nonetheless enjoys decidable type checking.
Furthermore, our implementation, called Solid, incorporates a type inference
engine based on Constrained Horn Clause (CHC) solvers (Bjørner et al., 2015)
and can therefore automatically infer useful type annotations, including non-
trivial contract invariants.

We evaluate Solid on 120 smart contracts and compare it against Verismart (So
et al., 2020), a state-of-the-art verifier for checking arithmetic safety in
smart contracts. Our evaluation shows that (1) Solid can discharge 86.3% of
unnecessary runtime overflow checks, and (2) Solid is both faster and has a
lower false positive rate compared to Verismart. We also perform ablation
studies to justify our key design choices and empirically validate that they
are important for achieving good results.

In summary, this paper makes the following contributions:

  * •

We present a new refinement type system called SolType for proving arithmetic
safety properties of smart contracts written in Solidity. Notably, our type
system allows expressing relationships between integers and aggregate
properties of complex data structures.

  * •

We implement the proposed type system in a tool called Solid, which also
incorporates a type inference procedure based on Constrained Horn Clause
solvers.

  * •

We evaluate Solid on 120 real-world smart contracts and show that it is useful
for eliminating many run-time checks for arithmetic safety. We also compare
Solid against Verismart and demonstrate its advantages in terms of false
positive rate and running time.

##  2\. Overview

In the section, we go through the high-level idea of our refinement type
system using a representative example.

###  2.1. Verifying Overflow Safety: A Simple Example

Figure 1 shows a snippet from a typical implementation of an ERC20 token.
Here, the mint function allows an authorized ”owner” address to generate
tokens, and the transfer function allows users of the contract to transfer
tokens between each other. User token balances are tracked in the mapping
bals, with the total number of issued tokens stored in tot. It is crucial that
the arithmetic does not overflow in either function; otherwise it would be
possible for a malicious agent to arbitrarily create or destroy tokens.

This contract does not contain any arithmetic overflows because it maintains
the invariant that the summation over the entries in bals is at most tot. This
invariant, together with the require clauses in mint and transfer, ensures
that there are no overflows. Such _contract invariants_ can be expressed as
refinement type annotations in Solid. In particular, as shown in line 4, bals
has the refinement type $\\{\nu\ |\ \mathrm{sum}(\nu)\leq\mathrm{tot}\\}$,
which is sufficient to prove the absence of overflows in this program. In the
remainder of this section, we illustrate some of the features of Solid using
this example and its variants.

⬇

1contract ExampleToken is IERC20 {

2 address owner;

3 uint tot;

4 mapping(address => uint) /* { sum(v) <= tot } */ bals;

5 constructor(address _owner) public {

6 owner = _owner;

7 }

8

9 function mint(uint amt) public {

10 require(msg.sender == owner);

11 require(tot + amt >= tot);

12 tot = tot + amt;

13 bals[msg.sender] = bals[msg.sender] + amt;

14 }

15

16 function transfer(address recipient, uint amt) public {

17 require(bals[msg.sender] >= amt);

18 bals[msg.sender] = bals[msg.sender] - amt;

19 bals[recipient] = bals[recipient] + amt;

20 }

21

22 /* ... other functions ... */

23}

Figure 1. Excerpt from a typical ERC20 token.

###  2.2. Intermediate Representation

Due to imperative features like loops and mutation, Solidity is not directly
amenable to refinement type checking. Thus, similar to prior work (Rondon et
al., 2010; Vekris et al., 2016), we first translate the contract to a
intermediate representation (IR) in SSA form that we call MiniSol. Our IR has
the following salient features:

  * •

Integer variables are assigned exactly once (i.e., SSA form)

  * •

Mappings, structs, and arrays are converted into immutable data structures,

  * •

A fetch statement is used to load the values of the storage variables at
function entry, and a commit statement is used to store the values of the
storage variables at function exit.

The resulting IR of the example contract is shown in Fig 2, which we will use
for the examples in this section. Our tool automatically converts Solidity
programs to this IR in a pre-processing step and automatically inserts _fetch_
/_commit_ statements at the necessary places. Similar to the _fold_ /_unfold_
operations from prior work (Rondon et al., 2010), the use of these _fetch_
/_commit_ statements in the MiniSol IR allows temporary invariant violations.

⬇

1contract ExampleToken {

2 owner : addr;

3 bals : map(addr => uint) /* { sum(v) <= tot } */;

4 tot : uint;

5

6 constructor(_owner : addr) public {

7 let owner0 : addr = _owner;

8 let bals0 : map(addr => uint) = zero_map[addr, uint];

9 let tot0 : uint = 0;

10 commit owner0, bals0, tot0;

11 }

12

13 fun mint(amt : uint) {

14 fetch owner1, bals1, tot1;

15 require(msg.sender == owner1);

16 require(tot1 + amt >= tot1);

17 let tot2 : uint = tot1 + amt;

18 let bals2 : map(addr => uint) =

19 bals1[msg.sender $\triangleleft$ bals1[msg.sender] + amt];

20 commit owner1, bals2, tot2;

21 }

22

23 fun transfer(recipient : address, amt : uint) {

24 fetch owner3, bals3, tot3;

25 require(bals3[msg.sender] >= amt);

26 let bals4 : map(addr => uint) =

27 bals3[msg.sender $\triangleleft$ bals3[msg.sender] - amt];

28 let bals5 : map(addr => uint) =

29 bals4[recipient $\triangleleft$ bals4[recipient] + amt];

30 commit owner3, bals5, tot3;

31 }

32}

Figure 2. Purely functional IR of the example token (with some irrelevant
details omitted)

###  2.3. Discharging Overflow Safety on Local Variables

We now demonstrate how our refinement type system can be used to verify
arithmetic safety in this example. Consider the mint function in Fig 2. The
require statement on line 16 is a runtime overflow check for tot1 + amt. If
the runtime check fails, then the contract will abort the current
transactions, meaning that it discards any changes to state variables. Since
Solid keeps track of this run-time check as a guard predicate, it is able to
prove the safety of the addition on line 17.

Next, we explain how Solid proves the safety of the addition on line 19. For
now, let us assume that the refinement type annotation for bals is indeed
valid, i.e., bals1 has the following refinement type (we omit base type
annotations for easier readability):

(1) $bals1:\\{\nu\ |\ \operatorname{\mathsf{Sum}}(\nu)\leq tot1\\}$

Since bals1 contains only unsigned integers, we refine bals1[msg.sender] with
the type:

$bals1[msg.sender]:\\{\nu\ |\ \nu\leq\operatorname{\mathsf{Sum}}(bals1)\\}$

From transitivity of $\leq$, this implies that $bals1[msg.sender]\leq tot1$.
Finally, using the guard predicate $tot1+amt\geq tot1$, Solid is able to
prove:

$bals1[msg.sender]+amt\leq\mathsf{MaxInt}$

which implies that the addition does not overflow. In a similar manner, Solid
can also prove the safety of the operations in transfer using the refinement
type of state variable bals and the require statement at line 25.

###  2.4. Type checking the contract invariant

In the previous subsection, we showed that contract invariants (expressed as
refinement type annotations on state variables) are useful for discharging
overflows. However, Solid needs to establish that these type annotations are
valid, meaning that contract invariants are preserved at the end of functions.
For instance, at the end of the mint function, the type checker needs to
establish that bals2 has the following refinement type:

(2) $bals2:\\{\nu\ |\ \operatorname{\mathsf{Sum}}(\nu)\leq tot2\\}$

To establish this, we proceed as follows: First, from line 19, Solid infers
the type of bals2 to be:

(3) $\begin{split}bals2:\\{\nu\
|\operatorname{\mathsf{Sum}}(\nu)=\operatorname{\mathsf{Sum}}(bals1)+amt)\\}\end{split}$

Then, since tot2 has the refinement type $\\{v\ |\ tot1+amt\\}$ and bals1 has
the refinement type $\\{v\ |\ \operatorname{\mathsf{Sum}}(\nu)\leq tot1\\}$,
we can show that $\operatorname{\mathsf{Sum}}(bals2)\leq tot2$. This
establishes the desired contract invariant (i.e., Eq.2). Using similar
reasoning, Solid can also type check that the contract invariant is preserved
in transfer.

###  2.5. Contract invariant inference

Although the type annotation is given explicitly in this example, Solid can
actually prove the absence of overflows without any annotations by performing
type inference. To do so, Solid first introduces a ternary uninterpreted
predicate $I$ (i.e., unknown contract invariant) for each state variable
(owner, bals, tot) that relates its value $\nu$ to the other two state
variables. This corresponds to the following type ”annotations” for the state
variables:

$\displaystyle owner$ $\displaystyle:\\{\nu\ |\ I_{1}(\nu,tot,bals)\\}$
$\displaystyle tot$ $\displaystyle:\\{\nu\ |\ I_{2}(owner,\nu,bals)\\}$
$\displaystyle bals$ $\displaystyle:\\{\nu\ |\ I_{3}(owner,tot,\nu)\\}$

Given these type annotations over the unknown predicates $I_{1}$-$I_{3}$,
Solid generates constraints on $I_{1}$-$I_{3}$ during type inference and
leverages a CHC solver to find an instantiation of each $I_{i}$. However, one
complication is that we cannot feed all of these constraints to a CHC solver
because the generated constraints may be unsatisfiable. In particular,
consider the scenario where the program contains a hundred arithmetic
operations, only one of which is unsafe. If we feed all constraints generated
during type checking to the CHC solver, it will correctly determine that there
is no instantiation of the invariants that will allow us to prove the safety
of _all_ arithmetic operations. However, we would still like to infer a type
annotation that will allow us to discharge the remaining 99 arithmetic
operations.

To deal with this difficulty, Solid tries to solve the CHC variant of the
well-known MaxSAT problem. That is, in the case where the generated Horn
clauses are unsatisfiable, we would like to find an instantiation of the
unknown predicates so that the maximum number of constraints are satisfied.
Solid solves this ”MaxCHC”-like problem by generating one overflow checking
constraint at a time and iteratively strengthening the inferred contract
invariant. For instance, for our running example, Solid can automatically
infer the desired contract invariant $I_{3}$, namely sum(bals) <= tot ($I_{1}$
and $I_{2}$ are simply $\operatorname{\mathsf{true}}$).

###  2.6. Refinements for Aggregations Over Nested Data Structures

A unique aspect of our type system is its ability to express more complex
relationships between integer values and data structures like nested mappings
over structs. To illustrate this aspect of the type system, consider Fig 3,
which is a modified version of Fig 1 that stores balance values inside a User
struct in a nested mapping. The addition on line 14 cannot overflow because
the contract maintains the invariant that the summation over the bal fields of
all the nested User entries in usrs is at most tot. Solid is able to infer
that the type of $usrs$ is

$\\{\nu\mid\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(\nu)))\leq
tot\\}$

In particular, this refinement type captures the contract invariant that the
sum of all user balances nested inside the struct of usrs is bounded by tot.
Using such a refinement type, we can prove the safety of the addition on line
14. Note that the use of operators like $\mathsf{Flatten}$ and
$\mathsf{Fld}_{\emph{bal}}$ is vital for successfully discharging the
potential overflow in this example.

⬇

1contract ExampleTokenWithStruct {

2 struct User {

3 uint bal;

4 /* ... other fields ... */

5 }

6

7 /* ... other state variables ... */

8 mapping(address => mapping(uint => User)) usrs;

9

10 function mint(uint amt, uint accno) public {

11 require(msg.sender == owner);

12 require(tot + amt >= tot);

13 tot += amt;

14 usrs[msg.sender][accno].bal += amt;

15 }

16

17 /* ... other functions ... */

18}

Figure 3. The Solidity source code of the running example (Fig. 1) modified to
use nested data structures.

##  3\. Language

$\begin{array}[]{r c l l}C&::=&\mathop{\mathsf{contract}}C\ \\{\textit{ctor}\
\overrightarrow{\textit{decl}}\ \\}&\textbf{Contract}\\\
\mathit{ctor}&::=&\mathsf{ctor}(\overrightarrow{x:\
\tau})=s&\textbf{Constructor}\\\ \mathit{decl}&::=&&\textbf{Body
declaration:}\\\ &&\mathop{\mathbf{fun}}f(\overrightarrow{x_{i}:\
\tau_{i}}):\tau_{r}=s;e&\text{function}\\\
&&\mathop{\mathbf{struct}}S\\{\overrightarrow{x_{i}:\
T_{i}}\\}&\text{struct}\\\ \\\ s&::=&&\textbf{Statement:}\\\
&&\mathop{\mathsf{let}}x:\tau=e&\text{(immutable) assignment}\\\
&\mid&s_{1};s_{2}&\text{sequence}\\\
&\mid&\mathop{\mathsf{skip}}&\text{skip}\\\
&\mid&\mathop{\mathsf{assert}}e&\text{assertion}\\\
&\mid&\mathop{\mathsf{assume}}e&\text{assumption}\\\
&\mid&\mathop{\mathsf{if}}e_{1}\mathop{\mathsf{then}}s_{1}\mathop{\mathsf{else}}s_{2}\mathop{\mathsf{join}}j&\text{if-
then-else}\\\
&\mid&\mathop{\mathsf{while}}j;e\mathop{\mathsf{do}}s&\text{while loop}\\\
&\mid&\mathop{\mathsf{fetch}}x_{1}^{\prime}\mathop{\mathsf{as}}x_{1},\dots,x_{n}^{\prime}\mathop{\mathsf{as}}x_{n}&\text{fetch
state variables}\\\
&\mid&\mathop{\mathsf{commit}}e_{1}\mathop{\mathsf{to}}x_{1},\dots,e_{n}\mathop{\mathsf{to}}x_{n}&\text{commit
state variables}\\\
&\mid&\mathop{\mathsf{call}}x:\tau=f(e_{1},\dots,e_{n})&\text{function
call}\\\ \\\
j&::=&\overrightarrow{x_{i}:\tau_{i}=\Phi(x_{i1},x_{i2})}&\textbf{Join
point}\\\ \\\ e&::=&&\textbf{Expression:}\\\
&&n\mid\operatorname{\mathsf{true}}\mid\operatorname{\mathsf{false}}\mid()&\text{constants}\\\
&\mid&x&\text{variable}\\\ &\mid&e_{1}\operatorname{\oplus}e_{2}\mid\lnot
e&\text{binary/unary operation}\\\
&\mid&\mathsf{mapping}(\overrightarrow{n_{i}\mapsto e_{i}})&\text{mapping with
uint keys}\\\ &\mid&\mathop{\mathsf{struct}}S(\overrightarrow{x_{i}\mapsto
e_{i}})&\text{struct}\\\ &\mid&e_{1}[e_{2}]&\text{data structure index}\\\
&\mid&e_{1}\left[e_{2}\mathop{\triangleleft}e_{3}\right]&\text{data structure
update}\\\ \\\
\oplus&\in&\\{+,-,\ast,/,=,\neq,\geq,\leq,>,<,\land,\lor\\}&\textbf{Binary
operators}\\\ \\\ T&::=&&\textbf{Base type:}\\\
&&\operatorname{\mathsf{UInt}}&\text{unsigned integer}\\\
&\mid&\operatorname{\mathsf{Bool}}&\text{boolean}\\\
&\mid&\mathsf{Map}(T)&\text{mapping with unsigned int keys}\\\
&\mid&\operatorname{\mathsf{Unit}}&\text{unit}\\\
&\mid&\mathop{\mathsf{Struct}}S&\text{struct}\\\ \\\
\tau&::=&\\{\nu:T\mid\phi\\}&\textbf{Refinement type}\\\
\phi&::=&t\operatorname{\oplus}t\mid\phi\land\phi\mid\phi\lor\phi\mid\lnot\phi&\textbf{Logical
qualifiers}\\\ t&::=&&\textbf{Refinement terms:}\\\ &&e&\text{expressions}\\\
&\mid&\operatorname{\mathsf{Sum}}(t)&\text{aggregate properties}\\\
&\mid&\operatorname{\mathsf{Fld}}_{x}(t)\mid\operatorname{\mathsf{Flatten}}(t)&\text{aggregate
operators}\\\ &\mid&\mathsf{MaxInt}&\text{largest actual integer}\end{array}$
Figure 4. Syntax of MiniSol

In this section, we present the syntax of MiniSol (Figure 4), an intermediate
representation for modeling Solidity smart contracts. In what follows, we give
a brief overview of the important features of MiniSol relevant to the rest of
the paper.

###  3.1. MiniSol Syntax

In MiniSol, a program is a contract $C$ that contains fields (referred to as
_state variables_), struct definitions $S$, and function declarations $f$.
State variables are declared and initialized in a constructor $ctor$.
Functions include a type signature, which provides a type $\tau_{i}$ for each
argument $x_{i}$ as well as return type $\tau_{r}$, and a method body, which
is a sequence of statements, followed by an expression.

Statements in MiniSol include let bindings, conditionals, function calls (with
pass-by-value semantics), assertions, and assumptions. As MiniSol programs are
assumed to be in SSA form, we include a _join point_ $j$ for if statements and
while loops. In particular, a join point consists of a list of $\Phi$-node
variable declarations, where each $x_{i}$ is declared to be of type $\tau_{i}$
and may take on the value of either $x_{i1}$ or $x_{i2}$, depending on which
branch is taken. In line with this SSA assumption, we also assume variables
are not redeclared.

As mentioned previously, another feature of MiniSol is that it contains fetch
and commit statements for reading the values of all state variables from the
blockchain and writing them to the blockchain respectively. Specifically, the
construct

$\mathop{\mathsf{fetch}}x_{1}^{\prime}\mathop{\mathsf{as}}x_{1},\dots,x_{n}^{\prime}\mathop{\mathsf{as}}x_{n}$

_simultaneously_ retrieves the values of state variables
$x_{1}^{\prime},\ldots,x_{n}^{\prime}$ and writes them into local variables
$x_{1},\ldots,x_{n}$. Similarly, the commit statement

$\mathop{\mathsf{commit}}e_{1}\mathop{\mathsf{to}}x_{1},\dots,e_{n}\mathop{\mathsf{to}}x_{n}$

simultaneously stores the result of evaluating expressions
$e_{1},\ldots,e_{n}$ into state variables $x_{1},\ldots,x_{n}$. Note that
Solidity does not contain such fetch and commit constructs; however, we
include them in MiniSol to allow temporary violations of contract invariants
inside procedures. Such mechanisms have also been used in prior work (Rondon
et al., 2010; Smith et al., 2000) for similar reasons.

Expressions in MiniSol consist of variables, unsigned integer and boolean
constants, binary operations, and data structure operations. Data structures
include maps and structs, and we use the same notation for accessing/updating
structs and maps. In particular, $e_{1}[e_{2}]$ yields the value stored at key
(resp. field) $e_{1}$ of map (resp. struct) $e_{2}$. Similarly,
$e_{1}[e_{2}\triangleleft e_{3}]$ denotes the new map (resp. struct) obtained
by writing value $e_{3}$ at key (resp. field) $e_{2}$ of $e_{1}$. We may
prefix the key with a dot when accessing a struct field (e.g. $e_{1}[.x]$) to
emphasize that the accessed data structure is a struct.

###  3.2. Types

Similar to previous refinement type works, MiniSol provides both _base type_
annotations as well as _refinement type_ annotations (bottom of Figure 4).
Base types correspond to standard Solidity types, such as unsigned integers
(256-bit), booleans, mappings, and structs. We shorten “mappings” to
$\mathsf{Map}$ and assume that all keys are $\operatorname{\mathsf{UInt}}$s,
as most key types in Solidity mappings are coercible to
$\operatorname{\mathsf{UInt}}$. Thus, $\mathsf{Map}(T)$ is a mapping from
unsigned integers to $T$s.

A refinement type $\\{\nu:T\mid\phi\\}$ refines the base type $T$ with a
logical qualifier $\phi$. In this paper, logical qualifiers belong to the
quantifier-free combined theory of rationals, equality with uninterpreted
functions, and arrays. Note that determining validity in this theory is
decidable, and we intentionally use the theory of rationals rather than
integers to keep type checking decidable in the presence of non-linear
multiplication. In more detail, logical qualifiers are boolean combinations of
binary relations $\oplus$ over refinement terms $t$, which include both
MiniSol expressions as well as terms containing the special constructs
$\operatorname{\mathsf{Sum}}$, $\operatorname{\mathsf{Fld}}$, and
$\operatorname{\mathsf{Flatten}}$ (represented as uninterpreted functions)
that operate over terms of type $\mathsf{Map}$. In particular,

  * •

$\operatorname{\mathsf{Sum}}(t)$ represents the sum of all values in $t$.

  * •

Given a mapping $t$ containing structs, $\operatorname{\mathsf{Fld}}_{x}(t)$
returns a mapping that only contains field $x$ of the struct. Thus,
$\operatorname{\mathsf{Fld}}$ is similar to the projection operator from
relational algebra.

  * •

Given a nested mapping $t$, $\operatorname{\mathsf{Flatten}}(t)$ flattens the
map. In particular, given a nested mapping $\mathsf{Map}(\mathsf{Map}(t))$,
$\operatorname{\mathsf{Flatten}}$ produces a mapping $\mathsf{Map}(t)$ where
each value of the mapping corresponds to a value of one of the nested mappings
from $\mathsf{Map}(\mathsf{Map}(t))$.

In addition to these constructs, refinement terms in MiniSol also include a
constant called $\mathsf{MaxInt}$, which indicates the largest integer value
representable in $\operatorname{\mathsf{UInt}}$.

###### Example 0.

Consider the usrs mapping in Fig. 3. The predicate

$\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(usrs)))\leq\mathsf{MaxInt}$

expresses that if we take the usrs mapping (which is of type
$\mathsf{Map}(\mathsf{Map}(\emph{User}))$) and (a) flatten the nested mapping
so that it becomes a non-nested mapping of User; (b) project out the bal field
of each struct to obtain a $\mathsf{Map}(\operatorname{\mathsf{UInt}})$; and
(c) take the sum of values in this final integer mapping, then the result
should be at most $\mathsf{MaxInt}$.

##  4\. Type system

In this section, we introduce the SolType refinement type system for the
MiniSol language.

###  4.1. Preliminaries

We start by discussing the environments and judgments used in our type system;
these are summarized in Figure 5.

$\begin{array}[]{rclr}\Gamma&::=&\epsilon\mid x:\tau,\Gamma&\text{(Local
variable bindings)}\\\ L&::=&\mathsf{Unlocked}\mid\mathsf{Locked}&\text{(Lock
status)}\\\ \gamma&::=&\epsilon\mid L,\gamma\mid t,\gamma&\text{(Guard
predicates)}\\\
\Delta&::=&\epsilon\mid\Delta[f\mapsto(\overrightarrow{x_{i}:\tau_{i}},\tau_{r})]\mid&\text{(Global
declarations)}\\\
&&\Delta[S\mapsto\overrightarrow{x_{i}:T_{i}}]\mid\Delta[x\mapsto\tau]&\\\ \\\
\lx@intercol\Gamma;\gamma\vdash e:\tau\hfil\lx@intercol&\text{(Expression
typing judgment)}\\\ \lx@intercol\Gamma;\gamma\vdash
s\dashv\Gamma^{\prime};\gamma^{\prime}\hfil\lx@intercol&\text{(Statement
typing judgment)}\\\
\lx@intercol\Gamma;\gamma;(\Gamma_{1};\gamma_{1});(\Gamma_{2};\gamma_{2})\vdash
j\dashv\Gamma^{\prime};L\hfil\lx@intercol&\text{(Join point typing
judgment)}\end{array}$
Figure 5. Environments and judgments used in our typing rules

##### Environments

Our type system employs a local environment $\Gamma$ and a set of _guard_
predicates $\gamma$. A local environment $\Gamma$ is a sequence of type
bindings (i.e., $x:\tau$), and we use the notation
$\operatorname{\mathsf{dom}}(\Gamma)$ to denote the set of variables bound in
$\Gamma$. The guard predicates $\gamma$ consist of (1) a set of path
conditions under which an expression is evaluated and (2) a _lock status_ $L$
($\mathsf{Locked}$ or $\mathsf{Unlocked}$) that tracks whether the state
variables are currently being modified.

In addition to $\Gamma$ and $\gamma$, our typing rules need access to struct
and function definitions. For this purpose, we make use of another environment
$\Delta$ that stores function signatures, struct definitions, and types of the
state variables. To avoid cluttering notation, we assume that $\Delta$ is
implicitly available in the expression and statement typing judgments, as
$\Delta$ does not change in a function body. We use the notation $\Delta(S)$
to indicate looking up the fields of struct $S$, and we write $\Delta(S,x)$ to
retrieve the type of field $x$ of struct $S$. Similarly, the notation
$\Delta(f)$ yields the function signature of $f$, which consists of a sequence
of argument type bindings as well as the return type. Finally, given a state
variable $x$, $\Delta(x)$ returns the type of $x$.

##### Typing Judgments

As shown in Figure 5, there are three different typing judgments in MiniSol:

  * •

_Expression typing judgments_ : We use the judgment $\Gamma;\gamma\vdash
e:\tau$ to type check a MiniSol expression $e$. In particular, this judgment
indicates that expression $e$ has refinement type $\tau$ under local
environment $\Gamma$, guard $\gamma$, and (implicit) global environment
$\Delta$.

  * •

_Statement typing judgments_ : Next, we use a judgment of the form
$\Gamma;\gamma\vdash s\dashv\Gamma^{\prime};\gamma^{\prime}$ to type check
statements. The meaning of this judgment is that statement $s$ type checks
under local environment $\Gamma$ and guard $\gamma$, and it produces a new
local type environment $\Gamma^{\prime}$ and guard $\gamma^{\prime}$. Note
that the statement typing judgments are flow-sensitive in that they modify the
environment and guard; this is because (1) let bindings can add new variables
to the local type environment, and (2) fetch/commit statements will modify the
guard.

  * •

_Join typing judgments_ : Finally, we have a third typing judgment for join
points of conditionals. This judgment is of the form
$\Gamma;\gamma;(\Gamma_{1};\gamma_{1});(\Gamma_{2};\gamma_{2})\vdash
j\dashv\Gamma^{\prime};L$ where $\Gamma,\gamma$ pertain to the state before
the conditional, $\Gamma_{i},\gamma_{i}$ are associated with the state after
executing each of the branches, and $\Gamma^{\prime}$ and $L$ are the
resulting environment and lock status after the join point.

##### Subtyping

Finally, our type system makes use of a subtyping judgment of the form:

$\Gamma;\gamma\vDash\tau_{1}<:\tau_{2}$

which states that, under $\Gamma$ and $\gamma$, the set of values represented
by $\tau_{1}$ is a subset of those represented by $\tau_{2}$. As expected and
as shown in Figure 6, the subtyping judgment reduces to checking logical
implication. In particular, we use a function $\mathsf{Encode}$ to translate
$\Gamma,\gamma$ and the two terms $t_{1},t_{2}$ to logical formulas which
belong to the quantifier-free fragment of the combined theory of rationals,
arrays, equality with uninterpreted functions. Thus, to check whether
$\tau_{1}$ is a subtype of $\tau_{2}$, we can use an off-the-shelf SMT solver.
Since our encoding of refinement types into SMT is the standard scheme used in
(Rondon et al., 2008, 2010; Vekris et al., 2016), we do not explain the
$\mathsf{Encode}$ procedure in detail.

###### Example 0.

Consider the following subtyping judgment:

$\Gamma;c\geq
d\vDash\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu=a\\}<:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu\geq
d\\}$

where $\Gamma$ contains four variables $a,b,c,d$ all with base type
$\operatorname{\mathsf{UInt}}$ and $a$ has the refinement $\nu=b+c$. This
subtyping check reduces to querying the validity of the following formula:

$\phi_{T}\land a=b+c\land c\geq d\land\nu=a\implies\nu\geq d$

where $\phi_{T}$ are additional clauses that restrict the terms of type
$\operatorname{\mathsf{UInt}}$ to be in the interval $[0,\mathsf{MaxInt}]$.

Sub-Base $\displaystyle\displaystyle{\hbox{\hskip
121.84717pt\vbox{\hbox{\hskip-121.84717pt\hbox{\hbox{$\displaystyle\displaystyle\left(\mathsf{Encode}(\Gamma)\land\mathsf{Encode}(\gamma)\land\mathsf{Encode}(t_{1})\implies\mathsf{Encode}(t_{2})\right)\text{
valid}$}}}\vbox{}}}\over\hbox{\hskip
61.24147pt\vbox{\vbox{}\hbox{\hskip-61.24146pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vDash\\{\nu:T\mid
t_{1}\\}<:\\{\nu:T\mid t_{2}\\}$}}}}}}$ Figure 6. Subtyping relation

###  4.2. Refinement Typing Rules

In this section, we discuss the basic typing rules of SolType, starting with
expressions. Note that the typing rules we describe in this subsection are
_intentionally_ imprecise for complex data structures involving nested
mappings or mapping of structs. Since precise handling of complex data
structures requires introducing additional machinery, we delay this discussion
until the next subsection.

####  4.2.1. Expression Typing

$\displaystyle\displaystyle{\hbox{\hskip
59.41583pt\vbox{\hbox{\hskip-59.41582pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e:\tau$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vDash\tau<:\tau^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
23.21964pt\vbox{\vbox{}\hbox{\hskip-23.21964pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e:\tau^{\prime}$}}}}}}$ TE-Sub $\displaystyle\displaystyle{\hbox{\hskip
36.71461pt\vbox{\hbox{\hskip-36.7146pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma(x)=\\{\nu:T\mid\phi\\}$}}}\vbox{}}}\over\hbox{\hskip
49.98482pt\vbox{\vbox{}\hbox{\hskip-49.9848pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
x:\\{\nu:T\mid\nu=x\\}$}}}}}}$ TE-Var $\displaystyle\displaystyle{\hbox{\hskip
112.8292pt\vbox{\hbox{\hskip-112.8292pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\operatorname{\mathsf{UInt}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu+e_{1}\leq\mathsf{MaxInt}\\}$}}}}\vbox{}}}\over\hbox{\hskip
71.81584pt\vbox{\vbox{}\hbox{\hskip-71.81583pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}+e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu=e_{1}+e_{2}\\}$}}}}}}$
TE-Plus $\displaystyle\displaystyle{\hbox{\hskip
111.4403pt\vbox{\hbox{\hskip-111.44029pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\operatorname{\mathsf{UInt}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu*e_{1}\leq\mathsf{MaxInt}\\}$}}}}\vbox{}}}\over\hbox{\hskip
69.03806pt\vbox{\vbox{}\hbox{\hskip-69.03804pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}*e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu=e_{1}*e_{2}\\}$}}}}}}$
TE-Mul $\displaystyle\displaystyle{\hbox{\hskip
93.38469pt\vbox{\hbox{\hskip-93.38467pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\operatorname{\mathsf{UInt}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu\leq
e_{1}\\}$}}}}\vbox{}}}\over\hbox{\hskip
67.37137pt\vbox{\vbox{}\hbox{\hskip-67.37135pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}-e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu=e_{1}-e_{2}\\}$}}}}}}$
TE-Minus $\displaystyle\displaystyle{\hbox{\hskip
92.15656pt\vbox{\hbox{\hskip-92.15656pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\operatorname{\mathsf{UInt}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu>0\\}$}}}}\vbox{}}}\over\hbox{\hskip
105.90857pt\vbox{\vbox{}\hbox{\hskip-105.90855pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}/e_{2}:\\{\nu:\operatorname{\mathsf{UInt}}\mid e_{2}*\nu\leq e_{1}\land
e_{1}<(\nu+1)*e_{2}\\}$}}}}}}$ TE-Div $\displaystyle\displaystyle{\hbox{\hskip
140.94019pt\vbox{\hbox{\hskip-140.94017pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathsf{Map}(T)\qquad\Gamma;\gamma\vdash
e_{2}:\operatorname{\mathsf{UInt}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi_{a}={\begin{cases}\nu\leq\operatorname{\mathsf{Sum}}(e_{1})&\text{if
$\displaystyle T=\operatorname{\mathsf{UInt}}$}\\\
\operatorname{\mathsf{true}}&\text{otherwise}\end{cases}}$}}}}\vbox{}}}\over\hbox{\hskip
74.75238pt\vbox{\vbox{}\hbox{\hskip-74.75238pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}[e_{2}]:\\{\nu:T\mid\nu=e_{1}[e_{2}]\land\phi_{a}\\}$}}}}}}$ TE-MapInd
$\displaystyle\displaystyle{\hbox{\hskip
207.96045pt\vbox{\hbox{\hskip-207.96043pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathsf{Map}(T)\qquad\Gamma;\gamma\vdash
e_{2}:\operatorname{\mathsf{UInt}}\qquad\Gamma;\gamma\vdash e_{3}:T$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi_{a}={\begin{cases}\operatorname{\mathsf{Sum}}(\nu)=\operatorname{\mathsf{Sum}}(e_{1})-e_{1}[e_{2}]+e_{3}&\text{if
$\displaystyle T=\operatorname{\mathsf{UInt}}$}\\\
\operatorname{\mathsf{true}}&\text{otherwise}\end{cases}}$}}}}\vbox{}}}\over\hbox{\hskip
97.06992pt\vbox{\vbox{}\hbox{\hskip-97.0699pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}\left[e_{2}\mathop{\triangleleft}e_{3}\right]:\\{\nu:\mathsf{Map}(T)\mid\nu=e_{1}\left[e_{2}\mathop{\triangleleft}e_{3}\right]\land\phi_{a}\\}$}}}}}}$
TE-MapUpd $\displaystyle\displaystyle{\hbox{\hskip
72.3601pt\vbox{\hbox{\hskip-72.36009pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathop{\mathsf{Struct}}S$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta(S,x)=T$}}}}\vbox{}}}\over\hbox{\hskip
62.99666pt\vbox{\vbox{}\hbox{\hskip-62.99664pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}[x]:\\{\nu:T\mid\nu=e_{1}[x]\\}$}}}}}}$ TE-SctInd
$\displaystyle\displaystyle{\hbox{\hskip
106.25146pt\vbox{\hbox{\hskip-106.25145pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathop{\mathsf{Struct}}S$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{2}:T$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta(S,x)=T$}}}}}\vbox{}}}\over\hbox{\hskip
74.06409pt\vbox{\vbox{}\hbox{\hskip-74.06407pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}\left[x\mathop{\triangleleft}e_{2}\right]:\\{\nu:T\mid\nu=e_{1}\left[x\mathop{\triangleleft}e_{2}\right]\\}$}}}}}}$
TE-SctUpd Figure 7. Main refinement typing rules for expressions

Fig 7 shows the key typing rules for expressions. Since the first two rules
and the rules involving structs are standard, we focus on the remaining rules
for arithmetic expressions and mappings.

##### Arithmetic expressions.

The TE-Plus and TE-Mul rules capture the overflow safety properties of 256-bit
integer addition and multiplication respectively. In particular, they check
that the sum/product of the two expressions is less than $\mathsf{MaxInt}$
(when treating them as mathematical integers). The next rule, TE-Minus, checks
that the result of the subtraction is not negative (again, when treated as
mathematical integers). Finally, the TE-Div rule disallows division by zero,
and constrains the result of the division to be in the appropriate range.

##### Mappings.

The next two rules refer to reading from and writing to mappings. As stated
earlier, we only focus on precise typing rules for variables of type
$\mathsf{Map(UInt)}$ in this section and defer precise typing rules for more
complex maps to the next subsection. Here, according to the Te-MapInd rule,
the result of an evaluating $e_{1}[e_{2}]$ is less than or equal to
$\mathsf{Sum}(e_{1})$, where $\mathsf{Sum}$ is an uninterpreted function.
According to the next rule, called Te-MapUpd, if we write value $e_{3}$ at
index $e_{2}$ of mapping $e_{1}$, the sum of the elements in the resulting
mapping is given by:

$\mathsf{Sum}(e_{1})-e_{1}[e_{2}]+e_{3}$

Thus, this rule, which is based on an axiom from a previous work (Permenev et
al., 2020), allows us to precisely capture the sum of elements in mappings
whose value type is $\operatorname{\mathsf{UInt}}$.

####  4.2.2. Statement Typing

$\displaystyle\displaystyle{\hbox{\hskip
78.20865pt\vbox{\hbox{\hskip-78.20865pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma_{1}\vdash
s_{1}\dashv\Gamma_{2};\gamma_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{2};\gamma_{2}\vdash
s_{2}\dashv\Gamma_{3};\gamma_{3}$}}}}\vbox{}}}\over\hbox{\hskip
40.07028pt\vbox{\vbox{}\hbox{\hskip-40.07027pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma_{1}\vdash
s_{1};s_{2}\dashv\Gamma_{3};\gamma_{3}$}}}}}}$ TS-Seq
$\displaystyle\displaystyle{\hbox{\hskip
94.75977pt\vbox{\hbox{\hskip-94.75975pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e:\tau$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x\notin\operatorname{\mathsf{dom}}(\Gamma)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\tau=\\{\nu:T\mid
t\\}$}}}}}\vbox{}}}\over\hbox{\hskip
86.9848pt\vbox{\vbox{}\hbox{\hskip-86.9848pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash\mathop{\mathsf{let}}x:\tau=e\dashv\Gamma[x\mapsto\\{\nu:T\mid\nu=e\\}];\gamma$}}}}}}$
TS-Let $\displaystyle\displaystyle{\hbox{\hskip
174.24532pt\vbox{\hbox{\hskip-30.3445pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma\vdash
e:\operatorname{\mathsf{Bool}}$}}}\vbox{\hbox{\hskip-174.24532pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};e,\gamma\vdash
s_{1}\dashv\Gamma_{11};\gamma_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\lnot
e,\gamma\vdash s_{2}\dashv\Gamma_{12};\gamma_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma;(\Gamma_{11},\gamma_{1});(\Gamma_{12},\gamma_{2})\vdash
j\dashv\Gamma_{2};L$}}}}}\vbox{}}}}\over\hbox{\hskip
75.37425pt\vbox{\vbox{}\hbox{\hskip-75.37424pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma\vdash\mathop{\mathsf{if}}e\mathop{\mathsf{then}}s_{1}\mathop{\mathsf{else}}s_{2}\mathop{\mathsf{join}}j\dashv\Gamma_{2};L,\gamma$}}}}}}$
TS-If $\displaystyle\displaystyle{\hbox{\hskip
58.06483pt\vbox{\hbox{\hskip-58.06482pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e:\\{\nu:\operatorname{\mathsf{Bool}}\mid\nu=\operatorname{\mathsf{true}}\\}$}}}\vbox{}}}\over\hbox{\hskip
39.65816pt\vbox{\vbox{}\hbox{\hskip-39.65814pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash\mathop{\mathsf{assert}}{e}\dashv\Gamma;\gamma$}}}}}}$
TS-Assert $\displaystyle\displaystyle{\hbox{\hskip
28.9445pt\vbox{\hbox{\hskip-28.94449pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e:\operatorname{\mathsf{Bool}}$}}}\vbox{}}}\over\hbox{\hskip
47.25017pt\vbox{\vbox{}\hbox{\hskip-47.25017pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash\mathop{\mathsf{assume}}{e}\dashv\Gamma;e,\gamma$}}}}}}$
TS-Assume $\displaystyle\displaystyle{\hbox{\hskip
154.18562pt\vbox{\hbox{\hskip-154.18562pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
all $\displaystyle i$},\qquad
x_{i}\notin\operatorname{\mathsf{dom}}(\Gamma_{1})\qquad\Delta(x_{i}^{\prime})=\tau_{i}\qquad\tau_{i}^{\prime}=\tau_{i}[x_{1}^{\prime}\mapsto
x_{1},\dots,x_{i}^{\prime}\mapsto\nu,\dots,x_{n}^{\prime}\mapsto
x_{n}]$}}}\vbox{\hbox{\hskip-56.54802pt\hbox{\hbox{$\displaystyle\displaystyle$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{2}=x_{1}:\tau_{1}^{\prime},\dots,x_{n}:\tau_{n}^{\prime},\Gamma_{1}$}}}}\vbox{}}}}\over\hbox{\hskip
79.6492pt\vbox{\vbox{}\hbox{\hskip-79.6492pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\mathsf{Unlocked},\gamma\vdash\mathop{\mathsf{fetch}}\overrightarrow{x_{i}^{\prime}\mathop{\mathsf{as}}x_{i}}\dashv\Gamma_{2};\mathsf{Locked},\gamma$}}}}}}$
TS-Fetch $\displaystyle\displaystyle{\hbox{\hskip
165.84406pt\vbox{\hbox{\hskip-165.84404pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
all $\displaystyle i$},\qquad\Gamma;\gamma\vdash
e_{i}:\tau_{i}\qquad\Delta(x_{i}^{\prime})=\tau_{i}^{\prime}\qquad\Gamma;\gamma\vDash\tau_{i}<:\tau_{i}^{\prime}[x_{1}^{\prime}\mapsto
e_{1},\dots,x_{i}^{\prime}\mapsto\nu,\dots,x_{n}^{\prime}\mapsto
e_{n}]$}}}\vbox{}}}\over\hbox{\hskip
113.02965pt\vbox{\vbox{}\hbox{\hskip-113.02963pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\mathsf{Locked},\gamma\vdash\mathop{\mathsf{commit}}e_{1}\mathop{\mathsf{to}}x_{1},\dots,e_{n}\mathop{\mathsf{to}}x_{n}\dashv\Gamma;\mathsf{Unlocked},\gamma$}}}}}}$
TS-Commit $\displaystyle\displaystyle{\hbox{\hskip
203.48047pt\vbox{\hbox{\hskip-203.48045pt\hbox{\hbox{$\displaystyle\displaystyle\Delta(f)=((x_{1}^{\prime}\mapsto\tau_{1}^{\prime},\dotsi,x_{n}^{\prime}\mapsto\tau_{n}^{\prime}),\tau_{r})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{2}=x:\tau_{r}[x_{1}^{\prime}\mapsto
e_{1},\dots,x_{n}^{\prime}\mapsto e_{n}],\Gamma_{1}$}\hskip
20.00003pt\hbox{\hskip-136.94916pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
all $\displaystyle i$},\qquad\Gamma_{1};\gamma\vdash
e_{i}:\tau_{i}\qquad\Gamma_{1};\gamma\vDash\tau_{i}<:\tau_{i}^{\prime}[x_{1}^{\prime}\mapsto
e_{1},\dots,x_{i}^{\prime}\mapsto\nu,\dots,x_{n}^{\prime}\mapsto
e_{n}]$}}}}}}\vbox{\hbox{\hskip-136.94916pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
all $\displaystyle i$},\qquad\Gamma_{1};\gamma\vdash
e_{i}:\tau_{i}\qquad\Gamma_{1};\gamma\vDash\tau_{i}<:\tau_{i}^{\prime}[x_{1}^{\prime}\mapsto
e_{1},\dots,x_{i}^{\prime}\mapsto\nu,\dots,x_{n}^{\prime}\mapsto
e_{n}]$}}}\vbox{}}}}\over\hbox{\hskip
118.14023pt\vbox{\vbox{}\hbox{\hskip-118.14023pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\mathsf{Unlocked},\gamma\vdash\mathop{\mathsf{call}}x:\tau_{r}=f(e_{1},\dots,e_{n})\dashv\Gamma_{2};\mathsf{Unlocked},\gamma$}}}}}}$
TS-Call $\displaystyle\displaystyle{\hbox{\hskip
171.88576pt\vbox{\hbox{\hskip-105.06262pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
every }x_{i},$}\hskip
20.00003pt\hbox{\hskip-137.98059pt\hbox{\hbox{$\displaystyle\displaystyle
x_{i}\notin\operatorname{\mathsf{dom}}(\Gamma)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma_{1}\vdash
x_{i1}:\\{\nu:T_{i1}\mid\phi_{i1}\\}\qquad\Gamma_{2};\gamma_{2}\vdash
x_{i2}:\\{\nu:T_{i2}\mid\phi_{i2}\\}$}}}}}}\vbox{\hbox{\hskip-137.98059pt\hbox{\hbox{$\displaystyle\displaystyle
x_{i}\notin\operatorname{\mathsf{dom}}(\Gamma)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma_{1}\vdash
x_{i1}:\\{\nu:T_{i1}\mid\phi_{i1}\\}\qquad\Gamma_{2};\gamma_{2}\vdash
x_{i2}:\\{\nu:T_{i2}\mid\phi_{i2}\\}$}}}}\vbox{\hbox{\hskip-171.88574pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1};\gamma_{1}\vDash\\{\nu:T_{i1}\mid\nu=x_{i1}\\}<:\tau_{i}[(\overrightarrow{x_{i}\mapsto
x_{i1}})]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{2};\gamma_{2}\vDash\\{\nu:T_{i2}\mid\nu=x_{i2}\\}<:\tau_{i}[(\overrightarrow{x_{i}\mapsto
x_{i2}})]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma^{\prime}=\overrightarrow{x_{i}:\tau_{i}},\Gamma$}}}}}\vbox{}}}}}\over\hbox{\hskip
74.55772pt\vbox{\vbox{}\hbox{\hskip-74.55772pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma;(\Gamma_{1};L,\gamma_{1});(\Gamma_{2};L,\gamma_{2})\vdash\overrightarrow{x_{i}:\tau_{i}=\Phi(x_{i1},x_{i2})}\dashv\Gamma^{\prime};L$}}}}}}$
T-Join $\displaystyle\displaystyle{\hbox{\hskip
160.22047pt\vbox{\hbox{\hskip-160.22047pt\hbox{\hbox{$\displaystyle\displaystyle\overrightarrow{x_{i}:\tau_{i}};\mathsf{Unlocked}\vdash
s\dashv\Gamma;\gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\gamma=\mathsf{Unlocked},\gamma^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e:\tau_{r}^{\prime}\qquad\Gamma;\gamma\vDash\tau_{r}^{\prime}<:\tau_{r}$}}}}}\vbox{}}}\over\hbox{\hskip
41.53714pt\vbox{\vbox{}\hbox{\hskip-41.53712pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathop{\mathbf{fun}}f(\overrightarrow{x_{i}:\
\tau_{i}}):\tau_{r}=s;e$}}}}}}$ T-FunDecl Figure 8. Main typing rules for
statements and function definitions

Next, we consider the statement typing rules shown in Figure 8. Again, since
some of the rules are standard, we focus our discussion on aspects that are
unique to our type system.

##### Conditionals.

In the conditional rule TS-If, we separately type check the true and false
branches, adding the appropriate predicate (i.e., $e$ or $\neg e$) to the
statement guard for each branch. The results of the two branches are combined
using the join typing judgment T-Join (also shown in Figure 8). In particular,
the join rule checks the type annotations for variables that are introduced
via $\Phi$ nodes in SSA form and requires that the type of the $x_{i}$
variants in each branch is a subtype of the declared type $\tau_{i}$ of
$x_{i}$. Note also that the join rule requires agreement between the lock
states in the two branches. This means that either (1) both branches commit
their changes to state variables, or (2) both have uncommitted changes.

##### Fetch and Commit.

As mentioned earlier, MiniSol contains $\mathsf{fetch}$ and $\mathsf{commit}$
statements, with the intention of allowing temporary violations of contract
invariants. The TS-Fetch and TS-Commit rules provide type checking rules for
these two statements. Specifically, the TS-Fetch rule says that, when no
“lock” is held on the state variables (indicated by a lock status
$\mathsf{Unlocked}$), a fetch statement can be used to “acquire” a lock and
copy the current values of the state variables into a set of freshly declared
variables. The contract invariant will be assumed to hold on these variables.

Next, according to the TS-Commit rule, a commit statement can be used to
“release” the lock and write the provided expressions back to the state
variables. The contract invariant will be checked to hold on the provided
expressions. Thus, our fetch and commit constructs allow temporary violations
of the contract invariant _in between_ these fetch and commit statements.

##### Function Calls.

The TS-Call rule in Figure 8 is used to type check function calls. In
particular, since the contract invariant should not be violated between
different transactions, our type system enforces that all state variables have
been committed by requiring that the current state is $\mathsf{Unlocked}$.
Since the type checking of function arguments and return value is standard,
the rest of the rule is fairly self-explanatory.

##### Function Definitions.

Finally, we consider the type checking rule for function definitions (rule
T-FunDecl rule in Figure 8). According to this rule, a function declaration is
well-typed if its body $s$ is well-typed (with the environment initially set
to the arguments and lock status being $\mathsf{Unlocked}$), and the returned
expression has type $T_{r}$ after executing $s$.

###  4.3. Generalizing Sum Axioms to Deeply Nested Mappings

The TE-MapInd and TE-MapUpd rules that we presented in Fig. 7 are sufficient
for handling maps over integers; however, they are completely imprecise for
more complex data structures, such as nested mappings or mappings of structs.
Since Solidity programs often employ deeply nested mappings involving structs,
it is crucial to have precise typing rules for more complex data structures.
Therefore, in this section, we show how to generalize our precise typing rules
for mappings over integers to arbitrarily nested mappings.

To gain some intuition about how to generalize these typing rules, consider
the usrs mapping in Fig. 3. The update to usrs on line 14 is expressed in our
IR as a sequence of map lookup operations followed by a sequence of updates:

⬇

// usrs0 has type mapping(address => mapping(uint => User))

let m0 = usrs0[msg.sender]; // lookup

let u0 = m0[accno]; // lookup

let b0 = u0[.bal]; // access bal field

let u1 = u0[.bal $\triangleleft$ b0 + amt]; // update bal field of struct

let m1 = m0[accno $\triangleleft$ u1]; // update usrs[msg.sender] with updated
struct

let usrs1 = usrs0[msg.sender $\triangleleft$ m1]; // update usrs with updated
nested mapping

Before we consider the revised typing rules, let us first consider the
constraints we would _want_ to generate for this example:

  * •

For the first line, usrs0 is a nested mapping containing a struct called User
which has an integer field called bal, and m0 is a mapping over Users. Based
on the semantics of our refinement terms, the assignment on the first line
imposes the following constraint on m0:

$\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(m0))\leq\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(usrs0)))$

  * •

Using similar reasoning, we can infer the following constraint on u0, which is
of type User:

$u0[.bal]\leq\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(m0))$

  * •

When we update m1 on the fourth line, this again imposes a constraint
involving $\operatorname{\mathsf{Sum}}$:

$\begin{split}\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(m1))=\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(m0))-m0[accno].bal+u1.bal\end{split}$

  * •

Finally, for the update on the last line, we can infer:

$\begin{array}[]{l}\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(usrs1)))=\\\
\qquad\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(m0)))-\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(m0))+\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(m1))\end{array}$

As we can see from this example, the _shape_ of the constraints we infer for
complex map reads and writes is very similar to what we had in the TE-MapInd
and the TE-MapUpd rules from Figure 7. In particular, reading from a map
imposes constraints of the form:

(4) $H_{2}(m[k])\leq H_{1}(m)$

whereas updating a map imposes constraints of the form:

(5)
$H_{1}(m\left[k\mathop{\triangleleft}v\right])=H_{1}(m)-H_{2}(m[k])+H_{2}(v)$

Therefore, we can easily generalize the TE-MapInd and the TE-MapUpd rules to
arbitrarily complex mappings as long as we have a way of figuring out how to
instantiate $H_{1},H_{2}$ in Equations 4 and 5.

####  4.3.1. Refinement Term Templates

Based on the above observation, given a source expression $e$ of some base
type $T$, we want a way to automatically generate relevant refinement terms of
the form $H(e)$. To facilitate this, we first introduce the notion of
_templatized refinement terms_ :

###### Definition 2.

(Templatized refinement term) A _refinement term template_ $H$ is a refinement
term containing a unique hole, denoted $\square$. Given such a template $H$,
we write $H(e)$ to denote the refinement term obtained by filling the hole
$\square$ in $H$ with $e$.

For instance,
$H=\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{\emph{bal}}(\square))$
is a valid template, and $H(m0)$ yields
$\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{\emph{bal}}(m0))$.

Next, given a type $T_{h}$, we need a way to generate all templates that can
be applied to expressions of type $T_{h}$. Towards this purpose, we introduce
a _template synthesis judgment_ of the following form:

$\begin{array}[]{rllr}\lx@intercol T_{h}\VDash
H:T,w\hfil\lx@intercol&\text{(Template synthesis judgment)}\end{array}$

The meaning of this judgment is that, given an expression $e$ of type $T_{h}$,
$H(e)$ is a well-typed term of type $T$. In this judgment, $w$ is a so-called
_access path_ that keeps track of the field accesses we need to perform to get
from $e$ to $H(e)$. In particular, an access path is a sequence of field names
defined according to the following grammar:

$\begin{array}[]{rllr}w&::=&\epsilon\mid x,w&\text{(Access path)}\\\ \\\
\end{array}$

where $x$ is the name of a field. As we will see shortly, we need this concept
of access path to ensure that we do not generate non-sensical constraints in
our generalized type checking rules for map reads and writes.

$\displaystyle\displaystyle{\hbox{\hskip
46.9298pt\vbox{\hbox{\hskip-46.9298pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash
H:\mathsf{Map}(\operatorname{\mathsf{UInt}}),w$}}}\vbox{}}}\over\hbox{\hskip
46.79091pt\vbox{\vbox{}\hbox{\hskip-46.79091pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash\operatorname{\mathsf{Sum}}(H):\operatorname{\mathsf{UInt}},w$}}}}}}$
TH-Sum $\displaystyle\displaystyle{\hbox{\hskip
54.15726pt\vbox{\hbox{\hskip-54.15724pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash H:\mathsf{Map}(\mathsf{Map}(T)),w$}}}\vbox{}}}\over\hbox{\hskip
60.33783pt\vbox{\vbox{}\hbox{\hskip-60.33781pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash\operatorname{\mathsf{Flatten}}(H):\mathsf{Map}(T),w$}}}}}}$ TH-
Flatten $\displaystyle\displaystyle{\hbox{\hskip
90.26483pt\vbox{\hbox{\hskip-90.26482pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash H:\mathsf{Map}(\mathop{\mathsf{Struct}}S),w$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta(S,x)=T$}}}}\vbox{}}}\over\hbox{\hskip
56.1846pt\vbox{\vbox{}\hbox{\hskip-56.1846pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash\operatorname{\mathsf{Fld}}_{x}(H):\mathsf{Map}(T),wx$}}}}}}$ TH-
Fld $\displaystyle\displaystyle{\hbox{\hskip
76.23701pt\vbox{\hbox{\hskip-76.237pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash H:\mathop{\mathsf{Struct}}S,w$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta(S,x)=T$}}}}\vbox{}}}\over\hbox{\hskip
38.48352pt\vbox{\vbox{}\hbox{\hskip-38.4835pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash H[.x]:T,wx$}}}}}}$ TH-FldAcc
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
27.30109pt\vbox{\vbox{}\hbox{\hskip-27.30107pt\hbox{\hbox{$\displaystyle\displaystyle
T_{h}\VDash\square:T_{h},\epsilon$}}}}}}$ TH-Hole Figure 9. Inference rules
for type-directed synthesis of refinement term templates

Figure 9 shows our rules for synthesizing refinement term templates. The first
rule, TH-Sum, states that we can apply the $\operatorname{\mathsf{Sum}}$
operator to an expression whose base type is
$\mathsf{Map}(\operatorname{\mathsf{UInt}})$. The second rule, TH-Flatten,
allows applying a $\operatorname{\mathsf{Flatten}}$ operation to any term of
type $\mathsf{Map}(\mathsf{Map}(T))$. The third rule, TH-Fld, states that we
can apply a projection operator to an expression that is a mapping of structs.
In other words, if $H$ is a mapping over structs $S$ and $S$ has a field
called $x$, then we can generate the template
$\operatorname{\mathsf{Fld}}_{x}(H)$. Since this involves a field access, note
that the TH-Fld rule adds $x$ to the access path. The next rule, Th-FldAcc, is
very similar but applies to structs instead of mappings of structs. In
particular, if $H$ has struct type $S$ with field $x$, it is valid to access
the $x$ field of $H$. As in the previous case, this rule appends $x$ to the
resulting access path. The final rule, TH-Hole is a base case and states that
the hole is constrained to have the specified type $T_{h}$.

####  4.3.2. Generalized Typing Rules for Map Reads and Writes

$\displaystyle\displaystyle{\hbox{\hskip
205.61507pt\vbox{\hbox{\hskip-205.61505pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathsf{Map}(T)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{2}:\operatorname{\mathsf{UInt}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi_{a}=\bigwedge_{i}H_{i2}(\nu)\leq
H_{i1}(e_{1})$}\hskip
20.00003pt\hbox{\hskip-122.7782pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
each $\displaystyle i$,}\qquad\mathsf{Map}(T)\VDash
H_{i1}:\operatorname{\mathsf{UInt}},w_{i}\qquad T\VDash
H_{i2}:\operatorname{\mathsf{UInt}},w_{i}$}}}}}}}\vbox{\hbox{\hskip-122.7782pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
each $\displaystyle i$,}\qquad\mathsf{Map}(T)\VDash
H_{i1}:\operatorname{\mathsf{UInt}},w_{i}\qquad T\VDash
H_{i2}:\operatorname{\mathsf{UInt}},w_{i}$}}}\vbox{}}}}\over\hbox{\hskip
74.75238pt\vbox{\vbox{}\hbox{\hskip-74.75238pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}[e_{2}]:\\{\nu:T\mid\nu=e_{1}[e_{2}]\land\phi_{a}\\}$}}}}}}$ TE-MapInd
$\displaystyle\displaystyle{\hbox{\hskip
242.73692pt\vbox{\hbox{\hskip-36.25252pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathsf{Map}(T)$}}}\vbox{\hbox{\hskip-242.73691pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{2}:\operatorname{\mathsf{UInt}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{3}:T$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi_{a}=\bigwedge_{i}\left(H_{i1}(\nu)=H_{i1}(e_{1})-H_{i2}(e_{1}[e_{2}])+H_{i2}(e_{3})\right)$}\hskip
20.00003pt\hbox{\hskip-122.7782pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
each $\displaystyle i$,}\qquad\mathsf{Map}(T)\VDash
H_{i1}:\operatorname{\mathsf{UInt}},w_{i}\qquad T\VDash
H_{i2}:\operatorname{\mathsf{UInt}},w_{i}$}}}}}}}\vbox{\hbox{\hskip-122.7782pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
each $\displaystyle i$,}\qquad\mathsf{Map}(T)\VDash
H_{i1}:\operatorname{\mathsf{UInt}},w_{i}\qquad T\VDash
H_{i2}:\operatorname{\mathsf{UInt}},w_{i}$}}}\vbox{}}}}}\over\hbox{\hskip
97.06992pt\vbox{\vbox{}\hbox{\hskip-97.0699pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}\left[e_{2}\mathop{\triangleleft}e_{3}\right]:\\{\nu:\mathsf{Map}(T)\mid\nu=e_{1}\left[e_{2}\mathop{\triangleleft}e_{3}\right]\land\phi_{a}\\}$}}}}}}$
TE-MapUpd Figure 10. Updated typing rules for mappings, where refinement term
templates are used to generate sum properties over nested data structures.

Equipped with the template synthesis rules, we are now ready to present the
generalized and precise versions of TH-MapInd and TH-MapUpd rules for
arbitrarily complex mappings.

The new TE-MapInd rule shown in Figure 10 generates precise constraints on
$e_{1}[e_{2}]$ where $e_{1}$ is has type $\mathsf{Map}(T)$. As illustrated
earlier through the example, this rule generates constraints of the form
$H_{2}(\nu)\leq H_{1}(e_{1})$, where $H_{1},H_{2}$ are templates that can be
applied to terms of type $\mathsf{Map}(T)$ and $T$ respectively. Since a given
struct can have multiple integer fields, this rule generates a conjunction of
such constraints, one for each integer field. Note that, for each constraint
of the form $H_{i2}(\nu)\leq H_{i1}(e_{1})$ in this rule, we enforce that the
corresponding access paths $w_{i}$ match, as, otherwise, the generated
constraints would not make sense.

Next, we consider the new TE-MapUpd rule in Figure 10 for updating maps.
Specifically, given an expression $e_{1}[e_{1}\triangleleft e_{3}]$ where
$e_{1}$ is of type $\mathsf{Map}(T)$, this rule generates a conjunction of
constraints of the form:

$H_{i1}(\nu)=H_{i2}(e_{1})-H_{i2}(e_{1}[e_{2}])+H_{i2}(e_{3}),$

one for each integer field accessible from $T$. As in the previous case, we
use the notion of access paths to ensure that the hole templates $H_{i1}$ and
$H_{i2}$ correspond to the same field sequence.

###### Example 0.

Consider again the update to usrs on line 14 of Fig 3. We demonstrate how the
TE-MapInd rule generates typing constraints. First, since usrs has type
$\mathsf{Map}(\mathsf{Map}(\emph{User}))$, we have
$T=\mathsf{Map}(\emph{User})$. From the synthesis rules, one such
instantiation for $H_{i1}$ is
$\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(\square)))$,
as shown by the following derivation tree:

TH-Sum $\displaystyle\displaystyle{\hbox{\hskip
143.27023pt\vbox{\hbox{\hskip-143.27023pt\hbox{\hbox{$\displaystyle\displaystyle\raise
10.5pt\hbox{\hbox to0.0pt{\hss$\displaystyle\hbox{\small\small{TH-
Fld}}\;$}$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
141.77023pt\vbox{\hbox{\hskip-141.77022pt\hbox{\hbox{$\displaystyle\displaystyle\raise
10.5pt\hbox{\hbox to0.0pt{\hss$\displaystyle\hbox{\small\small{TH-
Flatten}}\;$}$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
84.75394pt\vbox{\hbox{\hskip-84.75394pt\hbox{\hbox{$\displaystyle\displaystyle\raise
10.5pt\hbox{\hbox to0.0pt{\hss$\displaystyle\hbox{\small\small{TH-
Hole}}\;$}$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
83.25394pt\vbox{\vbox{}\hbox{\hskip-83.25392pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{Map}(\mathsf{Map}({User}))\VDash\square:\mathsf{Map}(\mathsf{Map}({User})),\epsilon$}}}}}}$}}\hbox{}$
}$}}}\vbox{}}}\over\hbox{\hskip
92.73102pt\vbox{\vbox{}\hbox{\hskip-92.73102pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{Map}(\mathsf{Map}({User}))\VDash\operatorname{\mathsf{Flatten}}(\square):\mathsf{Map}(User),bal$}}}}}}$}}\hbox{}$
}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta(User,bal)=\operatorname{\mathsf{UInt}}$}}}}\vbox{}}}\over\hbox{\hskip
105.33559pt\vbox{\vbox{}\hbox{\hskip-105.33557pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{Map}(\mathsf{Map}({User}))\VDash\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(\square)):\mathsf{Map}(\operatorname{\mathsf{UInt}}),bal$}}}}}}$}}\hbox{}$
}$}}}\vbox{}}}\over\hbox{\hskip
105.21059pt\vbox{\vbox{}\hbox{\hskip-105.21057pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{Map}(\mathsf{Map}({User}))\VDash\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(\square))):\operatorname{\mathsf{UInt}},bal$}}}}}}$

Next, we find an instantiation for $H_{i2}$ that accesses the same fields
$w=bal$. It can be proven that

$\mathsf{Map}(\mathop{\mathsf{Struct}})\VDash\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\square)):\operatorname{\mathsf{UInt}},bal$

which yields
$H_{i2}=\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\square))$.
Then, using the TE-MapInd rule, we obtain the constraint

(6)
$\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\nu))\leq\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(usrs)))$

Note that this is only _one_ of the predicates that we can derive. For
example, if the User had another integer field called frozen, we would also
generate the following predicate:

(7)
$\displaystyle\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{frozen}(\nu))$
$\displaystyle\leq\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{frozen}(\operatorname{\mathsf{Flatten}}(usrs)))$

Taking the conjunction of (6) and (7), we obtain the following type for
usrs[msg.sender]:

$\displaystyle usrs[msg.sender]:\\{\nu\mid$
$\displaystyle\nu=usrs[msg.sender]$
$\displaystyle\land\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\nu))\leq\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{bal}(\operatorname{\mathsf{Flatten}}(usrs)))$
$\displaystyle\land\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{frozen}(\nu))\leq\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Fld}}_{frozen}(\operatorname{\mathsf{Flatten}}(usrs)))\\}$

###  4.4. Soundness

We characterize the soundness of our type system in the typical way through
progress and preservation theorems for both expressions and statements. We
briefly state the key propositions and refer the reader to the supplementary
materials for details.

###### Proposition 4 (Progress for Expressions).

If $\Gamma;\gamma\vdash e:\tau$, then $e$ is a value or there exists an
$e^{\prime}$ such that $e\to e^{\prime}$.

Here, $e\to e^{\prime}$ is the standard expression evaluation relation, and
progress can be proven by induction in the standard way. On the other hand,
proving preservation is more interesting, mainly due to the rules from Fig. 10
for complex data structures. To prove preservation, we first need to prove a
lemma that that relates each sum function generated in the refinement of a
mapping to that of the corresponding sum function generated for each entry
(value) in the mapping. With such a lemma, we can prove the following
preservation theorem in a fairly standard way:

###### Proposition 5 (Preservation for Expressions).

If $\Gamma;\gamma\vdash e:\tau$ and $e\to e^{\prime}$, then
$\Gamma;\gamma\vdash e^{\prime}:\tau$.

Next, to state the progress and preservation theorems for statements, we first
introduce the following notation:

$\begin{array}[]{lr}\sigma&\text{(State variable store)}\\\
(s,\sigma)\to(s,\sigma^{\prime},\sigma_{sub})&\text{(Statement evaluation
relation)}\\\ \vDash\sigma&\text{(Store typing)}\end{array}$

The state variable store $\sigma$ contains the value bindings for the state
variables. The statement evaluation relation
$(s,\sigma)\to(s^{\prime},\sigma^{\prime},\sigma_{sub})$ indicates that,
starting with state variable bindings $\sigma$, the statement $s$ will step to
a statement $s^{\prime}$ with updated bindings $\sigma^{\prime}$ and a set of
local variable bindings $\sigma_{sub}$ to apply to the statements following
$s^{\prime}$. The store typing judgment $\vDash\sigma$ asserts that $\sigma$
is well-typed.

With this notation in place, we can state the progress and preservation
theorems for statements as follows:

###### Proposition 6 (Progress for Statements).

If $\Gamma_{1};\gamma_{1}\vdash s\dashv\Gamma_{2};\gamma_{2}$ and
$\vDash\sigma$, then $s=\mathop{\mathsf{skip}}$,
$s=\mathop{\mathsf{assume}}\operatorname{\mathsf{false}}$, or there exist
$s^{\prime},\sigma^{\prime},\sigma_{sub}$ such that
$(s,\sigma)\to(s^{\prime},\sigma^{\prime},\sigma_{sub})$.

###### Proposition 7 (Preservation for Statements).

If $\Gamma_{1};\gamma_{1}\vdash s\dashv\Gamma_{2};\gamma_{2}$ and
$\vDash\sigma$ and $(s,\sigma)\to(s^{\prime},\sigma^{\prime},\sigma_{sub})$,
then there exist $\Gamma_{1}^{\prime},\gamma_{1}^{\prime}$ such that
$\Gamma_{1}^{\prime};\gamma_{1}^{\prime}\vdash
s^{\prime}\dashv\Gamma_{2};\gamma_{2}$ and $\vDash\sigma^{\prime}$.

Note that $\mathop{\mathsf{assume}}\operatorname{\mathsf{false}}$ in
Proposition 6 corresponds to a failed runtime check.

##  5\. Type Inference

In this section, we describe our algorithm for automatically inferring
refinement type annotations. Since writing refinement type annotations for
every variable can be cumbersome, Solid infers types for both local and global
(state) variables.

As mentioned earlier, the key idea underlying our type inference algorithm is
to reduce the type inference problem to Constrained Horn Clause (CHC) solving
(Bjørner et al., 2015). However, since not all arithmetic operations in the
program are guaranteed to be overflow-safe, the CHC constraints generated by
the type checking algorithm will, in general, not be satisfiable. Thus, our
high-level idea is to treat the overflow safety constraints as _soft
constraints_ and find type annotations that try to satisfy as many soft
clauses as possible.

Before we explain our algorithm, we first clarify some assumptions that we
make about the type checking phase. First, we assume that, during constraint
generation, the refinement type of every variable $v$ without a type
annotation is represented with a fresh uninterpreted predicate symbol $p_{v}$.
Second, we assume that the generated constraints are marked as either being
hard or soft. In particular, the overflow safety constraints generated using
the TE-Plus, TE-Minus etc. rules are considered to be soft constraints, while
all other constraints are marked as hard. Third, we assume that the constraint
generation phase imposes a partial order on the soft constraints. In
particular, if $c,c^{\prime}$ are soft constraints generated when analyzing
expressions $e,e^{\prime}$ and $e$ must be evaluated before $e^{\prime}$, then
we have $c\prec c^{\prime}$. As we will see shortly, this partial order allows
us to assume, when trying to satisfy some soft constraint $c$, that overflow
safety checks that happened before $c$ did not fail.

Our type inference procedure InferTypes is shown in Figure 11 and takes three
inputs, namely a set of soft and hard constraints, $C_{s}$ and $C_{h}$
respectively, and a partial order $\preceq$ on soft constraints as described
above. The output of the algorithm is a mapping $\Sigma$ from each
uninterpreted predicate symbol to a refinement type annotation.

Initially, the algorithm starts by initializing every uninterpreted predicate
symbol $p_{v}$ to true (line 5) and then enters a loop where the
interpretation for each $p_{v}$ is gradually strengthened. In particular, in
every loop iteration, we pick one of the soft constraints $c$ and try to
satisfy $c$ along with all the hard constraints $C_{H}$. In doing so, we can
assume all the overflow safety checks that happened to prior to $c$; thus, at
line 8, we feed the following constraint to an off-the-shelf CHC solver:

$\Big{(}\Big{(}\bigwedge_{c_{i}\prec c}c_{i}\Big{)}\rightarrow
c\Big{)}\land\bigwedge_{c_{j}\in C_{h}}c_{j}$

In other words, we try to satisfy this particular soft constraint together
with all the hard constraints, under the assumption that previous overflow
checks did not fail. This assumption is safe since Solid inserts run-time
overflow checks for any operation that cannot be statically verified. If this
constraint is unsatisfiable, we move on and try to satisfy the next soft
constraint. On the other hand, if it is satisfiable, we strengthen the type
annotation for the unknown predicates by conjoining it with the assignment
produced by the CHC solver (line 12).

1:procedure InferTypes($C_{s}$, $C_{h}$, $\preceq$)

2: Input: Soft clauses $C_{s}$, hard clauses $C_{h}$, partial order $\preceq$
on $C_{s}$

3: Output: Mapping $\Sigma$ from uninterpreted predicates $C_{s}\cup C_{h}$ to
refinement type annotations

4: $\mathcal{P}\leftarrow\mathsf{Preds}(C_{s}\cup C_{h})$

5: $\Sigma\leftarrow\\{p\mapsto\top\ |\ p\in\mathcal{P}\\}$

6: for $c\in C_{s}$ do

7: $\Phi_{A}\leftarrow\bigwedge_{c_{i}\prec c}c_{i}$;
$\Phi_{H}\leftarrow\bigwedge_{c_{j}\in C_{h}}c_{j}$

8: $(r,\sigma)\leftarrow\mathsf{SolveCHC}((\Phi_{A}\rightarrow
c)\land\Phi_{H})$

9: if $r=\mathsf{UNSAT}$ then

10: continue

11: for $p\in\mathsf{Dom}(\sigma)$ do

12: $\phi\leftarrow\Sigma(p)\land\sigma(p)$

13: $\Sigma\leftarrow\Sigma[p\mapsto\phi]$

14: return $\Sigma$

Figure 11. Type inference procedure

##  6\. Implementation

We implemented our type checking and type inference algorithms in a prototype
called Solid. Our tool is written in Haskell, with about 3000 lines of code
for the frontend (e.g., Solidity preprocessing, lowering, SSA transformation)
and 4000 lines of code for the backend (e.g., constraint generation, SMT
embedding, solving). Solid uses the Z3 SMT solver (De Moura and Bjørner, 2008)
and the Spacer CHC solver (Komuravelli et al., 2014) in its backed, and it
leverages the Slither (Feist et al., 2019) analyzer as part of its front-end.
In what follows, we discuss various aspects of Solidity and how we handle them
in the MiniSol IR.

##### Preprocessing Solidity code.

To facilitate verification, we preprocess Solidity smart contracts before we
translate them to the MiniSol IR. In particular, we partially evaluate
constant arithmetic expressions such as 6 * 10**26, which frequently appear in
constructors and initialization expressions. We also inline internal function
calls.

##### Function call handling

Our implementation automatically inserts fetch and commit statements between
function call boundaries, such as at the beginning of a function, before and
after function calls or calls to external contracts, and before returning from
a function. This includes most function calls, including monetary transfers
like msg.sender.send(..) and calls to “non-pure” functions in the same file.
In Solidity, functions may be marked “pure”, meaning they do not read or write
to state variables. We modified the TS-Call rule to not require the state
variables to be unlocked when making calls to a pure function.

##### Loops

Our implementation supports while-loops and for-loops using a variation of the
TS-If rule. Performing effective type inference in the presence of loops
(particularly, doubly-nested loops) is challenging, as existing CHC solvers
have a hard time solving the resulting constraints. Inferring invariants for
complex loops could be an interesting direction for future work, however, in
practice, such loops are rare (Mariano et al., 2020) and we found they are
mostly irrelevant to proving overflow safety. Our prototype implementation
does not support complex control flow inside loops such as break or continue
statements.

##### References and aliasing.

Since everything is passed by value in MiniSol, the language shown in Figure 4
does not have aliasing. Thus, as standard (Flanagan et al., 2002; Barnett et
al., 2005), our translation from Solidity to MiniSol introduces additional
mappings to account for possible aliasing. At a high-level, the idea is that,
for any variables $X=\\{x_{1},\ldots,x_{n}\\}$ that may alias each other, we
introduce a mapping $M_{X}$ and model stores (resp. loads) to any $x_{i}$ as
writing to (resp. reading from) $M_{X}[x_{i}]$.

##### Unsupported features.

Our implementation does not support some Solidity features such as inline
assembly, states of external contracts, bitwise operations, and
exponentiation. When translating to the MiniSol IR, we model these statements
using ”havoc” expressions as is standard (Barnett et al., 2005).

##  7\. Evaluation

In this section, we describe a series of experiments that are designed to
answer the following research questions:

  * •

RQ1: Can Solid successfully remove redundant overflow checks without manual
annotations?

  * •

RQ2: What is Solid’s false positive rate?

  * •

RQ3: How long does Solid take to type check real-world smart contracts?

  * •

RQ4: How does Solid compare against existing state-of-the art tools?

  * •

RQ5: How important are type inference and the proposed refinement typing rules
for more complex data structures?

##### Baseline.

To answer our fourth research question, we compare Solid against Verismart,
which is a state-of-the-art Solidity verifier that focuses on proving
arithmetic safety properties (So et al., 2020). We choose Verismart as our
baseline because it has been shown to outperform other smart contract
verifiers for checking arithmetic safety (So et al., 2020). Verismart infers
so-called _transaction invariants_ through a domain-specific instantiation of
the _counterexample-guided inductive synthesis (CEGIS)_ framework (Solar-
Lezama, 2009) and uses the inferred invariants to discharge potential overflow
errors. To perform this evaluation, we built the latest version of Verismart
from source (version from May 31, 2020) and ran both tools on all the
benchmarks, using versions 0.4.26 and 0.5.17 of the Solidity compiler.

##### Setup

We performed all experiments on a computer with an AMD Ryzen 5900X CPU and
32GB of RAM. We used version 4.8.9 of the Z3 SMT solver, which also has the
built-in Spacer CHC solver (Komuravelli et al., 2014). In our experiments, we
set a time limit of 10 seconds per Z3 query.

##### Settings

Our implementation can be used in two modes that we refer to as Auto-Solid and
Semi-Solid. In particular, Auto-Solid is fully automated and uses our type
inference procedure to infer type annotations for state variables (i.e.,
contract invariants). On the other hand, Semi-Solid requires the programmer to
provide contract invariants but automatically infers types for local
variables. To use Solid in this semi-automated mode, we manually wrote
refinement type annotations for state variables by inspecting the source code
of the contract.

###  7.1. Benchmarks

We evaluate Solid on two different sets of benchmark suites that we refer to
as “Verismart benchmarks” and “Etherscan benchmarks”. As its name indicates,
the former one is taken from the Verismart evaluation and consists of 60 smart
contracts that have at least one vulnerability reported in the CVE database.
Since these benchmarks are from 2018 and do not reflect rapid changes in smart
contract development, we also evaluate our approach on another benchmark suite
collected from Etherscan. The latter benchmark suite consists of another 60
contracts randomly sampled from Etherscan in March 2021. Table 1 presents some
relevant statistics about the contracts in this dataset.

Description | Stats
---|---
% contracts containing mappings of structs | 26.7%
% contracts containing nested mappings | 81.3%
Average lines of code | 389
Average number of methods | 29.6
Table 1. Statistics about our benchmarks from Etherscan

###  7.2. Discharging Redundant SafeMath Calls

We performed a manual inspection of all 120 benchmarks to determine how many
of the SafeMath 111Recall that SafeMath is a library that inserts runtime
checks before each arithmetic operation. run-time checks are redundant. In
total, among the 1309 run-time checks, we determined 853 of them to be
redundant (390 in Verismart and 463 in Etherscan). In this experiment, we
evaluate what percentage of these redundant checks Verismart, Auto-Solid, and
Semi-Solid are able to discharge.

The results from this evaluation are shown in Table 2. The key-take away is
that Auto-Solid is able to discharge more run-time checks in both benchmark
suites. In particular, for the Verismart benchmarks, Auto-Solid can discharge
approximately 12% more overflow checks, and for the Etherscan benchmarks, this
difference increases to 27%. If we additionally leverage manually-written
refinement type annotations, then Semi-Solid can discharge almost 90% of the
redundant checks across both datasets.

Dataset | Ops | #redundant | Verismart |  Auto-Solid |  Semi-Solid
---|---|---|---|---|---
Safe | % | Safe | % | Safe | %
Verismart | 642 | 390 | 294 | 75.4% | 340 | 87.2% | 351 | 90.0%
Etherscan | 667 | 463 | 272 | 58.7% | 396 | 85.5% | 417 | 90.1%
Total | 1309 | 853 | 566 | 66.4% | 736 | 86.3% | 768 | 90.0%
Table 2. Number and percentage of redundant overflow checks that can be
eliminated by each tool. The Ops column displays the total number of SafeMath
checks. Under each tool, the Safe column lists the number of arithmetic
operations that can be proven safe by that tool, and the % column shows the
percentage of redundant overflow checks that can be discharged.

Result for RQ1: Solid can automatically prove that 86.3% of the redundant
SafeMath calls are unnecessary. In contrast, Verismart can only discharge
66.4%.

###  7.3. False Positive Evaluation

| Verismart |  Auto-Solid |  Semi-Solid
---|---|---|---
Verismart Benchmarks |  |  |
# false positives | 97 | 50 | 41
# true positives | 251 | 252 | 252
False positive rate | 27.9% | 16.2% | 14.0%
Etherscan Benchmarks |  |  |
# false positives | 195 | 67 | 46
# true positives | 200 | 204 | 204
False positive rate | 49.4% | 24.7% | 18.4%
Overall |  |  |
# false positives | 292 | 117 | 87
# true positives | 451 | 456 | 456
False positive rate | 39.3% | 20.4% | 16.0%
Table 3. Comparison of false positive rates

Next, we evaluate Solid’s false positive rate in both the fully-automated and
semi-automated modes and compare it against Verismart. In particular, Table 3
shows the number of true and false positives as well as the false positive
rate for each tool for both benchmark suites. Across all benchmarks, Verismart
reports 292 false alarms, which corresponds to a false positive rate of 39.3%.
On the other hand, Auto-Solid only reports 117 false alarms with a false
positive rate of 20.4%. Finally, Semi-Solid has an ever lower false positive
rate of 16.0%.

It is worth noting that the false positive rate for Semi-Solid can be further
reduced by spending additional effort in strengthening our refinement type
annotations. When performing this evaluation, we did not refine our initial
type annotations based on feedback from the type checker.

##### Cause of false positives for Auto-Solid

As expected, the cause of most false positives for Auto-Solid is due to the
limitations of the CHC solver. There are several cases where the CHC solver
times-out or returns unknown, causing Auto-Solid to report false positives.

##### Qualitative comparison against Verismart

We believe that Solid outperforms Verismart largely due to its ability to
express relationships between integers and aggregate properties of data
structures. In particular, while Verismart can reason about summations over
basic mappings, it cannot easily express aggregate properties of more complex
data structures.

Result for RQ2 and RQ4. In its fully automated mode, Solid has a false
positive rate of 20.4%. In contrast, Verismart has a significantly higher
false positive rate of 39.3%.

###  7.4. Running Time

Next, we investigate the running time of Solid and compare it against
Verismart. Table 4 gives statistics about the running time of each tool. As
expected, Semi-Solid is faster than Auto-Solid, as it does not need to rely on
the CHC solver to infer contract invariants. However, even Auto-Solid is
significantly faster than Verismart despite producing fewer false positives.

Result for RQ3 and RQ4: In its fully automated mode, Solid takes an average of
41 seconds to analyze each benchmark, and is significantly faster compared to
Verismart despite generating fewer false positives.

Dataset | Verismart |  Auto-Solid |  Semi-Solid
---|---|---|---
Verismart | 476 | 62 | 9
Etherscan | 425 | 24 | 10
Overall | 451 | 41 | 10
Table 4. Comparison of average running times in seconds

###  7.5. Impact of Type Inference

In this section, we perform an experiment to assess the impact of the type
inference procedure discussed in Section 5. Towards this goal, we consider the
following two ablations of Solid:

|  Solid-NoInfer |  Solid-NoSoft | Solid
---|---|---|---
False positive rate | 48.7% | 69.4% | 24.7%
Table 5. Experiments to evaluate type inference. This experiment is conducted
on the Etherscan benchmarks.

  * •

Solid-NoInfer: This is a variant of Solid that does not perform global type
inference to infer contract invariants. In particular, Solid-NoInfer uses true
as the type refinement of all state variables; however, it still performs
local type inference.

  * •

Solid-NoSoft: This variant of Solid differs from the type inference procedure
in Figure 11 in that it treats all overflow checks as hard constraints.

In this experiment, we compare the false positive rate of each ablated version
against Solid on the Etherscan benchmarks. The results of this experiment are
summarized in Table 5.

##### Importance of contract invariant inference.

As we can see by comparing Solid against Solid-NoInfer, global type inference
is quite important. In particular, if we do not infer contract invariants, the
percentage of false positives increases from 24.7% to 48.7%.

##### Importance of soft constraints.

Next, we compare the false positive rate of Solid against that of Solid-
NoSoft. Since Solid-NoSoft treats all overflow checks as hard constraints,
type inference fails if _any_ potential overflow in the contract cannot be
discharged. Since most contracts contain at least one unsafe overflow, Solid-
NoSoft fails for most benchmarks, meaning that all overflows are considered as
potentially unsafe. Thus, the false positive rate of Solid-NoSoft jumps from
24.7% to 69.4%.

###  7.6. Impact of the Type Checking Rules from Section 4.3

In this section, we describe an ablation study to assess the impact of the
more complex typing rules from Figure 10 for non-trivial mappings. Towards
this goal, we consider the following ablation:

|  Solid-NoNested | Solid
---|---|---
False positive rate | 39.0% | 23.5%
Table 6. Ablation study to evaluate rules from Section 4.3. This experiment is
conducted on Etherscan benchmarks that contain non-trivial mappings.

  * •

Solid-NoNested: This variant of Solid uses the simpler refinement type
checking rules from Section 4.2 but it does not utilize the typing rules from
Section 4.3 that pertain to complex data structures.

In this experiment, we compare Solid-NoNested against Solid on those contracts
from Etherscan that contain complex data structures. As shown in Table 6, the
more involved typing rules from Section 4.3 are quite important for
successfully discharging overflows in contracts with non-trivial mappings. In
particular, without our refinement templates from Section 4.3, the false
positive rate increases from 23.5% to 39.0% on these benchmarks.

Result for RQ5: Our proposed typing rules from Section 4.3 for more complex
data structures and the proposed type inference algorithm from Section 5 are
both important for achieving good results.

##  8\. Limitations

In this section, we discuss some of the limitations of both our type system as
well as prototype implementation. First, while logical qualifiers in SolType
express relationships between integers and aggregate properties of mappings,
they do not allow quantified formulas. In principle, there may be situations
that necessitate quantified refinements to discharge arithmetic safety;
however, this is not very common. Second, Solid uses an off-the-shelf CHC
solver to infer refinement type annotations. Since this problem is, in
general, undecidable, the CHC solver may return unknown or fail to terminate
in a reasonable time. In practice, we set a small time limit of 10 seconds per
call to the CHC solver. Third, Solid is designed with checking arithmetic
overflows in mind, so the proposed refinement typing rules may not be as
effective for checking other types of properties.

##  9\. Related Work

Smart contract correctness has received significant attention from the
programming languages, formal methods, and security communities in recent
years. In this section, we discuss prior work on refinement type systems and
smart contract security.

##### Refinement types

Our type system is largely inspired by and shares similarities with prior work
on liquid types (Rondon et al., 2008, 2010; Vazou et al., 2014a; Vekris et
al., 2016). For instance, our handling of temporary contract violations via
fetch/commit statements is similar to a simplified version of the fold and
unfold operators used in (Rondon et al., 2010). However, a key novelty of our
type system is its ability to express and reason about relationships between
relationships between integer variables and aggregate properties of complex
data structures (e.g., nested maps over struct) that are quite common in smart
contracts. Also, similar to the liquid type work, our system also performs
type inference; however, a key novelty in this regard is the use of soft
constraints to handle programs where not all arithmetic operations can be
proven safe.

##### Smart contract verification

Many popular security analysis tools for smart contracts are based on symbolic
execution (King, 1976). Well-known tools include Oyente (Luu et al., 2016),
Mythril (myt, 2018) and Manticore (man, 2016), and they look for an execution
path that violates a given property or assertion. In contrast to these tools,
our proposed approach is based on a refinement type system and offers stronger
guarantees compared to bug finding tools for smart contracts.

To bypass the scalability issues associated with symbolic execution,
researchers have also investigated sound and scalable static analyzers
(Grossman et al., 2018; Tsankov et al., 2018; Grech et al., 2018; Kalra et
al., 2018). Both Securify (Tsankov et al., 2018) and Madmax (Grech et al.,
2018) are based on abstract interpretation (Cousot and Cousot, 1977), which
does not suffer from the path explosion problem. ZEUS (Kalra et al., 2018)
translates Solidity code into the LLVM IR and uses an off-the-shelf verifier
to check the specified policy (Rakamaric and Emmi, 2014). The ECF (Grossman et
al., 2018) system is designed to specifically detect the DAO vulnerability. In
contrast to these techniques, the focus of our work is on proving arithmetic
safety which is a prominent source of security vulnerabilities.

Similar to Solid, Verismart (So et al., 2020) is also (largely) tailored
towards arithmetic properties of smart contracts. In particular, Verismart
leverages a CEGIS-style algorithm for inferring contract invariants. As we
show in our experimental evaluation, Solid outperforms Verismart in terms of
false positive rate as well as running time.

Some systems (Hirai, 2017; Grishchenko et al., 2018; Park et al., 2018;
Permenev et al., 2020) for reasoning about smart contracts rely on formal
verification. These systems typically prove security properties of smart
contracts using existing interactive theorem provers (coq, 2016), or leverage
temporal verification for checking functional correctness (Permenev et al.,
2020). They typically offer strong guarantees that are crucial to smart
contracts. However, unlike our system, all of them require significant manual
effort to encode the security properties and the semantics of smart contracts.
Furthermore, Solythesis (Li et al., 2020) inserts runtime checks into smart
contract source code to revert transactions that violate contract invariants.
We note that this approach is complementary to static verifier such as Solid.

##### Verifying overflow/underflow safety

The problem of checking integer overflow/underflow in software systems is a
well-studied problem in the verification community. In particular, Astree
(Blanchet et al., 2003) and Sparrow (Oh et al., 2014) are both based on
abstract interpretation (Cousot and Cousot, 1977) and are tailored towards
safety-critical code such as avionics software. As we argue throughout the
paper, verifying arithmetic safety of smart contracts requires reasoning about
aggregate properties over mappings; hence, standard numeric abstract domains
such as the ones used in Astree would not be sufficient for discharging over-
and under-flows in Solidity programs.

##### CHC Solving

We are not the first to use CHC solvers in the context of refinement type
checking. For example, Liquid Haskell (Vazou et al., 2014b) uses a predicate-
abstraction based horn clause solver for refinement type inference. However,
in contrast to our work, Liquid Haskell does not tackle the problem of MaxCHC
type inference, which is critical for discharging the maximum number of
runtime overflow checks in smart contracts.

To the best of our knowledge, the only prior work that can potentially address
our MaxCHC problem is in the context of network repair. In particular, (Hojjat
et al., 2016) formulate the problem of repairing buggy SDN configurations as
an optimization problem over constrained Horn clauses. They generalize their
proposed method to Horn clause optimization over different types of lattices,
and our type inference algorithm may be viewed as an instantiation of their
more general framework. However, in contrast to their approach, our algorithm
leverages domain-specific observations for efficient (but potentially
suboptimal) type inference in the context of smart contracts. In particular,
we use the fact that all soft constraints correspond to overflow checks that
are guaranteed to be satisfied (either because they are safe or we insert a
runtime check) to check each soft constraint independently.

##  10\. Conclusion

We have presented SolType, a refinement type system for Solidity that can be
used to prove the safety of arithmetic operations. Since integers in smart
contracts often correspond to financial assets (e.g., tokens), ensuring the
safety of arithmetic operation is particularly important in this context. One
of the distinguishing features of our type system is its ability to express
and reason about arithmetic relationships between integer variables and
aggregations over complex data structures such as multi-layer mappings. We
have implemented our proposed type system in a prototype called Solid, which
also has type inference capabilities. We have evaluated Solid on 120 smart
contracts from two datasets and demonstrated that it can fully automatically
discharge 86.3% of redundant SafeMath calls in our benchmarks. Furthermore,
Solid, even when used in a fully automated mode, significantly outperforms
Verismart, a state-of-the-art Solidity verifier, in terms of both false
positive rate and running time.

While the design of SolType was largely guided from the perspective of proving
arithmetic safety, our proposed type system could also be used for proving
other types of properties. In future work, we plan to explore the
applicability of our refinement type system in other settings and extend it
where necessary.

## References

  * (1)
  * coq (2016) 2016\.  The Coq Proof Assistant.  https://coq.inria.fr/.  [Online; accessed 01/09/2019].
  * att (2016) 2016\.  GovernMental’s 1100 ETH payout is stuck because it uses too much gas.  https://tinyurl.com/y83dn2yf/.  [Online; accessed 01/09/2019].
  * man (2016) 2016\.  Manticore.  https://github.com/trailofbits/manticore/.  [Online; accessed 01/09/2019].
  * att (2017a) 2017a.  On the parity wallet multisig hack.  https://tinyurl.com/yca83zsg/.  [Online; accessed 01/09/2019].
  * att (2017b) 2017b.  Understanding The DAO Attack.  https://tinyurl.com/yc3o8ffk/.  [Online; accessed 01/09/2019].
  * eth (2018) 2018\.  Etherscan.  https://etherscan.io/.  [Online; accessed 01/09/2019].
  * myt (2018) 2018\.  Mythril Classic.  https://github.com/ConsenSys/mythril-classic.  [Online; accessed 12/01/2018].
  * cas (2018a) 2018a.  Real Estate Business Integrates Smart Contracts.  https://tinyurl.com/yawrkfpx/.  [Online; accessed 01/09/2019].
  * cas (2018b) 2018b.  Smart contracts for shipping offer shortcut.  https://tinyurl.com/yavel7xe/.  [Online; accessed 01/09/2019].
  * Atzei et al. (2017) Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017\.  A Survey of Attacks on Ethereum Smart Contracts (SoK). In _Principles of Security and Trust - 6th International Conference, POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings_. 164–186.
  * Barnett et al. (2005) Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005\.  Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In _Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures_ _(Lecture Notes in Computer Science)_ , Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.), Vol. 4111. Springer, 364–387.
  * Bjørner et al. (2015) Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, and Andrey Rybalchenko. 2015.  _Horn Clause Solvers for Program Verification_.  Springer International Publishing, Cham, 24–51.  https://doi.org/10.1007/978-3-319-23534-9_2
  * Blanchet et al. (2003) Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003.  A static analyzer for large safety-critical software. In _Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003_ , Ron Cytron and Rajiv Gupta (Eds.). ACM, 196–207.
  * Cousot and Cousot (1977) Patrick Cousot and Radhia Cousot. 1977.  Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In _Proc. Symposium on Principles of Programming Languages_. 238–252.
  * De Moura and Bjørner (2008) Leonardo De Moura and Nikolaj Bjørner. 2008.  Z3: An efficient SMT solver. In _International conference on Tools and Algorithms for the Construction and Analysis of Systems_. Springer, 337–340.
  * Feist et al. (2019) Josselin Feist, Gustavo Grieco, and Alex Groce. 2019\.  Slither: a static analysis framework for smart contracts. In _Proceedings of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB@ICSE 2019, Montreal, QC, Canada, May 27, 2019_. IEEE / ACM, 8–15.
  * Flanagan et al. (2002) Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. 2002.  Extended Static Checking for Java. In _Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002_ , Jens Knoop and Laurie J. Hendren (Eds.). ACM, 234–245.
  * Grech et al. (2018) Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2018.  MadMax: surviving out-of-gas conditions in Ethereum smart contracts. In _Proc. International Conference on Object-Oriented Programming, Systems, Languages, and Applications_. 116:1–116:27.
  * Grishchenko et al. (2018) Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018\.  A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In _Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings_. 243–269.
  * Grossman et al. (2018) Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2018.  Online detection of effectively callback free objects with applications to smart contracts. In _Proc. Symposium on Principles of Programming Languages_. 48:1–48:28.
  * Hirai (2017) Yoichi Hirai. 2017\.  Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In _Financial Cryptography and Data Security - FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema, Malta, April 7, 2017, Revised Selected Papers_. 520–535.
  * Hojjat et al. (2016) Hossein Hojjat, Philipp Rümmer, Jedidiah McClurg, Pavol Černỳ, and Nate Foster. 2016\.  Optimizing horn solvers for network repair. In _2016 Formal Methods in Computer-Aided Design (FMCAD)_. IEEE, 73–80.
  * Kalra et al. (2018) Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018\.  ZEUS: Analyzing Safety of Smart Contracts. In _Proc. The Network and Distributed System Security Symposium_.
  * King (1976) James C King. 1976\.  Symbolic execution and program testing.  _Commun. ACM_ 19, 7 (1976), 385–394.
  * Komuravelli et al. (2014) Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014\.  SMT-Based Model Checking for Recursive Programs. In _Computer Aided Verification_ , Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 17–34.
  * Li et al. (2020) Ao Li, Jemin Andrew Choi, and Fan Long. 2020.  Securing smart contract with runtime validation. In _Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020_ , Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 438–453.  https://doi.org/10.1145/3385412.3385982
  * Luu et al. (2016) Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016.  Making Smart Contracts Smarter. In _Proc. Conference on Computer and Communications Security_. 254–269.
  * Mariano et al. (2020) Benjamin Mariano, Yanju Chen, Yu Feng, Shuvendu K Lahiri, and Isil Dillig. 2020.  Demystifying Loops in Smart Contracts. In _2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE)_. IEEE, 262–274.
  * Oh et al. (2014) Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. 2014.  Selective context-sensitivity guided by impact pre-analysis. In _ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014_ , Michael F. P. O’Boyle and Keshav Pingali (Eds.). ACM, 475–484.
  * Park et al. (2018) Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, and Grigore Rosu. 2018.  A formal verification tool for Ethereum VM bytecode. In _Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018_. 912–915.
  * Permenev et al. (2020) Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin T. Vechev. 2020\.  VerX: Safety Verification of Smart Contracts. In _2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020_. IEEE, 1661–1677.
  * Rakamaric and Emmi (2014) Zvonimir Rakamaric and Michael Emmi. 2014.  SMACK: Decoupling Source Language Details from Verifier Implementations. In _Proc. International Conference on Computer Aided Verification_. 106–113.
  * Rondon et al. (2008) Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008\.  Liquid types. In _Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008_. 159–169.
  * Rondon et al. (2010) Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2010\.  Low-level liquid types. In _Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010_. 131–144.
  * Smith et al. (2000) Frederick Smith, David Walker, and Greg Morrisett. 2000\.  Alias Types. In _Programming Languages and Systems_ , Gert Smolka (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 366–381.
  * So et al. (2020) S. So, M. Lee, J. Park, H. Lee, and H. Oh. 2020.  VERISMART: A Highly Precise Safety Verifier for Ethereum Smart Contracts. In _2020 IEEE Symposium on Security and Privacy (SP)_. IEEE Computer Society, Los Alamitos, CA, USA, 1678–1694.  https://doi.org/10.1109/SP40000.2020.00032
  * Solar-Lezama (2009) Armando Solar-Lezama. 2009\.  The sketching approach to program synthesis. In _Asian Symposium on Programming Languages and Systems_. Springer, 4–13.
  * Tsankov et al. (2018) Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin T. Vechev. 2018.  Securify: Practical Security Analysis of Smart Contracts. In _Proc. Conference on Computer and Communications Security_. 67–82.
  * Vazou et al. (2014a) Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014a.  Refinement types for Haskell. In _Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014_ , Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 269–282.
  * Vazou et al. (2014b) Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014b.  Refinement types for Haskell. In _Proceedings of the 19th ACM SIGPLAN international conference on Functional programming_. 269–282.
  * Vekris et al. (2016) Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. 2016\.  Refinement Types for TypeScript. In _Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Santa Barbara, CA, USA) _(PLDI ’16)_. Association for Computing Machinery, New York, NY, USA, 310–325.  https://doi.org/10.1145/2908080.2908110

##  Appendix A Expression Rules

Syntax and judgments:

$\begin{array}[]{r c l l}v&::=&&\textbf{Value}\\\
&&n\mid\operatorname{\mathsf{true}}\mid\operatorname{\mathsf{false}}\mid\\\
&\mid&\mathsf{mapping}[T](\overrightarrow{n_{i}\mapsto
v_{i}})\mid\mathop{\mathsf{struct}}S(\overrightarrow{x_{i}\mapsto v_{i}})\\\
\mathbb{E}&::=&&\textbf{Expression evaluation context}\\\
&&\cdot\mid\mathbb{E}\operatorname{\oplus}e_{2}\mid
v\operatorname{\oplus}\mathbb{E}&\\\ &\mid&\mathbb{E}\left[e_{2}\right]\mid
v_{1}\left[\mathbb{E}\right]\mid\mathbb{E}\left[e_{2}\mathop{\triangleleft}e_{3}\right]\mid
v_{1}\left[\mathbb{E}\mathop{\triangleleft}e_{3}\right]\mid
v_{1}\left[v_{2}\mathop{\triangleleft}\mathbb{E}\right]&\text{mapping
index/update}\\\
&\mid&\mathbb{E}\left[.x\right]\mid\mathbb{E}\left[.x\mathop{\triangleleft}e\right]\mid
v\left[.x\mathop{\triangleleft}\mathbb{E}\right]&\text{struct index/update}\\\
\\\ \lx@intercol\hfil e\to e^{\prime}\hfil\lx@intercol&\textbf{Expression
evaluation relation}\end{array}$

The expression evaluation relation $e\to e^{\prime}$ and the expression
evaluation context $\mathbb{E}$ have the standard meanings.

###  A.1. Expression Rules

We now present the operational semantics for expressions. First, we define
$\mathsf{ZeroVal}(T)$, the _zero value_ of a base type $T$, similar to how it
is defined in Solidity:

$\mathsf{ZeroVal(T)}=\begin{cases}0&\text{ if
}T=\operatorname{\mathsf{UInt}}\\\ \operatorname{\mathsf{false}}&\text{ if
}T=\operatorname{\mathsf{Bool}}\\\ \mathsf{mapping}[T]()&\text{ if
}T=\mathsf{Map}(T)\\\
\mathop{\mathsf{struct}}S(\overrightarrow{x_{i}\mapsto\mathsf{ZeroVal}(T_{i})})&\text{
if }T=\mathop{\mathsf{Struct}}S\text{ and }\forall
x_{i}.\Delta(S,x_{i})=T_{i}\end{cases}$

The evaluation rules are shown below. Here we subscript binary operations with
$\mathbb{N}$ to indicate an operation performed in the $\mathbb{N}$ domain
instead of as a syntactic object.

$\displaystyle\displaystyle{\hbox{\hskip
10.70398pt\vbox{\hbox{\hskip-10.70398pt\hbox{\hbox{$\displaystyle\displaystyle
e\to e^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
23.8985pt\vbox{\vbox{}\hbox{\hskip-23.8985pt\hbox{\hbox{$\displaystyle\displaystyle\mathbb{E}(e)\to\mathbb{E}(e^{\prime})$}}}}}}$
EE-Ctx $\displaystyle\displaystyle{\hbox{\hskip
24.45905pt\vbox{\hbox{\hskip-24.45903pt\hbox{\hbox{$\displaystyle\displaystyle
n=n_{1}+_{\mathbb{N}}n_{2}$}}}\vbox{}}}\over\hbox{\hskip
20.69238pt\vbox{\vbox{}\hbox{\hskip-20.69237pt\hbox{\hbox{$\displaystyle\displaystyle
n_{1}+n_{2}\to n$}}}}}}$ EE-Plus $\displaystyle\displaystyle{\hbox{\hskip
47.02808pt\vbox{\hbox{\hskip-47.02806pt\hbox{\hbox{$\displaystyle\displaystyle
n_{1}\geq_{\mathbb{N}}n_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
n=n_{1}-_{\mathbb{N}}n_{2}$}}}}\vbox{}}}\over\hbox{\hskip
18.47014pt\vbox{\vbox{}\hbox{\hskip-18.47014pt\hbox{\hbox{$\displaystyle\displaystyle
n_{1}-n_{2}\to n$}}}}}}$ EE-Minus $\displaystyle\displaystyle{\hbox{\hskip
83.87442pt\vbox{\hbox{\hskip-83.8744pt\hbox{\hbox{$\displaystyle\displaystyle
v_{M}=\mathsf{mapping}[T](n_{1}\mapsto v_{1},\dots,n_{i}\mapsto
v_{i},\dots,n_{k}\mapsto v_{k})$}}}\vbox{}}}\over\hbox{\hskip
19.26155pt\vbox{\vbox{}\hbox{\hskip-19.26154pt\hbox{\hbox{$\displaystyle\displaystyle
v_{m}\left[n_{i}\right]\to v_{i}$}}}}}}$ EE-MapInd1
$\displaystyle\displaystyle{\hbox{\hskip
26.88393pt\vbox{\hbox{\hskip-26.88393pt\hbox{\hbox{$\displaystyle\displaystyle\not\exists
i.\ n_{i}=n$}}}\vbox{}}}\over\hbox{\hskip
93.87036pt\vbox{\vbox{}\hbox{\hskip-93.87036pt\hbox{\hbox{$\displaystyle\displaystyle\left(\mathsf{mapping}[T](n_{1}\mapsto
v_{1},\dots,n_{k}\mapsto
v_{k})\right)\left[n\right]\to\mathsf{ZeroVal(T)}$}}}}}}$ EE-MapInd2
$\displaystyle\displaystyle{\hbox{\hskip
83.87442pt\vbox{\hbox{\hskip-83.8744pt\hbox{\hbox{$\displaystyle\displaystyle
v_{M}=\mathsf{mapping}[T](n_{1}\mapsto v_{1},\dots,n_{i}\mapsto
v_{i},\dots,n_{k}\mapsto v_{k})$}}}\vbox{}}}\over\hbox{\hskip
93.3675pt\vbox{\vbox{}\hbox{\hskip-93.3675pt\hbox{\hbox{$\displaystyle\displaystyle
v_{M}\left[n_{i}\mathop{\triangleleft}v\right]\to\mathsf{mapping}[T](n_{1}\mapsto
v_{1},\dots,n_{i}\mapsto v,\dots,n_{k}\mapsto v_{k})$}}}}}}$ EE-MapUpd1
$\displaystyle\displaystyle{\hbox{\hskip
103.64163pt\vbox{\hbox{\hskip-103.64162pt\hbox{\hbox{$\displaystyle\displaystyle
v_{M}=\mathsf{mapping}[T](n_{1}\mapsto v_{1},\dots,n_{k}\mapsto v_{k})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\not\exists i.\
n_{i}=n$}}}}\vbox{}}}\over\hbox{\hskip
86.85487pt\vbox{\vbox{}\hbox{\hskip-86.85486pt\hbox{\hbox{$\displaystyle\displaystyle
v_{M}\left[n\mathop{\triangleleft}v\right]\to\mathsf{mapping}[T](n_{1}\mapsto
v_{1},\dots,n_{k}\mapsto v_{k},n\mapsto v)$}}}}}}$ EE-MapUpd2
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
84.98846pt\vbox{\vbox{}\hbox{\hskip-84.98846pt\hbox{\hbox{$\displaystyle\displaystyle\left(\mathop{\mathsf{struct}}S(x_{1}\mapsto
v_{1},\dots,x_{i}\mapsto v_{i},\dots,x_{k}\mapsto
v_{k})\right)\left[.x_{i}\right]\to v_{i}$}}}}}}$ EE-SctInd
$\displaystyle\displaystyle{\hbox{\hskip
73.46034pt\vbox{\hbox{\hskip-73.46033pt\hbox{\hbox{$\displaystyle\displaystyle
v_{R}=\mathop{\mathsf{struct}}S(x_{1}\mapsto v_{1},\dots,x_{i}\mapsto
v_{i},\dots,x_{k}\mapsto v_{k})$}}}\vbox{}}}\over\hbox{\hskip
85.03209pt\vbox{\vbox{}\hbox{\hskip-85.03207pt\hbox{\hbox{$\displaystyle\displaystyle
v_{R}\left[.x_{i}\mathop{\triangleleft}v\right]\to\mathop{\mathsf{struct}}S(x_{1}\mapsto
v_{1},\dots,x_{i}\mapsto v,\dots,x_{k}\mapsto v_{k})$}}}}}}$ EE-SctUpd

All of these rules are standard with the exception of the mapping rules. The
EE-MapInd1 rule retrieves the accessed value if it is contained in the
mapping; otherwise, the EE-MapInd2 rule returns the zero value of the value
type. Similarly, EE-MapUpd1 replaces the currently existing entry if the key
exists; otherwise, the key is added to the mapping in EE-MapUpd2.

###  A.2. Template Families

We introduce new, less ambiguous notation for constructing the templates used
for the TE-MapInd and TE-MapUpd rules. A _template family_ is a function
$\mathcal{H}$ that takes a pair $T,T_{h}$ and produces a set of tuples of
templates of sort $T$ that can be synthesized using holes of type
$\mathsf{Map}(T_{h}),T_{h}$ (resp.), along with the access path $w$ used.

$\mathcal{H}(T,T_{h})=\\{(H_{1},H_{2},w)\mid\mathsf{Map}(T_{h})\VDash
H_{1}:T,w\text{ and }T_{h}\VDash H_{2}:T,w\\}$

Observe that for any given pair of $T$ and $T_{h}$, $\mathcal{H}(T,T_{h})$
will be finite, so by convention we assume that there exists a unique ordering

$\mathcal{H}(T,T_{h})=\\{(H_{11},H_{12},w_{1}),\dots,(H_{n1},H_{n2},w_{n})\\}$

###  A.3. New Notation in TE-MapInd and TE-MapUpd Rules

Using the template family notation, we update the TE-MapInd and TE-MapUpd
rules:

$\displaystyle\displaystyle{\hbox{\hskip
158.9534pt\vbox{\hbox{\hskip-75.2776pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathsf{Map}(T)\qquad\Gamma;\gamma\vdash
e_{2}:\operatorname{\mathsf{UInt}}$}}}\vbox{\hbox{\hskip-158.9534pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{H}(\operatorname{\mathsf{UInt}},T)=\\{(H_{i1},H_{i2},w_{i}),\dots,(H_{\ell
1},H_{\ell 2},w_{\ell})\\}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi_{a}=\bigwedge_{i=1}^{\ell}H_{i2}(\nu)\leq
H_{i1}(e_{1})$}}}}\vbox{}}}}\over\hbox{\hskip
74.75238pt\vbox{\vbox{}\hbox{\hskip-74.75238pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}[e_{2}]:\\{\nu:T\mid\nu=e_{1}[e_{2}]\land\phi_{a}\\}$}}}}}}$ TE-MapInd
$\displaystyle\displaystyle{\hbox{\hskip
208.43645pt\vbox{\hbox{\hskip-109.16896pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}:\mathsf{Map}(T)\qquad\Gamma;\gamma\vdash
e_{2}:\operatorname{\mathsf{UInt}}\qquad\Gamma;\gamma\vdash
e_{3}:T$}}}\vbox{\hbox{\hskip-208.43643pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{H}(\operatorname{\mathsf{UInt}},T)=\\{(H_{i1},H_{i2},w_{i}),\dots,(H_{\ell
1},H_{\ell 2},w_{\ell})\\}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi_{a}=\bigwedge_{i=1}^{\ell}\left(H_{i1}(\nu)=H_{i1}(e_{1})-H_{i2}(e_{1}[e_{2}])+H_{i2}(e_{3})\right)$}}}}\vbox{}}}}\over\hbox{\hskip
97.06992pt\vbox{\vbox{}\hbox{\hskip-97.0699pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
e_{1}\left[e_{2}\mathop{\triangleleft}e_{3}\right]:\\{\nu:\mathsf{Map}(T)\mid\nu=e_{1}\left[e_{2}\mathop{\triangleleft}e_{3}\right]\land\phi_{a}\\}$}}}}}}$
TE-MapUpd

###  A.4. Typing Rules Omitted in the Main Text

We omitted some typing rules in the main text, notably that of the constants,
so we provide them here.

$\displaystyle\displaystyle{\hbox{\hskip
36.36784pt\vbox{\hbox{\hskip-36.36784pt\hbox{\hbox{$\displaystyle\displaystyle
0\leq_{\mathbb{N}}n\leq_{\mathbb{N}}\mathsf{MaxInt}$}}}\vbox{}}}\over\hbox{\hskip
54.29454pt\vbox{\vbox{}\hbox{\hskip-54.29453pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
n:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu=n\\}$}}}}}}$ TE-Nat
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
61.93121pt\vbox{\vbox{}\hbox{\hskip-61.9312pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash\operatorname{\mathsf{true}}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu=\operatorname{\mathsf{true}}\\}$}}}}}}$
TE-True $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
63.34789pt\vbox{\vbox{}\hbox{\hskip-63.34787pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash\operatorname{\mathsf{false}}:\\{\nu:\operatorname{\mathsf{UInt}}\mid\nu=\operatorname{\mathsf{false}}\\}$}}}}}}$
TE-False $\displaystyle\displaystyle{\hbox{\hskip
148.75145pt\vbox{\hbox{\hskip-148.75145pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
all $\displaystyle x_{i}$ such that
}\Delta(S,x_{i})=T_{i},\qquad\Gamma;\gamma\vdash v_{i}:T_{i}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathop{\mathsf{struct}}S(\overrightarrow{x_{i}\mapsto
v_{i}})$}}}}\vbox{}}}\over\hbox{\hskip
61.44955pt\vbox{\vbox{}\hbox{\hskip-61.44955pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
v:\\{\nu:\mathop{\mathsf{Struct}}S\mid\nu=v\\}$}}}}}}$ TE-StructConst
$\displaystyle\displaystyle{\hbox{\hskip
189.07347pt\vbox{\hbox{\hskip-164.70891pt\hbox{\hbox{$\displaystyle\displaystyle\text{for
$\displaystyle i=1\dots k$,}\qquad\Gamma;\gamma\vdash v_{i}:T$}\hskip
20.00003pt\hbox{\hskip-189.07346pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{H}(\operatorname{\mathsf{UInt}},T)=\\{(H_{11},H_{12},w_{1}),\dots,(H_{\ell
1},H_{\ell 2},w_{\ell})\\}$}\hskip
20.00003pt\hbox{\hskip-162.68013pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathsf{mapping}[T](n_{1}\mapsto v_{1},\dots,n_{k}\mapsto v_{k})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi=\bigwedge_{j=1}^{\ell}H_{j1}(\nu)=\mathsf{ConstAgg}(T,H_{j1},w_{j},v)$}}}}}}}}\vbox{\hbox{\hskip-189.07346pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{H}(\operatorname{\mathsf{UInt}},T)=\\{(H_{11},H_{12},w_{1}),\dots,(H_{\ell
1},H_{\ell 2},w_{\ell})\\}$}\hskip
20.00003pt\hbox{\hskip-162.68013pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathsf{mapping}[T](n_{1}\mapsto v_{1},\dots,n_{k}\mapsto v_{k})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi=\bigwedge_{j=1}^{\ell}H_{j1}(\nu)=\mathsf{ConstAgg}(T,H_{j1},w_{j},v)$}}}}}}\vbox{\hbox{\hskip-162.68013pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathsf{mapping}[T](n_{1}\mapsto v_{1},\dots,n_{k}\mapsto v_{k})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\phi=\bigwedge_{j=1}^{\ell}H_{j1}(\nu)=\mathsf{ConstAgg}(T,H_{j1},w_{j},v)$}}}}\vbox{}}}}}\over\hbox{\hskip
70.37141pt\vbox{\vbox{}\hbox{\hskip-70.37141pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\gamma\vdash
v:\\{\nu:\mathsf{Map}(T)\mid\nu=v\land\phi\\}$}}}}}}$ TE-MappingConst

$\displaystyle\mathsf{ConstAgg}(T,H,w_{j},v)$
$\displaystyle=\begin{cases}\bot&\text{if }H=\square\\\
\mathsf{ConstSum}(w,v)&\text{if
}H=\operatorname{\mathsf{Sum}}(H^{\prime})\text{ and
}T=\operatorname{\mathsf{UInt}}\end{cases}$
$\displaystyle\mathsf{ConstSum}(w,v)$ $\displaystyle=\begin{cases}n&\text{if
}v=n\\\ \sum_{i=1}^{k}\mathsf{ConstSum}(w,v_{i})&\text{if
}v=\mathsf{mapping}[T](\overrightarrow{n_{i}\mapsto v_{i}})\text{ for
}i=1\dots k\\\ \mathsf{ConstSum}(w^{\prime},v^{\prime})&\text{if
}w=xw^{\prime}\text{ and }v=\mathop{\mathsf{struct}}S(\dots,x\mapsto
v^{\prime},\dots)\end{cases}$

The TE-True and TE-False rules are standard. The TE-StructConst rule directly
refines the type of a struct constant with its exact concrete value, since a
struct can be directly encoded into SMT in our chosen theory. The TE-Nat rule
is similar to what would be an integer typing rule in a typical type system,
except that it explicitly enforces the number to be within machine bounds.
Note that this only affects numbers appear in the program and does not
necessarily include numbers appearing in refinements.

The most interesting rule is TE-MappingConst. Similar to TE-StructConst, the
type of a mapping constant is refined with its exact concrete value (since the
number of values is finite), but further includes the clause $\phi$ that sets
the values of the synthesized symbolic sum functions. Specifically, $\phi$
equates the symbolic value $H_{j1}(\nu)$ representing the aggregation to the
concrete, numerical value of the aggregation computed by the
$\mathsf{ConstAgg}$ helper function.

$\mathsf{ConstAgg}(T,H,w,v)$ computes the concrete value of the aggregation of
$v$, where the aggregated values are only those obtained by accessing the
struct fields in $w$. In our presentation, we only have the sum aggregation,
which is computed by the $\mathsf{ConstSum}$ helper function.
$\mathsf{ConstSum}(w,v)$ computes the concrete sum of a number, mapping, or
struct field in the natural number domain.

###### Example 0.

Suppose $v_{i}=\mathop{\mathsf{struct}}S(x_{a}\mapsto i,x_{b}\mapsto 1)$ for
$i=1,\dots,10$. Then if
$v=\mathsf{mapping}[\mathop{\mathsf{Struct}}S](\overrightarrow{i\mapsto
v_{i}})$, then

$\displaystyle\mathsf{ConstSum}(x_{a},v)$ $\displaystyle=55$
$\displaystyle\mathsf{ConstSum}(x_{b},v)$ $\displaystyle=10$

##  Appendix B Progress and Preservation for Expressions

###  B.1. Some useful lemmas

###### Lemma 0 (Zero values are well-typed).

For every $T$, there exists a $\tau$ such that
$\Gamma;\gamma\vdash\mathsf{ZeroVal}(T):\tau$ and
$\Gamma;\gamma\vDash\tau<:T$.

###### Proof.

By induction on $T$. ∎

###### Lemma 0 (Inversion for evaluation context type).

If $\Gamma;\gamma\vdash\mathbb{E}(e):\tau$, then there exists a
$\tau^{\prime}$ such that $\Gamma;\gamma\vdash e:\tau^{\prime}$.

###### Proof sketch.

By induction. ∎

###### Lemma 0 (Well-typedness of swapping evaluation context argument).

If $\Gamma;\gamma\vdash\mathbb{E}(e):\tau$ and $\Gamma;\gamma\vdash
e:\tau^{\prime}$ and $\Gamma;\gamma\vdash e^{\prime}:\tau^{\prime}$, then
$\Gamma;\gamma\vdash\mathbb{E}(e^{\prime}):\tau$.

###### Proof sketch.

By induction. ∎

###  B.2. Relating symbolic sum functions to their concrete counterparts

The following lemma shows that the $\mathsf{ConstSum}$ function is well-
defined with respect to the aggregation function templates synthesized for the
TE-MapInd and TE-MapUpd rules. Furthermore, it relates the symbolic value of
an aggregation of mapping (i.e. some sum function) to the concrete value of
the aggregation.

###### Lemma 0 (Correctness of template synthesis for Sum).

Suppose

(8) $\displaystyle(H_{1},H_{2},w)$
$\displaystyle\in\mathcal{H}(\operatorname{\mathsf{UInt}},T)$ (9)
$\displaystyle H_{1}$
$\displaystyle=\operatorname{\mathsf{Sum}}(H_{1}^{\prime})$ (10)
$\displaystyle v$ $\displaystyle=\mathsf{mapping}[T](n_{1}\mapsto
v_{1},\dots,n_{k}\mapsto v_{k})$ (11) $\displaystyle\forall v_{i},\quad$
$\displaystyle\Gamma;\gamma\vdash v_{i}:T$

and let $\phi$ be the additional clauses generated when encoding $v$ into SMT.
Then $\mathsf{ConstSum}(w,v)$ is well-defined, and for all $v_{i}$, the
formula

(12) $\phi\implies\mathsf{Encode}(H_{2}(v_{i})=\mathsf{ConstSum}(w,v_{i}))$

is valid.

###### Example 0.

Consider the mapping

$\begin{array}[]{l}v=\mathsf{mapping}[\mathop{\mathsf{Struct}}S](\\\ \qquad
1\mapsto\mathop{\mathsf{struct}}S(a\mapsto\mathsf{mapping}[\operatorname{\mathsf{UInt}}](5\mapsto
11)),\\\ \qquad
2\mapsto\mathop{\mathsf{struct}}S(a\mapsto\mathsf{mapping}[\operatorname{\mathsf{UInt}}](4\mapsto
6,10\mapsto 3))\\\ )\end{array}$

It is only possible to sum over the nested mapping values at the $a$ field in
each struct, so the templates corresponding to this mapping are

$\displaystyle H_{1}$
$\displaystyle=\operatorname{\mathsf{Sum}}(\operatorname{\mathsf{Flatten}}(\operatorname{\mathsf{Fld}}_{a}(\square)))$
$\displaystyle H_{2}$ $\displaystyle=\operatorname{\mathsf{Sum}}(\square[.a])$
$\displaystyle\mathcal{H}(\operatorname{\mathsf{UInt}},\mathop{\mathsf{Struct}}S)$
$\displaystyle=\\{(H_{1},H_{2},a)\\}$

Let us write $v_{2}$ to be the struct value at index 2 of $v$. The concrete
aggregation values of $v$ and $v_{2}$ are given, respectively, by

$\displaystyle\mathsf{ConstSum}(a,v)$ $\displaystyle=11+6+3=20$
$\displaystyle\mathsf{ConstSum}(a,v_{2})$ $\displaystyle=6+3=9$

Intuitively, the value of $\operatorname{\mathsf{Sum}}(v_{2}[.a])$ should be
equal to the concrete sum $\mathsf{ConstSum}(a,v_{2})$, which is what the
lemma says:

$H_{2}(v_{2})=\operatorname{\mathsf{Sum}}(v_{2}[.a])=9$

This concludes the example of Lemma 4.

###### Proof of Lemma 4.

By induction on $T$.

  * •

Case $T=\operatorname{\mathsf{UInt}}$: By inversion of the derivation of the
synthesis judgment used for $H_{2}$, we see that the derivation must have used
TH-Hole, so

(13) $\displaystyle H_{2}(v_{i})$ $\displaystyle=v_{i}$ (14) $\displaystyle w$
$\displaystyle=\epsilon$

By inversion on the derivation of Eq. (11), we must have $v_{i}\in\mathbb{N}$.
Thus, we have

$\mathsf{ConstSum}(w,v)=\sum_{j=1}^{k}v_{j}$

The required result follows immediately.

  * •

Case $T=\mathsf{Map}(T^{\prime})$: By definition of $\mathcal{H}$, we have

(15) $\mathsf{Map}(T^{\prime})\VDash H_{2}:\operatorname{\mathsf{UInt}},w$

By inversion on the derivation of this judgment, we see that TH-Sum must have
been used.

(16) $\displaystyle H_{2}$
$\displaystyle=\operatorname{\mathsf{Sum}}(H_{2}^{\prime})$ (17)
$\displaystyle\mathsf{Map}(T^{\prime})$ $\displaystyle\VDash
H_{2}^{\prime}:\mathsf{Map}(\operatorname{\mathsf{UInt}}),w$

By inversion on the derivation of Eq. (11), we see that TE-MapConst must have
been used.

(18) $\displaystyle v_{i}$
$\displaystyle=\mathsf{mapping}[T^{\prime}](n_{1}\mapsto
v_{1}^{\prime},\dots,n_{q}\mapsto v_{q}^{\prime})$

Note that there must exist at least one $H_{2}^{\prime\prime}$ such that
$(H_{2},H_{2}^{\prime\prime},w)\in\mathcal{H}(\operatorname{\mathsf{UInt}},T^{\prime})$.
By applying the inductive hypothesis, we see that for every $p=1\dots q$,
$\mathsf{ConstSum}(w,v_{p}^{\prime})$ is well-defined. Thus, we have

(19)
$\mathsf{ConstSum}(w,v_{i})=\sum_{p=1}^{q}\mathsf{ConstSum}(w,v_{p}^{\prime})$

So $\mathsf{ConstSum}(w,v)$ is well-defined as well. It follows that the
following formula appears in the type of $v_{i}$:

(20) $\displaystyle H_{2}(\nu)$
$\displaystyle=\sum_{p=1}^{q}\mathsf{ConstSum}(w,v_{p}^{\prime})$

The required result follows by transitivity of equality.

  * •

Case $T=\mathop{\mathsf{Struct}}S$: By inversion on the derivation of Eq.
(11), we must have

(21) $\displaystyle v_{i}$
$\displaystyle=\mathop{\mathsf{struct}}S(\dots,x\mapsto v_{i}^{\prime},\dots)$
(22) $\displaystyle\Delta(S,x)$ $\displaystyle=T^{\prime}$ (23)
$\displaystyle\Gamma;\gamma$ $\displaystyle\vdash v_{i}^{\prime}:T^{\prime}$

By definition of $\mathcal{H}$, we have

(24) $\mathop{\mathsf{Struct}}S\VDash H_{2}:\operatorname{\mathsf{UInt}},w$

By inversion, the derivation of Eq. (24), must have used TH-Hole as the very
first axiom, followed by an application of TH-FldAcc.

$\displaystyle\displaystyle{\hbox{\hskip
103.27345pt\vbox{\hbox{\hskip-103.27344pt\hbox{\hbox{$\displaystyle\displaystyle\raise
11.44443pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
89.73177pt\vbox{\hbox{\hskip-89.73175pt\hbox{\hbox{$\displaystyle\displaystyle\raise
11.44443pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
88.0651pt\vbox{\hbox{\hskip-88.0651pt\hbox{\hbox{$\displaystyle\displaystyle\raise
10.38887pt\hbox{\hbox to0.0pt{\hss$\displaystyle\hbox{\small\small{TH-
Hole}}\;$}$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
49.13368pt\vbox{\vbox{}\hbox{\hskip-49.13368pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{\mathsf{Struct}}S\VDash\square:\mathop{\mathsf{Struct}}S,\epsilon$}}}}}}$}}\hbox{}$
}\qquad\Delta(S,x)=T^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
46.8932pt\vbox{\vbox{}\hbox{\hskip-46.89319pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{\mathsf{Struct}}S\VDash\square[.x]:T^{\prime},x$}}}}}}$}}\hbox{\hbox{}\hbox
to0.0pt{$\displaystyle\;\hbox{\small\small{TH-FldAcc}}$\hss}}$
}$}}}\vbox{}}}\over\hbox{\hskip
62.7687pt\vbox{\vbox{}\hbox{\hskip-62.76869pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{\mathsf{Struct}}S\VDash
H_{2}^{\prime}(\square[.x]):T^{\prime\prime},xw^{\prime\prime}$}}}}}}$}}\hbox{}$
}$}\hskip