1 basicstyle=, identifierstyle=, keywordstyle=[1], keywordstyle=[2],
keywordstyle=[3], keywordstyle=[4], keywordstyle=[5], keywordstyle=[6],
commentstyle=, stringstyle=, literate=!matches!!matches!1,
columns=spaceflexible, keepspaces=true, showspaces=false, showtabs=false,
showstringspaces=true

# Resource Specifications for Resource-Manipulating Programs

Zachary Grannan  University of British ColumbiaVancouverCanada and  Alexander
J. Summers  University of British ColumbiaVancouverCanada

###### Abstract.

Specifications for modular program verifiers are expressed as constraints on
program states (e.g. preconditions) and relations on program states (e.g.
postconditions). For programs whose domain is managing _resources_ of any kind
(e.g. cryptocurrencies), such state-based specifications must make explicit
properties that a human would implicitly understand for free. For example,
it’s clear that depositing into your bank account will not change other
balances, but classically this must be stated as a _frame condition_. As a
result, specifications for resource-manipulating programs quickly become
verbose and difficult to interpret, write and debug.

In this paper, we present a novel methodology that introduces user-defined
first-class resources in the specification language, allowing resource-related
operations and properties to be expressed directly and eliminating the need to
reify implicit knowledge in the specifications. We implement our methodology
as an extension of the program verifier Prusti, and use it to verify a key
part of a real-world blockchain application. As we demonstrate in our
evaluation, specifications written with our methodology are more concise,
syntactically simpler, and easier to understand than alternative
specifications written purely in terms of program states.

††journal: PACMPL††journalvolume: 1††journalnumber: CONF††article:
1††journalyear: 2018††publicationmonth: 1††copyright: none††ccs: Software and
its engineering General programming languages††ccs: Social and professional
topics History of programming languages

##  1\. Introduction

The goal of program verification is to ensure that a program will always
operate in accordance with a formal specification. In practice, this requires
encoding the desired properties in the specification language of a program
verifier that will be used to check conformance to such properties. The
difference between our intuitive, human language description of desired
properties and their representation in the specification language is called
the _semantic gap_ (Hein, 2010). The larger this gap is in practice, the more
difficult it becomes to write, read, maintain, and debug specifications.

In modular program verifiers, specifications are written and checked for each
function separately. Specification preconditions describe requirements on the
program state at function call sites, and postconditions describe the
corresponding guarantees about the program state at return sites; the verifier
reasons about function calls with respect to these specifications rather than
the function’s implementation. For example, the specification for a function
sort() that sorts a list in-place could be written as an expression relating
the values of the input list both before and after the call; namely, stating
that the latter should be a sorted version of the former. This design
effectively minimises the semantic gap for properties naturally expressed as
relations on program states, such as sortedness.

However, properties about programs that manipulate resources, such as money,
are more challenging to specify correctly in this manner. For example, in a
banking application, one might consider describing the effect of a function
deposit(acct_id, amt), using a postcondition:

⬇

#[ensures(balance(acct_id) == old(balance(acct_id)) + amt)]

which specifies that after calling deposit() the balance for acct_id will have
increased appropriately. However, this specification misses an important
property: the balance of all _other_ accounts in the bank must remain
_unchanged_ after the call. To address this, it is necessary to add a _frame
condition_ (McCarthy and Hayes, 1981) to the specification, resulting in the
postcondition:

⬇

#[ensures(balance(acct_id) == old(balance(acct_id)) + amt) &&

forall(|a_id: AcctId| a_id != acct_id ==> balance(a_id) ==
old(balance(a_id))))]

This specification is longer and more complicated; most of the complexity
stems from describing what’s _unchanged_ by deposit() (this extra complexity
grows rapidly for more complicated functions). But in terms of an intuitive
understanding of bank deposits, this property simply doesn’t _need_ to be
stated: it’s obvious to humans that depositing money into one account will not
change other balances. This suggests a wide semantic gap between the way we
think about resources in the real-world, and what can be expressed in
classical techniques for formal specification.

In this paper, we present a novel specification methodology that narrows this
gap by introducing custom resources and a language of resource properties and
operations as _first-class elements_ of our specification language. Our
methodology allows resource-related properties to be expressed directly, and
eliminates the need to reify properties that are implicit in our intuitive
understanding of resources, while building in ubiquitous properties by
default, e.g. that the amount of a resource should remain constant unless
explicitly created or destroyed.

The usage of our custom resources in specification methodology is an
abstraction decoupled from the underlying program representations of these
notions. However, our technique allows coupling invariants to be defined,
specifying once and for all the mapping between abstract resource notions and
concrete program states. Specifications per function can be written concisely
and more simply using resource abstractions, and the coupling invariants
automatically and implicitly entail the right proof obligations concerning
changes to and constraints on concrete program states.

Our paper makes the following main contributions:

  1. (1)

We demonstrate the typical problems that arise when writing specifications of
resource-manipulating programs in terms of program states (Sec. 2)

  2. (2)

We present a methodology to solve these problems using first-class resources
(Sec. 3)

  3. (3)

We implement our methodology, extending the Prusti verifier (Astrauskas et
al., 2019) (Sec. 4)

  4. (4)

As a case study, we apply our methodology and implementation to verify a key
component of a real-world Rust implementation of a cross-chain token transfer
protocol (Sec. 5)

  5. (5)

We perform a comparative evaluation of our methodology, showing that it
enables users to write shorter and simpler specifications for resource-
manipulating programs (Sec. 6)

##  2\. Motivation

⬇

1impl Bank {

2 pub fn balance(&self, acct_id: AcctId) -> u32 {

3 self.map.get(acct_id).unwrap_or(0) // 0 returned if no entry in map

4 }

5 pub fn deposit(&mut self, acct_id: AcctId, amt: u32) {

6 let bal = self.balance(acct_id); self.map.insert(acct_id, bal + amt);

7 }

8 pub fn withdraw(&mut self, acct_id: AcctId, amt: u32) {

9 let bal = self.balance(acct_id); self.map.insert(acct_id, bal - amt);

10 }

11}

Figure 1. Rust code defining a Bank struct and implementation of banking
operations. Account balances are stored in a U32Map mapping AcctIds to u32
values; deposits and withdrawals update the map entries.

To motivate our methodology, we first present the challenges that arise when
writing specifications for a resource-manipulating program. Throughout this
section, we consider a Rust implementation of a multi-account bank that stores
(dollar) balances, shown in Fig. 1. The struct Bank manages the balances for
multiple accounts in the field map, each account is identified by a
corresponding AcctId. Clients of the Bank cannot access map directly; they
interact with the Bank object via the functions balance(), deposit(), and
withdraw(), within the impl Bank {...} block.

These functions take as first parameter a reference to the Bank instance. The
syntax &self indicates a Rust _shared reference_ , with which the balance
function cannot modify the Bank, while a _mutable reference_ such as the &mut
self parameter of the other functions allows modifications. A Bank stores
account balances in a U32Map that maps account identifiers to u32 values. The
balance() function looks up an account identifier in the map, returning 0 if
there is no entry. The functions deposit() and withdraw() update the map,
overwriting any existing entry.

Specifications for the Bank API play two main roles: defining what it means
for the _implementation_ of these functions to be correct (e.g. withdraw must
correctly update the right balance), and defining what _client code_ should
consider when using this API. For example, withdrawing more than the current
balance should be forbidden, while to specify (and modularly verify) a client
function such as transfer below relies on having suitable specifications for
withdraw and deposit:

⬇

1 bank.withdraw(from, amt); bank.deposit(to, amt);

2}

Our bank example is substantially less complex than typical real-world code,
but writing correct specifications for it in a classical fashion can
nonetheless be challenging and subtle. We now demonstrate three specific
issues that we encounter when trying to specify this kind of code.

⬇

2 forall(|acct_id2: AcctId| if acct_id == acct_id2 {

⬇

3 self.balance(acct_id) == old(self.balance(acct_id)) + amt

⬇

4 } else {

5 self.balance(acct_id2) == old(self.balance(acct_id2))

6 })

⬇

7)]

8fn deposit(&mut self, acct_id: AcctId, amt: u32) { ... }

9#[requires(self.balance(acct_id) >= amt)]

10#[ensures(

⬇

12 forall(|acct_id2: AcctId| if acct_id == acct_id2 {

⬇

13 self.balance(acct_id) == old(self.balance(acct_id)) - amt

⬇

14 } else {

15 self.balance(acct_id2) == old(self.balance(acct_id2))

16 })

⬇

17)]

18fn withdraw(&mut self, acct_id: AcctId, amt: u32) { ... }

Figure 2. Specifications for the deposit() and withdraw() functions. Each
includes an explicit frame condition; specification lines used to encode the
frame condition are highlighted in red.

###  2.1. Three Issues of Specifying Resource-Manipulating Programs

A typical specification for our Bank implementation would define
postconditions for deposit() and withdraw() in terms of calls to balance(). As
discussed in the introduction, an intuitive (but ultimately insufficient)
postcondition for deposit() could be written as follows:

⬇

1fn deposit(&mut self, acct_id: AcctId, amt: u32) { ... }

Although this is a correct postcondition for the implementation, it is not
sufficient for (modular) client reasoning: it specifies the change to
balance(acct_id) but doesn’t say anything about _other_ balances (which should
be unchanged). The standard solution is to extend the postcondition with a
_frame condition_ , specifying that the balances of all other accounts remain
unchanged. The withdraw() function also requires similar frame conditions. A
correct such specification for deposit(), and the analogous specification for
withdraw(), are presented in Fig. 2. Adding frame conditions makes the
resulting specifications more complex: much of the specification effort is
concerned with precisely specifying what does _not_ change. Similar frame
conditions are also necessary for any function with a mutable reference to the
Bank, such as transfer() above, whose postcondition must specify overall what
has not changed.

