11institutetext: Novi Research, Meta Platforms, Menlo Park, USA

# Fast and Reliable Formal Verification of Smart Contracts with the Move
Prover††thanks: To appear in TACAS’22. This is the extended version with
appendices.

David Dill  Wolfgang Grieskamp(✉) Correspondence to<EMAIL_ADDRESS>
Junkil Park  Shaz Qadeer  Meng Xu  Emma Zhong

###### Abstract

The Move Prover (MVP) is a formal verifier for smart contracts written in the
Move programming language. MVP has an expressive specification language, and
is fast and reliable enough that it can be run routinely by developers and in
integration testing. Besides the simplicity of smart contracts and the Move
language, three implementation approaches are responsible for the practicality
of MVP: (1) an alias-free memory model, (2) fine-grained invariant checking,
and (3) monomorphization. The entirety of the Move code for the Diem
blockchain has been extensively specified and can be completely verified by
MVP in a few minutes. Changes in the Diem framework must be successfully
verified before being integrated into the open source repository on GitHub.

###### Keywords:

Smart contracts formal verification Move language Diem blockchain

##  1 Introduction

The Move Prover (MVP) is a formal verification tool for smart contracts that
intends to be used routinely during code development. The verification
finishes fast and predictably, making the experience of running MVP similar to
the experience of running compilers, linters, type checkers, and other
development tools. Building a fast verifier is non-trivial, and in this paper,
we would like to share the most important engineering and architectural
decisions that have made this possible.

One factor that makes verification easier is applying it to smart contracts.
Smart contracts are easier to verify than conventional software for at least
three reasons: 1) they are small in code size, 2) they execute in a well-
defined, isolated environment, and 3) their computations are typically
sequential, deterministic, and have minimal interactions with the environment
(e.g., no explicit I/O operations). At the same time, formal verification is
more appealing to the advocates for smart contracts because of the large
financial and regulatory risks that smart contracts may entail if misbehaved,
as evidenced by large losses that have occurred already [28, 18, 21].

The other crucial factor to the success of MVP is a tight coupling with the
_Move_ programming language [25]. Move is developed as part of the Diem
blockchain [23] and is designed to be used with formal verification from day
one. Move is currently co-evolving with MVP. The language supports specifying
pre-, post-, and aborts conditions of functions, as well as invariants over
data structures and over the content of the global persistent memory (i.e.,
the state of the blockchain). One feature that makes verification harder is
that quantification can be used freely in specifications.

Despite this specification richness, MVP is capable of verifying the full Move
implementation of the Diem blockchain (called the Diem framework [24]) in a
few minutes. The framework provides functionality for managing accounts and
their interactions, including multiple currencies, account roles, and rules
for transactions. It consists of about 8,800 lines of Move code and 6,500
lines of specifications (including comments for both), which shows that the
framework is extensively specified. More importantly, _verification is fully
automated and runs continuously with unit and integration tests_ , which we
consider a testament to the practicality of the approach. Running the prover
in integration tests requires more than speed: it requires reliability,
because tests that work sometimes and fail or time out other times are
unacceptable in that context.

MVP is a substantial and evolving piece of software that has been tuned and
optimized in many ways. As a result, it is not easy to define exactly what
implementation decisions lead to fast and reliable performance. However, we
can at least identify three major ideas that resulted in dramatic improvements
in speed and reliability since the description of an early prototype of MVP
[31]:

  * •

an _alias-free memory model_ based on Move’s semantics, which are similar to
the Rust programming language;

  * •

_fine-grained invariant checking_ , which ensures that invariants hold at
every state, except when developer explicitly suspends them; and

  * •

monomorphization, which instantiates type parameters in Move’s generic
structures, functions, and specification properties.

The combined effect of all these improvements transformed a tool that worked,
but often exhibited frustrating, sometimes random [11], timeouts on complex
and especially on erroneous specifications, to a tool that almost always
completes in less than 30 seconds. In addition, there have been many other
improvements, including a more expressive specification language, reducing
false positives, and error reporting.

The remainder of the paper first introduces the Move language and how MVP is
used with it, then discusses the design of MVP and the three main
optimizations above. There is also an appendix that describes injection of
function specifications.

##  2 Move and the Prover

Move was developed for the Diem blockchain [23], but its design is not
specific to blockchains. A Move execution consists of a sequence of updates
evolving a _global persistent memory state_ , which we just call the _(global)
memory_. Similar to other blockchains, updates are a series of atomic
transactions. All runtime errors result in a transaction abort, which does not
change the blockchain state except to transfer some currency (“gas”) from the
account that sent the transaction to pay for cost of executing the
transaction.

The global memory is organized as a collection of resources, described by Move
structures (data types). A resource in memory is indexed by a pair of a type
and an address (for example the address of a user account). For instance, the
expression exists<Coin<USD>>(addr) will be true if there is a value of type
Coin<USD> stored at addr. As seen in this example, Move uses type generics,
and working with generic functions and types is rather idiomatic for Move.

A Move application consists of a set of _transaction scripts_. Each script
defines a Move function with input parameters but no output parameters. This
function updates the global memory and may emit events. The execution of this
function can abort because of an abort instruction or implicitly because of a
runtime error such as an out-of-bounds vector index.

####  2.0.1 Programming in Move

Figure 1:  Account Example Program

⬇

module Account {

struct Account has key {

balance: u64,

}

fun withdraw(account: address, amount: u64) acquires Account {

let balance = &mut borrow_global_mut<Account>(account).balance;

assert(*balance >= amount, Errors::limit_exceeded());

*balance = *balance - amount;

}

fun deposit(account: address, amount: u64) acquires Account {

let balance = &mut borrow_global_mut<Account>(account).balance;

assert(*balance <= Limits::max_u64() - amount, Errors::limit_exceeded());

*balance = *balance + amount;

}

public(script) fun transfer(from: &signer, to: address, amount: u64)

acquires Account {

assert(Signer::address_of(from) != to, Errors::invalid_argument());

withdraw(Signer::address_of(from), amount);

deposit(to, amount);

}

}

In Move, one defines transactions via _script functions_ which take a set of
parameters. Those functions can call other functions. Script and regular
functions are encapsulated in _modules_. Move modules are also the place where
structs are defined. An illustration of a Move contract is given in Fig. 1
(for a more complete description see the Move Book [25]). The example is a
simple account which holds a balance in the struct Account, and offers the
script function transfer to manipulate this resource. Scripts generally have
_signer_ arguments, which are tokens which represent an account address that
has been authenticated by a cryptographic signature. The assert statement in
the example causes a Move transaction to abort execution if the condition is
not met. Notice that Move, similar as Rust, supports references (as in
&signer) and mutable references (as in &mut T). However, references cannot be
part of structs stored in global memory.

####  2.0.2 Specifying in Move

Figure 2:  Account Example Specification

⬇

module Account {

spec transfer {

let from_addr = Signer::address_of(from);

aborts_if from_addr == to;

aborts_if bal(from_addr) < amount;

aborts_if bal(to) + amount > Limits::max_u64();

ensures bal(from_addr) == old(bal(from_addr)) - amount;

ensures bal(to) == old(bal(to)) + amount;

}

spec fun bal(acc: address): u64 {

global<Account>(acc).balance

}

invariant forall acc: address where exists<Account>(acc):

bal(acc) >= AccountLimits::min_balance();

invariant update forall acc: address where exists<Account>(acc):

old(bal(acc)) - bal(acc) <= AccountLimits::max_decrease();

}

The specification language supports Design By Contract [17]. Developers can
provide pre and post conditions for functions, which include conditions over
parameters and global memory. Developers can also provide invariants over data
structures, as well as the contents of the global memory. Universal and
existential quantification over bounded domains, such as like the indices of a
vector, as well as effectively unbounded domains, such as memory addresses and
integers, are supported. Quantifiers make the verification problem undecidable
and cause difficulties with timeouts. However, in practice, we notice that
quantifiers have the advantage of allowing more direct formalization of many
properties, which increases the clarity of specifications.

Fig. 2 illustrates the specification language by extending the account example
in Fig. 1 (for the definition of the specification language see [26]). This
adds the specification of the transfer function, a helper function bal for use
in specs, and two global memory invariants. The first invariant states that a
balance can never drop underneath a certain minimum. The second invariant
refers to an update of global memory with pre and post state: the balance on
an account can never decrease in one step more than a certain amount. Note
that while the Move programming language has only unsigned integers, the
specification language uses arbitrary precision signed integers, making it
convenient to specify something like x + y <= limit, without the complication
of arithmetic overflow.

Specifications for the withdraw and deposit functions have been omitted in
this example. MVP supports omitting specs for non-recursive functions, in
which case they are treated as being inlined at caller site.

####  2.0.3 Running the Prover

MVP is fully automatic, like a type checker or linter, and is expected to
finish in a reasonable time, so it can be integrated in the regular
development workflow. Running MVP on the module Account produces multiple
errors. The first is this one:

⬇

error: abort not covered by any of the ‘aborts_if‘ clauses

\-- account.move:24:3

|

13 | let balance = &mut borrow_global_mut<Account>(account).balance;

| \----------------- abort happened here

|

= at account.move:18: transfer

= from = signer{0x18be}

= to = 0x18bf

= amount = 147u8

= at ...

MVP detected that an implicit abort condition is missing in the specification
of the withdraw function. It prints the context of the error, as well as an
_execution trace_ which leads to the error. Values of variable assignments
from the counterexample found by the SMT solver are printed together with the
execution trace. Logically, the counterexample presents an assignment to
variables where the program fails to meet the specification. In general, MVP
attempts to produce readable diagnostics for Move developers without the need
of understanding any internals of the prover.

