centerframe[1][]

# The Move Borrow Checker

Sam Blackshear  Mysten LabsUSA<EMAIL_ADDRESS>,  John Mitchell
StanfordUSA<EMAIL_ADDRESS>,  Todd Nowacki  Mysten LabsUSA
<EMAIL_ADDRESS>and  Shaz Qadeer  MetaUSA<EMAIL_ADDRESS>
###### Abstract.

The Move language provides abstractions for programming with digital assets
via a mix of value semantics and reference semantics. Ensuring memory safety
in programs with references that access a shared, _mutable_ global ledger is
difficult, yet essential for the use-cases targeted by Move. The language
meets this challenge with a novel memory model and a modular, intraprocedural
static reference safety analysis that leverages key properties of the memory.
The analysis ensures the absence of memory safety violations in all Move
programs (including ones that link against untrusted code) by running as part
of a load-time _bytecode verification_ pass similar to the JVM (Lindholm and
Yellin, 1997) and CLR (Meijer et al., 2000). We formalize the static analysis
and prove that it enjoys three desirable properties: absence of dangling
references, referential transparency for immutable references, and absence of
memory leaks.

*Author names are in alphabetical order

††conference: ; ; ††doi: ††copyright: none††ccs: Software and its engineering
General programming languages††ccs: Social and professional topics History of
programming languages

##  1\. Introduction

The Move language(for double-blind review, 2019b) provides abstractions for
writing safe _smart contracts_ (Szabo, 1997; Wood, 2014) via a mix of value
semantics and reference semantics. Programmers can use value semantics and the
move operator to transfer ownership of an asset to another user or to a
procedure. For example, a procedure signature like fun buy(c: Coin): Car
intuitively says: “if you give me ownership of a coin, I will give you
ownership of a car”. By contrast, references enable programmers to temporarily
share a value for reading or writing. The signature fun register(c: &Car, fee:
Coin): Registration says “if you show me that you own a car and pay a fee, I
will give you a registration for the car”.

However, careless mixing of value and reference semantics can lead to memory
safety issues. Code like let x = 5; return &x creates a dangling reference to
local memory (as in C). In addition, the move operator introduces new kinds of
reference errors: let y = move x; *x (“use-after-move”, similar to a null
dereference) and let y = &x; let z = move x; (y is a dangling reference to
moved memory).

Smart contract languages like Move must prevent memory safety issues _by
design_ because they need to support deterministic execution in an adversarial
environment.

#### Deterministic execution

A blockchain is a replicated state machine (Lamport, 1984; Schneider, 1990)
where replicas are known as _validators_. Users in the system send
transactions (i.e., programs in a language like Move) to a validator that
advances the state machine. The validators execute a consensus protocol (e.g.,
(Nakamoto, 2008; for double-blind review, 2019c)) to agree on the ordering and
results of executing transactions. State-machine replication requires
determinism; if execution is nondeterministic, validators may not achieve
consensus and the system cannot make progress. Since violation of memory
safety typically manifests as undefined behavior, the resulting nondeterminism
could stall the entire system.

#### Adversarial environment

Smart contracts deployed on a blockchain store digital assets with real-world
value, but must tolerate arbitrary interactions with untrusted code running in
the same address space. Even if the deployed code is completely safe on its
own, an attacker can intentionally write memory-unsafe code that attempts to
break the integrity of the deployed code. Thus, Move must prevent memory
safety issues in _both_ the deployed code and the attacker code.

#### Existing approaches are inadequate

Unfortunately, traditional approaches for ensuring memory safety are not
suitable for Move’s deployment model. For example, Move cannot rely on a
source language with a strong type system (e.g., Rust, OCaml) to prevent
memory safety issues because Move _bytecode_ is stored and executed on the
ledger. An attacker that wishes to subvert the source-level type system can
write and deploy bytecode directly.

Similarly, Move cannot utilize GC for safe memory management. Like other
blockchain languages, Move uses _gas metering_(Grech et al., 2020) to provide
a deterministic metric for execution cost of contracts. The gas cost of a
program must closely track its execution time to avoid denial-of-service
vulnerabilities(Pérez and Livshits, 2020). The unpredictable nature of GC does
not mix well with the precise accounting required by gas metering.

#### Contributions

Move must support a rich programming model. An account-based blockchain is a
shared, _mutable_ global ledger. A single transaction can mutate an arbitrary
number of accounts in the ledger (e.g., by sending funds to each). Move must
expose a programming model that supports mutable references to global state,
but without sacrificing reference safety.

Move addresses safe programming of smart contracts by chaining together three
new ideas. First, memory management in Move is built atop a forest of tree-
shaped values. The roots of this forest are either local variables on the call
stack or global memory indexed by a statically-known type and dynamically
determined account address. Move allows the creation of references to values
and embedded sub-values, but does not allow references to be embedded inside a
value. This design ensures that a reference can be canonically represented as
a rooted path of fields.

Second, Move imposes the abstraction of a directed and acyclic borrow graph
over the forest of values comprising the program memory. The nodes in this
borrow graph are abstract locations representing values on the call stack,
values indexed by a particular type in global memory, or references stored on
the call stack or operand stack. Each edge in the borrow graph is labeled by a
relative path indicating an ownership transfer along that path.

Third, Move provides an intraprocedural static analysis to automatically check
that a Move bytecode program adheres to the ownership discipline enforced by
the borrow graph abstraction. This analysis ensures important properties —no
memory leaks, no dangling references, and referential transparency— on Move
bytecode programs.

We have implemented our analysis in the Move bytecode verifier which is run
whenever new bytecode is loaded into the Anon blockchain(for double-blind
review, 2019a), in a manner similar to the JVM (Lindholm and Yellin, 1997) and
CLR (Meijer et al., 2000). Therefore, runtime memory-safety properties are
enforced on all loaded bytecode regardless of provenance. Our implementation
is fast; we report numbers in $\S\ref{sec:evaluation}$.

We have also implemented our analysis in the compiler for the Move source
language. The Move language is being used by Anon developers to implement the
rules governing the Anon Payment Network. Anecdotal experience indicates that
the source borrow checker is a useful tool that helps developers write safe
code.

##  2\. Language Design for Reference Safety

In this section, we will first give an overview of memory management in the
Move language with emphasis on the key feature for facilitating static
analysis: tree-shaped values that enable us to represent reference values as
structured paths (§2.1).

Next, we present a static analysis that builds on these features to prevent
dangling references. We organize our discussion around the three primary
challenges our analysis faces: preventing dangling references to memory in the
same procedure (§2.2), to memory in different procedures (§2.3), and to global
memory (§2.4). The global reference analysis leverages Move’s type-indexed
global memory and encapsulation features to enforce a global property with
intraprocedural checks.

Each of the analysis sections contain examples of bad Move code that must be
rejected. The analysis operates on Move bytecode, but we will write our
examples in Move source code for readability. The table below summarizes how
source code instructions compile to stack-based bytecode instructions.

x = &y | ${{\bf{BorrowLoc}}}\left<y\right>;{{\bf{StoreLoc}}}\left<x\right>$
---|---
x = &y.f | ${{\bf{BorrowField}}}\left<f,y\right>;{{\bf{StoreLoc}}}\left<x\right>$
x = *y | ${{\bf{CopyLoc}}}\left<y\right>;{\bf{ReadRef}};{{\bf{StoreLoc}}}\left<x\right>$
*x = y | ${{\bf{MoveLoc}}}\left<y\right>;{{\bf{BorrowLoc}}}\left<x\right>;{\bf{WriteRef}}$

Although the source language abstracts away some bytecode features such as the
operand stack, we have chosen examples that capture the essence of reference
issues in the bytecode.

###  2.1. Memory management

Move has three kinds of storage:

  1. (1)

Procedure-local variables Each procedure frame in the call stack has a fixed
set of local variables that are uninitialized at the beginning of a procedure.
Initialized variables can store values and references.

  2. (2)

Shared operand stack All procedures in the call stack share a single operand
stack that can store both values and references. Procedures can use the
operand stack both for local computation and to share arguments/return values
with other procedures. At the beginning of program execution, the call stack
holds one frame and the operand stack is empty. The same conditions must hold
for a program to terminate without an error.

  3. (3)

Global storage Move has no global variables, no heap, and cannot access the
filesystem or network. However, programs can access persistent data by reading
from and writing to shared global storage that persists across program
executions. Global storage is organized as a partial map from 16 byte _account
addresses_ to record values:
($\textsf{Addr}\times\textsf{Type})\rightharpoonup\textsf{Record}$. § 2.4
explains the design of and motivation for the global storage in more detail.

#### Values are Tree-Shaped

Move has primitive data values, nominally typed records, resizable vectors,
and reference values. Move programmers can create references that point into
local variables or into global storage, but not into the operand stack.
Reference types are tagged with _permissions_ : either mutable (written &mut
T) or immutable (written &T). References to other references (e.g., &&u64) are
not allowed.

Both records and vectors can store primitive values, and other
records/vectors, but not references. Global storage can hold records, but not
references. This ensures that non-reference values and the global storage are
always tree-shaped.

#### References are Structured Paths

In a byte-addressable memory, a reference value is a dynamically determined
index into the array of memory. This unstructured representation makes it
difficult to reason about the relationship between two different reference
values–e.g., “can writing through reference i change the memory pointed to by
reference j?”