Deriving a frame condition for transfer() is not simply a matter of, say,
conjoining those for the two called functions; instead, one should rethink
these specifications as describing _state updates_ , mentally compose these
updates, and deduce the right end-to-end specification of their composition:
the appropriate postcondition of transfer() is presented in Fig. 3. Note that
the postcondition does not directly use the specification expressions from
deposit() or withdraw().

⬇

1#[ensures(forall(|a_id: AcctId|

2 if a_id == from { bank.balance(a_id) == old(bank.balance(a_id)) - amt }

3 else if a_id == to { bank.balance(a_id) == old(bank.balance(a_id)) + amt }

4 else { bank.balance(a_id) == old(bank.balance(a_id)) }))]

5fn transfer(bank: &mut Bank, from: AcctId, to: AcctId, amt: u32) { ... }

Figure 3. A specification for the transfer() function, which makes calls to
withdraw() and then deposit()

This demonstrates the first issue with classical specifications in this
context:

Issue 1: Specifying resource operations using program states requires frame
conditions

⬇

1 bank.withdraw(acct_id1, 1); bank.withdraw(acct_id2, 2);

2}

Figure 4. A function that performs two withdrawals in sequence. When acct_id1
and acct_id2 are the same, this function performs two operations on the same
account.

Deriving frame conditions for the composition of multiple operations requires
syntactic and mental overhead. But similar composition issues can arise even
without consideration of frame conditions. For example, consider the function
withdraw2() in Fig. 4, which performs two withdrawal operations in sequence.
When we consider how to specify the precondition of this function, based on
the precondition of the withdraw() function (Fig. 2), we might consider using:

⬇

#[requires(bank.balance(acct_id1) >= 1 && bank.balance(acct_id2) >= 2)]

This precondition is not strong enough however: when acct_id1 = acct_id2, the
withdraw2() function would withdraw $3 from the account. Therefore, a precise
precondition needs to explicitly branch on whether both identifiers are the
same. Furthermore, the analogous issue exists with the _postcondition_ : the
way we represent the change in program state differs depending on the aliasing
of the parameters. An accurate specification for the withdraw2() function is
presented in Fig. 5.

⬇

1 else { bank.balance(acct_id1) >= 1 && bank.balance(acct_id2) >= 2 })]

2#[ensures(if(acct_id1 == acct_id2) {

3 bank.balance(acct_id1) == old(bank.balance(acct_id1) - 3)

4} else {

5 bank.balance(acct_id1) == old(bank.balance(acct_id1) - 1) &&

6 bank.balance(acct_id2) == old(bank.balance(acct_id2) - 2)

7} && forall(|acct_id: AcctId| (acct_id != acct_id1 && acct_id != acct_id2)
==>

8 bank.balance(acct_id) == old(bank.balance(acct_id))

9))]

10fn withdraw2(bank: &mut Bank, acct_id1: AcctId, acct_id2: AcctId) { ... }

Figure 5. The specifications for the withdraw2() function in Fig. 4. The
conditional in the precondition is necessary to handle the possible aliasing
between acct_id1 and acct_id2. The postcondition includes an analogous
conditional, as well as a frame condition stating that other account balances
remain unchanged.

Again, to systematically derive such a specification requires considering the
_updates_ described by the specifications of the called functions, mentally
composing these side-effects, and mapping the resulting transformation back to
a state-based specification (case-splitting for aliasing as needed). The
complexity of this process increases significantly as the number of operations
increases. For example, the specification for a hypothetical withdraw3()
function would need to branch on all of the aliasing possibilities between
three parameters. This illustrates the second issue:

Issue 2: Specifications of resource operations using program states do not
easily compose

The specifications for the Bank should dictate how clients are allowed to
interact with it. They prevent e.g. overdrawing an account via the
precondition self.balance(acct_id) >= amt on withdraw(). But they doesn’t
enforce _inherent_ properties of how resources should behave. Note that
deposit does not have a precondition: the specifications do not restrict calls
to deposit().

⬇

1fn transfer(bank: &mut Bank, from: AcctId, to: AcctId, amt: u32) {

2 bank.withdraw(from, amt); bank.deposit(to, amt); bank.deposit(to, amt);

3}

Figure 6. A buggy transfer function that performs two deposits instead of one

Fig. 6 shows an alternative (faulty) transfer implementation: it deposits more
money in account to than was withdrawn from account from, effectively creating
money out of nowhere. The specifications of the Bank do not prevent this
behaviour: the transfer() function verifies. Technically, transfer() is
underspecified: with the complete functional specification of its intended
effect on the to account, the function _would_ fail to verify. But the
conceptual source of the bug is clear from the code even with a weak
specification: it’s wrong for a resource acquired once to be spent twice.
Intuitively, the money spent by deposit should come from somewhere, but this
relies on an understanding of the specific resources the program works with,
and of properties _all_ resources should have, that is only partially explicit
in the program state and its classical specifications.

Issue 3: Specifications using program states cannot easily enforce resource
properties

The root cause underlying all three of these issues is that program states are
not the ideal abstraction for expressing and reasoning about the behaviour of
resource-manipulating programs. Intuitively, we think about such programs in
terms of their operations on resources (e.g. spending money), including
implicit common-sense understanding of how resources work in reality: for
example, resources cannot be duplicated. The key idea behind our work is to
make this abstraction directly available in the specification language,
reifying this informal intuition and all its benefits in a formal technique.
Our technique is presented concretely in the next section, but the basic idea
is to allow (possibly multiple) custom resource types to be declared for a
given program: we might use a resource type to represent money known to be
stored in the bank and/or a resource type to represent money taken _out_ of
the bank. The notion of _how much_ of each of these resources is currently
held is made a (ghost) part of the program state (the _resource state_), and
new specification features are provided that define how much resource is
_transferred_ in and out of function calls.

The default interpretation of these transfers is that if we don’t specify that
one happens, it _cannot_ , allowing specifications to describe local updates
without explicit frame conditions (Issue 1). Since resource transfers directly
express _changes_ to the resource state, they compose easily (Issue 2). Using
a custom resource to represent _withdrawn_ money prevents the faulty code in
Fig. 6, since the attempt to spend a resource which is no-longer held can be
made explicit with our first-class resources and the built-in properties that
come with our resource model (Issue 3).

In the next section, we demonstrate how our methodology enables this kind of
reasoning.

##  3\. Methodology

The core idea of our approach is to enable program behaviour to be specified
directly in terms of notions of resource relevant to the program. _Resources_
in our methodology are conceptually a pair of a _resource type_ and a
_resource amount_ (an integer). Resource types are organised into
parameterised _resource kind_ s: a named _resource constructor_ with fixed
arity (possibly zero) and corresponding parameter types; each instantiation of
these parameters yields a distinct _resource type_. For example, we might use
a resource kind Money with a single parameter representing an account ID to
represent currency known to be deposited in the corresponding bank account.

In our Prusti implementation, such a resource kind is declared as a Rust
struct annotated with a #[resource_kind] tag, listing its parameter types;
resource types are denoted by instantiating the struct with appropriate (Rust)
expressions. For example, we can declare a resource constructor for the amount
of money belonging to a particular account as follows:

⬇

#[resource_kind] struct Money(AcctId);

Resources of the same type are always aggregated to the sum of their amounts,
and resources of different types are incomparable. In our example, the fact
that for two _different_ account IDs id1 and id2, the corresponding resource
types Money(id1) and Money(id2) are different encodes the property that money
in different accounts should not be fungible; withdrawing money from your
account should have a meaning distinct from withdrawing from someone else’s!

We use the syntax resource(rtype, amt) to denote resources, where rtype is a
resource type, and amt is the amount. For example, the expression
resource(Money(a_id), amt) refers to an amount amt of money for the account
associated with the identifier a_id.

###  3.1. Resource Operations

Our methodology defines three _resource operations_ : resources can be
created, _destroyed_ , and _transferred_. We denote creation and destruction
by produce!() and consume!() respectively. In our Bank example, using the
resource type Money(a_id) to represent deposited currency, deposits should
create resource and withdrawals destroy it. This idea is realised by
instrumenting the bodies of the deposit and withdraw functions as shown in
Fig. 7.

Intuitively, it is only possible to destroy a resource if it is currently
held: our methodology requires that the resource resource(Money(acct_id), amt)
is available to destroy at the point of the consume!() inside withdraw()
(otherwise verification will fail). Conceptually, the caller of withdraw needs
to give up this resource: we express that they must _transfer_ it from their
(calling) context by specifying the resource in the function precondition (cf.
Fig. 7). Analogously, we specify that deposit() transfers a resource back to
the caller by placing it in the function’s postcondition.

⬇

1 #[ensures(resource(Money(acct_id), amt))]

2 fn deposit(&mut self, acct_id: AcctId, amt: u32) {

3 ...; produce!(resource(Money(acct_id), amt));

4 }

5 #[requires(resource(Money(acct_id), amt))]

6 fn withdraw(&mut self, acct_id: AcctId, amt: u32) {

7 ...; consume!(resource(Money(acct_id), amt));

8 }

9}

Figure 7. The specification of Bank, described in terms of the resource Money.

###  3.2. Resource State

Our methodology associates every stack frame with a _resource state_ ,
tracking the resources currently held by the function invocation. This is
_ghost state_ ; we use it as a concept for static reasoning about the program
only, but it need not (and will not) actually exist at runtime. A resource
state is a map from resource types to resource amounts, and resource
operations are interpreted with respect to the current resource state.
Creation of resource increments the corresponding map entry, while destruction
decrements it. Destruction operations entail a proof obligation: we need to
prove that sufficient resource is held before it is destroyed, otherwise a
verification error is raised.

Resources are transferred between stack frames at call (and return) sites. The
resource state of each frame is initialised with _only_ the resources
transferred to it from its caller, according to the function’s precondition.
Resources in a function’s postcondition are those it transfers back to its
caller. Transfers also entail proof obligations: the verifier must prove that
the resources transferred away are actually held. This model of resource state
is suitable for modular verification: each function’s initial resource state
is determined purely by its precondition, independently of call site.

###  3.3. Resource State Expressions