There are more verification errors in this example, related to the global
invariants: the code makes no attempt to respect the limits in min_balance()
and max_decrease(). The problem can be fixed by adding more assert statements
to check that the limits are met (see Appendix 0.B).

The programs and specifications MVP deals with are much larger than this
example. The conditions under which a transaction in the Diem framework can
abort typically involve dozens of individual predicates, stemming from other
functions called by this transaction. Moreover, there are hundreds of memory
invariants specified, encoding access control and other requirements for the
Diem blockchain.

##  3 Move Prover Design

Figure 3: Move Prover Architecture

The architecture of MVP is illustrated in Fig. 3. Move code (containing
specifications) is given as input to the tool chain, which produces two
artifacts: an abstract syntax tree (AST) of the specifications, and the
generated bytecode. The _Move Model_ merges both bytecode and specifications,
as well as other metadata from the original code, into a unified object model
which is input to the remaining tool chain.

The next phase is the actual _Prover Compiler_ , which is a pipeline of
bytecode transformations. We focus on the transformations shown (Reference
Elimination, Specification Injection, and Monomorphization). The Prover uses a
modified version of the Move VM bytecode as an intermediate representation for
these transformations, but, for clarity, we describe the transformations at
the Move source level.

The transformed bytecode is next compiled into the Boogie intermediate
verification language [3]. Boogie supports an imperative programming model
which is well suited for the encoding of the transformed Move code. Boogie in
turn can translate to multiple SMT solver backends, namely Z3 [19] and CVC5
[22]; the default choice for the Move prover is currently Z3.

###  3.1 Reference Elimination

The reference elimination transformation is what enables the alias-free memory
model in the Move Prover, which is one of the most important factors
contributing to the speed and reliability of the system. In most software
verification and static analysis systems, the explosion in number of possible
aliasing relationships between references leads either to high computational
complexity or harsh approximations.

In Move, the reference system is based on _borrow semantics_ [5] as in the
Rust programming language. The initial borrow must come from either a global
memory or a local variable on stack (both referred to as _locations_ from now
on). For local variables, one can create immutable references (with syntax &x)
and mutable references (with syntax &mut x). For global memories, the
references can be created via the borrow_global and borrow_global_mut built-
ins. Given a reference to a whole struct, field borrowing can occur via &mut
x.f and &x.f. Similarly, with a reference to a vector, element borrowing
occurs via native functions Vector::borrow(v, i) and Vector::borrow_mut(v, i).
Move provides the following guarantees, which are enforced by the borrow
checker:

  * •

For any location, there can be either exactly one mutable reference, or $n$
immutable references. Enforcing this rule is similar to enforcing the borrow
semantics in Rust, except for global memories, which do not exist in Rust. For
global memories, this rule is enforced via the acquires annotations. Using
Fig. 1 as an example, function withdraw acquires the Account global location,
therefore, withdraw is prohibited from calling any other function that might
also borrow or modify the Account global memory (e.g., deposit).

  * •

The lifetime of references to data on the stack cannot exceed the lifetime of
the stack location. This includes global memories borrowed inside a function
as well—a reference to a global memory cannot be returned from the function,
neither in whole nor in parts.

These properties effectively permit the _elimination of references_ from a
Move program, eliminating need to reason about aliasing.

####  3.1.1 Immutable References

Immutable references are replaced by values. An example of the applied
transformation is shown below. We remove the reference type constructor and
all reference-taking operations from the code:

⬇

fun select_f(s: &S): &T { &s.f } $\leadsto$ fun select_f(s: S): T { s.f }

When executing a Move program, immutable references are important to avoid
copies for performance and to enforce ownership; however, for symbolic
reasoning on correct Move programs, the distinction between immutable
references and values is unimportant.

####  3.1.2 Mutable References

Each mutation of a location l starts with an initial borrow for the whole data
stored in this location. This borrow creates a reference r. As long as r is
alive, Move code can either update its value (*r = v), or derive a sub-
reference (r’ = &mut r.f). The mutation ends when r (and the derived r’) go
out of scope.

The borrow checker guarantees that during the mutation of the data in l, no
other reference can exist into the same data in l – meaning that it is
impossible for other Move code to test whether the value has mutated while the
reference is held.

These semantics allow mutable references to be handled via _read-update-write_
cycles. One can create a copy of the data in l and perform a sequence of
mutation steps which are represented as purely functional data updates. Once
the last reference for the data in l goes out of scope, the updated value is
written back to l. This converts an imperative program with references into an
imperative program which only has state updates on global memory or variables
on the stack, with no aliasing. We illustrate the basics of this approach by
an example:

⬇

fun increment(x: &mut u64) { *x = *x + 1 }

fun increment_field(s: &mut S) { increment(&mut s.f) }

fun caller(): S { let s = S{f:0}; update(&mut s); s }

$\leadsto$

fun increment(x: u64): u64 { x + 1 }

fun increment_field(s: S): S { s[f = increment(s.f)] }

fun caller(): S { let s = S{f:0}; s = update(s); s }

####  3.1.3 Dynamic Mutable References

While the setup in above example covers a majority of the use cases in every
day Move code, the general case is more complex, since the referenced location
may not be known statically. Consider the following Move code:

⬇

let r = if (p) &mut s1 else &mut s2;

increment_field(r);

Additional information in the logical encoding is required to deal with such
cases. When a reference goes out of scope, we need to know from which location
it was derived in order to write back the updated value. Fig. 4 illustrates
the approach for doing this. Essentially, a new type Mut<T>, which is internal
to MVP, is introduced to track both the location from which T was derived and
the value of T. Mut<T> supports the following operations:

  * •

Mvp::mklocal(value, LOCAL_ID) creates a new mutation value for a local with
the given local id. A local id uniquely identifies a local variable in the
function.

  * •

Similarly, Mvp::mkglobal(value, TYPE_ID, addr) creates a new mutation for a
global with given type and address.

  * •

With r’ = Mvp::field(r, FIELD_ID) a mutation value for a sub-reference is
created for the identified field.

  * •

The value of a mutation is replaced with r’ = Mvp::set(r, v) and retrieved
with v = Mvp::get(r).

  * •

With the predicate Mvp::is_local(r, LOCAL_ID) one can test whether r was
derived from the given local, and with Mvp::is_global(r, TYPE_ID, addr) for a
specific global location. Mvp::is_field(r, FIELD_ID) tests whether r is
derived from the given field.

Figure 4: Elimination of Mutable References

⬇

1 fun increment(x: &mut u64) { *x = *x + 1 }

2 fun increment_field(s: &mut S) {

3 let r = if (s.f > 0) &mut s.f else &mut s.g;

4 increment(r)

5 }

6 fun caller(p: bool): (S, S) {

7 let s1 = S{f:0, g:0}; let s2 = S{f:1, g:1};

8 let r = if (p) &mut s1 else &mut s2;

9 increment_field(r);

10 (s1, s2)

11 }

12 $\leadsto$

13 fun increment(x: Mut<u64>): Mut<u64> { Mvp::set(x, Mvp::get(x) + 1) }

14 fun increment_field(s: Mut<S>): Mut<S> {

15 let r = if (s.f > 0) Mvp::field(s.f, S_F) else Mvp::field(s.g, S_G);

16 r = increment(r);

17 if (Mvp::is_field(r, S_F))

18 s = Mvp::set(s, Mvp::get(s)[f = Mvp::get(r)]);

19 if (Mvp::is_field(r, S_G))

20 s = Mvp::set(s, Mvp::get(s)[g = Mvp::get(r)]);

21 s

22 }

23 fun caller(p: bool): S {

24 let s1 = S{f:0, g:0}; let s2 = S{f:1, g:1};

25 let r = if (p) Mvp::mklocal(s1, CALLER_s1)

26 else Mvp::mklocal(s2, CALLER_s2);

27 r = increment_field(r);

28 if (Mvp::is_local(r, CALLER_s1))

29 s1 = Mvp::get(r);

30 if (Mvp::is_local(r, CALLER_s2))

31 s2 = Mvp::get(r);

32 (s1, s2)

33 }

MVP implements the illustrated transformation by construction a _borrow graph_
from the program via data flow analysis. This graph tracks both when
references are released as well as how they relate to each other: e.g. r’ =
&mut r.f creates an edge from r to r’ labeled with f, and r’ = &mut r.g
creates another also starting from r. The borrow analysis is inter-procedural,
requiring computed summaries for the borrow graph of called functions.

The resulting borrow graph is then used to guide the transformation, inserting
the operations of the Mut<T> type as illustrated in Fig 4. Specifically, when
the borrow on a reference ends, the associated mutation value must be written
back to its parent mutation or the original location (e.g. line 29 in Fig. 4).
The presence of multiple possible origins leads to case distinctions via
Mvp::is_X predicates; however, these cases are rare in actual Move programs.

###  3.2 Global Invariant Injection

Correctness of smart contracts is largely about the correctness of the
blockchain state, so global invariants are particular important in the move
specification language. For example, in the Diem framework, global invariants
can capture the requirement that an account be accompanied by various other
types that are be stored at the same address and the requirement certain state
changes are only permitted for certain accounts by the access control scheme.

Most software verification tools prove that functions preserve invariants by
assuming the invariant at the entry to each function and proving them at the
exit. In a module or class, it is only necessary to prove that invariants are
preserved by public functions, since invariants are often violated internally
in the implementation of a module or class. An earlier version of the Move
Prover used exactly this approach.