By contrast, Move storage, values, and reference-related instructions are
designed to ensure that a reference can be represented as a structured _access
path_ (Jones and Muchnick, 1979). For example: say we have a record value { f:
{ g: 1 }, h: [2,3] } of type T, where the { syntax denotes a record and the [
syntax denotes a vector. If this value is stored in a local variable x, we can
represent a reference to the value stored by field g as the path x/f/g.
Similarly, we can represent a reference stored at index 1 of the vector in
field h as x/h/1. If the same record value is in global storage at account
address A, we can represent these paths as A/T/f/g and A/T/h/1.

A path is a canonical representation for a particular location in memory.
Syntactically distinct paths refer to distinct memory locations. In addition,
the structured nature of paths introduces a partial order on reference values.
Two reference values either have a prefix relationship (e.g., x/f is a prefix
of x/f/g), an extension relationship (e.g., x/f/g is an extension of x/f), or
are incomparable (e.g., y/f/g and x/f/g). Writing to a path cannot change the
memory named by incomparable paths. As we will see, our reference safety
analysis takes advantage of these nice properties to simplify static reasoning
about code that uses references.

###  2.2. Preventing Dangling References to Locals

We begin our discussion of the reference safety analysis with a pair of code
snippets that exemplify the problems the analysis must prevent. The code
comments in the snippet show the abstract state of the analysis, but we will
ignore them at first.

The program below creates a reference r to the f field of formal parameter c,
_moves_ the value stored in c into x and then reads r. The move assignment
works by assigning the value bound to c to x and then “clearing” c by
assigning it to $\bot$.

⬇

fun dangle_after_move(c: Coin) {

let r = &c.f; //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{c}\xRightarrow{\texttt{f}}\texttt{r}$

let x = move c; //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

let y = *r; // read from dangling ref!

}

The ability (and in some cases, requirement) to move values instead of copying
them is a key feature of the Move language—it prevents “double spending” of
monetary values like c. However, the move causes the reference value stored in
r to become dangling.

Similarly, if the programmer creates a reference to a value that is
overwritten via a destructive update, a dangling reference may result. The
snippet below creates a vector v of size 1, acquires a reference ref into
index 0 of the vector, and then reassigns v to an empty vector via the write
to v_ref. As a result, the write *ref accesses a dangling reference.

⬇

let v = Vector::singleton(5);

let v_ref = &mut v; //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{v}\xRightarrow{\varepsilon}\texttt{v\\_ref}$

let ref = &mut v[0]; //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{v}\xRightarrow{*}\texttt{ref}$,
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{v}\xRightarrow{\varepsilon}\texttt{v\\_ref}$

*v_ref = Vector::empty(); // $\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

*ref = 10; // write to dangling ref!

#### Ownership and Borrowing

Our analysis enforces a programming discipline based on ownership to prevent
the problems above. A location in memory (either a local variable, stack
location, or global key) of type T is the _owner_ of the value it stores. A
value of type T can only be moved or (if T is a mutable reference) written via
its owning location. However, a value stored in a local or global can be
_borrowed_ from its owner by creating a reference to it (e.g. &v) or extending
an existing reference (e.g. &ref.f). The analysis will not allow the value to
be moved or written until all borrows have ended (i.e., the reference values
produced by the borrows have been destroyed). This discipline has a natural
recursive structure: if y borrows from x and then z subsequently borrows from
y, x does not regain ownership until both the y and the z borrows have ended.

As we will show in §4, a program that follows these rules cannot create a
dangling reference by writing path $p$ when a reference path that is a strict
extension of $p$ exists elsewhere or moving a variable $x$ when a reference
path that is an extension of $x$ exists elsewhere. As a side benefit, this
discipline ensures referential transparency for immutable references.

#### Borrow Analysis Mechanics

The key piece of analysis state is a _borrow graph_ where nodes represents
references or values and a directed edge
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}A\xRightarrow{p}B$
means “path $A/p$ is borrowed by $B$”. Here, $A/p$ is an abstraction of the
path representation described in §2.1 extended with some additional
components: $\epsilon$ for a direct borrow of a local variable and $*$ for all
suffixes of a path. The analysis adds a borrow edge when a reference value is
created and eliminates borrow edges when a reference value is destroyed (e.g.,
popped off the stack or consumed by an instruction).

Returning to our examples above, each instruction is annotated with the borrow
graph after it executes. A
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$
indicates that the borrow checker would reject the program after processing
the instruction. The first program is straightforward: the &c.f instruction
creates a borrow of c, then the analysis rejects the program at move c because
there is a borrow edge rooted in c.

In the second program, the borrow edge
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{v}\xRightarrow{\varepsilon}\texttt{v\\_ref}$
represents that the local v_ref holds a direct reference to the vector in v.
The next instruction let ref = &mut v[0] generates the edge
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{v}\xRightarrow{*}\texttt{ref}$.
This is our first encounter with abstraction in the analysis: the $*$ means
that the analysis does not know which offsets of v have been borrowed by ref.
Finally, the analysis chooses to reject the write to v_ref because it borrows
from v and the * edge represents an outstanding borrow on v.

###  2.3. Borrow Discipline Across Procedures

Move procedures can accept reference arguments and return references, which
introduces new ways to create dangling references. However, we can extend the
borrow discipline and its corresponding analysis to prevent these as well.

First, we consider the problem of returning dangling references. Each
procedure below returns a reference value to its caller by pushing the return
value on the operand stack (we write $S_{i}$ for the $i$th operand stack slot)
and then executing the Ret instruction (not shown). The first two procedures
in the snippet below return dangling references to local variables of the
procedure, but the second two return safe references to memory that will
outlive the procedure.

⬇

fun ret_local(): &u64 { let x = 7; &x /*
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{x}\xRightarrow{\varepsilon}S_{0}$
*/ }
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

fun ret_param(x: u64): &u64 { &x /*
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{x}\xRightarrow{\varepsilon}S_{0}$
*/ }
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

fun ret_ref_param(x: &u64): &u64 { x /*
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\emptyset$
*/ }

fun ret_borrowed_param(s: &S): &u64 { &s.f
/*$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{s}\xRightarrow{\texttt{f}}S_{0}$*/
}

Each procedure shows the borrow graph before the procedure returns. The
analysis will not allow a return value to have any borrow of a local variable
(ret_local) or a formal with a non-reference type (ret_param). The
ret_ref_param procedure is safe because it has no borrows—it returns a copy of
a reference parameter. Finally, ret_borrowed_param has a borrow of formal s,
but this is ok because s is a reference parameter rather than a local. The
analysis has access to a procedure’s type information, and it also tracks the
type of each stack location in a separate abstract domain.

#### Procedure Calls Require Ownership

Lastly, we consider the problem of handling procedure calls. Our static
analysis is modular, so it must soundly summarize the effects of a procedure
call with no information other than the callee’s type signature. A reference
value returned by a callee is conservatively assumed to be borrowed from all
of the procedure’s reference arguments, with extra care to avoid conflating
immutable and mutable references (see the Call rule in §4 for details).

A subtle consequence of the borrow discipline described in the previous
section is that every non-reference value pushed on the operand stack has no
outstanding borrows. Since procedures pass arguments to their callees on the
operand stack, this ensures that a caller cannot retain references to a value
passed to a callee. With this possibility out of the way, the only danger that
remains is a dangling reference caused by a reference value written in a
callee. To prevent this, the analysis enforces a single rule: an argument with
a mutable reference type must not have any outstanding borrows.

The two examples below show unsafe call sites. In both cases, the arguments
are evaluated left to right and pushed on the operand stack before the Call
instruction. The borrow graphs are at the program point before this
instruction. The analysis rejects each example because stack slot $S_{1}$ is
passed as an argument, but is borrowed by $S_{0}$.

⬇

a(&mut x, &mut x) //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{x}\xRightarrow{\varepsilon}S_{1},\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}S_{1}\xRightarrow{\varepsilon}S_{0}$
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

b(&mut y, &mut y.f) //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{y}\xRightarrow{\varepsilon}S_{1},\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}S_{1}\xRightarrow{\texttt{f}}S_{0}$
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

In addition to preventing dangling references, this strategy for handling
calls ensures a very useful property: a mutable reference parameter cannot
alias with any other parameter! Eliminating aliased mutable data allows Move
programmers to write procedures without defensive checks for aliasing and
greatly facilitates precise and scalable static program verification in the
Move Prover (for double-blind review, 2020).

###  2.4. Dangling References to Global Memory

We conclude our informal presentation of the analysis by considering the
thorny problem of allowing mutable access to global memory while preventing
dangling references. At first blush, this might seem impossible to do with a
modular analysis–the whole point of global memory is that you can access it
from anywhere! However, Move’s global memory instructions are carefully
designed to enable local reasoning about the safety of global memory accesses.
The two analysis extensions described in this section build on this design to
prevent dangling references to global memory using the existing borrow
analysis machinery.

#### Global Memory Indexed By Encapsulated Types

Move’s global memory is a partial map indexed by a pair of a statically chosen
record type T and a dynamically chosen account address a. A value stored at
key (T, a) is a record of type T. Record types are declared in _modules_
consisting of type and procedure declarations. The following table summarizes
the global state operations available in Move.

move_to<T>(a, T) | Publish T at address a
---|---
move_from<T>(a): T | Remove T from a
borrow_global<T>(a): &mut T | Get mutable ref to T at a

Programmers can publish a value of type T to an address in global state,
remove the value of type T stored at an address, and acquire references to a
value already published in global state. Modules encapsulate access to their
declared types; in particular, the global state access operations can only be
used on a type declared _inside the current module_.

The decision to include a type in these operations simplifies static reasoning
about aliasing of locations in global memory. Two global access operations
involving keys (T1, a1) and (T2, a2) can only touch the same memory if T1 = T2
and a1 = a2. Combined with type encapsulation, this means that global accesses
in distinct modules touch distinct memory by construction. Without this
property, a local reference safety analysis would not be practical.

#### Abstracting Dynamic Global Accesses

Each instruction that accesses global memory indexes into it using an address
value chosen at runtime. This means that code like:

⬇

fun address_aliasing(a1: address, a2: address) acquires T {

let t_ref = borrow_global<T>(a1); //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{T}\xRightarrow{\varepsilon}\texttt{t\\_ref}$

let t = move_from<T>(a2); //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

*t_ref = ... // accessing a dangling ref

}

may create a dangling reference if a1 and a2 are bound to the same address
value. Similarly, performing a move_to<T>(a, T while a reference created by a
borrow_global<T>(a) is still active creates a dangling reference.

Rather than attempting to reason about address equality, our analysis
conservatively assumes that all global accesses indexed by type T touch the
same address. This decision suggests a simple extension to the borrow graph: a
T node that abstracts all concrete cells in global memory keyed by type T. In
the example above, the analysis introduces a borrow from T at the
borrow_global instruction and rejects the program at move_from<T> because
there is an active borrow on T. This is exactly how the analysis deals with
programs like let x = &y; let z = move y only with T in place of x and global
access instructions in the place of local ones.

#### Global Accesses Across Procedure Boundaries

A similar, but more insidious problem arises if the global accesses occur in
procedures with a caller/callee relationship:

⬇

fun borrow_then_remove_bad(a: address) acquires T {

let t_ref = = borrow_global<T>(a); //
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\texttt{T}\xRightarrow{\varepsilon}\texttt{t\\_ref}$

let t = remove_t(a);
$\color[rgb]{0,0.4,0.200000000000001}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0.200000000000001}\dagger$

*t_ref = ...// accessing a dangling reference

}

fun remove_t(a: address): T acquires T {

move_from<T>(a)

}

However, the acquires annotation on remove_t allows the borrow analysis to
reject this program–an invocation of a procedure marked with acquires T is
treated as a move of T.

A separate intraprocedural analysis checks that any procedure containing a
borrow_global<T> or move_from<T> instruction is annotated with acquires T. Any
procedure that invokes an acquires T-annotated procedure in the same module
must also be annotated. A procedure that calls an acquires procedure declared
in a different module need not be annotated.

#### Global References Cannot Be Returned

The scheme described so far prevents dangling references to a global memory
cell of type T inside the module that declares T. Only one issue remains:
leaking a reference to a global cell of type T outside of the module where T
is declared:

⬇

module M1 {

fun f(a: address): &mut T acquires T { borrow_global<T>(a) }

fun g(a: address): T acquires T { move_from<T>(a) }

}

module M2 {

fun bad(a: address) {

let ref = M1::f(a);

let t = M1::g(a); // ref now dangling!

}}

The possibility of this leakage undermines our efforts to modularize reasoning
about reference invalidation. Thus, our analysis prevents it by banning
returns of references to global memory. This happens implicitly by following
the return discipline described in §2.3: only borrows of reference parameters
may remain on the stack when a procedure returns, and a global is not a
reference parameter.

##  3\. Move Operational Semantics

$\inferrule*[Right=\text{\bf{}}]{z=(\rho,\ell,L)\quad\mathcal{P}[\rho].\mathit{C}\left[\ell\right]={{\bf{Call}}}\left<\rho^{\prime}\right>}{{\mathcal{P}}\vdash{\left<{z}{::}{P},{\overline{v}}{::}{S},M\right>}\rightarrow{\left<{(\rho^{\prime},0,\mathit{rev}(\overline{v}))}{::}{{z}{::}{P}},S,M\right>}}$
$\inferrule*[Right=\text{\bf{Emp}}]{z=(\rho,\ell,L)\quad\mathcal{P}[\rho].\mathit{C}\left[\ell\right]={\bf{Ret}}\quad
M^{\prime}=M-img(L)}{{\mathcal{P}}\vdash{\left<z,[],M\right>}\rightarrow{\left<[],[],M^{\prime}\right>}}$
$\inferrule*[Right=\text{\bf{Ret}}]{z=(\rho,\ell,L)\quad\mathcal{P}[\rho].\mathit{C}\left[\ell\right]={\bf{Ret}}\quad
M^{\prime}=M-img(L)}{{\mathcal{P}}\vdash{\left<{z}{::}{{(\rho^{\prime},\ell^{\prime},L^{\prime})}{::}{P}},S,M\right>}\rightarrow{\left<{(\rho^{\prime},\ell^{\prime}+1,L^{\prime})}{::}{P},S,M^{\prime}\right>}}$
$\inferrule*[Right=\text{\bf{}}]{\mathcal{P}[\rho].\mathit{C}\left[\ell\right]={{\bf{Branch}}}\left<\ell_{1},\ell_{2}\right>\quad\ell^{\prime}=\mathit{ite}(v,\ell_{1},\ell_{2})}{{\mathcal{P}}\vdash{\left<{(\rho,\ell,L)}{::}{P},{v}{::}{S},M\right>}\rightarrow{\left<{(\rho,\ell^{\prime},L)}{::}{P},S,M\right>}}$
$\inferrule*[Right=\text{\bf{{$\bf{Execute}$}}}]{{\mathcal{P}[\rho].\mathit{C}\left[\ell\right]}\vdash{\left<L,S,M\right>}\rightarrow{\left<L^{\prime},S^{\prime},M^{\prime}\right>}}{{\mathcal{P}}\vdash{\left<{(\rho,\ell,L)}{::}{P},S,M\right>}\rightarrow{\left<{(\rho,\ell+1,L^{\prime})}{::}{P},S^{\prime},M^{\prime}\right>}}$
$\inferrule*[Right=\text{\bf{}}]{v=\mathit{ite}(L(x)\in
dom({M}),M(L(x)),L(x))}{{{{\bf{MoveLoc}}}\left<x\right>}\vdash{\left<L,S,M\right>}\rightarrow{\left<{L}\setminus{x},{v}{::}{S},{M}\setminus{L(x)}\right>}}$
$\inferrule*[Right=\text{\bf{}}]{v=\mathit{ite}(L(x)\in
dom({M}),M(L(x)),L(x))}{{{{\bf{CopyLoc}}}\left<x\right>}\vdash{\left<L,S,M\right>}\rightarrow{\left<L,{v}{::}{S},M\right>}}$
$\inferrule*[Right=\text{\bf{Ref}}]{}{{{{\bf{StoreLoc}}}\left<x\right>}\vdash{\left<L,{r}{::}{S},M\right>}\rightarrow{\left<{L}\left[{x}\mapsto{r}\right],S,M\right>}}$
$\inferrule*[Right=\text{\bf{Val}}]{L(x)=c\vee(x\not\in dom({L})\wedge c\notin
dom({M}))}{{{{\bf{StoreLoc}}}\left<x\right>}\vdash{\left<L,{v}{::}{S},M\right>}\rightarrow{\left<{L}\left[{x}\mapsto{c}\right],S,{M}\left[{c}\mapsto{v}\right]\right>}}$
$\inferrule*[Right=\text{\bf{}}]{}{{{{\bf{BorrowLoc}}}\left<x\right>}\vdash{\left<L,S,M\right>}\rightarrow{\left<L,{{\bf
ref}\\!\\!\\!~{}\left<{L(x)},{[]}\right>}{::}{S},M\right>}}$
$\inferrule*[Right=\text{\bf{}}]{L(x)={\bf
ref}\\!\\!\\!~{}\left<{c},{p}\right>}{{{{\bf{BorrowField}}}\left<f,x\right>}\vdash{\left<L,S,M\right>}\rightarrow{\left<L,{{\bf
ref}\\!\\!\\!~{}\left<{c},{p::f}\right>}{::}{S},M\right>}}$
$\inferrule*[Right=\text{\bf{}}]{}{{{\bf{FreezeRef}}}\vdash{\left<L,{r}{::}{S},M\right>}\rightarrow{\left<L,{r}{::}{S},M\right>}}$
$\inferrule*[Right=\text{\bf{}}]{}{{{\bf{ReadRef}}}\vdash{\left<L,{{\bf
ref}\\!\\!\\!~{}\left<{c},{p}\right>}{::}{S},M\right>}\rightarrow{\left<L,{M(c)[p]}{::}{S},M\right>}}$
$\inferrule*[Right=\text{\bf{}}]{r={\bf
ref}\\!\\!\\!~{}\left<{c},{p}\right>\quad
v=M(c)}{{{\bf{WriteRef}}}\vdash{\left<L,{v^{\prime}}{::}{{r}{::}{S}},M\right>}\rightarrow{\left<L,S,{M}\left[{c}\mapsto{v[p:=v^{\prime}]}\right]\right>}}$
$\inferrule*[Right=\text{\bf{}}]{t=\left\\{(f_{i},\\_)\mid 1\leq i\leq
n\right\\}\quad v=\left\\{(f_{i},v_{i})\mid 1\leq i\leq
n\right\\}}{{{{\bf{Pack}}}\left<t\right>}\vdash{\left<L,{v_{1}{::}\cdots{::}v_{n}}{::}{S},M\right>}\rightarrow{\left<L,{v}{::}{S},M\right>}}$
$\inferrule*[Right=\text{\bf{}}]{v=\left\\{(f_{i},v_{i})\mid 1\leq i\leq
n\right\\}}{{{\bf{Unpack}}}\vdash{\left<L,{v}{::}{S},M\right>}\rightarrow{\left<L,{v_{1}{::}\cdots{::}v_{n}}{::}{S},M\right>}}$
$\inferrule*[Right=\text{\bf{}}]{}{{{\bf{Pop}}}\vdash{\left<L,{\\_}{::}{S},M\right>}\rightarrow{\left<L,S,M\right>}}$
$\inferrule*[Right=\text{\bf{}}]{}{{{\bf{Op}}}\vdash{\left<L,{v_{1}{::}\cdots{::}v_{n}}{::}{S},M\right>}\rightarrow{\left<L,{{{\bf{Op}}(v_{1},\dots,v_{n})}}{::}{S},M\right>}}$

Figure 1. Operational semantics

In this section, we formalize the operational semantics of a subset of the
Move language chosen to illustrate the key challenges of reference safety.

#### Partial functions and lists

We use partial functions to represent record values and for mappings that are
parts of semantic states. Lists are used for sequences of field accesses and
for the stack component of semantic states.

Following common convention, if $f:A\to B$ is a partial function, then
$dom({f})$ is its domain and $img({f})$ is its range. We write
${f}\left[{a}\mapsto{b}\right]$ for the function that is the same as $f$ on
every argument except $a$, and which maps $a$ to $b$. Similarly,
${f}\setminus{a}$ is the partial function equivalent to $f$ except that it is
undefined at $a$.

We write $[]$ for the empty list and $e::l$ for the result of placing $e$ at
the front of list $l$. Similarly, $l::e$ is the list with $e$ appended to $l$
and, by slight overloading of notation, $l::l^{\prime}$ is the concatenation
of lists $l$ and $l^{\prime}$.

#### Types

Let $\mathit{PrimType}$ be the set of primitive types, including Bool (of
Boolean values), Int (of integers), and Addr (of account addresses). Let $F$
be a fixed, finite set of _field names_. The set $\mathit{ValType}$ of value
types is the least set satisfying: (1)
$\mathit{PrimType}\subseteq\mathit{ValType}$; and (2) if $f_{1}\dots f_{n}\in
F$ are pair-wise distinct and $t_{1}\dots t_{n}\in\mathit{ValType}$, then
$\\{(f_{i},t_{i})|1\leq i\leq n\\}\in\mathit{ValType}$. Let
$\mathit{ImmRefType}=\\{\mathit{Imm}(t)\mid t\in\mathit{ValType}\\}$,
$\mathit{MutRefType}=\\{\mathit{Mut}(t)\mid t\in\mathit{ValType}\\}$,
$\mathit{RefType}=\mathit{ImmRefType}\cup\mathit{MutRefType}$, and
$\mathit{Type}=\mathit{ValType}\cup\mathit{RefType}$.

#### Values

We define the set of values used in computation inductively. Let
$\mathit{PrimVal}$ be the set of primitive data values. The set $Val$ of
values is the least set satisfying: (1) $\mathit{PrimVal}\subseteq Val$; (2)
if $f_{1}\dots f_{n}\in F$ are pair-wise distinct and $v_{1}\dots v_{n}\in
Val$, then $\\{(f_{i},v_{i})|1\leq i\leq n\\}\in Val$. The judgment ${v}:{t}$,
indicating that value $v$ has type $t$, is defined in the natural way.

#### Paths

A path is a possibly empty list of field names, representing a sequence of
field selections. A path represents a way to start at any location in memory
and follow a sequence of field selections to reach a value. It is helpful to
visualize a value as a labeled tree whose edges are labeled by field names. A
primitive value is a tree consisting of a single leaf. The tree associated
with a record value consists of a node and a subtree for each record
component. If $r$ is a record value, then for each $(f,v)\in r$, the edge from
$r$ to the subtree for $v$ is labeled by $f$.

Two useful operations on values are (1) the subtree $v[p]$ of $v$ located at
path $p$, and (2) the tree $v[p:=v^{\prime}]$ obtained by replacing the
subtree at path $p$ with tree $v^{\prime}$. Using the association between
values and trees, $v[p]$ is the subtree reached by path $p$ from root $v$, and
$v[p:=v^{\prime}]$ is the tree with the subtree $v[p]$ replaced with
$v^{\prime}$.

#### Concrete states

The set $\mathit{Loc}$ is an uninterpreted set of locations; the memory of a
program is a partial map from $\mathit{Loc}$ to $Val$. A reference $r$ is a
pair ${\bf ref}\\!\\!\\!~{}\left<{c},{p}\right>$, where $c\in\mathit{Loc}$ and
$p$ is a path. A _concrete state_ $s$ is a tuple $\left<P,S,M\right>$ where:
(1) Call stack $P$ is a list of frames. Each frame is a triple comprising a
procedure $\rho$, a program counter $\ell$, and a local store $L$ that maps
variables to locations or references. (2) Operand stack $S$ is a list of
values and references. (3) Memory $M$ maps locations to values.

A program $\mathcal{P}$ maps each procedure $\rho$ to a tuple
$\mathcal{P}[\rho]$ which contains a nonempty sequence of bytecodes
$\mathcal{P}[\rho].\mathit{C}$, and a sequence of input/output types
$\mathcal{P}[\rho].\mathit{I}$ and $\mathcal{P}[\rho].\mathit{O}$.

#### Semantics

Figure 1 shows the formal operational semantics. The first four rules capture
the execution of a program $\mathcal{P}$ as a transition relation
$\mathcal{P}\vdash\left<P,S,M\right>\rightarrow\left<P^{\prime},S^{\prime},M^{\prime}\right>$.
Each of these rules looks up the instruction
$\mathcal{P}[\rho].\mathit{C}[\ell]$ pointed to by the top frame on the call
stack, executes the instruction, and updates the state accordingly.
$\bf{Call}$ establishes a new frame at the top of the call stack. $\bf{Ret}$
tears down the frame at the top of the call stack and increments the program
counter for the new topmost frame.
${{\bf{Branch}}}\left<\ell_{1},\ell_{2}\right>$ consumes a Boolean value from
the top of the operand stack and updates the program counter to $\ell_{1}$ if
the value is true and to $\ell_{2}$ otherwise. The $\bf{Execute}$ rule is a
wrapper for executing the remaining instructions.

The $\bf{MoveLoc}$, $\bf{CopyLoc}$, and $\bf{StoreLoc}$ instructions move or
copy values between local variables and the operand stack; $\bf{BorrowLoc}$,
$\bf{BorrowField}$, $\bf{ReadRef}$, and $\bf{WriteRef}$ to operate on
reference values stored on the operand stack. The $\bf{FreezeRef}$ rule
converts a mutable reference into an immutable one. This instruction is a no-
op in the concrete semantics, but performs several important checks in the
analysis (see Section 4). $\bf{Pack}$ and $\bf{Unpack}$ to create and destroy
record values by binding values on the stack to fields or pushing values bound
to fields onto the stack (respectively). $\bf{Pop}$ destroys a value on the
operand stack. This is simple in the concrete semantics, but the analysis must
perform careful bookkeeping when popping references. The generic $\bf{Op}$
instruction represents arithmetic/bitwise operations that use the operand
stack.

The correctness of executions of $\mathcal{P}$ requires that only instructions
in the valid bytecode range are accessed and that each instruction operates on
the correct number of values of appropriate type producing the appropriate
result and updating the state without violating reference safety. The first
requirement is easily handled by a syntactic check that the bytecode sequence
of each procedure is nonempty, branch targets are legal indices, and the last
instruction is either $\bf{Branch}$ or $\bf{Ret}$. The second requirement is
the subject of the next section.

##  4\. Move Borrow Checker

In this section, we present the guarantees offered by the Move borrow checker
on the subset of the language formalized in §3. Our formalization requires
that there is a type annotation on each bytecode of each procedure. Our
analysis will check that the program is well-typed, i.e., all type annotations
are consistent with each other. The annotations are derived automatically via
a simple fixpoint based on abstract interpretation; this fixpoint is described
informally in §5. The annotations on a well-typed program allow us to define
an abstraction function $\mathit{Abs}$ from a concrete state
$\left<P,S,M\right>$ to an abstract state $\left<\hat{P},\hat{S},B\right>$
that replaces each concrete value or reference in $P$ ($S$) with its type in
$\hat{P}$ ($\hat{S}$), drops the memory $M$ entirely replacing it with a
borrow graph $B$ that captures the borrow relationships among values and
references in $P$ and references in $S$. Finally, we show that every concrete
state $s$ reachable by program $\mathcal{P}$ is connected to $\mathit{Abs}(s)$
by an invariant that is sufficient to prove type safety, absence of leaks, and
absence of dangling references.

In the abstract semantics used to formalize static checking, a path may
optionally end with the distinguished symbol $*$, representing an unknown
(possibly empty) sequence of additional field selections. A path is extensible
if it ends in $*$ and fixed otherwise. We include both kinds of paths in the
definitions of path operations below. We write $p\leq q$ if path $p$ is a
prefix of path $q$. We write $p::q$ for _path concatenation_ which is ordinary
concatenation of $p$ and $q$ if $p$ is fixed and $p$ otherwise.

#### Borrow graph

An abstract location is either $\Pi(x,y)$ for some non-negative integers $x$
and $y$ or $\Omega(x)$ for some non-negative integer $x$. Let $\mathit{ALoc}$
be the set of all abstract locations. The abstract location $\Pi(x,y)$
represents the contents of the local variable $y$ in the call stack frame at
position $x$. The abstract location $\Omega(x)$ represents the contents of the
operand stack at position $x$. In both cases, we count up from the bottom of
the stack. An abstract location can be looked up in a concrete state to return
either a reference (both call stack and operand stack), a value (only operand
stack), or a concrete location in $\mathit{Loc}$ (only call stack).

For abstract locations $x,y\in\mathit{ALoc}$ and path $p$, the assertion
$\mathit{Borrow}(x,p,y)$, called a borrow edge, is interpreted in a concrete
state $s$ to indicate that $x.p$ is borrowed by $y$. If $p$ is fixed, the
reference in $s$ at position $y$ has jurisdiction over $m.p$, where $m$ is the
reference or concrete location at position $x$ in $s$. If $p$ is extensible,
then $x.q$ is borrowed by $y$ for some extension $q$ of $p$. In our static
analysis, we therefore assume (to preserve soundness) that $y$ has
jurisdiction over each $x.q$, for any extension $q$ of the path $p$.

A _borrow graph_ $B$ is a collection of borrow edges. An edge
$\mathit{Borrow}(x,p,y)$ is subsumed by edge $\mathit{Borrow}(x,q,y)$ if
either $p=q$ or $q=r*$ and $r\leq p$. If $G$ and $H$ are borrow graphs, we
write $G\sqsubseteq H$, if every edge $\mathit{Borrow}(x,p,y)$ in $G$ is
subsumed by some edge $\mathit{Borrow}(x,q,y)$ in $H$. Note that this
definition allows additional edges in $H$ that are not implied by edges in
$G$. Semantically, if $G\sqsubseteq H$, then $G$ imposes every restriction on
concrete execution that is expressed by $H$, and possibly additional
restrictions. As a result, we will see that every state that satisfies $G$
also satisfies $H$.

#### Abstract state

An _abstract state_ $\hat{s}$ is a tuple $\left<\hat{P},\hat{S},B\right>$ with
three components. The first component $\hat{P}$, an abstract call stack that
matches the concrete call stack, is a list of triples, each comprising a
procedure name $\rho$, a program counter $\ell$, and a partial map $\hat{L}$
from variables to $\mathit{Type}$. The stack $\hat{P}$ defines a set of stack
positions $\emph{Pos}(\hat{P})=\\{\Pi(x,y)\mid 0\leq
x<\mathit{len}(\hat{P})\wedge y\in\hat{P}[x].\hat{L}\\}$, with $\Pi(x,y)$
indicating the $y$-th local variable in the $x$-th call frame of the stack.
The second component $\hat{S}$, an abstract operand stack that matches the
concrete operand stack, is a list of types. The stack $\hat{S}$ defines a set
of meaningful stack positions $\emph{Pos}(\hat{S})=\\{\Omega(x)\mid 0\leq
x<\mathit{len}(\hat{S})\\}$. Treating the abstract state $\hat{s}$ as a
partial map from positions
$dom({\hat{s}})=\emph{Pos}(\hat{P})\cup\emph{Pos}(\hat{S})$ to types, we let
$\hat{s}(\Pi(x,y))$ be the type $\hat{P}[x].\hat{L}[y]$ and
$\hat{s}(\Omega(x))$ be the type $\hat{S}[x]$. The third component $B$ of the
abstract state is a borrow graph with edges connecting nodes from
$dom({\hat{s}})$.

#### Local abstract state

Since abstract states represent type information, abstract execution of an
imperative program instruction is a form of type propagation. The rules for
type propagation of local instructions (§4.1) operate over a local abstract
state $\left<\hat{L},\hat{S},B\right>$. The first component $\hat{L}$ maps the
variables in the local store of the top frame of the call stack to their
types. The second component $\hat{S}$ contains the types of the values and
references for the portion of the operand stack visible to the execution of
the procedure in the top frame. This component is empty at the starting
bytecode at position $0$ and grows and shrinks as values or references are
pushed on and popped off it. The third component $B$ contains the borrow edges
for locations in $\hat{L}$ and $\hat{S}$.

Let $\mathit{ls}=\left<\hat{L},\hat{S},B\right>$ be an abstract local state.
We define $dom({\mathit{ls}})=\\{\Pi(0,i)\mid i\in
dom({\hat{L}})\\}\cup\\{\Omega(i)\mid i\in 0..\mathit{len}(\hat{S})\\}$. The
locations in $dom({\mathit{ls}})$ are defined using the offset $0$ for the
position of its frame and the bottom of its operand stack. Later, when we
define the abstract state corresponding to a concrete state, we will show how
local abstract states of each frame on the call stack, can be stitched
together by adjusting their locations with respect to an appropriate offset.

We call $\\{\Pi(0,i)\mid i\in
0..\mathit{len}(\mathcal{P}[\rho].\mathit{I})\\}$ the input locations of
$\rho$. The abstract local state $\mathit{ls}$ is well-formed for $\rho$ if
(1) every input location of $\rho$ is in $dom({\mathit{ls}})$, (2)
$\mathit{ls}.B$ is a directed acyclic graph, and (3) for all
$\mathit{Borrow}(x,\\_,y)\in\mathit{ls}.B$, we have $x,y\in
dom({\mathit{ls}})$, and $y$ is not an input location of $\rho$. The
propagation on local abstract states (§4.1) uses judgments of the form
$\rho,{\mathrm{o}p}\vdash\left<\hat{L},\hat{S},B\right>\rightarrow\left<\hat{L}^{\prime},\hat{S}^{\prime},B^{\prime}\right>$
indicating that procedure $\rho$ executing instruction ${\mathrm{o}p}$ from
$\left<\hat{L},\hat{S},B\right>$ results in
$\left<\hat{L}^{\prime},\hat{S}^{\prime},B^{\prime}\right>$. These rules are
designed to ensure that if $\left<\hat{L},\hat{S},B\right>$ is well-formed for
$\rho$, then $\left<\hat{L}^{\prime},\hat{S}^{\prime},B^{\prime}\right>$ is
also well-formed for $\rho$.

#### Well-typed programs

In addition to input types $\mathcal{P}[\rho].\mathit{I}$ and output types
$\mathcal{P}[\rho].\mathit{O}$, our analysis requires that each procedure
$\rho$ contains an abstract local state $\mathcal{P}[\rho].\mathit{T}[i]$ for
each offset $i\in 0..\mathit{len}(\mathcal{P}[\rho].\mathit{C})$ that is well-
formed for $\rho$. Let $\mathit{Next}(\rho)[i]$ be the (empty, singleton, or
doubleton) set of program counters to which control transfer is possible after
executing instruction at position $i$.

$\begin{array}[]{llll}\mathit{Next}(\rho)[i]&=&\\{\\},&\mathit{if}\
\mathcal{P}[\rho].\mathit{C}[i]={\bf{Ret}}\\\
&&\\{\ell_{1},\ell_{2}\\},&\mathit{if}\
\mathcal{P}[\rho].\mathit{C}[i]={{\bf{Branch}}}\left<\ell_{1},\ell_{2}\right>\\\
&&\\{\ell+1\\},&\mathit{otherwise}\end{array}$

We write
$\left<\hat{L},\hat{S},B\right>\sqsubseteq\left<\hat{L}^{\prime},\hat{S}^{\prime},B^{\prime}\right>$
if $\hat{L}=\hat{L}^{\prime}$, $\hat{S}=\hat{S}^{\prime}$, and $B\sqsubseteq
B^{\prime}$. Thus, every concrete local state represented by
$\left<\hat{L},\hat{S},B\right>$ can also be represented by
$\left<\hat{L^{\prime}},\hat{S^{\prime}},B^{\prime}\right>$. A program
$\mathcal{P}$ is well-typed if for all $\rho\in dom({\mathcal{P}})$:

  1. (1)

$\left<\mathcal{P}[\rho].\mathit{I},[],\\{\\}\right>=\mathcal{P}[\rho].\mathit{T}[0]$.

  2. (2)

For all $i\in dom({\mathcal{P}[\rho].\mathit{C}})$, there exists
$\left<\hat{L},\hat{S},B\right>$ such that (a)
$\rho,\mathcal{P}[\rho].\mathit{C}[i]\vdash\mathcal{P}[\rho].\mathit{T}[i]\rightarrow\left<\hat{L},\hat{S},B\right>$,
and (b)
$\left<\hat{L},\hat{S},B\right>\sqsubseteq\mathcal{P}[\rho].\mathit{T}[j]$ for
all $j\in\mathit{Next}(\rho)[i]$.

The first condition states that initially the operand stack and borrow graph
are empty. The second condition expresses that the restrictions imposed after
executing an instruction continue to the next instruction.

#### Abstraction function

While the rules mention only abstract local states, they also define abstract
execution on (full) abstract states. We define an abstraction function from a
concrete state to an abstract state. As a concrete execution steps through
concrete states, its abstract execution steps through the corresponding
abstract states.

We define the abstract state $\left<\hat{P},\hat{S},B\right>$ corresponding to
a concrete state $\left<P,S,M\right>$ of a well-typed program $\mathcal{P}$ by
looking only at $P$ and the annotations on $\mathcal{P}$. The component
$\hat{P}$ is obtained by processing each frame $\left<\rho,\ell,L\right>$ in
$P$ separately, replacing $L$ with
$\mathcal{P}[\rho].\mathit{T}[\ell].\hat{L}$, and concatenating the results:

$\begin{array}[]{l}\mathit{AP}(P)=\mathit{match}\ P\\\
\phantom{xx}\mid[]\rightarrow[]\\\
\phantom{xx}\mid{\left<\rho,\ell,\\_\right>}{::}{P^{\prime}}\rightarrow\mathit{let}\
x=\mathcal{P}[\rho].\mathit{T}[\ell].\hat{L}\ \mathit{in}\
{\left<\rho,\ell,x\right>}{::}{\mathit{AP}(P^{\prime})}\\\
\hat{P}=\mathit{AP}(P)\end{array}$

The definition of $\hat{S}$ is not a straightforward concatenation of the
operand stacks $\mathcal{P}[\rho].\mathit{T}[i]$ for each position $i\in
dom({P})$ because the operand stack for each frame other than the topmost
contains the arguments for the callee. These arguments are removed from the
operand stack as a result of the call; consequently, they must be removed
prior to concatenation as well. We first derive
$\mathcal{P}[\rho].\overline{\mathit{T}}[i]$ which removes the callee
arguments from the operand stack if instruction $i$ in $\rho$ is a call.

$\begin{array}[t]{l}\mathit{if}\
\mathcal{P}[\rho].\mathit{C}[i]={{\bf{Call}}}\left<\rho^{\prime}\right>\\\
\hskip 5.69054pt\begin{array}[t]{lll}\mathit{let}\\\
x=\mathcal{P}[\rho^{\prime}].\mathit{I}\\\
\left<\hat{L},{\mathit{rev}(x)}{::}{\hat{S}},B\right>=\mathcal{P}[\rho].\mathit{T}[i]\\\
R=\\{(\Omega(\mathit{len}(\hat{S})+i),\Pi(1,i))\mid i\in
0..\mathit{len}(x)\\}\ \mathit{in}\\\
\left<\hat{L},\hat{S},\mathit{rename}(B,R)\right>\end{array}\\\
\mathit{else}\\\ \hskip
5.69054pt\begin{array}[t]{l}\mathcal{P}[\rho].\mathit{T}[i]\end{array}\end{array}$

This derivation uses the operation $\mathit{rename}(B,R)$ which renames the
nodes of edges in $B$ according to the bijection $R$. Here $R$ renames the
positions on the operand stack corresponding to callee arguments to
appropriate positions in the next frame with offset $1$. We now define
$\hat{P}$ by concatenating operand stacks obtained by looking up
$\mathcal{P}[\rho].\mathit{T}$ for the top frame and
$\mathcal{P}[\rho].\overline{\mathit{T}}$ for all other frames:

$\begin{array}[]{l}\mathit{AS}(P)=\mathit{match}\ P\\\
\phantom{xx}\mid[]\rightarrow[]\\\
\phantom{xx}\mid{\left<\rho,\ell,\\_\right>}{::}{P^{\prime}}\rightarrow\mathit{let}\
x=\mathcal{P}[\rho].\overline{\mathit{T}}[\ell].\hat{S}\ \mathit{in}\
{x}{::}{\mathit{AS}(P^{\prime})}\\\ \hat{S}=\mathit{let}\
{\left<\rho,\ell,\\_\right>}{::}{P^{\prime}}=P,\
x=\mathcal{P}[\rho].\mathit{T}[\ell].\hat{S}\ \mathit{in}\
{x}{::}{\mathit{AS}(P^{\prime})}\end{array}$

The last component $B$ is defined similarly to $\hat{S}$, by looking up the
borrow graph for each frame, renaming it appropriately to account for the
offset of the frame and its corresponding operand stack, and taking the union
of all such renamed borrow graphs. The top frame is looked up in
$\mathcal{P}[\rho].\mathit{T}$ but all other frames are looked up in
$\mathcal{P}[\rho].\overline{\mathit{T}}$.

$\begin{array}[]{l}\mathit{AB}(P,n)=\mathit{match}\ P\\\
\phantom{xx}\mid[]\rightarrow[]\\\
\phantom{xx}\mid{\left<\rho,\ell,\\_\right>}{::}{P^{\prime}}\rightarrow\mathit{let}\\\
\phantom{xxxx}B=\mathit{if}\ n=\mathit{len}(P)\ \mathit{then}\
\mathcal{P}[\rho].\mathit{T}[\ell].B\ \mathit{else}\
\mathcal{P}[\rho].\overline{\mathit{T}}[\ell].B,\\\
\phantom{xxxx}R=\\{(\Pi(x,y),\Pi(x+\mathit{len}(P^{\prime}),y))\mid\Pi(x,y)\\}\
\cup\\\
\phantom{xxxxxxxx}\\{(\Omega(x),\Omega(x+\mathit{len}(\mathit{AS}(P^{\prime}))))\mid\Omega(x)\\}\
\mathit{in}\\\
\phantom{xxxx}\mathit{rename}(B,R)\cup\mathit{AB}(P^{\prime},n)\\\
B=\mathit{AB}(P,\mathit{len}(P))\end{array}$

The constraints on the annotations of a well-typed program, explained earlier,
allow us to prove that $B$ is acylic, an important property that we leverage
in the proof of reference safety. Finally, we get
$\mathit{Abs}(\left<P,S,M\right>)=\left<\hat{P},\hat{S},B\right>$, where
$\hat{P}$, $\hat{S}$, and $B$ are defined as above.

We use the abstraction function to prove critical invariants about executions
of well-typed programs. These invariants establish useful properties—type
agreement, no memory leaks, no dangling references, and referential
transparency. We state the invariants as a predicate $\mathit{Inv}(s,\hat{s})$
over a concrete state $s$ and an abstract state $\hat{s}$. We use type
propagation on local abstract states (§4.1) to prove the following theorem:

###### Theorem 1.

Let program $\mathcal{P}$ be well-typed. If $s$ is a concrete state with
$\mathit{Inv}(s,\mathit{Abs}(s))$ and $\mathcal{P}\vdash s\rightarrow
s^{\prime}$, then $\mathit{Inv}(s^{\prime},\mathit{Abs}(s^{\prime}))$.

A proof sketch for this theorem is available in the supplemental material. A
corollary is that if $\mathcal{P}$ starts execution in a concrete state
$s_{0}$ such that $\mathit{Inv}(s_{0},\mathit{Abs}(s_{0}))$ holds, then
$\mathit{Inv}(s,\mathit{Abs}(s))$ holds for all states reachable from $s_{0}$.
Any initial state $s_{0}$ of $\mathcal{P}$ is of the form
$\left<(\rho,0,\overline{x}),[],\\{\\}\right>$ representing the beginning of a
transaction that invokes $\rho$ with inputs $\overline{x}$ comprising only
values (no references), empty operand stack, and empty memory. It is easy to
see that $\mathit{Inv}(s_{0},\mathit{Abs}(s_{0}))$ holds if $\mathcal{P}$ is
well-typed. We present $\mathit{Inv}$ as the conjunction of four predicates,
$\mathit{InvA}$, $\mathit{InvB}$, $\mathit{InvC}$, $\mathit{InvD}$, described
below.

#### Type Agreement

Concrete state $s=\left<P,S,M\right>$ and abstract state
$\hat{s}=\left<\hat{P},\hat{S},B\right>$ are shape-matching if (1)
$\mathit{len}(P)=\mathit{len}(\hat{P})$, (2)
$\mathit{len}(S)=\mathit{len}(\hat{S})$, (3) for all $i\in dom({P})$, we have
$P[i].\rho=\hat{P}[i].\rho$, $P[i].\ell=\hat{P}[i].\ell$, and
$dom({P[i].L})=dom({\hat{P}[i].\hat{L}})$. Intuitively, shape-matching states
have the same call stack height, the same operand stack height, and agreement
between corresponding procedure names, program counters, and set of local
variables in each stack frame. Shape-matching states $s=\left<P,S,M\right>$
and $\hat{s}=\left<\hat{P},\hat{S},B\right>$ are further _type-matching_ if
for all positions $n$ in the identical sets of call stack positions
$\emph{Pos}(P)=\emph{Pos}(\hat{P})$ or in the identical sets of operand stack
positions $\emph{Pos}(S)=\emph{Pos}(\hat{S})$, we have ${s(n)}:{\hat{s}(n)}$.

$\mathit{InvA}(s,\hat{s}):$ $s$ and $\hat{s}$ are shape-matching and type-
matching.

#### No Memory Leaks

The following invariant indicates that (1) every local variable on the call
stack of $s$ contains a different location, and (2) locations are not leaked,
i.e., $s.M$ does not contain any location not present in a local variable.

#### $\mathit{InvB}(s,\hat{s}):$

The relation $\\{(n,s(n))\mid n\in dom({\hat{s}})\wedge
s(n)\in\mathit{Loc}\\}$ is a bijection from its domain to $dom({s.M})$.

#### No Dangling References

For shape-matching $s=\left<P,S,M\right>$ and
$\hat{s}=\left<\hat{P},\hat{S},B\right>$, a borrow edge
$\mathit{Borrow}(m,p,n)$ in $B$ is _realized in_ $s$ if the path $p$ leads
from $s(m)$ to $s(n)$, optionally involving additional field selections if $p$
ends in $*$. More precisely, we say this graph edge is realized if either

  1. (1)

$s(m)=c$, $s(n)={\bf ref}\\!\\!\\!~{}\left<{c},{q^{\prime}}\right>$, and path
$p$ matches $q^{\prime}$, or

  2. (2)

$s(m)={\bf ref}\\!\\!\\!~{}\left<{c},{q}\right>$, $s(n)={\bf
ref}\\!\\!\\!~{}\left<{c},{q^{\prime}}\right>$, and $q.p$ matches
$q^{\prime}$.

Note that the two conditions express the same basic relationship if we
identify $c$ and ${\bf ref}\\!\\!\\!~{}\left<{c},{\varepsilon}\right>$. The
following invariant allows us to conclude that every reference is rooted in a
memory location present in some local variable on the call stack.

#### $\mathit{InvC}(s,\hat{s}):$

  1. (1)

$\hat{s}.B$ is acyclic.

  2. (2)

For all $n\in dom({\hat{s}})$ such that $\hat{s}(n)\in\mathit{ValType}$, there
is no borrow edge in $\hat{s}.B$ coming into $n$.

  3. (3)

For all $n\in dom({\hat{s}})$ such that $\hat{s}(n)\in\mathit{RefType}$, there
is a borrow edge in $\hat{s}.B$ coming into $n$ that is realized in $s$.

#### Referential Transparency

We write ${\bf ref}\\!\\!\\!~{}\left<{c},{p}\right>\leq{\bf
ref}\\!\\!\\!~{}\left<{d},{q}\right>$ if $c=d$ and $p\leq q$. We extend $\leq$
so that $c\leq{\bf ref}\\!\\!\\!~{}\left<{c},{p}\right>$ for any $p$. The
following invariant indicates that the absence of borrow edges out of an
abstract location containing a value or a mutable reference guarantees that
mutation via that abstract location, either of the stored value or the value
pointed to by the mutable reference, will not invalidate any live reference.

#### $\mathit{InvD}(s,\hat{s}):$

For any distinct $m,n\in dom({\hat{s}})$ such that
$\hat{s}(n)\in\mathit{RefType}$ and $s(m)\leq s(n)$, one of the following
hold:

  1. (1)

$\hat{s}(m)\in\mathit{ImmRefType}$ and $\hat{s}(n)\in\mathit{ImmRefType}$.

  2. (2)

$\hat{s}(m)\not\in\mathit{ImmRefType}$ and there is a path in $\hat{s}.B$ from
$m$ to $n$ comprising realized edges in $s$.

  3. (3)

$s(m)=s(n)$ and there is a path in $\hat{s}.B$ from $n$ to $m$ comprising
realized edges in $s$.

###  4.1. Propagating Local Abstract States

$\inferrule*[Right=\text{\bf{}}]{x\not\in
0..\mathit{len}(\mathcal{P}[\rho].\mathit{I})\quad x\in
dom({\hat{L}})\quad\hat{L}(x)\in\mathit{ValType}\Rightarrow\mathit{Borrow}(\Pi(0,x),\\_,\\_)\not\in
B\quad
B^{\prime}=\mathit{rename}(B,\\{(\Pi(0,x),\Omega(\mathit{len}(\hat{S})))\\})}{{\rho,{{\bf{MoveLoc}}}\left<x\right>}\vdash{\left<\hat{L},\hat{S},B\right>}\rightarrow{\left<{\hat{L}}\setminus{x},{\hat{L}(x)}{::}{\hat{S}},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{}}]{B^{\prime}=\mathit{elim}(B,\Omega(\mathit{len}(\hat{S})))}{{\rho,{\bf{Pop}}}\vdash{\left<\hat{L},{\\_}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},\hat{S},B^{\prime}\right>}}$
$\inferrule*[Right=\text{\bf{Ref}}]{x\not\in
0..\mathit{len}(\mathcal{P}[\rho].\mathit{I})\quad\hat{L}(x)\in\mathit{RefType}\quad
B^{\prime}=\mathit{rename}(\mathit{elim}(B,\Pi(0,x)),\\{(\Omega(\mathit{len}(\hat{S})),\Pi(0,x))\\})}{{\rho,{{\bf{StoreLoc}}}\left<x\right>}\vdash{\left<\hat{L},{t}{::}{\hat{S}},B\right>}\rightarrow{\left<{\hat{L}}\left[{x}\mapsto{t}\right],\hat{S},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{Val}}]{x\not\in
0..\mathit{len}(\mathcal{P}[\rho].\mathit{I})\quad x\not\in
dom({\hat{L}})\vee\hat{L}(x)\in\mathit{ValType}\\\ \\\
\mathit{Borrow}(\Pi(0,x),\\_,\\_)\not\in B\quad
B^{\prime}=\mathit{rename}(B,\\{(\Omega(\mathit{len}(\hat{S})),\Pi(0,x))\\})}{{\rho,{{\bf{StoreLoc}}}\left<x\right>}\vdash{\left<\hat{L},{t}{::}{\hat{S}},B\right>}\rightarrow{\left<{\hat{L}}\left[{x}\mapsto{t}\right],\hat{S},B\right>}}$
$\inferrule*[Right=\text{\bf{}}]{x\in dom({\hat{L}})\quad\hat{L}(x)=t\quad
t\in\mathit{ValType}\\\ \\\
B^{\prime}=\mathit{factor}(B,\Pi(0,x),\Omega(\mathit{len}(\hat{S})))}{{\rho,{{\bf{BorrowLoc}}}\left<x\right>}\vdash{\left<\hat{L},\hat{S},B\right>}\rightarrow{\left<\hat{L},{\mathit{Mut}(t)}{::}{\hat{S}},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{Mut}}]{x\in
dom({\hat{L}})\quad\hat{L}(x)=\mathit{Mut}(\left\\{(f,t),\ldots\right\\})\\\
\\\
B^{\prime}=\mathit{factor}_{f}(B,\Pi(0,x),\Omega(\mathit{len}(\hat{S})))}{{\rho,{{\bf{BorrowField}}}\left<f,x\right>}\vdash{\left<\hat{L},\hat{S},B\right>}\rightarrow{\left<\hat{L},{\mathit{Mut}(t)}{::}{\hat{S}},B^{\prime}\right>}}$
$\inferrule*[Right=\text{\bf{Immut}}]{x\in
dom({\hat{L}})\quad\hat{L}(x)=\mathit{Imm}(\left\\{(f,t),\ldots\right\\})\\\
\\\
B^{\prime}=B\cup\\{\mathit{Borrow}(\Pi(0,x),f,\Omega(\mathit{len}(\hat{S}))\\}}{{\rho,{{\bf{BorrowField}}}\left<f,x\right>}\vdash{\left<\hat{L},\hat{S},B\right>}\rightarrow{\left<\hat{L},{\mathit{Imm}(t)}{::}{\hat{S}},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{}}]{x\in dom({\hat{L}})\quad
B^{\prime}=\mathit{ite}(\hat{L}(x)\in\mathit{RefType},\mathit{factor}(B,\Pi(0,x),\Omega(\mathit{len}(\hat{S}))),B)}{{\rho,{{\bf{CopyLoc}}}\left<x\right>}\vdash{\left<\hat{L},\hat{S},B\right>}\rightarrow{\left<\hat{L},{\hat{L}(x)}{::}{\hat{S}},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{}}]{\mathit{Borrow}(\Omega(\mathit{len}(\hat{S})),\\_,\\_)\not\in
B\quad
B^{\prime}=\mathit{elim}(B,\Omega(\mathit{len}(\hat{S})))}{{\rho,{\bf{WriteRef}}}\vdash{\left<\hat{L},{t}{::}{{\mathit{Mut}(t)}{::}{\hat{S}}},B\right>}\rightarrow{\left<\hat{L},\hat{S},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{}}]{t=\mathit{Imm}(t^{\prime})\vee
t=\mathit{Mut}(t^{\prime})\\\ \\\ \forall n.\
\mathit{Borrow}(\Omega(\mathit{len}(\hat{S})),\\_,n)\in
B\Rightarrow\left<\hat{L},\hat{S}\right>[n]\in\mathit{ImmRefType}}{{\rho,{\bf{FreezeRef}}}\vdash{\left<\hat{L},{t}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},{\mathit{Imm}(t^{\prime})}{::}{\hat{S}},B\right>}}$
$\inferrule*[Right=\text{\bf{}}]{t=\mathit{Imm}(t^{\prime})\vee
t=\mathit{Mut}(t^{\prime})\quad
B^{\prime}=\mathit{elim}(B,\Omega(\mathit{len}(\hat{S})))\\\ \\\ \forall n.\
\mathit{Borrow}(\Omega(\mathit{len}(\hat{S})),\\_,n)\in
B\Rightarrow\left<\hat{L},\hat{S}\right>[n]\in\mathit{ImmRefType}}{{\rho,{\bf{ReadRef}}}\vdash{\left<\hat{L},{t}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},{t^{\prime}}{::}{\hat{S}},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{}}]{\overline{t}=[t_{1},\ldots,t_{n}]\quad
t=\left\\{(f_{i},t_{i})\mid 1\leq i\leq
n\right\\}}{{\rho,{{\bf{Pack}}}\left<t\right>}\vdash{\left<\hat{L},{\overline{t}}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},{t}{::}{\hat{S}},B\right>}}$
$\inferrule*[Right=\text{\bf{}}]{\overline{t}=[t_{1},\ldots,t_{n}]\quad
t=\left\\{(f_{i},t_{i})\mid 1\leq i\leq
n\right\\}}{{\rho,{\bf{Unpack}}}\vdash{\left<\hat{L},{t}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},{\overline{t}}{::}{\hat{S}},B\right>}}$
$\inferrule*[Right=\text{\bf{}}]{{{\bf{Op}}}:{\overline{t}\rightarrow
t}}{{\rho,{\bf{Op}}}\vdash{\left<\hat{L},{\overline{t}}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},{t}{::}{\hat{S}},B\right>}}$