The specifications presented in Fig. 7 suffice to characterise the behaviour
of the program in terms of its resource operations. Reifying these resource
transfers make some important properties of the program clearer: e.g. it is
impossible to overdraw an account because withdrawals require a resources
representing at least part of the current balance (see Fig. 8).

⬇

1 bank.deposit(acct_id, amt); bank.withdraw(acct_id, amt);

2 bank.withdraw(acct_id, amt) ; // ERROR: insufficient permission to resource

3}

Figure 8. An example program that would not verify after annotating Bank with
resource operations. The first withdraw() is permitted, because sufficient
resource Money(acct_id) is made available by the preceding deposit() call. A
verification error is raised because there is no resource available for the
second withdraw().

However, our resource specifications so far are completely independent of the
_actual_ implementation state used to track resources. In particular, there is
no specified relationship between resource operations and Bank.balance()
calls. Working towards this, we introduce _resource state expressions_ , which
are used inside specifications to introspect on the resource state. These
expressions are written holds(rtype), and (when used _outside_ of function
specifications (e.g. as inline assertions) denote the amount of resource type
rtype held in the current resource state. For example, holds(Money(acct_id))
denotes the amount of acct_id’s money in the current state.

When holds() is used in function specifications, we define its semantics
differently, considering the fact that the caller and callee resource states
may differ. In such positions, our technique interprets holds() expressions
with respect to the _amount of resource transferred so far_ by the
corresponding pre-/post-condition; this notion has the same meaning for both
caller and callee.

Fig. 9 illustrates this semantics. The first precondition
#[requires(resource(Money(a), 1))] at line 1 specifies a resource to be
transferred from caller to callee. As that is the only resource transferred so
far, the (commented) assertion holds(Money(a)) == 1 holds at 1. The subsequent
line specifies the same resource transfer again, resulting in holds(Money(a))
== 2 (2).

The first postcondition old(holds(Money(a))) == 2) at 3 concerns (via old) the
amount of Money(a) transferred _from the caller_ (this refers to the overall
transfers made by the preconditions together), while the second (4 ) states
that no money has been transferred by the _postconditions_ up to this point.
At 5, located after the postcondition transferring resource(Money(a),1) to the
caller, the commented assertion holds(Money(a)) == 1 would instead be true.

⬇

1#[requires(resource(Money(a), 1))] // holds(Money(a)) == 2 2

2#[ensures(old(holds(Money(a))) == 2)] 3

3#[ensures(holds(Money(a)) == 0)] 4

4#[ensures(resource(Money(a), 1))] // holds(Money(a)) == 1 5

5fn take2return1(bank: &mut Bank, a:AcctId){ bank.withdraw(a, 1); }

6

7#[requires(resource(Money(a),3))]

8fn client(bank: &mut Bank, a: AcctId){ take2return1(bank, a); }

Figure 9. A program demonstrating resource operations and resource state
expressions in specifications.

###  3.4. Coupling Invariants

Finally, we use our resource state expressions to define connections between
the resource state and the actual program state. In our methodology, users
declare _coupling invariants_ to define these connections. Coupling invariants
are expressed as two-state expressions (using old to describe the prior state,
as in a postcondition) that relate the program _and resource_ states at two
points in the program; these invariants are enforced at function return sites.
Coupling invariants are expressed using annotations of the form
#[invariant_twostate($t$)], where $t$ is an expression that can include
specification constructs such as holds() and old() expressions. Although
declared once per type, a coupling invariant $t$ is interpreted as an
additional, implicit postcondition on _every_ function taking a mutable
reference to this type as a parameter; effectively, it is equivalent to adding
the postcondition #[ensures($t$)] to all such functions (this happens
implicitly).

⬇

1 holds(Money(a_id)) - old(holds(Money(a_id))) ==

2 self.balance(a_id) - old(self.balance(a_id))))]

Figure 10. A coupling invariant for the Bank struct, which is enforced between the beginning (via old) and end of each function involving a mutable reference to a Bank. deposit() Specification (Fig. 7) Pre: | <none>
---|---
Post: | #[ensures(resource(Money(acct_id), amt))]
Resource Transfers Denoted by Specification Transferred In: | $\epsilon$
---|---
Transferred Out: | $\\{\texttt{Money}(\texttt{acct\\_id})\to\texttt{amt}\\}$
View of Resource Transfers via holds() Before: | $\forall\texttt{a\\_id}~{}.~{}\texttt{old(holds(Money(a\\_id)))}=0$
---|---
After: | $\forall\texttt{a\\_id}~{}.~{}\texttt{holds(Money(a\\_id))}=\begin{cases}\texttt{amt}&\text{if }\texttt{a\\_id}=\texttt{acct\\_id}\\\ 0&\text{otherwise}\end{cases}$
Derived Postcondition for deposit() (c.f. Fig. 2)
$\forall\texttt{a\\_id}~{}.~{}\texttt{balance(a\\_id)}=\texttt{old(balance(a\\_id))}+\begin{cases}\texttt{amt}&\text{if
}\texttt{a\\_id}=\texttt{acct\\_id}\\\ 0&\text{otherwise}\end{cases}$ Coupling
Invariant Shown in Fig. 10 Figure 11. A diagram indicating how the coupling
invariant from Fig. 10 combines with resource operations of deposit() (Fig. 7)
to derive a postcondition specifying the effect deposit() has on the value of
balance(). The derived postcondition is equivalent to the manually written
postcondition of Fig. 2.

Fig. 10 shows a suitable coupling invariant for our Bank struct. It states
that (across each function it applies to) the change in the value of
balance(a_id) should correspond to the change in resource Money(a_id) for all
account identifiers a_id. To demonstrate the implications of this invariant,
we can consider how it applies to the deposit() function (depicted graphically
in Fig. 11).