The current implementation of the Prover takes the opposite approach: it
ensures that invariants hold after every instruction, unless explicitly
directed to suspend some invariants by a user. This _fine-grained_ approach
has performance advantages, because, unless suspended, _invariants are only
proven when an instruction is executed that could invalidate them_ , and the
proofs are often computationally simple because _the change from a single
instruction is usually small_. Relatively few invariants are suspended, and,
when they are, it is over a relatively small span of instructions, preserving
these advantages. There is another important advantage, which is that
invariants hold almost everywhere in the code, so they are available to
approve other properties, such as abort conditions. For example, if a function
accesses type T1 and then type T2, the access to T2 will never abort if the
presence of T1 implies the presence of T2 at every state in the body of the
function. This situation occurs with some frequency in the Diem framework.

####  3.2.1 Invariant Types and Proof Methodology

_Inductive_ invariants are properties declared in Move modules that must (by
default) hold for the global memory at all times. Those invariants often
quantify over addresses (See Fig. 2 for example.) Based on Move’s borrow
semantics, inductive invariants don’t need to hold while memory is mutated
because the changes are not visible to other code until the change is written
back. This is reflected by the reference elimination described in Sec. 3.1,

_Update_ invariants are properties that relate two states, a previous state
and the current state. Typically they are enforced after an update of global
memory. The old operator is used to evaluate specification expressions in the
previous state.

Verification of both kinds of invariants can be _suspended_. That means,
instead of being verified at the time a memory update happens, they are
verified at the call site of the function which updates memory. This feature
is necessitated by fine-grained invariant checking, because invariants
sometimes do not hold in the midst of internal computations of a module. For
example, a relationship between state variables may not hold when the
variables are being updated sequentially. Functions with external callers
(public or script functions) cannot suspend invariant verification, since the
invariants are assumed to hold at the beginning and end of each such function.

Inductive invariants are proven by induction over the evolution of the global
memory. The base case is that the invariant must hold in the empty state that
precedes the genesis transaction. For the induction step, we can assume that
the invariant holds at each verified function entry point for which it is not
suspended, and now must prove that it holds after program points which are
either direct updates of global memory, or calls to functions which suspend
invariants.

For update invariants, no induction proof is needed, since they just relate
two memories. The pre-state is some memory captured before an update happens,
and the post state the current state.

####  3.2.2 Modular Verification

We wish to support open systems to which untrusted modules can be added with
no chance of violating invariants that have already been proven. For each
invariant, there is a defined subset of Move modules (called a cluster). If
the invariant is proven for the modules in the cluster, it is guaranteed to
hold in all other modules – even those that were not yet defined when the
invariant was proven. The cluster must contain every function that can
invalidate the invariant, and, in case of invariant suspension, all callers of
such a function. Importantly, functions outside the cluster can never
invalidate an invariant. Those functions trivially preserve the invariant, so
it is only necessary to verify functions defined in the cluster.

MVP verifies a given set of modules at a time (typically one). The modules
being verified are called the target modules, and the global invariants to be
verified are called target invariants, which are all invariants defined in the
target modules. The cluster is then the smallest set as specified above such
that all target modules are contained.

####  3.2.3 Basic Translation

Figure 5: Basic Global Invariant Injection

⬇

fun f(a: address) {

let r = borrow_global_mut<S>(a);

r.value = r.value + 1

}

invariant [I1] forall a: address: global<S>(a).value > 0;

invariant [I2] update forall a: address:

global<S>(a).value > old(global<S>(a).value);

$\leadsto$

fun f(a: address) {

spec assume I1;

Mvp::snapshot_state(I2_BEFORE);

r = <increment mutation>;

spec assert I1;

spec assert I2[old = I2_BEFORE];

}

We first look at injection of global invariants in the absence of type
parameters. Fig. 5 contains an example for the supported invariant types and
their injection into code. The first invariant, I1, is an inductive invariant.
It is assumed on function entry, and asserted after the state update. The
second, I2, is an update invariant, which relates pre and post states. For
this a state snapshot is stored under some label I2_BEFORE, which is then used
in an assertion.

Global invariant injection is optimized by knowledge of the prover, obtained
by static analysis, about accessed and modified memory. Let accessed(f) be the
memory accessed by a function, and modified(f) be the memory modified. Let
accessed(I) by an invariant (including transitively by all functions it
calls).

  * •

Inject assume I at entry to f _if_ accessed(f) has overlap with accessed(I).

  * •

Inject assert I after each program step if one of the following is true (a)
the step modifies a memory location M in accessed(I) or, (b) the step is a
call to function f’ in which I is suspended and modifies(f’) intersects with
accessed(I). Also, if I is an update invariant, inject a save of a memory
snaptshot before the update or call.

####  3.2.4 Genericity

Figure 6: Global Invariant Injection and Genericity

⬇

invariant [I1] global<S<u64>>(0).value > 1;

invariant<T> [I2] global<S<T>>(0).value > 0;

fun f(a: address) { borrow_global_mut<S<u8>>(0).value = 2 }

fun g<R>(a: address) { borrow_global_mut<S<R>>(0).value = 3 }

$\leadsto$

fun f(a: address) {

spec assume I2[T = u8];

<<mutate>>

spec assert I2[T = u8];

}

fun g<R>(a: address) {

spec assume I1; spec assume I2[T = R];

<<mutate>>

spec assert I1; spec assert I2[T = R];

}

Generic type parameters make the problem of determining whether a function can
modify an invariant more difficult. Consider the example in Fig. 6. Invariant
I1 holds for a specific type instantiation S<u64>, whereas I2 is generic over
all type instantiations for S<T>.

The non-generic function f which works on the instantiation S<u8> will have to
inject the _specialized_ instance I2[T = u8]. The invariant I1, however, does
not apply for this function, because there is no overlap with S<u64>. In
contrast, g is generic in type R, which could be instantiated to u64. So, I1,
which applies to S<u64> needs to be injected in addition to I2.

The general solution depends on type unification. Given the accessed memory of
a function f<R> and an invariant I<T>, we compute the pairwise unification of
memory types. Those types are parameterized over R resp. T. Successful
unification results in a substitution for both type parameters, and we include
the invariant with T specialized according to the substitution.

###  3.3 Monomorphization

Monomorphization is a transformation which removes generic types from a Move
program by _specializing_ the program for relevant type instantiations. In the
context of verification, the goal is that the specialized program verifies if
and only if the generic program verifies in an encoding which supports types
as first class values. We expect the specialized program to verify faster
because it avoids the problem of generic representation of values, supporting
a multi-sorted representation in the SMT logic.

Figure 7: Basic Monomorphization

⬇

struct S<T> { .. }

fun f<T>(x: T) { g<S<T>>(S(x)) }

fun g<S:key>(s: S) { move_to<S>(.., s) }

$\leadsto$

struct T{}

struct S_T{ .. }

fun f_T(x: T) { g_S_T(S_T(x)) }

fun g_S_T(s: S_T) { move_to<S_T>(.., s) }

To verify a generic function for all possible instantiations, monomorphization
skolemizes the type parameter, i.e. the function is verified for a new type
with no special properties that represents an arbitrary type. It then
specializes all called functions and used data types with this new type and
any other concrete types they may use. Fig. 7 sketches this approach.

However, this approach has one issue: the type of genericity Move provides
does not allow for full type erasure (unlike many programming languages)
because types are used to _index_ global memory (e.g. global<S<T>>(addr) where
T is a generic type). Consider the following Move function:

⬇

fun f<T>(..) { move_to<S<T>>(s, ..); move_to<S<u64>>(s, ..) }

Depending on how T is instantiated, this function behaves differently.
Specifically, if T is instantiated with u64 the function will always abort at
the second move_to, since the target location is already occupied.

The important property enabling monomorphization in the presence of such type
dependent code is that one can identify the situation by looking at the memory
accessed by code and injected specifications. From this one can derive
_additional instantiations of the function_ which need to be verified. In the
example above, verifying both f_T and an instantiation f_u64 will cover all
relevant cases of the function behavior.

The algorithm for computing the instances that require verification works as
follows. Let f<T1,..,Tn> be a verified target function which has all
specifications injected and inlined function calls expanded.

  * •

For each memory M in modified(f), if there is a memory M’ in modified(f) +
accessed(f) such that M and M’ can unify via T1,..,Tn, collect an
instantiation of the type parameters Ti from the resulting substitution. This
instantiation may not assign values to all type parameters, and those
unassigned parameters stay as is. For instance, f<T1, T2> might have a partial
instantiation f<T1, u8>.

  * •

Once all partial instantiations are computed, the set is extended by unifying
the instantiations against each other. If <T> and <T’> are in the set, and
they unify under the substitution s, then <s(T)> will also be part of the set.
For example, consider f<T1, T2> which modifies M<T1> and R<T2>, as well as
accesses M<u64> and R<u8>. From this the instantiations <u64, T2> and <T1, u8>
are computed, and the additional instantiation <u64, u8> will be added to the
set.

  * •

If after computing and extending instantiations any type parameters remain,
they are skolemized into a given type as described earlier.

To understand the correctness of this procedure, consider the following
arguments (a full formal proof is outstanding):

  * •

_Direct interaction_ Whenever a modified memory M<t> can influence the
interpretation of M<t’>, a unifier must exist for the types t and t’, and an
instantiation will be verified which covers the overlap of t and t’.

  * •

_Indirect interaction_ If there is an overlap between two types which
influences whether another overlap is semantically relevant, the combination
of both overlaps will be verified via the extension step.

Notice that even though it is not common in regular Move code to work with
both memory S<T> and, say, S<u64> in one function, there is a scenario where
such code is implicitly created by injection of global invariants. Consider
the example in Fig. 6. The invariant I1 which works on S<u64> is injected into
the function g<R> which works on S<R>. When monomorphizing g, we need to
verify an instance g_u64 in order to ensure that I1 holds.