$\inferrule*[Right=\text{\bf{}}]{\mathit{is}=0..\mathit{len}(\mathcal{P}[\rho^{\prime}].\mathit{I})\quad\mathit{os}=0..\mathit{len}(\mathcal{P}[\rho^{\prime}].\mathit{O})\\\
\\\ \forall i\in\mathit{is}.\
\mathcal{P}[\rho^{\prime}].\mathit{I}[i]\in\mathit{MutRefType}\Rightarrow\mathit{Borrow}(\Omega(\mathit{len}(\hat{S})+i),\\_,\\_)\not\in
B\\\ \\\
B_{1}=\mathit{rename}(B,\\{i\in\mathit{is}\mid(\Omega(\mathit{len}(\hat{S})+i),\Pi(1,i))\\})\\\
\\\ B_{2}=\mathit{extend}(B_{1},\\{\Pi(1,i)\mid
i\in\mathit{is}\wedge\mathcal{P}[\rho^{\prime}].\mathit{I}[i]\in\mathit{MutRefType}\\},\\{\Omega(\mathit{len}(\hat{S})+i)\mid
i\in\mathit{os}\wedge\mathcal{P}[\rho^{\prime}].\mathit{O}[i]\in\mathit{RefType}\\})\\\
\\\ B_{3}=\mathit{extend}(B_{2},\\{\Pi(1,i)\mid
i\in\mathit{is}\wedge\mathcal{P}[\rho^{\prime}].\mathit{I}[i]\in\mathit{ImmRefType}\\},\\{\Omega(\mathit{len}(\hat{S})+i)\mid
i\in\mathit{os}\wedge\mathcal{P}[\rho^{\prime}].\mathit{O}[i]\in\mathit{ImmRefType}\\})\\\
\\\ B^{\prime}=\mathit{elim}(B_{3},\\{\Pi(1,i)\mid
i\in\mathit{is}\\})}{{\rho,{{\bf{Call}}}\left<\rho^{\prime}\right>}\vdash{\left<\hat{L},{\mathit{rev}(\mathcal{P}[\rho^{\prime}].\mathit{I})}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},{\mathit{rev}(\mathcal{P}[\rho^{\prime}].\mathit{O})}{::}{\hat{S}},B^{\prime}\right>}}$