The function’s specifications using resource assertions prescribe the
resources to be transferred into and out of the function call; in this
example, none for the (empty) precondition and resource(Money(acct_id), amt)
for the postcondition. This is elaborated (automatically) to a complete
pointwise specification of the effects on all resource types, making explicit
the cases of _no_ transfer via e.g. holds(Money(a_id) == 0 constraints. By
conjoining the coupling invariant, this logically implies a precise
specification relating the values of balance calls between the pre-state and
post-state; exactly the complex postcondition that had to be written manually
for deposit() in Fig. 2. The combination of our novel resource specifications
describing only the effects that _do_ happen, our native resource semantics
and an appropriate coupling invariant, results implicitly in a logically-
equivalent specification expressed much more simply.

Coupling invariants apply to _all_ functions that take a (mutable) reference
to a Bank (in particular, they cannot be forgotten/ignored for a function;
they define a constraint on operations on this type in general). Fig. 12 shows
the specifications for the transfer() function implemented using our
methodology; unlike the original version in Fig. 3, the specification does not
require explicit frame conditions, and (with the exception of the extra
precondition from != to) is a simple composition of the corresponding
specifications of withdraw() and deposit() from Fig. 7. Important resource
notions such as non-duplicability and a built-in notion of resource amount are
built-in: in short, our new methodology addresses the three main specification
issues detailed in Sec. 2.

⬇

1#[requires(resource(Money(from), amt))]

2#[ensures(resource(Money(to), amt))]

3fn transfer(bank: &mut Bank, from: AcctId, to: AcctId, amt: u32) { ... }

Figure 12. The specification of transfer(), described in terms of the resource
Money.

##  4\. Implementation

We implemented our verification technique as an extension of the Rust program
verifier Prusti. Prusti verifies Rust code by encoding the program and
specifications into the intermediate verification language Viper (Müller et
al., 2016), which supports permission-based reasoning using a variant of
implicit dynamic frames (Smans et al., 2009). Although Prusti does not allow
users to directly access Viper’s permission primitives in specifications, it
uses Viper permissions to encode the guarantees provided by Rust’s ownership
model. Our methodology uses Viper’s permission-based reasoning capabilities to
extend Prusti with support for our novel resource reasoning technique.

###  4.1. The Viper Intermediate Verification Language

Viper is an imperative intermediate verification language, in the spirit of
Boogie (Leino, 2008) and Why3 (Bobot et al., 2011). Program verifiers are
built to translate source language (in our case, Rust) verification problems
into Viper programs, which can then be checked by a Viper verifier.

A Viper program consists of a set of methods; Viper methods (whose bodies are
statements) are similar to functions in an imperative language. Viper
statements include variable assignments and method calls, as well as assume
and assert statements that are interpreted in the standard way. Viper also
includes label statements: the statement label $l$ associates the point in the
method where the statement appears with the label $l$. The labels are used in
Viper’s old expressions: the expression old[$l$]($e$) refers to the value of
the expression $e$ at the program point $l$.

Viper supports separation-logic style reasoning: its language and logic has
its own notion of resource state, used to track a variety of _resource
assertions_ (Müller et al., 2016). For the purposes of this paper, the only
relevant Viper resources are _abstract predicate instances_. Viper allows the
declaration of custom _abstract predicates_ using the syntax predicate
$P(x_{1}:T_{1},\ldots,x_{n}:T_{n})$, where $P$ is the predicate name, and
$x_{1}:T_{1},\ldots,x_{n}:T_{n}$ are the names and types of its arguments.
Each instantiation $P(e_{1},\ldots,e_{n})$ of the predicate is treated as a
type of resource to be tracked.

Expressions $\mathtt{acc}(p,\mathit{amt})$ denote an amount $\mathit{amt}$ of
the predicate instantiation $p$. Viper statements inhale $e$ and exhale $e$
add/remove resources described by acc expressions in $e$; for non-resource
expressions they behave as assume/assert statements. Removing (via exhale)
resources not in the state causes a verification error. Viper also supports
perm() expressions that query an amount of resource: an expression
$\texttt{perm(}p\texttt{)}$ refers to the amount of the predicate
instantiation $p$.

###  4.2. Encoding of Resources into Viper

An overview of our translation from our resource specifications into Viper is
shown in Fig. 13. The (overloaded) syntax
$\left\llbracket{}\right\rrbracket{}$ denotes the translation of Prusti
declarations, Rust statements, and Rust types into Viper. We omit the
translation of types, which is unchanged from the prior Prusti encoding
(Astrauskas et al., 2019). Prusti’s encoding of pre-existing features is
unchanged, except for adding additional label statements (used for encoding
our holds() expressions).

The syntax $\left\llbracket{}\right\rrbracket{}_{c}^{o}$ denotes the encoding
of a Prusti expression in the context $c$, $o$. The context changes the way
that holds() expressions are translated into Viper. The first element, $c$,
represents the _current context_ : either _no label_ $\epsilon{}$, or a
_signed label_ $\texttt{-}{}l$ or $\texttt{+}{}l$ (denoting whether we are
currently removing or adding resources). The second element, $o$, represents
the _old context_ taking the form of either $\textit{old}(l)$ or
$\textit{cur}(l)$. These contexts prescribe where (with respect to which
existing label) generated perm() expressions should be evaluated and how they
should be composed. For example, the context $+l^{\prime},\textit{old}(l)$, is
used to encode old(holds()) expressions that occur in the postcondition of a
called function; and are computed by taking the difference of the perm()
expressions taken before and after exhaling the function precondition,
corresponding to labels $l$ and $l^{\prime}$ respectively.

Declarations
$\begin{array}[]{l}\left\llbracket{}\mathtt{\\#[resource\\_kind]~{}struct~{}}R(T_{1},\ldots,T_{n});\right\rrbracket{}\rightsquigarrow\mathtt{predicate~{}}R(\texttt{arg1}:\left\llbracket{}T_{1}\right\rrbracket{},\ldots,\texttt{argn}:\left\llbracket{}T_{n}\right\rrbracket{})\\\
\\\
\left\llbracket{}\begin{array}[]{l}\mathtt{\\#[requires}(f_{\mathit{pre}})\mathtt{]}\\\
\mathtt{\\#[ensures}(f_{\mathit{post}})\mathtt{]}\\\
\mathtt{fn~{}}f(x_{1}:T_{1},\ldots,x_{n}:T_{n})~{}\\{s_{1};\ldots;s_{m}\\}\end{array}\right\rrbracket{}\rightsquigarrow\begin{array}[]{l}\mathtt{method~{}}f(x_{1}:\left\llbracket{}T_{1}\right\rrbracket{},\ldots,x_{n}:\left\llbracket{}T_{n}\right\rrbracket{})\\{\\\
~{}~{}\mathtt{inhale~{}}\left\llbracket{}f_{pre}\right\rrbracket{}_{\epsilon}^{\textit{cur}(l_{\epsilon})};~{}~{}\mathtt{label}~{}\texttt{pre};\\\
~{}~{}\left\llbracket{}s_{1}\right\rrbracket{};\ldots;\left\llbracket{}s_{m}\right\rrbracket{}\\\
~{}~{}\mathtt{label}~{}\texttt{post};~{}~{}~{}\mathtt{exhale}~{}\left\llbracket{}f_{post}\right\rrbracket{}_{\texttt{-}{}\texttt{post}}^{\textit{cur}(\texttt{pre})}\\\
\mathtt{\\}}\end{array}\\\ \end{array}$

Statements
$\begin{array}[]{l}\left\llbracket{}\mathtt{produce!}(t);\right\rrbracket{}\rightsquigarrow\mathtt{inhale~{}}\left\llbracket{}t\right\rrbracket{}_{\epsilon}^{\textit{cur}(\texttt{pre})}\par\quad\quad\par\left\llbracket{}\mathtt{consume!}(t);\right\rrbracket{}\rightsquigarrow\mathtt{exhale~{}}\left\llbracket{}t\right\rrbracket{}_{\epsilon}^{\textit{cur}(\texttt{pre})}\vskip
12.0pt plus 4.0pt minus 4.0pt\\\
\left\llbracket{}f(t_{1},\ldots,t_{n});\right\rrbracket{}\rightsquigarrow\begin{array}[]{l}\mathtt{label}~{}l_{\textit{pre}};~{}\mathtt{exhale~{}}\left\llbracket{}f_{\textit{pre}}[x_{1}:=t_{1},\ldots,x_{n}:=t_{n}]\right\rrbracket{}_{\texttt{-}{}l_{\textit{pre}}}^{\textit{cur}(l_{\epsilon})}\\\
\mathtt{label}~{}l_{\textit{post}};~{}\mathtt{inhale~{}}\left\llbracket{}f_{\textit{post}}[x_{1}:=t_{1},\ldots,x_{n}:=t_{n}]\right\rrbracket{}_{\texttt{+}{}l_{\textit{post}}}^{\textit{cur}(l_{\textit{pre}})}\end{array}\\\
\\\ \end{array}$

Expressions
$\begin{array}[]{l}\left\llbracket{}\mathtt{old}(t)\right\rrbracket{}_{c}^{\textit{cur}(l)}\rightsquigarrow\left\llbracket{}t\right\rrbracket{}_{c}^{\textit{old}(l)}\par\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
\left\llbracket{}R(t_{1},\ldots,t_{n})\right\rrbracket{}_{c}^{o}\rightsquigarrow
R(\left\llbracket{}t_{1}\right\rrbracket{}_{c}^{o},\ldots,\left\llbracket{}t_{n}\right\rrbracket{}_{c}^{o})\par\quad\quad\par\left\llbracket{}\mathtt{resource}(r,t)\right\rrbracket{}_{c}^{o}\rightsquigarrow\mathtt{acc}(\left\llbracket{}r\right\rrbracket{}_{c}^{o},\left\llbracket{}t\right\rrbracket{}_{c}^{o})\vskip
12.0pt plus 4.0pt minus 4.0pt\\\
\left\llbracket{}\mathtt{holds}(r)\right\rrbracket{}_{\epsilon}^{\textit{cur}(l)}\rightsquigarrow\mathtt{perm}(\left\llbracket{}r\right\rrbracket{}_{\epsilon}^{\textit{cur}(l)})\par\quad\quad\quad\hskip
5.0pt\par\left\llbracket{}\mathtt{holds}(r)\right\rrbracket{}_{\epsilon}^{\textit{old}(l)}\rightsquigarrow\texttt{old[}l\texttt{](}\mathtt{perm}(\left\llbracket{}r\right\rrbracket{}_{\epsilon}^{\textit{old}(l)})\texttt{)}\vskip
12.0pt plus 4.0pt minus 4.0pt\\\
\left\llbracket{}\mathtt{holds}(r)\right\rrbracket{}_{\texttt{+}{}l^{\prime}}^{\textit{cur}(l)}\rightsquigarrow\texttt{perm(}\left\llbracket{}r\right\rrbracket{}_{\epsilon}^{\textit{cur}(l)}\texttt{)}~{}\texttt{-}~{}\texttt{old[}l^{\prime}\texttt{](}\texttt{perm(}\left\llbracket{}r\right\rrbracket{}_{\epsilon{}}^{\textit{cur}(l)}\texttt{)}\texttt{)}\\\
\left\llbracket{}\mathtt{holds}(r)\right\rrbracket{}_{\texttt{+}{}l^{\prime}}^{\textit{old}(l)}\rightsquigarrow~{}\texttt{old[}l\texttt{](}\texttt{perm(}\left\llbracket{}r\right\rrbracket{}_{\epsilon{}}^{\textit{old}(l)}\texttt{)}\texttt{)}~{}\texttt{-}~{}\texttt{old[}l^{\prime}\texttt{](}\texttt{perm(}\left\llbracket{}r\right\rrbracket{}_{\epsilon{}}^{\textit{old}(l)}\texttt{)}\texttt{)}\vskip
12.0pt plus 4.0pt minus 4.0pt\\\
\left\llbracket{}\mathtt{holds}(r)\right\rrbracket{}_{\texttt{-}{}l^{\prime}}^{\textit{cur}(l)}\rightsquigarrow\texttt{old[}l^{\prime}\texttt{](}\texttt{perm(}\left\llbracket{}r\right\rrbracket{}_{\epsilon{}}^{\textit{cur}(l)}\texttt{)}\texttt{)}~{}\texttt{-}~{}\texttt{perm(}\left\llbracket{}r\right\rrbracket{}_{\epsilon}^{\textit{cur}(l)}\texttt{)}\\\
\left\llbracket{}\mathtt{holds}(r)\right\rrbracket{}_{\texttt{-}{}l^{\prime}}^{\textit{old}(l)}\rightsquigarrow\texttt{old[}l\texttt{](}\texttt{perm(}\left\llbracket{}r\right\rrbracket{}_{\epsilon{}}^{\textit{old}(l)}\texttt{)}\texttt{)}\\\
\end{array}$

Figure 13. Encoding of Prusti resource constructs into Viper. Labels
$l_{\textit{pre}}$ and $l_{\textit{post}}$ are assumed to be fresh. The label
$l_{\epsilon}$ denotes an arbitrary fresh label that is never referenced,
i.e., a placeholder label used where old expressions are not permitted.

####  4.2.1. Resources and Resource Operations

As described previously, resource types (via their Resource constructors) are
declared in Prusti as a Rust struct, annotated with the tag #[resource_kind].
We encode resource constructors as abstract predicates in Viper; the fields of
the struct are encoded as the arguments to the abstract predicate. We chose
this encoding because abstract predicates in Viper are used to model resources
in Viper’s resource model. Accordingly, we translate resource() expressions
directly into acc() expressions in Viper. Our produce!() and consume!()
statements are encoded as inhale and exhale statements in Viper; these provide
our desired semantics directly.

holds() expressions in the body of a Rust function are encoded as perm()
expressions in Viper. However, as described in Sec. 3.3, our holds()
expressions have a different semantics in pre-/post-conditions (while Viper’s
perm() expressions do not). Encoding our semantics requires a more-complex
translation, using the contexts on our translation function to calculate the
correct differences between perm() expressions at different points in the
program.

###  4.3. Coupling Invariants and Reborrowing

We directly encode coupling invariants (declared with
#[invariant_twostate($t$)] annotations on Rust structs) as postconditions on
the corresponding translated Viper methods. One restriction of our current
methodology is that we do not support Rust functions that _reborrow_ mutable
references, returning to the caller a live mutable reference to e.g. the
internals of the Bank. An example of such a function is shown in Fig. 14,
where a mutable references to one of the balances is handed out to the caller.
Technically, this requires that the _client code_ would become responsible for
maintaining the Bank’s two-state invariant. For untrusted client code (such as
smart contracts running on a blockchain infrastructure), this should not be
relied upon, and rejecting such functions (as we currently do) is the right
approach. A similar issue and its solution has been discussed in the context
of _single-state_ invariants for Prusti (Astrauskas et al., 2022). However,
for _trusted_ client code (e.g. other verified layers of the same software
stack), we believe an adaptation of this idea to support reborrowing with our
two-state invariants, as future work (it remains to consider exactly which
pairs of states we would use to enforce our two-state invariants in potential
extension). This feature has not been needed in practice when applying our
methodology to examples (likely because this additional reliance on client
code for correctness is often not desirable for such programs).

With this encoding in place (and implemented), we can verify Rust code
specified in our methodology directly and automatically, as we evaluate in the
following sections.

⬇

1impl Bank {

2 fn get_balance_ref(&mut self, acct_id: AcctId) -> &mut u32 {

3 self.balances.get_mut(acct_id).unwrap()

4 }

5}

Figure 14. A function that performs a reborrow. The variable self is
inaccessible at the end of the function call and the returned reference can
modify its internal state; the Bank’s two-state invariant cannot yet be re-
established.

##  5\. Case Study

In this case study, we take the core of a Rust implementation (Informal
Systems Inc. and ibc-rs authors, 2022) of a cryptocurrency token transfer
application running on the Interblockchain Communication Protocol (IBC) (Goes,
2020). The token transfer application enables tokens to be sent from one
blockchain to another, without the need for a trusted intermediary; a bug in
the application could inadvertently cause tokens to be destroyed or
duplicated.

###  5.1. The Fungible Token Transfer Application

The IBC token transfer specification allows tokens to be sent between
blockchains with different implementations and consensus mechanisms. Its
design requires that each chain track token ownership for accounts on the
chain, but not for those on other chains. The application has access to a
ledger on each chain; allowing it to mint and burn tokens for arbitrary
accounts on that chain. It “transfers” a token between chains by making ledger
updates on both chains.

A naïve token transfer implementation could operate by destroying the tokens
on one chain and creating them on another. However, the naïve approach has two
issues. First, a chain may not have the capacity to mint some kinds of tokens,
i.e., tokens with fixed supply. Second, this approach would allow an exploit
allowing unrestricted minting of a token on one compromised chain to allow
obtaining an arbitrary amount of that token on any connected chain. In
particular, if a chain $A$ had a vulnerability allowing malicious arbitrary
minting, an attacker could mint on $A$ a token that exists on chain $B$, and
then transfer it to chain $B$.

Instead, the fungible token transfer application performs a token transfer
from chain $A$ to chain $B$ by first sending the token to a special escrow
account on chain $A$, and then minting a _voucher token_ on chain $B$ (shown
in Fig. 15(a)). The denomination of the voucher token is created by prefixing
the denomination of $A$’s token with the identifier of the channel connecting
the two chains.

$t$$\emph{escrow}_{B}$$t$_source_ escrowChain $A$Chain $B$$t^{\prime}$mintdest
(a) Operations performed when sending a native token on $A$ to another chain
$B$. The token is escrowed on $A$ and a voucher is minted on $B$.

$t$$\emph{escrow}_{B}$$t$_dest_ unescrowChain $A$Chain
$B$$t^{\prime}$burnsource (b) Operations performed when sending a voucher
token back to its originating chain. The voucher is burned on $B$ and the
native token is unescrowed on $A$.

Figure 15. Operations of the Token Transfer Application.

Intuitively, the voucher token on $B$ corresponds to the escrowed token on
$A$. In particular, when the application transfers the voucher token back to
$A$, it is burned on chain $B$, and the tokens in the escrow account in chain
$A$ are sent to the recipient (as shown in Fig. 15(b)). The advantage of this
design is that it does not require the token transfer application to mint or
burn _native_ (i.e., non-voucher) tokens. Because this design ensures that
native tokens are never minted, exploits on one chain cannot use the protocol
to inflate the supply of native tokens on other chains.

When a voucher token is transferred to a chain other than its originating
chain, it is treated the same as any other token. This enables tokens to be
transferred transitively across multiple chains. For example, suppose $A$, $B$
and $C$ are blockchains, and $B$ is connected to both $A$ and $C$. Then, a
token on $A$ can be sent to $C$ by first making a transfer from $A$ to $B$,
and sending the voucher minted on $B$ to $C$. $C$ ends up with a voucher for
the token on $B$, which itself is a voucher for the token on $A$.

###  5.2. Application Architecture

The token transfer application is defined with respect to the BankKeeper trait
shown in Fig. 16. The application uses the BankKeeper to manage the ledger on
a particular chain; transfers are accomplished by interacting with instances
of the BankKeeper trait on both chains.

⬇

1struct PrefixedCoin {denom: PrefixedDenom, amount: u32}

2trait BankKeeper {

3 fn send_tokens(&mut self, from: AccountId, to: AccountId, coin:
PrefixedCoin);

4 fn burn_tokens(&mut self, from: AccountId, coin: PrefixedCoin);

5 fn mint_tokens(&mut self, to: AccountId, coin: PrefixedCoin);

6}

Figure 16. The BankKeeper interface

The struct AccountId identifies an account; within BankKeeper these refer to
local accounts (not those on other chains). The struct PrefixedCoin consists
of a token denomination and an integer amount; this type is used in the bank
interface to specify which token should be minted, burned, or transferred. The
struct PrefixedDenom refers to a token denomination: base_denom is the name of
the token on the originating chain, and trace_path denotes the sequence of
token transfers necessary to exchange a token of this denomination with the
one on its original chain.

###  5.3. Properties of the Fungible Token Transfer Application

For our case study, we focused on verifying two key properties of the token
transfer application. We decided on the properties based on suggestions from
collaborators at Informal Systems (responsible for the code). The properties
are as follows:

  * •

Two-Way Peg: After transferring a token from one chain to another, it should
be possible to send the token back to the original account. Performing this
round-trip token transfer should not result in any balance changes on either
chain.

  * •

Preservation of Supply: For any given native token, the sum of the native
token (excluding tokens in escrow accounts) and all derived voucher tokens
should remain constant.

These properties originate from the IBC specification (Goes, 2022), although
the two-way peg property we consider is stronger than the version in the
original specification. To verify the implementation, it was necessary to make
some changes to the code in order to workaround limitations of Prusti. For
example, the TracePath data structure is implemented using data structures
that are not fully supported by Prusti, therefore, we simplified the
definitions of such types. However, these changes are orthogonal to our
verification methodology.

In addition, we have not yet implemented support for coupling invariants on
_traits_ , therefore, to verify the implementation we changed the interface to
define BankKeeper as a struct instead. As the expected properties and
behaviour of the BankKeeper remain the same, this change is not significant,
and the results of our verification are still applicable to the original
design.

The token transfer application relies on implementations of the IBC core
standards (IBC Standards Committee, 2023) to coordinate communication across
chains. For example, executing code on the remote chain involves generating
cryptographic proofs, serialising message data, and routing messages
appropriately. These aspects are unrelated to the application logic itself,
furthermore, verification of these aspects would likely not benefit from our
resource reasoning methodology. Therefore, we assume that these components
function correctly.

###  5.4. Encoding the Specification with Resources

We present our specification by first explaining the resource types that are
used to model the resources in the program (Sec. 5.4.1). We then demonstrate
the specifications for the BankKeeper (Sec. 5.4.2) and constituent functions
of the token-transfer application (Sec. 5.4.3). In Sec. 5.4.4 we present the
specifications used to verify the properties.

####  5.4.1. Representing Tokens with Resource Types

We begin our presentation by identifying appropriate resource types for use in
specifications. First, we note that the two properties above refer to
different aspects of tokens: the two-way peg property is concerned with the
tokens in each account, while the preservation of supply considers the sum of
unescrowed tokens across all accounts. The latter property does not
distinguish between native and voucher tokens, however this distinction is
relevant for the former. Therefore, we define _two_ different resource
constructors, each corresponding to a different aspect of the same tokens. We
declare the first constructor, which is used to encode the two-way peg
property, as follows:

⬇

#[resource_kind] struct Money(BankID, AccountId, PrefixedDenom)

Resources constructed using the constructor Money have distinct resource types
if they belong to different banks, differ in denomination, or have different
owners. We can ensure the two-way peg property by showing that round-trip
transfers do not change the amount of tokens of this type in the resource
state.

Proving the second property requires showing that the total amount of all
unescrowed tokens of a particular base denomination remain unchanged. For this
property, we use a different resource constructor, that treats tokens as
having the same type when they are in the same bank and have the same base
denomination. We declare the constructor as follows:

⬇

#[resource_kind] struct UnescrowedCoins(BankID, BaseDenom);

As previously mentioned, each resource constructor corresponds to a different
view of the same token. Therefore, operations on real tokens should affect the
corresponding resources for each view in a uniform manner. Therefore, we can
define a macro to describe these real-world operations in terms of how they
effect each view of the resource; this macro simplifies the specification,
since it eliminates the need to write resource operations for each view
separately.

⬇

1 resource(Money($bank_id, $to, $coin.denom), $coin.amount) &&

2 if !is_escrow_account($to) {

3 resource(UnescrowedCoins($bank_id, $coin.denom.base_denom), $coin.amount)

4 } else { true }

5}}

Figure 17. A macro that specifies what Prusti resources are changed (i.e.,
either created or destroyed) in response to token operations. An operation on
tokens will always change the Money resource, and also changes the
UnescrowedCoins resource if the target account is not an escrow account.

The resulting macro is presented in Fig. 17. The macro states that a transfer
of a token should always move an instance of the Money resource constructor,
but should only move the corresponding UnescrowedCoins resource if the account
$to is not an escrow account.

####  5.4.2. Specifying the BankKeeper

We use the transfer_money()! macro to annotate BankKeeper’s associated
functions with appropriate resource operations, as presented in Fig. 18.

⬇

1 #[requires(transfer_money!(self.id(), from, coin))]

2 #[ensures(transfer_money!(self.id(), to, coin))]

3 fn send_tokens(&mut self, from: AccountId, to: AccountId, coin:
PrefixedCoin);

4

5 #[requires(transfer_money!(self.id(), from, coin))]

6 fn burn_tokens(&mut self, from: AccountId, coin: PrefixedCoin);

7

8 #[ensures(transfer_money!(self.id(), to, coin))]

9 fn mint_tokens(&mut self, to: AccountId, coin: PrefixedCoin);

10}

Figure 18. The BankKeeper annotated with the appropriate resource operations.

We then connect the resource operations to properties about the program state
by establish coupling invariants on the BankKeeper function, which describe
how changes to Money and UnescrowedCoins in the resource state correspond to
changes in functions balance and unescrowed_coin_balance respectively. These
invariants are shown in Fig. 19.

⬇

1 holds(Money(self.id(), acct_id, denom)) -

2 old(holds(Money(self.id(), acct_id, denom))) ==

3 self.balance(acct_id, denom) - old(self.balance(acct_id, denom))))]