##  4 Analysis

####  4.0.1 Reliability and Performance

The three improvements described above resulted in a major qualitative change
in performance and reliability. In the version of MVP released in September
2020, correct examples verified fairly quickly and reliably. But that is
because we needed speed and reliability, so we disabled some properties that
always timed out and others that timed out unpredictably when there were small
changes in the framework. We learned that incorrect programs or specifications
would time out predictably enough that it was a good bet that examples that
timed out were erroneous. However, localizing the error to fix it was _very_
hard, because debugging is based on a counterexample that violates the
property, and getting a counterexample requires termination!

With each of the transformations described, we witnessed significant speedups
and, more importantly, reductions in timeouts. Monomorphization was the last
feature implemented, and, with it, timeouts almost disappeared. Although this
was the most important improvement in practice, it is difficult to quantify
because there have been many changes in Diem framework, its specifications,
MVP, and even the Move language over that time.

It is simpler (but less important) to quantify the changes in run time of MVP
on one of our more challenging modules, the DiemAccount module, which is the
biggest module in the Diem framework. This module implements basic
functionality to create and maintain multiple types of accounts on the
blockchain, as well as manage their coin balances. It was called LibraAccount
in release 1.0 of MVP, and is called DiemAccount today. The comparison
requires various patches as described in [16]. The table below lists the
consolidated numbers of lines, functions, invariants, conditions (requires,
ensures, and aborts-if), as well as the verification times:

Module | Lines | Functions | Invariants | Conditions | Timing
---|---|---|---|---|---
LibraAccount | 1975 | 72 | 10 | 113 | 9.899s
DiemAccount | 2554 | 64 | 32 | 171 | 7.340s

Notice that DiemAccount has significantly grown in size compared to the older
version. Specifically, additional specifications have been added. Moreover, in
the original LibraAccount, some of the most complex functions had to be
disabled for verification because the old version of MVP would time out on
them. In contrast, in DiemAccount and with the new version, all functions are
verified. Verification time has been improved by roughly 20%, _in the presence
of three times more global invariants, and 50% more function conditions_.

We were able to observe similar improvements for the remaining of the 40
modules of the Diem framework. All of the roughly half-dozen timeouts resolved
after introduction of the transformations described in this paper.

####  4.0.2 Causes for the Improvements

It’s difficult to pin down and measure exactly why the three transformations
described improved performance and reliability so dramatically. We have
explained some reasons in the subsections above: the alias-free memory model
reduced search through combinatorial sharing arrangments, and the fine-grained
invariant checking results in simpler formulas for the SMT solver.

We found that most timeouts in specifications stemmed from our liberal use of
quantifiers. To disprove a property $P_{0}$ after assuming a list of
properties, $P_{1},\ldots p_{n}$, the SMT solver must show that $\neg
P_{0}\wedge P_{1}\wedge\ldots\wedge P_{n}$ is satisfiable. The search usually
involves instantiating universal quantifiers in $P_{1},\ldots,P_{n}$. The SMT
solver can do this endlessly, resulting in a timeout. Indeed, we often found
that proving a post-condition false would time out, because the SMT solver was
instantiating quantifiers to find a satisfying assignment of
$P_{1}\wedge\ldots\wedge P_{n}$. Simpler formulas result in fewer intermediate
terms during solving, resulting in fewer opportunities to instantiate
quantified formulas.

We believe that one of the biggest impacts, specifically on removing timeouts
and improving predictability, is monomorphization. The reason for this is that
monomorphization allows a multi-sorted representation of values in Boogie (and
eventually the SMT solver). In contrast, before monomorphization, we used a
universal domain for values in order to represent values in generic functions,
roughly as follows:

⬇

type Value = Num(int) | Address(int) | Struct(Vector<Value>) | ...

This creates a large overhead for the SMT solver, as we need to exhaustively
inject type assumptions (e.g. that a Value is actually an Address), and
pack/unpack values. Consider a quantifier like forall a: address: P(x) in
Move. Before monomorphization, we have to represent this in Boogie as forall
a: Value: is#Address(a) => P(v#Address(a)). This quantifier is triggered where
ever is#Address(a) is present, independent of the structure of P. Over-
triggering or inadequate triggering of quantifiers is one of the suspected
sources of timeouts, as also discussed in [11].

Moreover, before monomorphization, global memory was indexed in Boogie by an
address and a type instantiation. That is, for struct R<T> we would have one
Boogie array [Type, int]Value. With monomorphization, the type index is
eliminated, as we create different memory variables for each type
instantiation. Quantification over memory content works now on a one-
dimensional instead of an n-dimensional Boogie array.

####  4.0.3 Discussion and Related Work

Many approaches have been applied to the verification of smart contracts; see
e.g. the surveys [13, 28]. [28] refers to at least two dozen systems for smart
contract verification. It distinguishes between _contract_ and _program_ level
approaches. Our approach has aspects of both: we address program level
properties via pre/post conditions, and contract (“blockchain state”) level
properties via global invariants. To the best of our knowledge, among the
existing approaches, the Move ecosystem is the first one where contract
programming and specification language are fully integrated, and the language
is designed from first principles influenced by verification.
Methodologically, Move and the Move prover are thereby closer to systems like
Dafny [10], or the older Spec# system [4], where instead of adding a
specification approach posterior to an existing language, it is part from the
beginning. This allows us not only to deliver a more consistent user
experience, but also to make verification technically easier by curating the
programming language.

In contrast to other approaches that only focus on specific vulnerability
patterns [6, 14, 20, 30], MVP offers a universal specification language. To
the best of our knowledge, no existing specification approach for smart
contracts based on inductive Hoare logic has similar expressiveness. We
support universal quantification over arbitrary memory content, a suspension
mechanism of invariants to allow non-atomic construction of memory content,
and generic invariants. For comparison, the SMT Checker build into Solidity
[7, 8, 9] does not support quantifiers, because it interprets programming
language constructs (requires and assert statements) as specifications and has
no dedicated specification language. While in Solidity one can simulate
aspects of global invariants using modifiers by attaching pre/post conditions,
this is not the same as our invariants, which are guaranteed to hold
independent of whether a user may or (accidentally) may not attach a modifier,
and which are optimized to be only evaluated as needed.

While the expressiveness of Move specifications comes with the price of
undecidability and the dependency from heuristics in SMT solvers, MVP deals
with this by its elaborated translation to SMT logic, as described in this
paper. The result is a practical verification system that is fully integrated
into the Diem blockchain production process, running in continuous
integration, which is (to the best of our knowledge) a first in the industry.

The individual techniques we described are novel each by themselves.
_Reference elimination_ relies on borrow semantics, similar as in the Rust
[15] language. We expect reference elimination to apply for the safe subset of
Rust, though some extra work would be needed to deal with references
aggregated by structs. However, we are not aware of that something similar has
been attempted in existing Rust verification work [1, 2, 12, 29]. _Global
invariant injection_ and the approach to minimize the number of assumptions
and assertions is not applied in any existing verification approach we know
of; however, we co-authored a while ago a similar line of work for _runtime
checking_ of invariants in Spec# [27], yet that work never left the conceptual
state. _Monomorphization_ is well known as a technique for compiling languages
like C++ or Rust, where it is called specialization; however, we are not aware
of it being generalized for modular verification of generic code where full
type erasure is not possible, as it is the case in Move.

####  4.0.4 Future Work

MVP is conceived as a tool for achieving higher assurance systems, not as a
bug hunting tool. Having at least temporarily achieved satisfactory
performance and reliability, we are turning our attention to the question of
the goal of higher assurance, which raises several issues. If we’re striving
for high assurance, it would be great to be able to measure progress towards
that goal. Since system requirements often stem from external business and
regulatory needs, lightweight processes for exposing those requirements so we
know what needs to be formally specified would be highly desirable.

As with many other systems, it is too hard to write high-quality
specifications. Our current specifications are more verbose than they need to
be, and we are working to require less detailed specifications, especially for
individual functions. We could expand the usefulness of MVP for programmers if
we could make it possible for them to derive value from simple reusable
specifications. Finally, software tools for assessing the consistency and
completeness of formal specifications would reduce the risk of missing bugs
because of specification errors.

However, as more complex smart contracts are written and as more people write
specifications, we expect that the inherent computational difficulty of
solving logic problems will reappear, and there will be more opportunities for
improving performance and reliability. In addition to translation techniques,
it will be necessary to identify opportunities to improve SMT solvers for the
particular kinds of problems we generate.

##  5 Conclusion

We described key aspects of the Move prover (MVP), a tool for formal
verification of smart contracts written in the Move language. MVP has been
successfully used to verify large parts of the Diem framework, and is used in
continuous integration in production. The specification language is
expressive, specifically by the powerful concept of global invariants. We
described key implementation techniques which (as confirmed by our benchmarks)
contributed to the scalability of MVP. One of the main areas of our future
research is to improve specification productivity and reduce the effort of
reading and writing specs, as well as to continue to improve speed and
predictability of verification.

####  5.0.1 Acknowledgements

This work would not have been possible without the many contributions of the
Move platform team and collaborators. We specifically like to thank Bob
Wilson, Clark Barrett, Dario Russi, Jack Moffitt, Jake Silverman, Mathieu
Baudet, Runtian Zhou, Sam Blackshear, Tim Zakian, Todd Nowacki, Victor Gao,
and Kevin Cheang.

##  Appendix 0.A Injection of Function and Data Specifications

In this appendix we describe, for the interested reader, the design of
function and data specification injection (requires, ensures, aborts_if,
modifies, emits, and data invariants). While the impact on speed and
reliability of verification might have been not that significant, these
designs were fine tuned over time as well. With this, a comprehensive coverage
of the translation of all specification constructs in MVP is provided.