$\inferrule*[Right=\text{\bf{}}]{\hat{L}=\mathcal{P}[\rho].\mathit{I}\quad\forall
x\in dom({\hat{L}}).\
\hat{L}(x)\in\mathit{ValType}\Rightarrow\mathit{Borrow}(\Pi(0,x),\\_,\\_)\not\in
B\\\ \\\ \hat{S}=\mathit{rev}(\mathcal{P}[\rho].\mathit{O})\quad\forall i\in
dom({\hat{S}}).\
\hat{S}[i]\in\mathit{MutRefType}\Rightarrow\mathit{Borrow}(\Omega(i),\\_,\\_)\not\in
B}{{\rho,{\bf{Ret}}}\vdash{\left<\hat{L},\hat{S},B\right>}\rightarrow{\left<\hat{L},\hat{S},B\right>}}$
$\inferrule*[Right=\text{\bf{}}]{t={\tt
Bool}}{{\rho,{{\bf{Branch}}}\left<\ell_{1},\ell_{2}\right>}\vdash{\left<\hat{L},{t}{::}{\hat{S}},B\right>}\rightarrow{\left<\hat{L},\hat{S},B\right>}}$

Having explained the overall structure of our soundness argument, we now
provide intuition for type propagation on local abstract states. The rule for
operation ${\mathrm{o}p}$ derives a judgment of the form
$\rho,{\mathrm{o}p}\vdash\left<\hat{L},\hat{S},B\right>\rightarrow\left<\hat{L}^{\prime},\hat{S}^{\prime},B^{\prime}\right>$
if certain conditions are satisfied. These conditions include availability of
appropriately-typed values in $\hat{L}$ or $\hat{S}$ and absence of certain
edges in the borrow graph $B$. The state transformation adds or removes a
variable-to-type binding in $\hat{L}$, pushes or pops types in $\hat{S}$, and
adds or removes edges in $B$. The rules for $\bf{MoveLoc}$ and $\bf{StoreLoc}$
also prevent an input of procedure $\rho$ from being moved or overwritten to
enable accurate tracking of transitive borrow relationships across a procedure
call.