4#[invariant(forall(|coin: BaseDenom|

5 holds(UnescrowedCoins(self.id(), coin)) -

6 old(holds(UnescrowedCoins(self.id(), coin))) ==

7 self.unescrowed_coin_balance(coin) -
old(self.unescrowed_coin_balance(coin))))]

Figure 19. Invariants connecting the resources Money and UnescrowedCoins to
the methods balance() and unescrowed_coin_balance() respectively.

####  5.4.3. Verifying the Application Logic

We now focus our attention to the logic of the token-transfer application
itself. The application performs a token transfer from a chain $A$ to chain
$B$ in two steps. The first step is performed by calling the function
send_fungible_tokens() (Fig. 20) on chain $A$, which disposes of the tokens on
$A$ by either escrowing or burning them. In the second step, it effectively
causes the function on_recv_packet() to be called on chain $B$, which produces
the tokens by either minting or unescrowing tokens as necessary111Technically,
on_recv_packet() in the original version is a callback that is triggered when
a relayer sends a message to chain $B$, however for verification we consider
this as a regular function call. The routing of callbacks is implemented as
part of the IBC core standard, which we assume to be correct and do not
attempt to verify..

Fig. 20 shows a specification and implementation of the send_fungible_tokens()
function (we simply some details for presentation here), which performs the
initial step in the cross-chain token transfer. The arguments port and channel
identify the chain that tokens will be transferred to. The condition on line 8
checks if the token being sent is a voucher for a token on that chain. If so,
then the voucher is burned on this chain (and the next step will unlock the
corresponding token on the other chain). Otherwise, the token is moved to an
escrow account on this chain.