###  0.A.1 Function Specifications

The injection of basic function specifications is illustrated in Fig. 8. An
extension of the Move source language is used to specify abort behavior. With
fun f() { .. } onabort { conditions } a Move function is defined where
conditions are assume or assert statements that are evaluated at every program
point the function aborts (either implicitly or with an abort statement). This
construct simplifies the presentation and corresponds to a per-function abort
block on bytecode level which is target of branching.

Figure 8: Requires, Ensures, and AbortsIf Injection

⬇

1 fun f(x: u64, y: u64): u64 { x + y }

2 spec f {

3 requires x < y;

4 aborts_if x + y > MAX_U64;

5 ensures result == x + y;

6 }

7 fun g(x: u64): u64 { f(x, x + 1) }

8 spec g {

9 ensures result > x;

10 }

11 $\leadsto$

12 fun f(x: u64, y: u64): u64 {

13 spec assume x < y;

14 let result = x + y;

15 spec assert result == x + y; // ensures of f

16 spec assert // negated abort_if of f

17 !(x + y > MAX_U64);

18 result

19 } onabort {

20 spec assert // abort_if of f

21 x + y > MAX_U64;

22 }

23 fun g(x: u64): u64 {

24 spec assert x < x + 1; // requires of f

25if inlined

26 let result = inline f(x, x + 1);

27elif opaque

28 if (x + x + 1 > MAX_U64) abort; // aborts_if of f

29 spec assume result == x + x + 1; // ensures of f

30endif

31 spec assert result > x; // ensures of g

32 result

33 }

An aborts condition is translated into two different asserts: one where the
function aborts and the condition must hold (line 21), and one where it
returns and the condition must _not_ hold (line 17). If there are multiple
aborts_if, they are or-ed. If there is no abort condition, no asserts are
generated. This means that once a user specifies aborts conditions, they must
completely cover the abort behavior of the code. (The prover also provides an
option to relax this behavior, where aborts conditions can be partial and are
only enforced on function return.)

For a function call site we distinguish two variants: the call is _inlined_
(line 25) or it is _opaque_ (line 27). For inlined calls, the function
definition, with all injected assumptions and assertions turned into
assumptions (as those are considered proven) is substituted. For opaque
functions the specification conditions are inserted as assumptions.
Methodologically, opaque functions need precise specifications relative to a
particular objective, where as in the case of inlined functions the code is
still the source of truth and specifications can be partial or omitted.
However, inlining does not scale arbitrarily, and can be only used for small
function systems.

Notice we have not discussed the way how to deal with relating pre and post
states yet, which requires taking snapshots of state (e.g. ensures x == old(x)
+ 1); the example in Fig. 8 does not need it. Snapshots of state are discussed
for global update invariants in Sec. 3.2.

####  0.A.1.1 Modifies

Figure 9: Modifies Injection

⬇

1 fun f(addr: address) { move_to<T>(addr, T{}) }

2 spec f {

3 pragma opaque;

4 ensures exists<T>(addr);

5 modifies global<T>(addr);

6 }

7 fun g() { f(0x1) }

8 spec g {

9 modifies global<T>(0x1); modifies global<T>(0x2);

10 }

11 $\leadsto$

12 fun f(addr: address) {

13 let can_modify_T = {addr}; // modifies of f

14 spec assert addr in can_modify; // permission check

15 move_to<T>(addr, T{});

16 }

17 fun g() {

18 let can_modify_T = {0x1, 0x2}; // modifies of g

19 spec assert {0x1} <= can_modify_T; // permission check

20 spec havoc global<T>(0x1); // havoc modified memory

21 spec assume exists<T>(0x1); // ensures of f

22 }

The modifies condition specifies that a function only changes specific memory.
It comes in the form modifies global<T>(addr), and its injection is
illustrated in Fig. 9.

A type check is used to ensure that if a function has one or more modifies
conditions all called functions which are _opaque_ have a matching modifies
declaration. This is important so we can relate the callees memory
modifications to that what is allowed at caller side.

At verification time, when an operation is performed which modifies memory, an
assertion is emitted that modification is allowed (e.g. line 14). The
permitted addresses derived from the modifies clause are stored in a set
can_modify_T generated by the transformation. Instructions which modify memory
are either primitives (like move_to in the example) or function calls. If the
function call is inlined, modifies injection proceeds (conceptually) with the
inlined body. For opaque function calls, the static analysis has ensured that
the target has a modifies clause. This clause is used to derive the modified
memory, which must be a subset of the modified memory of the caller (line 19).

For opaque calls, we also need to _havoc_ the memory they modify (line 20), by
which is meant assigning an unconstrained value to it. If present, ensures
from the called function, injected as subsequent assumptions, are further
constraining the modified memory.

####  0.A.1.2 Emits

Figure 10: Emits Injection

⬇

1 use Std::Event;

2 struct E has drop, store { m: u64 }

3 fun f(h: &mut Event::EventHandle<E>, x: u64) {

4 Event::emit_event(h, E{m:0});

5 if (x > 0) {

6 Event::emit_event(h, E{m:x});

7 }

8 }

9 spec f {

10 emits E{m:0} to h;

11 emits E{m:x} to h if x > 0;

12 }

13 $\leadsto$

14 fun f(h: &mut Event::EventHandle<E>, x: u64) {

15 es = Mvp::ExtendEventStore(es, h, E{m:0}); // emitting event

16 if (x > 0) {

17 es = Mvp::ExtendEventStore(es, h, E{m:x}); // emitting event

18 }

19 let actual_es = Mvp::subtract(es, old(es)); // events emitted by f

20 let expected_es = Mvp::CondExtendEventStore( // specified events

21 Mvp::ExtendEventStore(Mvp::EmptyEventStore, E{m:x}, h),

22 E{m:x}, h, x>0);

23 spec assert Mvp::includes(expected_es, actual_es); // spec completeness

24 spec assert Mvp::includes(actual_es, expected_es); // spec relevance

25 }

The injection for the emits clause is illustrated in Fig. 10. The emits clause
specifies the events that a function is expected to emit. It comes in the form
emits message to handle if condition (e.g., line 11). The condition part
(i.e., if condition) can be omitted if the event is expected to be emitted
unconditionally (e.g., line 10).

The function call to Event::emit_event (e.g., line 4) is transformed into the
statement to extend es with the event to emit (e.g., line 15). es is a global
variable of type EventStore which is a map where the key is an event handle
and the value is the event stream of the handle (modeled as a bag of
messages).

In line 19, actual_es represents the portion of the EventStore that only
comprises the events that the program (i.e., f) actually emits. In line 20,
expected_es is constructed from the emits specification which contains all of
the expected events specified by the emits clauses. Having these, two
assertions using Mvp::includes (multiset inclusion relation per event handle)
are injected.

  * •

One asserts that expected_es includes actual_es, meaning that the function
only emits the events that are expected (e.g., line 23). This would be
violated if there is any event emitted by f that is not covered by some emits
clause.

  * •

The other asserts that actual_es includes expected_es, meaning that the
function emits all of the events that are expected (e.g., line 24). This would
be violated if f does not emit the expected event which a emits clause
specifies.

We also handle opaque calls properly although it is not illustrated in Fig.
10. Suppose f is an opaque function, and another function g calls f. In the
transformation of g, the event store es extends with the expected events of f
(i.e., the events specified by the emits clauses of f) in a similar way to how
expected_es is constructed in line 20.

###  0.A.2 Data Invariants

Figure 11: Data Invariant Injection

⬇

1 struct S { a: u64, b: u64 }

2 spec S { invariant a < b }

3 fun f(s: S): S {

4 let r = &mut s;

5 r.a = r.a + 1;

6 r.b = r.b + 1;

7 s

8 }

9 $\leadsto$

10 fun f(s: S): S {

11 spec assume s.a < s.b; // assume invariant for s

12 let r = Mvp::local(s, F_s); // begin mutation of s

13 r = Mvp::set(r, Mvp::get(r)[a = Mvp::get(r).a + 1]);

14 r = Mvp::set(r, Mvp::get(r)[b = Mvp::get(r).b + 1]);

15 spec assert // invariant enforced

16 Mvp::get(r).a < Mvp::get(r).b;

17 s = Mvp::get(r); // write back to s

18 s

19 }

A data invariant specifies a constraint over a struct value. The value is
guaranteed to satisfy this constraint at any time. Thus, when a value is
constructed, the data invariant needs to be verified, and when it is consumed,
it can be assumed to hold.

In Move’s reference semantics, construction of struct values is often done via
a sequence of mutations via mutable references. It is desirable that _during_
such mutations, assertion of the data invariant is suspended. This allows to
state invariants which reference multiple fields, where the fields are updated
step-by-step. Move’s borrow semantics and concept of mutations provides a
natural way how to defer invariant evaluation: at the point a mutable
reference is released, mutation ends, and the data invariant can be enforced.
In other specification formalisms, we would need a special language construct
for invariant suspension. Fig. 11 gives an example, and shows how data
invariants are reduced to assert/assume statements.

The implementation of data invariants hooks into reference elimination,
described in Sec. 3.1. As part of this the lifetime of references is computed.
Whenever a reference is released and the mutated value is written back, we
also assert the data invariant. In addition, the data invariant is asserted
when a struct value is directly constructed.

##  Appendix 0.B Corrected Account Example

To fix the verification errors from the account example in Fig. 1 and Fig. 2,
the following changes would need to be made:

⬇