The rule for ${{\bf{MoveLoc}}}\left<x\right>$ moves the type of variable $x$
to the top of operand stack. The rule checks that $x$ is available in
$\hat{L}$ and there are no outgoing borrow edges from $\Pi(0,x)$, the abstract
location of $x$, in case $x$ is a value. The rule also renames the old
position of the moved value to its new position.

The rule for ${\bf{Pop}}$ pops the top of the operand stack and eliminates the
location corresponding to it using a new operation $\mathit{elim}$. The
expression $\mathit{elim}(B,u)$ creates a new borrow graph by eliminating
location $u$ in $B$ as follows: (1) For every edge $\mathit{Borrow}(a,p,u)$
coming into $u$ and edge $\mathit{Borrow}(u,q,b)$ going out of $u$, add an
edge $\mathit{Borrow}(a,p::q,b)$. (2) Delete all edges coming into and going
out of $u$. The definition of $\mathit{elim}(B,u)$ ensures that all transitive
borrow relationships going through the reference at the top of the operand
stack are maintained even when the top is popped.

The two rules for ${{\bf{StoreLoc}}}\left<x\right>$ use a combination of the
techniques introduced for handling ${{\bf{MoveLoc}}}\left<x\right>$ and
${\bf{Pop}}$. If $x$ is available in the local store and is a reference type,
$\Pi(0,x)$ is eliminated in the borrow graph. If $x$ is available in the local
store and is a value type, then it is checked that there are no borrow edges
going out of $\Pi(0,x)$. In both cases, the position for the previous top of
stack is renamed to $\Pi(0,x)$ since it is being moved into variable $x$.