⬇

1#[ensures(!coin.denom.trace_path.starts_with(port, channel) ==>

2 transfer_money!(bank.id(), escrow_address(channel), coin))]

3fn send_fungible_tokens(bank: &mut Bank, coin: &PrefixedCoin, sender:
AccountId,

4 port: Port, channel: ChannelEnd) {

5 if coin.denom.trace_path.starts_with(port, channel) { bank.burn(sender,
coin);}

6 else { bank.send(sender, escrow_address(channel), coin); }

7}

Figure 20. The first step of the fungible token transfer.

The precondition of send_fungible_tokens() specifies that calling the function
transfers the token out of the sender’s account. The postcondition indicates
that when the token did not originate on the opposite chain (i.e., the chain
identified by port and channel), it will be transferred to the escrow account.
Due to space constraints, we do not present the specifications of the second
step of the transfer here; the relevant specification is available in our
supplementary material (Anonymous Authors, 2023).

####  5.4.4. Verifying the Desired Properties

With the above specifications, we can then prove that the token transfer
application satisfies the properties described in Sec. 5.3. To prove the two-
way peg property, we construct a method that performs a round trip token
transfer, and show that the balances of all accounts are unchanged after the
transfer. The relevant specifications are presented in Fig. 21 (the body of
the method is omitted for brevity). We verify the preservation of supply
property by showing that the supply is preserved after an arbitrary transfer;
the specifications are presented in Fig. 22. The specifications of both
properties are expressed in terms of the functions balance() and
unescrowed_coin_balance() respectively.

⬇

1 bank1.balance(acct_id2, denom) == old(bank1).balance(acct_id2, denom)))]

2#[ensures(forall(|acct_id2: AccountId, denom: PrefixedDenom|

3 bank2.balance(acct_id2, denom) == old(bank2).balance(acct_id2, denom)))]

4fn round_trip(bank1: &mut Bank, bank2: &mut Bank, coin: &PrefixedCoin,

5 sender: AccountId, receiver: AccountId, ...) { ... }

Figure 21. The relevant specifications for the two-way peg property. The
function round_trip() performs a token transfer from account sender to
receiver, and then performs the same transfer in the opposite direction.

⬇

1 bank1.unescrowed_coin_balance(c) + bank2.unescrowed_coin_balance(c) ==

2 old(bank1.unescrowed_coin_balance(c) + bank2.unescrowed_coin_balance(c))))]

3fn transfer(bank1: &mut Bank, bank2: &mut Bank, coin: &PrefixedCoin,

4 sender: AccountId, receiver: AccountId, ...) { ... }

Figure 22. The relevant specifications for the supply preservation property.
The function transfer() performs a token transfer from account sender to
receiver.

In conclusion, we’ve shown that our methodology can be applied to a real-world
resource-manipulating program. Using our methodology, we were able to prove
two important properties about the token-transfer application: that it
maintains a two-way peg and preserves total token supply. Our technique allow
us to verify the desired properties in a straightforward manner by describing
resource operations directly, without having to write frame conditions.

##  6\. Evaluation

To evaluate our technique, we consider how specifications written using our
methodology compare to alternative specifications written in terms of program
states. We consider four research questions:

  1. RQ1

(_Conciseness_): Are our specifications _smaller_ than the alternative?

  2. RQ2

(_Complexity_): Are our specifications _simpler_ than the alternative?

  3. RQ3

(_Interpretability_): Are our specifications _easier to understand compared_
to the alternative?

  4. RQ4

(_Verification Time_): Do our specifications _require more time to verify_
than the alternative?

To answer these questions, we compare the specifications we developed in Sec.
5 to an alternative version we constructed, that verifies the same
implementation using specifications written without using our methodology. In
addition, we also apply our methodology to a simplified implementation of the
IBC Non-Fungible Token (NFT) Transfer application (Xi, 2022), again comparing
the results to an alternative version of the specification. The NFT transfer
application has a similar architecture to the token transfer application. We
wrote the implementation ourselves, based on pseudocode in the specification.
We are not aware of a functioning Rust implementation of the protocol;
ultimately we intend to develop our prototype into a verified reference
implementation. A key difference in the application of our methodology between
the two protocols, is that we use resources to model the _permission_ to
change ownership of a token, rather than modelling the token itself. The
specifications and implementation of the NFT transfer application are included
in our supplementary material (Anonymous Authors, 2023).

We now consider each research question in order, describing how we compared
the specifications and presenting our results. We discuss the results in Sec.
6.5.

###  6.1. Conciseness

To measure conciseness, we compared the number of lines of code used to
specify resource-related operations in both specifications. Lines that are
unrelated to resource operations, which are identical in both versions, are
not considered in the comparison. Table 1 provides a comparison between the
number of specification lines required for both specification versions. In
total, the specifications concerned with resource properties (including
invariants and helper macro definitions) consist of 165 lines of code.
Encoding the equivalent specifications without resources required 240 lines.

Context | Usage | Without Resources | With Resources
---|---|---|---
TT-Resources | Resource Constructors | N/A | 4
Coupling Invariants | N/A | 21
transfer_money!() macro | N/A | 10
TT-Bank | burn() | 27 | 1
mint() | 26 | 1
send() | 41 | 2
TT-App | send_fungible_tokens() | 13 | 3
on_recv_packet() | 19 | 6
TT-Properties | send_preserves() | 16 | 26
round_trip() | 19 | 23
NFT-Resources | Resource Constructors | N/A | 2
Coupling Invariants | N/A | 5
transfer_tokens!() macro | N/A | 5
NFT-Bank | burn() | 8 | 2
mint() | 9 | 3
send() | 8 | 3
create_or_update_class() | 4 | 0
NFT-App | send_nft() | 12 | 13
on_recv_packet() | 17 | 11
NFT-Properties | round_trip() | 21 | 24
Total |  | 240 | 165
Table 1. Comparison of the number of specification lines required for the
specifications written with and without resources. Rows prefixed with TT\-
refer to the token transfer specifications, those prefixed with NFT\- refer to
the NFT transfer specifications.

Our methodology requires fewer lines of code to encode the specifications for
the token transfer application’s BankKeeper implementation, as well as the two
main functions of the fungible token transfer application. Our specifications
of the final properties require more lines of code, because they also indicate
the resource operations of send_preserves() and round_trip(). However, the
trade-off is acceptable, because these extra lines also make the specification
more expressive compared to the alternative specification. Furthermore, a
larger difference would be seen if we considered a program with more
functions, because the invariants only need to be written once. The function
create_or_update_class() in the NFT transfer application does modify token
ownership, and therefore does not require any specifications in our
specification; in contrast, the alternative specification requires four lines
of code to explicitly state this property.

###  6.2. Syntactic Complexity