module Account {

...

fun withdraw(account: address, amount: u64) acquires Account {

assert(amount <= AccountLimits::max_decrease(), Errors::invalid_argument());
// MISSING

let balance = &mut borrow_global_mut<Account>(account).balance;

assert(*balance >= amount, Errors::limit_exceeded());

assert(*balance - amount >= AccountLimits::min_balance(),
Errors::invalid_argument()); // MISSING

*balance = *balance - amount;

}

spec transfer {

...

aborts_if !exists<Account>(from_addr); // MISSING

aborts_if !exists<Account>(to); // MISSING

aborts_if amount > AccountLimits::max_decrease(); // MISSING

aborts_if bal(from_addr) - amount < AccountLimits::min_balance(); // MISSING

}

}

## References

  * [1] Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. PACMPL 3(OOPSLA), 147:1–147:30 (2019)
  * [2] Baranowski, M.S., He, S., Rakamaric, Z.: Verifying rust programs with SMACK. In: ATVA. Lecture Notes in Computer Science, vol. 11138, pp. 528–535. Springer (2018)
  * [3] Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: International Symposium on Formal Methods for Components and Objects. pp. 364–387. Springer (2005)
  * [4] Barnett, M., DeLine, R., Fähndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# Programming System: Challenges and Directions, pp. 144–152. Springer Berlin Heidelberg, Berlin, Heidelberg (2008), https://doi.org/10.1007/978-3-540-69149-5_16
  * [5] Clarke, D., Östlund, J., Sergey, I., Wrigstad, T.: Ownership types: A survey. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification, Lecture Notes in Computer Science, vol. 7850, pp. 15–58. Springer (2013). https://doi.org/10.1007/978-3-642-36946-9_3
  * [6] ConsenSys: Mythril Classic: Security analysis tool for Ethereum smart contracts, https://github.com/skylightcyber/mythril-classic
  * [7] Foundation, E.: Solidity documentation (2018), http://solidity.readthedocs.io
  * [8] Hajdu, Á., Jovanovic, D.: solc-verify: A modular verifier for solidity smart contracts. CoRR abs/1907.04262 (2019)
  * [9] Hajdu, Á., Jovanovic, D.: SMT-Friendly Formalization of the Solidity Memory Model. In: ESOP. Lecture Notes in Computer Science, vol. 12075, pp. 224–250. Springer (2020)
  * [10] Leino, K.M.: Accessible software verification with dafny. IEEE Software 34(06), 94–97 (nov 2017). https://doi.org/10.1109/MS.2017.4121212
  * [11] Leino, K.R.M., Pit-Claudel, C.: Trigger Selection Strategies to Stabilize Program Verifiers. In: Proceedings of the 28th International Conference on Computer Aided Verification, Part I. pp. 361–381. Springer (2016). https://doi.org/10.1007/978-3-319-41528-4_20
  * [12] Lindner, M., Aparicius, J., Lindgren, P.: No panic! verification of rust programs by symbolic execution. In: INDIN. pp. 108–114. IEEE (2018)
  * [13] Liu, J., Liu, Z.: A survey on security verification of blockchain smart contracts. IEEE Access 7, 77894–77904 (2019)
  * [14] Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM Conference on Computer and Communications Security. pp. 254–269. ACM (2016)
  * [15] Matsakis, N.D., Klock, II, F.S.: The Rust Language, nourl = http://doi.acm.org/10.1145/2692956.2663188. Ada Lett. 34(3), 103–104 (Oct 2014). https://doi.org/10.1145/2692956.2663188
  * [16] Meng Xu: Artifact for Paper “Fast and Reliable Formal Verification of Smart Contracts with the Move Prover” (2020), https://github.com/meng-xu-cs/mvp-artifact
  * [17] Meyer, B.: Applying "design by contract". Computer 25(10), 40–51 (Oct 1992). https://doi.org/10.1109/2.161279
  * [18] Morisander: The Biggest Smart Contract Hacks in History Or How to Endanger up to US $2.2 Billion. https://medium.com/solidified/the-biggest-smart-contract-hacks-in-history-or-how-to-endanger-up-to-us-2-2-billion-d5a72961d15d (2018)
  * [19] de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)
  * [20] Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: ACSAC. pp. 653–663. ACM (2018)
  * [21] Sigalos, M.: Bug Puts $162 Million up for Grabs, Says Founder of DeFi Platform Compound. https://www.cnbc.com/2021/10/03/162-million-up-for-grabs-after-bug-in-defi-protocol-compound-.html (2021)
  * [22] The CVC Team: CVC5, https://github.com/cvc5/cvc5
  * [23] The Diem Association: An Introduction to Diem (2019), https://www.diem.com/en-us/
  * [24] The Diem Association: The Diem Framework (2020), https://github.com/diem/diem/tree/release-1.5/diem-move/diem-framework
  * [25] The Move Team: The Move Programming Language (2020), https://diem.github.io/move
  * [26] The Move Team: The Move Specification Language (2020), https://github.com/diem/diem/blob/release-1.5/language/move-prover/doc/user/spec-lang.md
  * [27] Tillmann, N., Grieskamp, W., Schulte, W.: Efficient checking of state-dependent constraints (US Patent 20050198621A1, 2004)
  * [28] Tolmach, P., Li, Y., Lin, S., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. CoRR abs/2008.02712 (2020), https://arxiv.org/abs/2008.02712
  * [29] Toman, J., Pernsteiner, S., Torlak, E.: Crust: A bounded verifier for rust (N). In: ASE. pp. 75–80. IEEE Computer Society (2015)
  * [30] Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.T.: Securify: Practical security analysis of smart contracts. In: ACM Conference on Computer and Communications Security. pp. 67–82. ACM (2018)
  * [31] Zhong, J.E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C., Dill, D.L.: The Move Prover. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification. pp. 137–150. Springer International Publishing (2020)