The rule for ${{\bf{BorrowLoc}}}\left<x\right>$ uses the operation
$\mathit{factor}$. The expression $\mathit{factor}(B,u,v)$, where $u$ may but
$v$ may not have borrow edges incident in $B$, creates a new borrow graph by
redirecting edges going out of $u$ to go out of $v$ and adding a new edge
$\mathit{Borrow}(u,\varepsilon,v)$. This operation ensures that borrows from
$u$ are propagated to $v$.

The first rule for ${{\bf{BorrowField}}}\left<f,x\right>$ addresses the case
when the source reference is mutable and creates a mutable borrow from it.
This rule uses a variation of factor named $\mathit{factor}_{f}$, a partial
operation with similar inputs as $\mathit{factor}$. This operation succeeds if
there is no edge labeled $\varepsilon$ or $*$ coming out of $u$ in $B$,
converting each edge of the form $\mathit{Borrow}(u,f::p,a)$ to
$\mathit{Borrow}(v,p,a)$ and adding the edge $\mathit{Borrow}(u,f,v)$. This
rule ensures that any borrows from variable $x$ along the field $f$ are
instead borrows from the new reference pushed on the operand stack which is
itself borrowed from $x$.

The second rule for ${{\bf{BorrowField}}}\left<f,x\right>$ addresses the case
when the source reference is immutable and creates an immutable borrow from
it. This rule simply adds a borrow edge labeled $f$ between the source
reference and the new reference.