More concise specifications are not necessarily simpler or more desirable. For
example, a longer specification may be preferable to a shorter one if the
latter involves complex nesting of conditionals, implications, and
quantifiers. To evaluate syntactic complexity, we considered the AST nodes of
#[requires()] and #[ensures()] clauses, as well as those of associated
specification-related expressions 222For example, the function
burn_tokens_post(), which expresses the postcondition of burn(), is also used
in the specification of send_fungible_tokens(). We associate the body of
burn_tokens_post() towards the count of burn(), rather than
send_fungible_tokens().. We quantify the complexity of an AST using three
metrics: the total number of nodes in the AST, the maximum depth of the AST,
and the number of unique node types occurring within the AST. We classify the
node types by differentiating arithmetic and comparison operators, and among
Prusti constructs such as forall and old, while disregarding children in the
classification and treating variables and constants uniformly. For example,
the expression a + (b - c) has three different node types: identifiers (a, b,
and c), addition, and subtraction. An overview of the different node types we
consider, and the program we implemented to calculate AST complexity, are
available in our supplementary material (Anonymous Authors, 2023).

Context | Usage | Without Resources | With Resources
---|---|---|---
Size | Depth | Uniq. | Size | Depth | Uniq.
TT-Resources | Resource Constructors | N/A | N/A | N/A | 7 | 2 | 2
Coupling Invariants | N/A | N/A | N/A | 90 | 9 | 9
transfer_money!() macro | N/A | N/A | N/A | 26 | 7 | 8
TT-Bank | burn() | 92 | 10 | 12 | 5 | 3 | 2
mint() | 84 | 10 | 11 | 5 | 3 | 2
send() | 136 | 11 | 14 | 10 | 3 | 2
TT-App | send_fungible_tokens() | 34 | 6 | 7 | 20 | 6 | 5
on_recv_packet() | 45 | 6 | 7 | 20 | 5 | 4
TT-Properties | send_preserves() | 47 | 7 | 9 | 79 | 7 | 10
round_trip() | 53 | 6 | 8 | 72 | 6 | 7
NFT-Resources | Resource Constructors | N/A | N/A | N/A | 4 | 2 | 2
Coupling Invariants | N/A | N/A | N/A | 42 | 10 | 10
transfer_tokens!() macro | N/A | N/A | N/A | 9 | 4 | 5
NFT-Bank | burn() | 29 | 8 | 7 | 10 | 3 | 3
mint() | 37 | 8 | 7 | 18 | 3 | 3
send() | 31 | 8 | 7 | 16 | 3 | 3
create_or_update_class() | 14 | 6 | 5 | 0 | 0 | 0
NFT-App | send_nft() | 56 | 9 | 8 | 50 | 6 | 8
on_recv_packet() | 67 | 9 | 8 | 55 | 7 | 6
NFT-Properties | round_trip() | 65 | 6 | 7 | 81 | 6 | 8
Table 2. Comparison between the syntactic complexity of specifications written
with and without resources. Each column considers the ASTs of the
specification expressions for the function in that row. Size refers to the
total number of nodes in the ASTs. Depth refers to the height of the tallest
AST. Uniq. refers to the number of distinct node types occurring in the ASTs.

We present our results in Table 2. Our results demonstrate that the
specifications written using our methodology are syntactically simpler in most
cases. In particular, specifications related to BankKeeper compare favourably
to the alternative w.r.t. all three metrics: specifications are less than
$1/10^{\text{th}}$ the size, $1/3^{\text{rd}}$ of the depth, and contain less
than $1/5^{\text{th}}$ as many unique nodes. The only area where our
specifications are markedly more complex is with respect to the size of the
specifications for send_preserves() (79 vs 47) and round_trip() (72 vs 53). As
mentioned in the prior subsection, this is due to the requirement to indicate
the resource operations of the functions in additional to the program-state
properties. We note that although the size of the coupling invariants is
relatively large (comparable with the size of mint() and burn()), the
invariant only needs to be written once, regardless of the number of functions
in the program. Therefore, we expect that we our methodology would compare
even more favourably if applied to larger programs.

###  6.3. Interpretability

Interpretability, refers to how easy it is to understand the meaning of a
specification. We approximate interpretability by considering how much of the
specification expresses the _essential aspects_ of the program, that is,
aspects that would also be explicit in a human language description of the
program. For example, the part of a postcondition for mint() that specifies
the balance will increase is essential, however frame conditions in the
specification would not. Intuitively, specifications that mix essential and
non-essential aspects are challenging to interpret, because the reader must
differentiate between the two in order to understand the intent of the
specification.

Our specifications compare favourably w.r.t. this metric: by design, our
methodology only considers essential aspects of resource operations. We have
not formally quantified how much non-essential code is present in the
alternative specifications; however, we note that most of the annotations for
BankKeeper express non-essential aspects. For example, the postcondition of
send_tokens(), shown in Fig. 23(a) consists mostly of non-essential code. In
particular, it includes frame conditions, and also considers separately
different cases depending on whether from and to are escrow accounts. In
contrast, our specification using resources (Fig. 23(b)) expresses the
essential aspects in just lines: the first specifying that the sender’s tokens
are destroyed, and the second specifying that the receiver’s tokens are
created.

⬇

1 self.unescrowed_coin_balance(coin.denom.base_denom) ==

2 if (is_escrow_account(to) && !is_escrow_account(from)) { ... }

3 else if (!is_escrow_account(to) && is_escrow_account(from)) { ... }

4 else { old_bank.unescrowed_coin_balance(coin.denom.base_denom) } &&

5 forall(|acct_id2: AccountId, denom2: PrefixedDenom|

6 self.balance(acct_id2, denom2) ==

7 if(acct_id2 == from && coin.denom == denom2) { ... }

8 else if (acct_id2 == to && coin.denom == denom2) { ... }

9 else { old_bank.balance(acct_id2, denom2) }) &&

10 forall(|c: BaseDenom| c != coin.denom.base_denom ==>

11 self.unescrowed_coin_balance(c) == old_bank.unescrowed_coin_balance(c)

12 )

13}

(a) The postcondition for BankKeeper’s send_tokens() function, specified in
terms of program states.

⬇

1#[ensures(transfer_money!(self.id(), to, coin))]

(b) The specification of send_tokens() written using resource reasoning
constructs. The macro transfer_money!() is defined in Fig. 17.

###  6.4. Verification Time

Application | Without Resources (mean / sd) | With Resources (mean / sd)
---|---|---
Token Transfer | 65.12s / 0.15s | 83.00s / 0.78s
NFT Transfer | 57.04s / 0.23s | 59.88s / 0.36s
Table 3. Comparison of verification time for the specifications written in the
different styles. Results are presented for five runs of the verifier.

We compared the runtime of the specification written using our methodology,
and the alternate version. For each version, we performed five runs, all runs
were performed a 10-core Apple M1 Max. Our results are presented in Table 3.
The verification time for the NFT transfer application is similar for both
versions (59.88s vs 57.04s). There is a larger difference w.r.t. token
transfer application: the specification using resources is 27% slower (83s vs
65.12s). This is most likely due to the overhead of casting between the types
used to represent resource amounts and the types representing bank balances in
the underlying Viper encoding: changing the specification to instead express
balance using Viper’s permission amount types (i.e., rational numbers as
opposed to integers) eliminates the difference (resulting in timings of 88.74s
vs 90.38s respectively). As future work, we believe it could be possible to
reduce the performance overhead associated with such casts.

###  6.5. Analysis / Conclusion

Our evaluation shows that specifications written in our methodology compare
favourably to specifications written in terms of program states. Our
specifications require fewer lines of code and syntactically simpler.
Specifications written using our methodology are also easier to interpret:
this is demonstrated by the observation that specifications written in terms
of program states must express many non-essential properties in their
specifications (e.g. frame conditions). Although our specifications sometimes
require more time to verify, the increase in time is a reasonable trade-off to
make for the simpler specifications. Furthermore, our evaluation indicates
that the increase is due to the behaviour of the underlying Viper verifier
rather than a fundamental consequence of using our methodology.

##  7\. Related Work

Effect systems (Lucassen and Gifford, 1988) extend a type system to include
the side-effects via effect types, which typically over-approximate the side-
effects an expression is allowed to perform. Our resource specifications can
be seen as similar to a kind of effect, but are _precise_ , and apply only to
changes to our ghost resource state. This distinction (and indirection via our
coupling invariants) is crucial to obtaining strong frame properties while
still writing local specifications.

Separation logic (Reynolds, 2002) enables verification of heap-manipulating
programs using local reasoning: assertions describe only the relevant part of
the heap, rather than the heap as a whole. Our resource reasoning technique
takes clear inspiration from this idea of local reasoning, although our
technique intentionally avoids explicit resource reasoning about the concrete
program state. Extensions of separation logic facilitate abstraction with
user-defined predicates (Parkinson and Bierman, 2005), but we note that an
abstraction of our e.g.Bank data structure via abstract predicates would
typically suffer from the same need for frame conditions about _how_ the
internals change over a side-effectful function. Our holds() construct, which
allows introspection on the local resource state, does not have an analogue in
separation logic. However, the Viper intermediate language (Müller et al.,
2016) supports resource reasoning and resource introspection via the perm()
expressions explained in Sec. 4. In contrast to our holds() construct, Viper’s
perm() expressions cannot be used directly in method pre- and postconditions
in a generally-sound way; their semantics is not consistent between how a
caller and callee interpret their meaning (Müller et al., 2016). Being an
intermediate language, Viper provides features powerful enough to encode our
reasoning principles, but places the burden on the user to use these features
soundly. In contrast, our holds expressions can be used freely in pre- and
post-conditions without fear of unsoundness, and the trickier parts of our
encoding (Sec. 4) take care of a correct mapping to Viper automatically.