Open Access This chapter is licensed under the terms of the Creative
CommonsAttribution 4.0 International License
(http://creativecommons.org/licenses/by/4.0/), which permits use, sharing,
adaptation, distribution and reproduction in any medium or format, as long as
you give appropriate credit to the original author(s) and the source, provide
a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the
chapter’s Creative Commons license, unless indicated otherwise in a credit
line to the material. If material is not included in the chapter’s Creative
Commons license and your intendeduse is not permitted by statutory regulation
or exceeds the permitted use, you will need to obtain permission directly from
the copyright holder.


# Robust data analysis and imaging with computational ghost imaging

Jiangtao Liu<EMAIL_ADDRESS>College of Mechanical and Electrical
Engineering, Guizhou Minzu University, Guiyang 550025, China  Xunming Cai
College of Mechanical and Electrical Engineering, Guizhou Minzu University,
Guiyang 550025, China  Jinbao Huang  College of Mechanical and Electrical
Engineering, Guizhou Minzu University, Guiyang 550025, China  Kun Luo  Key
Laboratory of Microelectronic Devices and Integrated Technology, Institute of
Microelectronics, Chinese Academy of Sciences, Beijing 100029, China  Hongxu
Li  Guizhou Light Industry Technical College, Guiyang 550025, China  Dejian
Zhang<EMAIL_ADDRESS>Nanchang University, Department of Physics,
Nanchang, China  Zhenhua Wu<EMAIL_ADDRESS>Key Laboratory of
Microelectronic Devices and Integrated Technology, Institute of
Microelectronics, Chinese Academy of Sciences, Beijing 100029, China
University of CAS, Beijing 100049, China

###### Abstract

Nowadays the world has entered into the digital age, in which the data
analysis and visualization have become more and more important. In analogy to
imaging the real object, we demonstrate that the computational ghost imaging
can image the digital data to show their characteristics, such as periodicity.
Furthermore, our experimental results show that the use of optical imaging
methods to analyse data exhibits unique advantages, especially in anti-
interference. The data analysis with computational ghost imaging can be well
performed against strong noise, random amplitude and phase changes in the
binarized signals. Such robust data data analysis and imaging has an important
application prospect in big data analysis, meteorology, astronomy, economics
and many other fields.

The emergence of equipment and technologies for the optical imaging of real
objects such as telescopes and microscopes has led to rapid developments in
astronomy and biology. However, we have entered the digital age, and the
development of information technology, has made data analysis and
visualization increasingly important. Additionally, the exponential growth of
massive amounts of data makes data analysis increasingly difficult, and new
data analysis and visualization technologies are urgently needed. In view of
the great success of the optical imaging of physical objects, imaging data
with optical methods to obtain the characteristics of the data would be an
interesting challenge.

In this study, we found that ghost imaging can not only image a physical
object but also image data, presenting the characteristics of the data. Ghost
imaging is a new imaging technology based on the correlation function between
a reference light field and the target detection light fieldZETF90KDN ;
ZETF78BAV ; NP13MPE ; LPR18MPA . Ghost imaging has important applications in
3D imagingS340SB , imaging with atomsN540RIK ; PRL121LS , time domain
imagingNP10PR ; o6HW , X-ray imagingPRL92CJ ; o5axz , Neutron imagingPRA101KA
, THz wave imagingLSA9SCC ; O7LO , super-resolution imagingO6WL , thermal
light imagingPRL94VA ; ol34xhc ; APL117YZ ; PRA15ZDJ , difference
imagingPRA15YZ , helicity-dependent metasurface imagingSA3LH , ultrafast pump-
probe ghost imagingPRX9RD ; APL116WX , edge imagingAPL116SH , optical
encryptionOL35PC , etc. Ghost imaging is a nonlocal imaging method that is
robust against interference and penetrates scattering mediaNP13MPE ; LPR18MPA
; OE17JC ; APL98MRE .

Specifically, we use computational ghost imaging to image the periodicity in
data. Periodicity is one of the most important and basic trends. As early as
1705, Halley successfully predicted the reappearance of Halley’s comet by
analyzing the periodicity of the appearance of the comet. Today, periodic
analysis is also used to study the hidden trends of climate change N367MES ;
S268GP , earthquakes NSR6JH , astronomy ND89SVG ; TAJ837BS ; TAJ883BDN ,
infectious diseases PNAS99RX , biology NAR46ZX ; SR8HS , oceanography
PNAS109GD  and so on. At present, periodic analysis mainly includes singular
spectrum analysisBPP1996EJB , fast Fourier transformMC19JWC , uncoiled random
QR denoisingPNAS111CL , deviance information criterion minimization TAJ853KT ,
etc. However, in the digital age, due to the diversification of the data
collected, the accuracy of the data decreases, and the hybridity continues to
improve. There is substantial noise in too large of a dataset, and imprecise
acquisition makes the amplitude and phase of the collected periodic signal
highly random. In addition, to reduce the information storage and improve the
analysis speed, many data are binarized. These characteristics mean that
traditional periodic analysis methods are no longer applicable.

In our experiment applying ghost imaging to data, we find that random factors
such as noise, random amplitudes and phase changes in the data mainly affect
the object imaging area the but have little influence on the background
imaging and that the periodicity in the data is clearer in the background
imaging area. Thus, the signal and noise can be separated, and the influence
of the signal amplitude and phase randomness caused by inaccurate acquisition
and other factors can be eliminated. Moreover, in computational ghost imaging,
most speckle patterns are binary, so they are compatible with binary data. Our
experimental results show that the periodicity of binary data can be presented
when the signal-to-noise ratio (SNR) is 1:19 or when the SNR is 1:7, the phase
random amplitude reaches $210^{\circ}$, and the amplitude random amplitude
reaches 90%.

Figure 1: Schematic diagram of a lensless ghost imaging system based on a
liquid crystal display. (b)-(d) Different objects to be imaged and the
corresponding images under periodic signals, the period of the signal in (d)
is different. The brightness distribution of the image with different periodic
signal amplitudes $A_{SNR}$, where the left, middle and right insets are
$A_{SNR}=0.3$, $A_{SNR}=0.2$, and $A_{SNR}=0.1$, and the green solid line fits
the curve with $A_{SNR}=0.3$.

To eliminate the image distortion caused by a lens, we build a lensless ghost
imaging system using a ACER XB252Q liquid crystal display [Fig. 1 (a)]. The
data to be analyzed are used to generate the corresponding speckle pattern,
and the light emitted by the speckle pattern passes through the object to be
imaged and is received by the Thorlabs PDA36A2 light detector, and the signals
is collected by a NI USB 6002 data acquisition card, and the corresponding
image is obtained by the correlation calculation of the signal received by the
bucket detector and the speckle pattern. If the data to be analyzed contain
periodic signals, periodic stripes-shaped images are obtained [Figs. 1 (b) and
(c)]. The image shows the characteristics of the data independent of the shape
of the object to be imprinted, and the periodicity of the stripes is exactly
the same as that of the data. When the period of the signal changes, the
period of the image will also change [Fig. 1 (d)].

The main reason for this is that the computed ghost image is obtained by
association calculation between the received signal of the bucket detector
$I_{1}$ and the corresponding incident speckle field $I_{2}(x,y)$, i.e.,

$\displaystyle\Delta G(x,y)=$ $\displaystyle\langle(I_{1}-\langle
I_{1}\rangle)[I_{2}(x,y)-\langle I_{2}(x,y)\rangle]\rangle$ (1)
$\displaystyle=$ $\displaystyle\langle I_{1}I_{2}(x,y)-\langle
I_{1}\rangle\langle I_{2}(x,y)\rangle\rangle,$

where $\left<\cdots\right>$ denotes the ensemble average over thousands of
measurements. Speckle patterns are generated by periodic signals such as
$I_{2}(x,y)=\\{1+\cos[2\pi(x_{R0}+x)/P_{d}]\\}/2$, where $x_{R0}$ is a random
initial pixel position and $P_{d}$ is the period length. Suppose there is a
slit at $x=x_{0}$; thus, it is only around $x_{R0}+x_{0}=nP_{d}$ that $I_{1}$
does not equal 0, so we can obtain $\Delta G(x,y)\propto
1+\cos[2\pi(nP_{d}-x_{0}+x)/P_{d}]$. That is, the image shows the same
periodicity as the speckle pattern.

However, the actual periodic signal is often accompanied by a strong noise
signal, and the periodic signal itself often exhibits random amplitude and
phase changes. To better analyze the influence of periodic signal
characteristics and noise on the calculation of ghost imaging, we construct a
binary database containing one-dimensional periodic signals with noise signal,
random amplitude and random phase, which can be written as

$\Lambda(x_{ip})=A_{SNR}[1+P(x_{ip})]/2+(1-A_{SNR})\mathcal{R}_{0,1},$ (2)

where $P(x_{ip})=\mathcal{R}_{A}\cos(2\pi x_{ip}/P_{d}+\mathcal{R}_{\varphi})$
is a periodic signal, $\mathcal{R}_{A}=(1-A_{RAC})\mathcal{R}_{0,1}+A_{RAC}$,
$\mathcal{R}_{\varphi}=\pi A_{RPC}\mathcal{R}_{0,1}/180^{\circ}$,
$\mathcal{R}_{0,1}$ is a uniformly distributed random number from 0 to 1,
$A_{SNR}$ is the periodic signal amplitude, and $\mathcal{R}_{A}$ and
$\mathcal{R}_{\varphi}$ reflect the randomness of the amplitude and phase,
respectively. In addition, to make the imaging smoother, we add a two-
dimensional random modulation; that is,
$\Lambda^{\prime}(x_{ip},y_{ip})=0.5\Lambda(x_{ip})+0.5\mathcal{R}_{0,1}(x_{ip},y_{ip})$.
Therefore, when $A_{SNR}=0.1$, the corresponding signal (noise) amplitude is
0.05 (0.95), and the SNR is 1:19. We randomly obtain a segment from this
database and binarize it to generate the corresponding speckle image and use
it to achieve ghost imaging. Unless otherwise specified, we take $P_{d}=16$
during the imaging process, and the speckle pattern has a size of $240\times
240$ pixels. Each speckle has a size of $4\times 4$ pixels, and the number of
speckle images is 3000. The object to be imaged is a slit with a width of 4.3
mm.

We study the influence of noise on periodic signal acquisition. When the
signal amplitude $A_{SNR}=0.3$, that is, the SNR is 3:17, the generated image
presents clear periodic stripes [the left inset of Fig. 1(e)]. However,
compared with the noiseless periodic signal [Fig. 1(d)], the brightness of the
middle fringe (i.e., the image corresponding to the object to be imaged)
increases, while the brightness of the neighboring fringe decreases and the
contrast decreases. As shown in traditional computed ghost imaging, the noise
part of the speckle image images of the object, which increases the brightness
of the image corresponding to the object. When the signal amplitude further
decreases and the noise signal increases, such as $A_{SNR}=0.2$ or
$A_{SNR}=0.1$ (SNR is 1:19), the contrast of the stripes is reduced, and the
brightness of the middle stripes is increased, but the periodicity of the
fringe can still be observed by the naked eye.

To better display the periodicity in the image, we sum the brightness of each
pixel in the image along the vertical direction to obtain the brightness
distribution of the stripes [as shown in Fig. 1(e)]. Then, curve fitting is
performed on the area outside the middle bright stripe, and the error of the
periodic signal extracted by ghost imaging can be obtained, e.g., when
$A_{SNR}=0.3$, the period (relative amplitude) errors are 0% (1%).

Next, we study the influence of the amplitude randomness and phase randomness
of periodic signals on the acquisition of periodic signals. When $A_{RAC}$
changes from 0.5 to 0, that is, the signal amplitude randomness changes from
50% to 100%, the contrast of the fringe decreases slightly, but the generated
images all show clear periodic stripes and do not show the image of the object
to be measured [Fig. 2(a)]. The randomness of the amplitude of the periodic
signal leads to a very small error. However, in traditional periodic signal
extraction, such as with the least squares method, the randomness of periodic
signal amplitude increases the difficulty of signal extraction. When the phase
is random, the resulting image presents periodic stripes and the image of the
object. The effect of phase randomness on the image is similar to that of
noise. When the phase randomness increases, the contrast of the fringe
decreases, and the middle fringe increases the image brightness of the object.
When $A_{RPC}$ is 210∘ and 300∘, the period error is approximately 0.1%, and
the relative amplitude error values are 1.2% and 5.4%, respectively. The
brightness distribution curve of the image when noise, random amplitudes and
random phases exist at the same time is shown in Fig. 2 (c). When
$A_{SNR}=0.35$, $A_{RPC}=150^{\circ}$ and $A_{RAC}=0.3$ ($A_{SNR}=0.25$,
$A_{RPC}=210^{\circ}$, and $A_{RAC}=0.1$,), the period error is -0.2% (
-2.3%), and the relative amplitude error is 2.1% (9.6%). By comparing the
above results, we find that only when noise, random amplitudes and random
phases are all present and large can a small periodic error ($\sim 2.3\%$)
occur, while in other cases, the periodic error is very small, so this method
is excellent for periodic extraction in the signal.

Figure 2: (a) Periodic signal amplitude randomness and (b) phase randomness
effects on the image brightness distribution. (c) The brightness distribution
curve of the image when noise, random amplitude and random phase occur at the
same time. (d) The influence of the number of speckle images on the image
brightness distribution. The inset in (d) is the image generated when the
number of speckle patterns is 300.

In addition, ghost imaging is insensitive to the number of speckle images in
data imaging. Fig. 2 (d) shows the brightness distributions of images with
different numbers of speckle images when $A_{SNR}=0.3$, $A_{RPC}=180^{\circ}$,
and $A_{RAC}=0.2$. When the number of speckle images is 300, a clear periodic
distribution can be presented. When the numbers of speckle patterns are 3000,
500 and 300, the corresponding periodic errors (the relative errors of
amplitude) are $-0.9\%$ (6.1%), $-0.3\%$ (9.0%), and $1.1\%$ (10%),
respectively. This shows that this method can be used in data analysis with
both small samples and large samples, so it has good flexibility. In contrast,
traditional ghost imaging generally requires a higher number of speckle images
for physical imaging, and this defect limits the application of traditional
ghost imaging in physical imaging. Furthermore, in the era of big data, the
data itself is huge and fragmented, and each speckle pattern used in ghost
imaging analysis of signals can be generated from a piece of fragmented
information, and the number of speckle patterns can be more or less [Figure 2
(d)]. Therefore, ghost imaging can analyze both small fragmented data and huge
fragmented data. In addition, the number of calculations in this method is
proportional to the amount of data, while the number of calculations in
traditional methods such as singular spectrum analysis is proportional to the
square of the amount of data. When the amount of data is large, this method
has an advantage in calculation speed.

Figure 3: (a) The speckle pattern generated by the actual circuit signal and
(b) the resulting image when SNR is approximately 1:9; (c) The speckle pattern
generated by the actual circuit signal and (d) the resulting image when SNR is
approximately 1:2 and the random phase amplitude is approximately 290 degrees;
(d)Imaging brightness distribution, black line for SNR is approximately 1:2,
red line for SNR is approximately 1:2 and the random phase amplitude is
approximately 290 degrees.

To verify the practicability of ghost imaging for data imaging, we image an
actual circuit signal with ghost imaging. The results are shown in Figure 3.
Speckle pattern is directly converted from digital signal. The white speckle
in the speckle pattern corresponds to the high level and the black speckle
corresponds to the low level [Figs. 3 (a) and (c)]. When there is noise in the
actual circuit signal (the SNR is approximately 1:9), or when there is noise
in the actual circuit signal (the SNR is approximately 1:2) and phase
uncertainty (the random phase amplitude is approximately 290 degrees), ghost
imaging can clearly show the periodicity of the data in the image. The image
brightness distribution is consistent with that of ideal data.

Finally, we discuss the influence of noise in the experimental system on data
ghost imaging. In theory, the random factors in the data, such as noise,
random amplitudes and phase changes, affect only the image corresponding to
the object, while the nonrandom characteristics of the data are shown in the
background area of the imaging, so the signal and noise can be perfectly
separated. This means that in theory, any strong random noise does not affect
the extraction of nonrandom characteristics from the data. However, the strong
noise in the actual experiment affects the extraction of the data
characteristics, mainly due to the additional noise generated during the
experiment. In the current experiment, we use a common commercial display,
data acquisition card and barrel detector, which proves that this experiment
is very easy to implement, but if one wants to further improve the anti-
jamming ability of data ghost imaging, displays with higher contrast and
faster response speed such as OLED displays, data acquisition cards with
higher accuracy and low noise photoelectric detectors with low temperature
thermostat systems can be used. In additional, When there are multiple
periodic signals, similar to the discussion under Eq. (1), the resulting image
will be the superposition of multiple periodic signals after removing noise.
Further analysis of the image obtained by correlation reconstruction can
obtain the frequency and amplitude of their respective periodic signals.
Therefore, ghost imaging can also be used for the analysis of multiple
periodic signals.

In summary, the periodicity of data is successfully imaged by using a
computational ghost imaging experiment. It is found that the randomness
factors in the data, such as noise, random amplitudes and phase changes,
mainly affect the image corresponding to the object, and the periodicity in
the data is clearer in the background area of the image, so the signal and
noise can be separated. The experimental results show that the periodicity in
binarized data can be detected when the SNR is 1:19 or when the SNR is 1:7,
the random amplitude of the phase reaches $210^{\circ}$, and the random
amplitude reaches 90%. This kind of data ghost imaging system is very simple
and can be used in many fields such as big data analysis, meteorology,
astronomy, and economics.

This work was supported by National Natural Science Foundation of China (NSFC)
(Grants No. 11764008, No. 61774168, and No. 11964007, the National Key
Research and Development Program of China (Grant No. 2016YFA0202300), the
Science and Technology Talent Support Project of the Department of Education
in Guizhou Province (Grant No. KY[2018]045), the Science and Technology
Foundation of Guizhou Province, China (Grant No. [2020]1Y026), and
Construction project of characteristic key laboratory in Guizhou Colleges and
Universities (KY[2021]003).

## References

  * (1) D. N. Klyshko,  Zh. Eksp. Teor. Fiz. 90, 1131 (1988).
  * (2) A. V. Belinskii and D. N. Klyshko,  Zh. Eksp. Teor. Fiz. 78, 259 (1994).
  * (3) M. P. Edgar, G. M. Gibson, and M. J. Padgett,  Nature Photonics 13, 13 (2019).
  * (4) P.-A. Moreau, E. Toninelli, T. Gregory, and M. J. Padgett,  Laser & Photonics Reviews 12, 1700143 (2018).
  * (5) B. Sun et al.,  Science 340, 844 (2013).
  * (6) R. I. Khakimov et al.,  Nature 540, 100 (2016).
  * (7) S. Li et al.,  Phys. Rev. Lett. 121, 114801 (2018).
  * (8) P. Ryczkowski, M. Barbier, A. T. Friberg, J. M. Dudley, and G. Genty,  Nature Photonics 10, 167 (2016).
  * (9) H. Wu, P. Ryczkowski, A. T. Friberg, J. M. Dudley, and G. Genty,  Optica 6, 902 (2019).
  * (10) J. Cheng and S. Han,  Phys. Rev. Lett. 92, 093903 (2004).
  * (11) A.-X. Zhang, Y.-H. He, L.-A. Wu, L.-M. Chen, and B.-B. Wang,  Optica 5, 374 (2018).
  * (12) A. M. Kingston et al.,  Phys. Rev. A 101, 053844 (2020).
  * (13) S.-C. Chen et al.,  Light: Science & Applications 9, 99 (2020).
  * (14) L. Olivieri et al.,  Optica 7, 186 (2020).
  * (15) W. Li et al.,  Optica 6, 1515 (2019).
  * (16) A. Valencia, G. Scarcelli, M. D’Angelo, and Y. Shih,  Phys. Rev. Lett. 94, 063601 (2005).
  * (17) X.-H. Chen, Q. Liu, K.-H. Luo, and L.-A. Wu,  Opt. Lett. 34, 695 (2009).
  * (18) Z. Ye et al.,  Applied Physics Letters 117, 091103 (2020).
  * (19) D.-J. Zhang et al.,  Phys. Rev. A 92, 013823 (2015).
  * (20) Z. Ye, J. Xiong, and H.-C. Liu,  Phys. Rev. Applied 15, 034035 (2021).
  * (21) H.-C. Liu et al.,  Science Advances 3 (2017).
  * (22) D. Ratner, J. P. Cryan, T. J. Lane, S. Li, and G. Stupakov,  Phys. Rev. X 9, 011045 (2019).
  * (23) X. Wen et al.,  Applied Physics Letters 116, 191101 (2020).
  * (24) H. Song et al.,  Applied Physics Letters 116, 174001 (2020).
  * (25) P. Clemente, V. Durán, V. Torres-Company, E. Tajahuerce, and J. Lancis,  Opt. Lett. 35, 2391 (2010).
  * (26) J. Cheng,  Opt. Express 17, 7916 (2009).
  * (27) R. E. Meyers, K. S. Deacon, and Y. Shih,  Appl. Phys. Lett. 98, 111115 (2011).
  * (28) M. E. Schlesinger and N. Ramankutty,  Nature 367, 723 (1994).
  * (29) G. Plaut, M. Ghil, and R. Vautard,  Science 268, 710 (1995).
  * (30) J. Hao, J. Zhang, and Z. Yao,  National Science Review 6, 1016 (2019).
  * (31) S. V. George, G. Ambika, and R. Misra,  Nonlinear Dynamics 89, 465 (2017).
  * (32) B. Scherrer and D. McKenzie,  The Astrophysical Journal 837, 24 (2017).
  * (33) B. D. Nhan et al.,  The Astrophysical Journal 883, 126 (2019).
  * (34) X. Rodó, M. Pascual, G. Fuchs, and A. S. G. Faruque,  Proceedings of the National Academy of Sciences 99, 12901 (2002).
  * (35) Z. Xu et al.,  Nucleic Acids Res. 46, e109 (2018).
  * (36) H. Sanyour, J. Childs, G. A. Meininger, and Z. Hong,  Scientific Reports 8, 2899 (2018).
  * (37) D. Giannakis and A. J. Majda,  Proceedings of the National Academy of Sciences 109, 2222 (2012).
  * (38) J. B. Elsner and A. A. Tsonis, editors,  Singular Spectrum Analysis: A New Tool in Time Series Analysis,  Plenum Press, 1996.
  * (39) J. W. Cooley and J. W. Tukey,  Mathematics of Computation 19, 297 (1965).
  * (40) L. Chiron, M. A. van Agthoven, B. Kieffer, C. Rolando, and M.-A. Delsuc,  Proceedings of the National Academy of Sciences 111, 1385 (2014).
  * (41) K. Tauscher, D. Rapetti, J. O. Burns, and E. Switzer,  The Astrophysical Journal 853, 187 (2018).