The rule for ${{\bf{CopyLoc}}}\left<x\right>$ is similar to
${{\bf{BorrowLoc}}}\left<x\right>$ in case the variable $x$ being copied is a
reference. The rule for ${\bf{WriteRef}}$ checks that the target reference
does not have any borrow edges coming out of it. The rules for
${\bf{FreezeRef}}$ and ${\bf{ReadRef}}$ both check that the reference operand
at the top of the stack is freezable, i.e., all borrowed references from it
are immutable. If a mutable reference is freezable, it is safe to convert it
into an immutable reference. For space reasons, we skip over the rules for
${\bf{Pack}}$, ${\bf{Unpack}}$, and ${\bf{Op}}$ which do not perform any
reference-related operations.

The rule for ${{\bf{Call}}}\left<\rho^{\prime}\right>$ can be understood as a
sequence of simple steps. First, it checks that no mutable reference being
passed to $\rho^{\prime}$ is borrowed. Second, it renames the call arguments
present on the operand stack to the corresponding locals in the next frame to
simulate the call (see definition of $B_{1}$). Third, it simulates the return
from the call by adding borrow edges from input reference parameters to output
references returned by the call (see definition of $B_{2}$ and $B_{3}$) and
eliminating the locals in the callee frame (see definition of $B^{\prime}$).
The definitions of $B_{2}$ and $B_{3}$ use the $\mathit{extend}$ operation.
The expression $\mathit{extend}(B,\mathit{us},\mathit{vs})$, where
$\mathit{us}$ and $\mathit{vs}$ are sets of locations with borrow edges
incident on locations in $\mathit{us}$ but no borrow edges incident on
locations in $\mathit{vs}$, adds an edge $\mathit{Borrow}(u,*,v)$ for every
$u\in\mathit{us}$ and $v\in\mathit{vs}$. Furthermore, the definition of
$B^{\prime}$ uses a generalization of $\mathit{elim}$ that eliminates a set of
locations in the borrow graph one at a time.

The rule for ${\bf{Ret}}$ checks that no local of value type is borrowed, the
contents of the operand stack matches the output signature of $\rho$, and no
output that is a mutable reference is borrowed. This ensures that returned
references are valid and the caller’s expectations for borrow relationships
are sound.

###  4.2. Global Memory

We have formalized a borrow analysis that operates on a subset of Move with
references to local variables on the call stack. In this section, we
informally describe how to amend this model to support global storage. The
analysis extensions are straightforward additions to the borrow graph domain
that do not require changes to the existing rules.

We model global storage as an extra component $G$ in the concrete program
state $\left<P,S,M,G\right>$, where $G$ maps a type $t\in\mathit{ValType}$ and
an address $a\in{\tt Addr}$ to a location $c\in\mathit{Loc}$. The extended
borrow checker uses the acquires annotation described in §2.4 to abstract $G$
in the global access instructions described in Section2.4. We treat each type
$t$ in the acquires list of a procedure $\rho$ as an extra local variable
$l_{t}$ in the intraprocedural borrow checker rules. The borrow checker
ensures that if there is a reference into a value published at
$\left<t,a\right>$ for any address $a$, then there is a path to this reference
from $l_{t}$ in the borrow graph. This guarantee is achieved by treating
${{\bf{BorrowGlobal}}}\left<t\right>$ similar to
${{\bf{BorrowLoc}}}\left<x\right>$, which allows us to handle
${{\bf{MoveTo}}}\left<t\right>$ and ${{\bf{MoveFrom}}}\left<t\right>$ much
like ${{\bf{StoreLoc}}}\left<x\right>$ and ${{\bf{MoveLoc}}}\left<x\right>$
(respectively).

The borrow checker must perform one additional check: at a
${{\bf{MoveFrom}}}\left<t\right>$, ${{\bf{BorrowGlobal}}}\left<t\right>$, or a
call to a procedure that has $t$ in its acquires list, there must be no
outgoing edges from $l_{t}$ in the borrow graph. Additionally, a separate
acquires static analysis checks that a procedure with any such instructions
has an acquires annotation. Together, these ensure that global reference
instructions cannot create a dangling reference to global memory.

##  5\. Implementation

We have implemented two versions of the borrow checking algorithm in Rust: the
bytecode analysis described above as part of the Move bytecode verifier (1072
lines) and source code variant in the Move compiler (1807 lines). The two
implementations share a borrow graph abstract domain library (481 lines). All
of these components are open-source111Withheld for double-blind review.

###  5.1. Borrow Checker in Move Bytecode Verifier

The bytecode verifier plays the important role of gating the admission of code
to the Anon blockchain: a module can only be published if it is first
certified by the bytecode verifier. The borrow analysis is a key component of
the bytecode verifier, but it relies on several auxiliary analysis passes that
we will briefly describe. Each pass analyzes a single module in isolation
using the type signatures of its dependencies.

#### Control-flow graph construction

The bytecode of each procedure is converted into a control-flow graph over a
collection of basic blocks. Each basic block is a non-empty and contiguous
sub-sequence of the bytecode such that control-flow instructions —
$\bf{Branch}$ or $\bf{Ret}$— only occur as the last instruction of the basic
block. Together, the basic blocks are a partition of the entire bytecode
sequence. The construction of the control-flow graph attempts to create
maximal basic blocks such that there is no jump into the middle of a block.
Simple checks such as non-empty bytecode and ending with a control-flow
instruction are also performed in this analysis. The granularity of all
subsequent analyses is an entire basic block rather than an individual
bytecode instruction.

#### Stack usage analysis

This analysis ensures that the shape-matching property from §4 holds for all
programs. It tracks the height of the operand stack in each basic block and
checks that the heights are equal at each join point.

#### Value type analysis

The goal of this analysis is to make sure that a value is used only if has not
been moved and that each bytecode instruction is applied to values of
appropriate type. Each procedure is analyzed separately exploiting the type
annotations on inputs and outputs of called procedures. This analysis infers
unmoved locals and the types of values on the operand stack using a
straightforward dataflow analysis.

#### Acquires analysis

This straightforward analysis checks that acquires annotations on procedures
(see §4.2) are correct.

#### Borrow analysis

This analysis is the most complex part of reference safety verification. The
borrow checker (§4) requires that each instruction be annotated by an abstract
state. However, our analysis computes these annotations using a fixpoint
computation based on abstract interpretation. The fixpoint computation is
performed locally for each procedure with the local abstract state as its
abstract domain. The key new insight enabling this analysis is a suitable join
operation for the borrow graph. This join of $G$ and $H$ is defined
operationally as follows:

  1. (1)

Take the union of edges in $G$ and $H$.

  2. (2)