There is substantial prior work focused on verification of smart contracts
themselves (Ahrendt and Bubel, 2020)(Bräm et al., 2021)(Mohajerani et al.,
2022): while not the specific focus of our work, these are clearly resource-
manipulating programs (used to handle cryptocurrency assets). The verification
tool 2Vyper (Bräm et al., 2021) is closest to our work: it provides its own
resource reasoning via effect clauses for smart contracts in the Vyper
language: these can specify possible resource transfers, and users can also
define invariants that connect the resource state to the runtime state.
However, there are several technical differences with our work: unlike our
system, 2Vyper’s resource specifications describe approximations (in the style
of effect systems) of a function’s behaviour, and over representations of the
entire resource state; there is no way to partition the resource state into a
only a local part that a function is concerned with, which is what eliminates
heavyweight frame conditions in our work.

2Vyper’s effect-clauses consist of a multiset of the operations that will
occur in their execution, but these only refer to the resource operations
performed directly by the function itself: because 2Vyper considers
interactions with unverified external code, it is not possible to reason in
general about external resource operations. In contrast, because we do not
allow untrusted external calls, the specifications in our methodology
effectively summarise the resource operations that occur within a method call.
We have not yet applied our technique to verify interactions with untrusted
code; doing so could be interesting future work.

Ahrendt and Bubel verify Solidity contracts with a proof technique centred
around two-state invariants (Ahrendt and Bubel, 2020). They show that
_differences_ between _wei_ amounts (the built-in currency) are powerful for
expressing such invariants, similar to the encoding of our holds feature into
Viper. They address untrusted code and security properties while we do not; on
the other hand, their work does not support custom notions of resource, build
in resource-like properties, or address data structure framing; their
technique is concerned specifically with currency in Solidity.

Other prior work has focused on verification of smart contracts by modelling
them as extended finite state machines (Mohajerani et al., 2022). Our approach
is more general, as it is not limited to the domain of smart contracts and
does not assume any particular program architecture.

The specification language Chainmail (Drossopoulou et al., 2020) enables user-
defined invariants using holistic specifications, which can be used to enforce
a wide range of security-related properties, including some related to
resources in the program. For example, it is possible to define an invariant
that ensures any change in the balance of a particular account is associated
with a call to deposit() referencing that account. Specifications in Chainmail
must still ultimately be phrased in terms of program states; leading to less
direct and more-complex specifications. In contrast, our methodology, which
treats resources as first class, allows specifications concerning resource
operations directly.

Various smart contract languages provide first-class support for resources.
The Move language (Blackshear et al., 2019), originally developed by Facebook
for the Diem blockchain, supports first-class resources that are implemented
with linear types. Obsidian (Coblenz et al., 2020) uses both linear types and
typestate to prevent bugs related to improper handling of resources. Flint
(Schrans et al., 2018) supports asset types that encapsulate unsafe operations
and provide a safe interface. None of these support static verification
concerning resource quantities, or built-in rules to enforce e.g. that are by-
default preserved.

##  8\. Conclusion

In this paper, we examined the challenges encountered when writing
specifications of resource manipulating programs in terms of program state.
When using a modular verifier, this approach requires users to explicitly
write frame conditions in specifications, and these frame conditions make
specifications lengthier and harder to interpret. Furthermore, such
specifications do not easily compose, and are not expressive enough to rule
out certain kinds of resource-related bugs.

The root cause of these issues is the semantic gap between our high-level,
intuitive expectations of how resources behave, and the language used to write
specifications in the code. Therefore, we developed a new methodology to
support reasoning about resources directly inside specifications, thereby
narrowing the semantic gap.

The methodology we developed extends a program verifier with a first-class
notion of resources, without requiring support for resources in the source
language. Instead, we allow users to define coupling invariants to connect
resource operations to program state. These invariants are checked by the
verifier, allowing users to describe the behaviour of their program in terms
of resource operations rather than as relations on program states.

We implemented our methodology as an extension to the program verifier Prusti,
and evaluated our design by using our extended version of Prusti to verify a
real-world resource-manipulating program. Our evaluation shows that, compared
to a standard Prusti specification written in terms of program states,
specifications written using our methodology are more concise, syntactically
simpler, and easier to understand.

For future work, we would like to extend our methodology to facilitate
interactions with untrusted or external code, as such interactions are typical
in dealing with smart contracts. In particular, enforcing coupling invariants
for functions that reborrow could increase the applicability of our technique.
Finally, we could consider applying our methodology to reason about resources
within a program, such as locks, database connections, or file handles.

## References

  * (1)
  * Ahrendt and Bubel (2020) Wolfgang Ahrendt and Richard Bubel. 2020.  Functional Verification of Smart Contracts via Strong Data Integrity. In _Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III_ _(Lecture Notes in Computer Science, Vol. 12478)_ , Tiziana Margaria and Bernhard Steffen (Eds.). Springer, 9–24.  https://doi.org/10.1007/978-3-030-61467-6_2
  * Anonymous Authors (2023) Anonymous Authors. 2023\.  Supplementary Material.  Supplementary material for the paper: Resource Specifications for Resource-Manipulating Programs.
  * Astrauskas et al. (2022) Vytautas Astrauskas, Aurel Bílỳ, Jonáš Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, and Alexander J Summers. 2022.  The Prusti Project: Formal Verification for Rust. In _NASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings_. Springer, 88–108.
  * Astrauskas et al. (2019) Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J Summers. 2019.  Leveraging Rust Types for Modular Specification and Verification.  _Proceedings of the ACM on Programming Languages_ 3, OOPSLA (2019), 1–30.
  * Blackshear et al. (2019) Sam Blackshear, Evan Cheng, David L Dill, Victor Gao, Ben Maurer, Todd Nowacki, Alistair Pott, Shaz Qadeer, Dario Russi Rain, Stephane Sezer, et al. 2019\.  Move: A Language with Programmable Resources.  _Libra Assoc_ (2019), 1\.
  * Bobot et al. (2011) François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. 2011\.  Why3: Shepherd Your Herd of Provers. In _Boogie 2011: First International Workshop on Intermediate Verification Languages_. 53–64.
  * Bräm et al. (2021) Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, and Alexander J Summers. 2021\.  Rich Specifications for Ethereum Smart Contract Verification.  _Proceedings of the ACM on Programming Languages_ 5, OOPSLA (2021), 1–30.
  * Coblenz et al. (2020) Michael Coblenz, Reed Oei, Tyler Etzel, Paulette Koronkevich, Miles Baker, Yannick Bloem, Brad A Myers, Joshua Sunshine, and Jonathan Aldrich. 2020.  Obsidian: Typestate and Assets for Safer Blockchain Programming.  _ACM Transactions on Programming Languages and Systems (TOPLAS)_ 42, 3 (2020), 1–82.
  * Drossopoulou et al. (2020) Sophia Drossopoulou, James Noble, Julian Mackay, and Susan Eisenbach. 2020.  Holistic Specifications for Robust Programs.. In _FASE_. 420–440.
  * Goes (2020) Christopher Goes. 2020\.  The Interblockchain Communication Protocol: An Overview.  _arXiv preprint arXiv:2006.15918_ (2020).
  * Goes (2022) Christopher Goes. 2022\.  ICS-20 Fungible Token Transfer Specification.  https://github.com/cosmos/ibc/tree/main/spec/app/ics-020-fungible-token-transfer
  * Hein (2010) Andreas M Hein. 2010\.  Identification and Bridging of Semantic Gaps in the Context of Multi-domain Engineering. In _Forum on Philosophy, Engineering & Technology_. 58–57.
  * IBC Standards Committee (2023) IBC Standards Committee. 2023\.  Interchain Standards.  https://github.com/cosmos/ibc
  * Informal Systems Inc. and ibc-rs authors (2022) Informal Systems Inc. and ibc-rs authors. 2022.  ibc-rs.  https://github.com/cosmos/ibc-rs
  * Leino (2008) K Rustan M Leino. 2008\.  This is Boogie 2.  _manuscript KRML_ 178, 131 (2008), 9.
  * Lucassen and Gifford (1988) J. M. Lucassen and D. K. Gifford. 1988.  Polymorphic Effect Systems. In _Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Diego, California, USA) _(POPL ’88)_. Association for Computing Machinery, New York, NY, USA, 47–57.  https://doi.org/10.1145/73560.73564
  * McCarthy and Hayes (1981) John McCarthy and Patrick J Hayes. 1981.  Some Philosophical Problems from the Standpoint of Artificial Intelligence.  In _Readings in artificial intelligence_. Elsevier, 431–450.
  * Mohajerani et al. (2022) Sahar Mohajerani, Wolfgang Ahrendt, and Martin Fabian. 2022\.  Modeling and Security Verification of State-Based Smart Contracts.  _IFAC-PapersOnLine_ 55, 28 (2022), 356–362.
  * Müller et al. (2016) Peter Müller, Malte Schwerhoff, and Alexander J Summers. 2016\.  Viper: A Verification Infrastructure for Permission-based Reasoning. In _Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings 17_. Springer, 41–62.
  * Parkinson and Bierman (2005) Matthew Parkinson and Gavin Bierman. 2005.  Separation Logic and Abstraction. In _Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Long Beach, California, USA) _(POPL ’05)_. Association for Computing Machinery, New York, NY, USA, 247–258.  https://doi.org/10.1145/1040305.1040326
  * Reynolds (2002) John C Reynolds. 2002\.  Separation Logic: A Logic for Shared Mutable Data Structures. In _Proceedings 17th Annual IEEE Symposium on Logic in Computer Science_. IEEE, 55–74.
  * Schrans et al. (2018) Franklin Schrans, Susan Eisenbach, and Sophia Drossopoulou. 2018\.  Writing Safe Smart Contracts in Flint. In _Companion Proceedings of the 2nd International Conference on the Art, Science, and Engineering of Programming_. 218–219.
  * Smans et al. (2009) Jan Smans, Bart Jacobs, and Frank Piessens. 2009.  Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. In _ECOOP 2009–Object-Oriented Programming: 23rd European Conference, Genoa, Italy, July 6-10, 2009. Proceedings 23_. Springer, 148–172.
  * Xi (2022) Haifeng Xi. 2022\.  ICS-721 Non-Fungible Token Transfer Specification.  https://github.com/cosmos/ibc/tree/main/spec/app/ics-721-nft-transfer