For each edge $\mathit{Borrow}(x,p,y)$ in the result, drop the edge if it is
subsumed by another edge $\mathit{Borrow}(x,p^{\prime},y)$.

It is possible for the resulting graph to have cycles even if $G$ and $H$ are
acyclic. The join fails in this case and an error is reported. Thus, when a
fixpoint is reached successfully, we are guaranteed that the computed
annotations create a well-typed program.

###  5.2. Borrow Checker in the Move Compiler

The bytecode borrow checker is designed to simply and efficiently reject bad
code, not help users diagnose reference issues. However, the Move compiler
contains a source-level implementation of the borrow checker that augments the
core algorithm with important tracking information used to provide informative
error messages.

In addition, the compiler uses a liveness analysis to improve the programming
experience in two ways: (1) infer whether a use of a source-level variable
should emit a ${{\bf{CopyLoc}}}\left<x\right>$ bytecode instruction (if $x$ is
live) or a ${{\bf{MoveLoc}}}\left<x\right>$ instruction (otherwise), and (2)
immediately releasing dead references to prevent errors in the stricter
bytecode borrow checker.

##  6\. Evaluation

We claim that our analysis is useful, precise, and efficient.

#### Utility

Move is a new language that is not (yet) officially supported outside of the
Anon project. However, there are two open-source blockchain projects that use
Move by maintaining a fork of the Anon codebase:
dFinance222https://github.com/dfinance/dvm/tree/master/stdlib/modules and
StarCoin333https://github.com/starcoinorg/starcoin/tree/master/vm/stdlib/modules.
Figure 2 summarizes the use of references in each project. We observe that
references passed across procedure boundaries (&Proc) and references to global
storage (GProc) are common—over half of procedure signatures contain a
reference, and more than a third touch global storage.

Reference-related mistakes (e.g., null dereferences, dangling references) in
intricate, reference-heavy code with mutability are ubiquitous in other
languages. Anecdotally, Move is no different here—we frequently made such
mistakes while developing Anon. The difference is that Move reports these
errors at compile-time with a message that points out the unsafe action and
the borrow that precludes it (see Figure 3). This helps programmers
internalize the discipline enforced by the checker and write reference-safe
code.

Project | B | Proc |  &Proc (%) |  GProc (%) | B/ms
---|---|---|---|---|---
Anon | 6.9K | 327 | 196 (60) | 151 (46) | 1.2K
StarCoin | 6.2K | 351 | 171 (49) | 123 (35) | 1.3K
dFinance | 1.2K | 109 | 33 (40) | 30 (28) | 1.3K
Total | 14.6K | 787 | 400 (51) | 304 (39) | 1.2K
Figure 2. Usage of references in three Move codebases. B and Proc quantify the
number of bytecodes and declared procedures for each project. &Proc lists
procedures with a reference in their type signatures and GProc shows
procedures that access global storage. B/ms shows the average number of
bytecode instructions analyzed per millisecond on a 2.4 GHz Intel Core i9
laptop with 64GB RAM.

⬇

7| let x = move c;

^^^^^^ Invalid move of local ’c’

6| let r = &c.f;

\---- It is still being borrowed by this reference

Figure 3. Error message reported by the Move compiler for the first dangling
reference example from §2.2.

#### Precision

Like any static analysis, the Move borrow checker introduces approximations
that may lead it to reject safe programs. Sources of imprecision include
abstracting references either returned by procedures or created on different
sides of a conditional branch, abstracting values in global storage with their
types, and preventing returns of global references.

In our experience with Move, we have only encountered expressivity problems
with the last restriction. Issues usually arise when a module M1 wants to give
a module M2 the ability to perform arbitrary writes to a global value of type
M1::T. In these cases, we used workarounds such as exposing field
setters/getters for the global or combining the two modules.

These workarounds are inconvenient but not fatal—a Move module typically
encapsulates its global values to enforce key safety invariants, so the
pattern of “sharing” globals between modules is uncommon. By contrast,
eliminating references to global storage altogether would break key
programming patterns such as increasing the balance field of an Account value
in-place without removing it from storage.

#### Efficiency

The final column of Figure 2 quantifies the performance of the analysis using
bytecodes analyzed/millisecond as a metric. The results show that the modular,
intraprocedural analysis runs at a consistent rate on projects of different
size. We note that although our current implementation is single-threaded, it
would be easy to parallelize analysis of procedures to further increase the
speed of the analysis.

##  7\. Related Work

#### Borrow-Based Static Analyses

Rust (Matsakis and Klock, 2014) also uses a borrow-based static analysis to
prevent dangling references. Rust’s analysis provides reference safety at the
source level, whereas Move provides this guarantee directly for its executable
representation via bytecode verification. The analyses support different
language features (e.g., Rust allows references in records, Move allows
mutable references to global state) and require different annotations (e.g.,
Rust has reference _lifetime_ annotations, Move has procedure acquires
annotations). We prove that Move’s analysis ensures leak freedom (see §4), but
we are not aware of a similar proof for Rust.

There are also differences in the analysis mechanics. There are two
descriptions of the Rust borrow checker: one that abstracts _reference
lifetimes_ and ensures that the lifetimes of related references are properly
nested (core team, 2017) (formalized in (Reed, 2015; Jung et al., 2018)), and
another that abstracts the relationship between each value and the _set of
loans_ (Matsakis, 2018) involving the value and prevents accesses to loaned
values (formalized in (Weiss et al., 2019; Astrauskas et al., 2019)).

Move’s analysis is philosophically similar to the second approach, but differs
by using a borrow graph domain that preserves structural information about
loans and and values. This allows simpler handling of features like
_reborrowing_ (the Rust term for creating a copy of a unique reference), which
requires Rust formalizations (Weiss et al., 2019; Astrauskas et al., 2019) to
maintain additional state, but is the same as a normal borrow for Move. On the
other hand, Rust’s reference lifetime annotations allow programmers to
precisely specify the relationship between input and output parameters, but
Move does not allow this.

#### Low-Level Enforcement of Memory Safety

Move ensures reference safety for its executable representation without
trusting a compiler using the approach of the JVM (Freund and Mitchell, 2003;
Lindholm and Yellin, 1997) and CLR (Meijer et al., 2000): lightweight analysis
run in a bytecode verifier. Other approaches to certifying low-level memory
safety include typed assembly (Morrisett et al., 2003), proof-carrying code
(Necula, 2011), and _capability machines_ , specialized hardware with a
memory-safe instruction set (Skorstengaard et al., 2019, 2020; Woodruff,
2014). Each of these approaches has merits in its targeted application
domains. We chose a bytecode language with a co-designed verifier for Move to
accommodate mutable, persistent global storage, gas metering, resource
types(for double-blind review, 2019b), and other features required for Move’s
use-cases.

## References

  * (1)
  * Astrauskas et al. (2019) Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. 2019.  Leveraging rust types for modular specification and verification.  _Proc. ACM Program. Lang._ 3, OOPSLA (2019), 147:1–147:30.
  * core team (2017) Rust core team. 2017\.  RFCs: 2094-NLL.  https://github.com/rust-lang/rfcs/blob/master/text/2094-nll.md.
  * for double-blind review (2019a) Withheld for double-blind review. 2019a.  The Anon Blockchain.
  * for double-blind review (2019b) Withheld for double-blind review. 2019b.  Move: A Language With Programmable Resources.
  * for double-blind review (2019c) Withheld for double-blind review. 2019c.  State Machine Replication in the Anon Blockchain.
  * for double-blind review (2020) Withheld for double-blind review. 2020\.  The Move Prover. In _CAV_ _(Lecture Notes in Computer Science, Vol. 12224)_ , Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 137–150.
  * Freund and Mitchell (2003) Stephen N. Freund and John C. Mitchell. 2003.  A Type System for the Java Bytecode Language and Verifier.  _J. Autom. Reason._ 30, 3-4 (2003), 271–321.
  * Grech et al. (2020) Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2020.  MadMax: analyzing the out-of-gas world of smart contracts.  _Commun. ACM_ 63, 10 (2020), 87–95.
  * Jones and Muchnick (1979) Neil D. Jones and Steven S. Muchnick. 1979.  Flow Analysis and Optimization of LISP-like Structures. In _POPL_.
  * Jung et al. (2018) Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018.  RustBelt: securing the foundations of the rust programming language.  _PACMPL_ 2, POPL (2018), 66:1–66:34.
  * Lamport (1984) Leslie Lamport. 1984\.  Using Time Instead of Timeout for Fault-Tolerant Distributed Systems.  _ACM Trans. Program. Lang. Syst._ 6, 2 (April 1984), 254–280.
  * Lindholm and Yellin (1997) Tim Lindholm and Frank Yellin. 1997.  _The Java Virtual Machine Specification_.  Addison-Wesley.
  * Matsakis (2018) Niko Matsakis. 2018\.  An alias-based formulation of the borrow checker.  http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/.
  * Matsakis and Klock (2014) Nicholas D. Matsakis and Felix S. Klock, II. 2014.  The Rust Language.  _Ada Lett._ 34, 3 (Oct. 2014), 103–104.
  * Meijer et al. (2000) Erik Meijer, Redmond Wa, and John Gough. 2000.  Technical Overview of the Common Language Runtime.
  * Morrisett et al. (2003) J. Gregory Morrisett, Karl Crary, Neal Glew, and David Walker. 2003\.  Stack-based typed assembly language.  _J. Funct. Program._ 13, 5 (2003), 957–959.
  * Nakamoto (2008) Satoshi Nakamoto. 2008\.  Bitcoin: A peer-to-peer electronic cash system.  (2008).  http://bitcoin.org/bitcoin.pdf
  * Necula (2011) George C. Necula. 2011\.  Proof-Carrying Code.  In _Encyclopedia of Cryptography and Security, 2nd Ed_ , Henk C. A. van Tilborg and Sushil Jajodia (Eds.). Springer, 984–986.
  * Pérez and Livshits (2020) Daniel Pérez and Benjamin Livshits. 2020.  Broken Metre: Attacking Resource Metering in EVM. In _NDSS_. The Internet Society.
  * Reed (2015) Eric Reed. 2015\.  _Patina: A formalization of the Rust programming language_.  Technical Report. University of Washington.
  * Schneider (1990) Fred B. Schneider. 1990\.  Implementing Fault-tolerant Services Using the State Machine Approach: A Tutorial.  _ACM Comput. Surv._ 22, 4 (Dec. 1990), 299–319.
  * Skorstengaard et al. (2019) Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2019\.  StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities.  _Proc. ACM Program. Lang._ 3, POPL (2019), 19:1–19:28.
  * Skorstengaard et al. (2020) Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2020\.  Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management.  _ACM Trans. Program. Lang. Syst._ 42, 1 (2020), 5:1–5:53.
  * Szabo (1997) Nick Szabo. 1997\.  Formalizing and Securing Relationships on Public Networks.  _First Monday_ 2, 9 (1997).  https://ojphi.org/ojs/index.php/fm/article/view/548
  * Weiss et al. (2019) Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019.  Oxide: The Essence of Rust.  arXiv:1903.00982 [cs.PL]
  * Wood (2014) Gavin Wood. 2014\.  Ethereum: A secure decentralised generalised transaction ledger.  (2014).  https://ethereum.github.io/yellowpaper/paper.pdf
  * Woodruff (2014) Jonathan Woodruff. 2014\.  _CHERI: a RISC capability machine for practical memory safety_.  Ph.D. Dissertation. University of Cambridge, UK.