11institutetext:  ConsenSys, New York, USA
11email<EMAIL_ADDRESS>11email<EMAIL_ADDRESS>11email<EMAIL_ADDRESS>
# Deductive Verification of Smart Contracts
with Dafny††thanks: Extended version of the FMICS’22 conference paper.

Franck Cassez (✉) 11 Joanne Fuller 11 Horacio Mijail Antón Quiles 11

###### Abstract

We present a methodology to develop verified smart contracts. We write smart
contracts, their specifications and implementations in the verification-
friendly language Dafny. In our methodology the ability to write
specifications, implementations and to reason about correctness is a primary
concern. We propose a simple, concise yet powerful solution to reasoning about
contracts that have _external calls_. This includes arbitrary re-entrancy
which is a major source of bugs and attacks in smart contracts. Although we do
not yet have a compiler from Dafny to EVM bytecode, the results we obtain on
the Dafny code can reasonably be assumed to hold on Solidity code: the
translation of the Dafny code to Solidity is straightforward. As a result our
approach can readily be used to develop and deploy safer contracts.

##  1 Introduction

The Ethereum network provides the infrastructure to implement a decentralised
distributed ledger. At the core of the network is the Ethereum Virtual Machine
[29] (EVM) which can execute programs written in EVM _bytecode_. This
remarkable feature means that transactions that update the ledger are not
limited to assets’ transfers but may involve complex business logic that can
be executed _programmatically_ by _programs_ called _smart contracts_.

#### Smart Contracts are Critical Systems.

Smart contracts are programs and may contain bugs. For example, in some
executions, a counter may over/underflow, an array dereference may be outside
the range of the indices of the array. These runtime errors are
vulnerabilities that can be exploited by malicious actors to attack the
network: the result is usually a huge loss of assets, being either stolen or
locked forever. There are several examples of smart contract vulnerabilities
that have been exploited in the past: in 2016, a _re-entrance_ vulnerability
in the Decentralised Autonomous Organisation (DAO) smart contract was
exploited to steal more than USD50 Million [13]. The total value netted from
DeFi hacks in the first four months of 2022 [8], $1.57 billion, has already
surpassed the amount netted in all of 2021, $1.55 billion.

Beyond runtime errors, some bugs may compromise the business logic of a
contract: an implementation may contain subtle errors that make it deviate
from the initial intended specifications (e.g., adding one to a counter
instead of subtracting one).

The presence of bugs in smart contracts is exacerbated by the fact that the
EVM bytecode of the contract is recorded in the immutable ledger and cannot be
updated. The EVM bytecode of a contract is available in the ledger, and
sometimes the corresponding source code (e.g., in Solidity [11], the most
popular language to write smart contracts) is available too, although not
stored in the ledger. Even if the source code is not available, the bytecode
can be decompiled which makes it a target of choice for attackers. Overall
smart contracts have all the features of safety critical systems and this
calls for dedicated techniques and tools to ensure they are reliable and bug-
free.

#### Smart Contracts are Hard to Verify.

Ensuring that a smart contract is bug-free and correctly implements a given
business logic is hard. Among the difficulties that software engineers face in
the development process of smart contracts are:

  * •

The most popular languages Solidity, Vyper [27] (and in the early development
stage its offspring Fe [12]) to write smart contracts have cumbersome
features. For instance there is a default _fallback_ function that is executed
when a contract is called to execute a function that is not in its interface.
Some features like the composition of function modifiers have an ambiguous
semantics [31] and developing a formal semantics of Solidity is still a
challenge [19]. There are defensive mechanisms (reverting the effects of a
transaction, enforce termination with gas consumption) that aim to provide
some safety. However, these mechanisms neither prevent runtime errors nor
guarantee functional correctness of a contract.

  * •

Most of the languages (e.g., Solidity, Vyper for Ethereum) used to develop
smart contracts are not _verification-friendly_. It is hard to express safety
(and functional correctness properties) within the language itself. Proving
properties of a contract usually requires learning another specification
language to write specifications and then embed the source code into this
specification language.

  * •

Smart contracts operate in an _adversarial environment_. For instance, a
contract can call other contracts that are untrusted, and that can even call
back into the first contract. This can result in subtle vulnerabilities like
_re-entrancy_ , which are caused by other contracts.

#### Our Contribution.

We present a methodology to develop verified smart contracts. First, we write
smart contracts, their specifications and implementations in the verification-
friendly language Dafny. This is in contrast to most of the verification
approaches for smart contracts that build on top of existing languages like
Solidity or Vyper and require annotations or translations from one language to
another. In our methodology the ability to write specifications,
implementations and to reason about correctness is a primary concern. Second,
we use a minimal number of contract-specific primitives: those offered at the
EVM level. This has the advantage of reducing the complexity of compiling a
high-level language like Dafny to EVM bytecode. Third, we propose a simple,
concise yet powerful solution to reasoning about contracts that have _external
calls_. This includes arbitrary re-entrancy which is a major source of bugs
and attacks in smart contracts. To summarise, our methodology comprises 3 main
steps: 1) reason about the contract in isolation, _closed_ contract, Section
2; 2) take into account possible exceptions, Section 3.1; 3) take into account
arbitrary external calls, Section 3.2. Although we do not yet have a compiler
from Dafny to EVM bytecode, the results we obtain on the Dafny code can
reasonably be assumed to hold on Solidity code: the translation of the Dafny
code in Solidity is straightforward. As a result our approach can readily be
used to develop and deploy safer contracts.

#### Related Work.

Due to the critical nature of smart contracts, there is a huge body of work
and tools to test or verify them. Some of the related work targets highly
critical contracts, like the deposit smart contracts [22, 23, 7], including
the verification of the EVM bytecode.

More generally there are several techniques and
tools111https://github.com/leonardoalt/ethereum˙formal˙verification˙overview.
e.g., [14, 15, 2, 3, 9, 30], for auditing and analysing smart contracts
written in Solidity [11] or EVM bytecode, but they offer limited capabilities
to verify complex functional requirements or do not take into account the
possibility of re-entrant calls.

Most of the techniques [16, 10, 20, 4, 26, 1, 18, 18, 28] for the verification
of smart contracts using high-level code implement a translation from Solidity
(or Michelson for other chains) to some automated provers like Why3, F∗, or
proof assistants like Isabelle/HOL, Coq.

The work that is closest to our approach is [5]. In [5] a principled solution
to check smart contracts with re-entrancy is proposed and based on
instrumenting the code. Our solution (Section 3.2) is arguably simpler.
Another difference is that [5] does not use the _gas_ resource and is
restricted to safety properties. Our approach includes the proof of
termination using the fact that each computation has a bounded (though
potentially arbitrary large) amount of resources. Modelling the gas
consumption is instrumental in the solution we propose in Section 3.2 as it
enables us to prove termination and to reason by well-founded induction on
contracts with external calls.

##  2 Verification of Closed Smart Contracts

In this section, we introduce our methodology in the ideal case where the code
of a smart contract is _closed_. By closed, we mean that there are no calls to
functions outside (e.g., an external library or another smart contract) of the
contract itself.

#### An Abstract View of the EVM.

The Ethereum platform provides a global computer called the Ethereum Virtual
Machine, EVM, to execute smart contracts.

In essence, smart contracts are similar to classes/objects in OO programming
languages: they can be created/destructed, they have a non-volatile _state_ ,
and they offer some _functions_ (interface) to modify their state. Smart
contracts are usually written in high-level languages like Solidity or Vyper
and compiled into low-level EVM _bytecode_. The EVM bytecode of a contract is
recorded in the ledger and is immutable. The state of the contract can be
modified by executing some of its functions and successive states’ changes are
recorded in the ledger.

#### Transactions and Accounts.

Participants in the Ethereum network interact by submitting _transactions_.
Transactions can be simple ETH (Ethereum’s native cryptocurrency) transfer
requests or requests to execute some code in a smart contract. The initiator
of a transaction must bound the resources they are willing to use by providing
a maximum amount of _gas_ $maxG$. In the EVM, each instruction consumes a
given (positive) amount of gas. The execution of a transaction runs until it
(normally) ends or until it runs out of gas. Before running a computation, the
initiator agrees on a _gas price_ , $gp$, i.e., how much one gas unit is worth
in ETH. At the end of the computation, if there is $gl$ gas units left,222The
EVM tracks the amount of gas left relative to the maximum. the initiator is
charged with $(maxG-gl)\times gp$ ETH. To implement this type of bookkeeping,
the initiator must have an _account_ , the _balance_ of which is larger than
the maximum fee of $maxG\times gp$ ETH, before executing the transaction.

There are two types of accounts in Ethereum: a _user_ account which is
associated with a physical owner; and a _contract_ account which is associated
with a piece of code stored in the ledger. Both have a _balance_ , stored in
the ledger, which is the amount of ETH associated with the account. An account
is uniquely identified by its (160-bit) _address_.

#### Execution of a Transaction.

The execution of a transaction involving a contract account can be thought of
as a _message call_ : an account $m$ sends a message to a contract account $c$
to execute one of its functions $f(\cdot)$ with parameters $x$; this call is
denoted $c.f(x)$. The call can originate from a user account or from a
contract account. When executing $c.f(x)$ some information about the caller
$m$ is available such has $m$’s account’s address and the maximum amount of
gas $m$ is willing to pay for the execution of $c.f(x)$. The caller $m$ can
also transfer some ETH to $c$ at the beginning of the transaction. The general
form of a transaction initiated by $m$ and involving a contract $c$ is
written:

$m\rightarrow v,g,c.f(x)$

where $m$ is the _initiator_ of the transaction, $v$ the _amount of ETH_ to be
transferred to $c$ before executing $f(x)$, and $g$ the _maximum amount of
gas_ $m$ is willing to pay to execute $c.f(x)$. To reason about the
correctness of smart contracts in a high-level language (not EVM bytecode), we
use some features that are guided by the EVM semantics:

  * •

the values of $m,v,g$ in a transaction are fixed; this means that we can write
a transaction as a standard method call of the form $c.f(x,msg,g)$ where
$msg=(m,v)$ by just adding these values as (read-only) parameters to the
original function $f$. We specify all the contracts’ functions in this form
$c.f(x,msg,g)$. In $msg$, $m$ is the _message sender_ , $msg.sender$, $v$ the
message value, $msg.value$.

  * •

The only requirement on the gas consumption is that every function consumes at
least one unit of gas, and similar for every iteration of a loop. We use the
gas value to reason about termination, and we do not take into account the
actual gas cost that only makes sense on the EVM bytecode.

#### Specification with Dafny.

To mechanically and formally verify smart contracts, we use the verification-
friendly language Dafny [17]. Dafny natively supports Hoare style
specification in the form of pre- and post-conditions, as well as writing
proofs as programs, and offers both imperative, object-oriented and functional
programming styles. The Dafny verification engine checks that the methods
satisfy their pre- and post-conditions specifications and also checks for the
runtime errors like over/underflows. The result of a verification can be
either “no errors” – all the methods satisfy their specifications –, “possible
violation” of a specification – this may come with a counter-example – or the
verification can time out. The form of verification implemented in Dafny is
_deductive_ as the verifier does not try to synthesise a proof but rather
checks that a program adheres to its specification using the available hints.
The hints can range from bounds on integer values to more complex lemmas. We
refer the reader to [17] for a more detailed introduction to the language and
its implementation.

To model the concepts (transaction, accounts) introduced so far, we provide
some data types and an Account trait, Listing A.1. A trait is similar to an
interface in Java. It can be mixed in a class or in another trait to add some
specific capabilities. The trait Account provides two members: the balance of
the account and its type333In this paper we do not use any specific features
related to the type of an account. (contract or non-contract which is
equivalent to user). For example, a user account can be created as an instance
of the UserAccount class, line 16. A contract account is created by mixing in
the Account trait and by setting the type of the contract accordingly: for
instance, the Token contract, Listing A.2, mixes in Account providing the
balance and isContract members. For high-level reasoning purposes it is enough
to define a type Address as a synonym for Account.

Listing A.1: Datatypes and Account Trait in Dafny.

⬇

1/** A message. */

2datatype Msg = Msg(sender: Account, value: uint256)

3

4type Address = Account

5

6/** Provide an Account. */

7trait Account {

8 /** Balance of the account. */

9 var balance : uint256

10

11 /** Type of account. */

12 const isContract: bool

13}

14

15/** A user account. */

16class UserAccount extends Account {

17

18 constructor(initialBal: uint256)

19 ensures balance == initialBal

20 {

21 balance := initialBal;

22 isContract := false;

23 }

24}

#### Example: A Simplified Token Contract.

We now show how to use our methodology to specify, implement and reason about
a simple contract: a simplified Token contract. This contract implements a
cryptocurrency: tokens can be minted and transferred between accounts. The
contract’s functionalities are:

  * •

the contract’s _creator_ (an account) can mint new tokens at any time and
immediately assign them to an account. This is provided by the mint function;

  * •

tokens can be sent from an account from to another to provided the sender’s
(from) balance allows it. This is provided by the transfer function.

The complete Dafny code (specification and implementation) for the Token
contract is given in Listing A.2:

  * •

the contract is written as a class and has a _constructor_ that initialises
the values of the state variables;

  * •

each method has a _specification_ in the standard form of predicates: the
_pre-conditions_ , requires, and the _post-condition_ , ensures;

  * •

the Token contract has a _global invariant_ , Ginv(). The global invariant
must be maintained by each method call. To ensure that this is the case,
Ginv() is added to the pre- and post-conditions of each method444For the
constructor it is only required to hold after the constructor code is
executed. (inductive invariant);

  * •

the contract is instrumented with _ghost_ variables, and possibly ghost
functions and proofs. Ghost members are only used in proofs and do not need to
be executable. Moreover, a ghost variable cannot be used to determine the
behaviour of non-ghost methods for example in the condition of an if
statement;

  * •

the $sum(m)$ function is not provided but computes the $sum$ of the _values_
in the map $m$;

  * •

each method consumes at least one unit of gas and returns the gas left after
when it completes.

The Token contract has two non-volatile state variables: minter and balances.
The minter is the creator of the instance of the contract (constructor) and is
a constant, which enforces it can be written to only once. Initially no tokens
have been minted and the map that records the balances (in Token, not ETH) is
empty (line 20). In this specification the creator of the contract is free to
deposit some ETH into the contract account. Note that we can also specify
Solidity-like attributes: for instance, payable is a Solidity attribute that
can be assigned to a function to allow a contract to receive ETH via a call to
this function. If a function is not payable, ETH cannot be deposited in the
contract via this function. In our setting we can simply add a pre-condition:
msg.value == 0 (Listing A.2, line 36).

Listing A.2: A Simple Token Contract in Dafny.

⬇

1class Token extends Account {

2

3 const minter: Address // minter cannot be updated after creation

4 var balances : map<Address, uint256>

5

6 ghost var totalAmount: nat

7

8 /** Contract invariant. */

9 predicate GInv()

10 reads this‘totalAmount, this‘balances

11 {

12 totalAmount == sum(balances)

13 }

14

15 /** Initialise contract. */

16 constructor(msg: Msg)

17 ensures GInv()

18 ensures balance == msg.value && minter == msg.sender

19 {

20 isContract, minter, balances, balance := true, msg.sender, map[],
msg.value;

21 totalAmount := 0;

22 }

23

24 /**

25 * @param from Source Address.

26 * @param to Target Address.

27 * @param amount The amount to be transfered from ‘from‘ to ‘to‘.

28 * @param msg The ‘msg‘ value.

29 * @param gas The gas allocated to the execution.

30 * @returns The gas left after executing the call.

31 */

32 method transfer(from:Address,to:Address,

33 amount:uint256,msg:Msg,gas: nat) returns (g:nat)

34 requires from in balances && balances[from] >= amount && msg.sender == from

35 requires gas >= 1

36 requires msg.sender == from && msg.value == 0;

37 requires to !in balances ||

38 balances[to] as nat + amount as nat <= MAX_UINT256

39 requires GInv()

40 ensures GInv()

41 ensures from in balances && balances[from] >= old(balances[from]) - amount

42 ensures to in balances

43 ensures to != from ==> balances[to] >= amount

44 decreases gas

45 modifies this

46 {

47 balance := balance + msg.value;

48 var newAmount: uint256 := balances[from] - amount ;

49 balances :=

50 balances[to := (if to in balances then balances[to] else 0) + amount];

51 balances := balances[from := newAmount];

52 }

53

54 /**

55 * @param to Target Address.

56 * @param amount The amount to receiving the newly minted tokens

57 * @param msg The ‘msg‘ value.

58 * @param gas The gas allocated to the execution.

59 * @returns The gas left after executing the call.

60 */

61 method mint(to:Address,amount: uint256,msg:Msg,gas:nat) returns (g:nat)

62 requires msg.sender == minter

63 requires gas >= 1

64 requires to !in balances ||

65 balances[to] as nat + amount as nat <= MAX_UINT256

66 requires GInv()

67 ensures totalAmount == old(totalAmount) + amount as nat

68 ensures GInv()

69 modifies this‘balances, this‘totalAmount

70 {

71 balances :=

72 balances[to := (if to in balances then balances[to] else 0) + amount];

73 // The total amount increases.

74 totalAmount := totalAmount + amount as nat;

75 g := gas - 1;

76 }

77}

The global invariant of the contract (line 9) states that the total amount of
tokens is assigned to the accounts in balances. The ghost variable totalAmount
keeps track of the number of minted tokens. The transfer method (line 32)
requires that the source account is in the balances map whereas the target
account may not be in yet. In the latter case it is added to the map. Note
that the initiator must be the source account (msg.sender == from, line 36).

#### Verification of the Simplified Token Contract.

The Dafny verification engine can check whether implementations satisfy their
pre-/post-conditions. In the case of the Token contract, Dafny reports “no
errors” which means that:

  * •

there are no runtime errors in our program. For instance the two requirements
balances[from] >= amount (line 34) and balances[to] as nat + amount as nat <=
MAX_UINT256 guarantee that the result of the operation is an uint256 and there
is no over/underflows at lines 50, 51. The update of a map $m$ is written
$m[k:=v]$ and results in a map $m^{\prime}$ such that
$m^{\prime}[w]=m[w],k\neq w$ and $m^{\prime}[k]=v$ (lines 50, 51, 72).

  * •

The global invariant GInv() must be preserved by each method call: if it holds
at the beginning of the execution of a method, it also holds at the end. This
global invariant must also hold after the constructor has completed. If Dafny
confirms GInv() holds everywhere, we can conclude that GInv() holds after any
finite number of calls to either mint or transfer.

  * •

There are some other pre- and post-conditions that are in the specifications.
For example, the old keyword refers to the value of a variable at the
beginning of the method and line 41 states that the balance of the from
account has been decreased by amount.

The specification of the Token contract presented in this section assumes the
pre-conditions hold for each message (method) call. In practice, this has to
be ensured at runtime: it is impossible to force an initiator to submit a
transaction that satisfies the pre-conditions of a method. However, this is a
reasonable assumption as in case the pre-conditions do not hold, we can simply
abort the execution. This kind of behaviour is supported by the EVM semantics
where it is possible to return a status of a computation and abort (similar to
an exception) the execution of the function and _revert_ its effects on the
contract’s state. Another more serious simplification of the Token contract is
that there is no _external call_ to another contract’s method. It turns out
that external calls can be problematic in smart contracts and are the source
of several attacks.

In the next section we show how to reason about smart contracts under
adversarial conditions: exceptions and external calls.

##  3 Verification Under Adversarial Conditions

In this section we show how to take into account adversarial conditions: in
the first section we describe how to move pre-conditions into runtime checks
and enrich our specifications to precisely account for when a function call
should revert. In the second part we propose a general mechanism to capture
the possible adversarial effects of external calls.

###  3.1 Aborting a Computation

As mentioned before we cannot enforce the initiator of a transaction to
satisfy any pre-conditions when calling a method in a smart contract. However,
a simple way to handle exceptional cases is to explicitly check that some
conditions are satisfied before executing the actual body of a method, and if
it is not the case to abort the computation. In the EVM semantics this is
known as a _revert_ operation that restores the state of the contract before
the transaction. The EVM has a special opcode, Revert to return the status of
a failed computation.

In the previous section, we used pre-conditions to write the specification of the methods. We can automatically push these pre-conditions into runtime checks at the beginning of each method. To take into account the possibility of _exceptions_ in a clean way, we lift the return values of each method to capture the status of a computation using a standard return generic type of the form datatype Try<T> = Revert | Success(v: T). If a computation is successful, the value v of type T is returned and boxed in the Success constructor, otherwise Revert is returned.555Revert is sometimes called Failure and can return a string error message.

The implementation of the methods666The constructor has no pre-condition, so
we can assume it always succeeds. mint and transfer can be lifted using the
return datatype Try<T> as in Listing A.3, line 1. This datatype allows for the
return of arbitrary values of type T and as a special case when no value is
returned, we can set $\texttt{T}=\texttt{Unit}$ the type inhabited by a single
value.

The new code (Listing A.3) introduces the following features:

  * •

the conditions under the first if statements of mint and transfer
(respectively at lines 22 and 47) are the negation of the conjunction of all
the pre-conditions that are in Listing A.2.

  * •

The pre-condition GInv() remains in the code. It is not a runtime check but a
property of the contract that has to be preserved. This invariant is not part
of the executable code.

  * •

In this example of a closed contract we can characterise exactly when the
transaction should revert (r.T? is true if and only if r is of type T). For
instance the post-condition at line 7 precisely defines the conditions under
which the method should not abort.

  * •

The post-conditions at lines 15 and 40 ensures that the state of the contract
(balances) is unchanged.

Dafny returns “no errors” for this program, and we can conclude that the
global invariant is always satisfied after any number of calls to mint or
transfer. The code for each method does not enforce any pre-condition on the
caller and can be translated into runtime checks at the EVM bytecode level.

Listing A.3: The Token Contract with Revert.

⬇

1datatype Try<T> = Revert() | Success(v: T)

2

3method transfer(from:Address,to:Address,amount:uint256,msg:Msg,gas:nat)

4 returns (g: nat, r: Try<()>)

5

6 requires GInv()

7 ensures // if r is of type Success

8 r.Success? <==>

9 (from in old(balances)

10 && old(balances[from]) >= amount

11 && msg.sender == from

12 && gas >= 1

13 && (to !in old(balances)||old(balances[to]) as nat + amount as
nat<=MAX_UINT256))

14 /** State is unchanged on an revert. */

15 ensures r.Revert? ==> balances == old(balances)

16 ensures g == 0 || g <= gas - 1

17 ensures GInv()

18

19 decreases gas

20 modifies this

21{

22 if !(from in balances && balances[from]>=amount && msg.sender==from &&
gas>=1

23 && (to !in balances || balances[to] as nat + amount as nat<=MAX_UINT256) )
{

24 return (if gas >= 1 then gas - 1 else 0), Revert();

25 }

26 var newAmount := balances[from] - amount;

27 balances := balances[to := (if to in balances then balances[to] else 0) +
amount];

28 balances := balances[from := newAmount];

29 g, r := gas - 1, Success(());

30}

31

32method mint(to:Address,amount:uint256,msg:Msg,gas:nat) returns (g:nat,r:
Try<()>)

33 requires GInv()

34 ensures r.Success? ==> totalAmount == old(totalAmount) + amount as nat

35 ensures r.Revert? <==>

36 !(msg.sender == minter && gas >= 1 &&

37 (to !in old(balances)||

38 old(balances[to]) as nat + amount as nat<=MAX_UINT256))

39 // state unchanged on a revert.

40 ensures r.Revert? ==> balances == old(balances)

41 ensures g == 0 || g <= gas - 1

42 ensures GInv()

43

44 modifies this‘balances, this‘totalAmount

45 decreases gas

46{

47 if !(msg.sender == minter && gas >= 1 &&

48 (to !in balances || balances[to] as nat + amount as nat<=MAX_UINT256)) {

49 return (if gas >= 1 then gas - 1 else 0), Revert();

50 }

51 balances := balances[to := (if to in balances then balances[to] else 0) +
amount];

52 // The total amount increases.

53 totalAmount := totalAmount + amount as nat;

54 g, r := gas - 1, Success(());

55}

###  3.2 Reasoning with Arbitrary External Calls

We now turn our attention to smart contracts that have _external calls_. The
semantics of the EVM imposes the following restrictions on the mutations of
state variables for contracts: the state variables of a contract $c$ can only
be updated by a call to a method777We assume that all methods are _public_. in
$c$. In other words another contract $c^{\prime}\neq c$ cannot write the state
variables of $c$.

Assume that when we transfer some tokens to a contract via the transfer
method, we also _notify_ the receiver. The corresponding new code for transfer
is given in Listing A.4. If the method notify in contract to does not perform
any external call itself, the segment to.notify($\cdot$) cannot modify the
state variables of the Token contract, and the Token contract invariant GInv()
is preserved. We may not have access to the code of notify($\cdot$) and may be
unable to check whether this is the case.

If notify can call another contract it may result in unexpected consequences.
For instance if the external call to the method to.notify($\cdot$) occurs
before the update of balances[from], to.notify may itself call (and collude
with) from and call from to do the same transfer again. As a result many
transfers will be performed (as long as some gas is left) and tokens will be
_created_ without a proper call to mint. The result is that the number of
minted tokens does not correspond anymore to the number of tokens allocated to
accounts, and the global invariant Ginv() does not hold anymore after
transfer. This type of issue is commonly known as the _re-entrancy problem_.
This vulnerability was exploited in the past in the so-called DAO-exploit
[13].

Listing A.4: The Token Contract with a Notification.

⬇

method transfer(...) returns (g: nat, r: Try<()>)

...

{

...

balances := balances[to := (if to in balances then balances[to] else 0) +
amount];

balances := balances[from := newAmount];

// External call to contract ‘to‘.

// If we notify before updating balances, a re-entrant call may drain the
contract

// of its tokens.

g, status := to.notify(from, amount, gas - 1);

...

}

There are several solutions to mitigate the re-entrancy problem. A simple
solution is to require that calls to external contracts occur only as the last
instruction in a method (Check-Effect-Interaction pattern [6]). This is a
_syntactic sufficient condition_ to ensure that every update on a contract’s
state occurs before any external calls. This enforces re-entrant calls to
happen sequentially. A _semantic_ approach for taking into external calls is
proposed in [5] and rely on identifying segments of the code with external
calls and adding some local variables to capture the effects of a call and
reason about it.

We propose a similar but hopefully simpler technique888It can be implemented
directly in Dafny with no need for extra devices. to model external calls and
their effects. Similar to [5] we do not aim to identify re-entrant calls but
we want to _include and model_ the effect of possible external (including re-
entrant) calls and check whether the contract invariant can be violated or
not. For the sake of simplicity we describe our solution to this problem on
the to.notify($\cdot$) example, Listing A.4, and make the following (EVM
enforced) assumptions on to.notify($\cdot$):

  * •

it always terminates and returns the gas left and the status of the call
(revert or success),

  * •

it consumes at least one unit of gas,

  * •

it may itself make arbitrary external calls including callbacks to transfer
and mint in the Token contract. As a result there can be complex nested calls
to transfer and mint.

Our solution abstracts the call to to.notify($\cdot$) into a generic
externalCall. The new code for the transfer method is given in Listing A.5. We
model the effect of the external call to.notify($\cdot$) (line 17) by a call
to the externalCall($\cdot$) method.

The idea is that externalCall($\cdot$) is going to generate all possible re-
entrant calls including nested calls to transfer. To do so, we introduce some
_non-determinism_ to allow an external call to callback transfer and mint.
This occurs at lines 51 and 57. Note that the parameters (from, to, amount,
msg) of the re-entrant calls are randomly chosen using the havoc<T>() method
that returns an arbitrary value of type T.

The code of externalCall works as follows:

  * •

non-deterministically pick $k$ and use it to decide whether a re-entrant call
occurs or not (lines 42–58). There are three options, and we use $k\mod 3$ to
select among them. If $k\mod 3=0$ (and there is enough gas left), a re-entrant
call to transfer occurs. If $k\mod 3=1$ a re-entrant call to mint occurs.
Otherwise, ($k\mod 3=2)$, no re-entrant call occurs.

  * •

finally (lines 61–69), we non-deterministically pick a boolean variable $b$ to
decide whether a new external call occurs.

We do not provide a formal proof that this captures all the possible re-
entrant calls999This is beyond the scope of this paper., but rather illustrate
that it models several cases. First, externalCall can simulate an arbitrary
sequence $\texttt{mint}*$ of calls to mint. This is obtained by selecting
successive values of $k$ such that $k\mod 3=1$ and then selecting $b=true$.
For instance, the sequence of values $k=1$, $b=true$, $k=1$, $b=true$, $k=2$,
$b=false$ simulates two reentrant calls to mint, i.e., mint.mint. As the gas
value is also a parameter of all the methods and can be arbitrarily large,
this model can generate all the sequences of calls in $\texttt{mint}*$.
Second, externalCall can also simulate nested transfer/mint calls. For
instance, the sequence of values $k=0$, $b=true$, $k=1$, $b=false$, simulates
two reentrant calls to transfer with a nested call to mint. Third, nested
calls to transfer can also be generated by externalCall. The sequence of
values $k=0$, $b=true$, $k=0$, $b=false$ simulates two nested re-entrant calls
to transfer.

The re-entrant calls can be executed with arbitrary inputs and thus the input
parameters are _havoced_ i.e., non-deterministically chosen and externalCall
can generate an arbitrary number of external and re-entrant calls including
nested calls to transfer and mint.

Listing A.5: The Token Contract with External Calls.

⬇

1method transfer(from:Address,to:Address,amount:uint256,msg:Msg,gas:nat)

2 returns (g:nat,r:Try<()>)

3

4 ... // Ensures and requires same as Listing A.3

5{

6 if !(from in balances && balances[from]>=amount && msg.sender==from &&
gas>=1

7 && (to !in balances || balances[to] as nat + amount as nat <= MAX_UINT256) )
{

8 return (if gas >= 1 then gas - 1 else 0), Revert();

9 }

10 var newAmount := balances[from] - amount;

11 balances := balances[to := (if to in balances then balances[to] else 0) +
amount];

12 balances := balances[from := newAmount];

13 // If we swap the line above and the externalCall,

14 // we cannot prove invariance of GInv()

15 // At this location GInv() must hold which puts a restriction

16 // on where external call can occur.

17 var g1, r1 := externalCall(gas - 1); // to.notify( from, amount );

18 assert g1 == 0 || g1 <= gas - 1;

19 // We can choose to propagate or not the failure of external call.

20 // Here choose not to.

21 g, r := (if g1 >= 1 then g1 - 1 else 0), Success(());

22}

23

24/**

25 * Simulate an external call with possible re-entrant calls.

26 *

27 * @param gas The gas allocated to this call.

28 * @returns The gas left after execution of the call and the status of the
call.

29 *

30 * @note The state variables of the contract can only be modified by

31 * calls to mint and transfer.

32 */

33 method externalCall(gas: nat) returns (g: nat, r: Try<()>)

34 requires GInv()

35 ensures GInv()

36 ensures g == 0 || g <= gas - 1

37 modifies this

38 decreases gas

39{

40 g := gas;

41 // Havoc ‘k‘ to introduce non-determinism.

42 var k: nat := havoc();

43 // Depending on the value of k % 3,

44 // re-entrant call or not or another external call.

45 if k % 3 == 0 && g >= 1 {

46 // re-entrant call to transfer.

47 var from: Address := havoc();

48 var to: Address := havoc();

49 var amount: uint256 := havoc();

50 var msg: Msg := havoc();

51 g, r := transfer(from, to, amount, msg, g - 1);

52 } else if k % 3 == 1 && g >= 1 {

53 // re-entrant call to mint.

54 var to: Address := havoc();

55 var amount: uint256 := havoc();

56 var msg: Msg := havoc();

57 g, r := mint(to, amount, msg, g - 1);

58 }

59 // k % 3 == 2, no re-entrant call.

60 // Possible new external call

61 var b:bool := havoc();

62 if b && g >= 1 {

63 // external call makes an external call.

64 g, r := externalCall(g - 1);

65 } else {

66 // external call does not make another external call.

67 g := if gas >= 1 then gas - 1 else 0;

68 r := havoc();

69 }

70}

71

72/** Havoc a given type. */

73method {:extern} havoc<T>() returns (a: T)

The key ingredient that allows us to reason and prove correctness is the gas
value. We require that gas strictly decreases (line 38) after each recursive
call. This is stated in Dafny with the decreases clause. Dafny checks that the
value of the gas parameter strictly decreases on mutually recursive calls.

Our objective is now to prove, using this model of external calls, that the
global invariant GInv() of the contract is always satisfied. This seems to be
a complex task as our model includes an arbitrary and unbounded number of
possibly nested external calls. The result is a mutually recursive program:
transfer can call externalCall and externalCall can call transfer or
externalCall. However, the property that the gas value strictly decreases on
every call enables us to reason by induction. As the gas decreases on each new
call, the induction is well-founded. And Dafny can indeed prove that the
global invariant GInv() is preserved by all the methods including an arbitrary
number of possibly re-entrant externalCalls. Our solution provides a way to
model the effects of external calls abstractly but conservatively while still
being able to prove properties in modular manner in an adversarial environment
modelled by externalCall. Compared to other approaches we also guarantee
termination because we take into account the minimum amount of gas that
computations take.

Note that externalCall has the pre-condition GInv(). This means that in
transfer the predicate GInv() must be true before the call to externalCall.
This amounts to having restrictions on where external calls can occur.
However, without any knowledge of what external calls can do, this seems to be
a reasonable restriction. For instance, if the external call has a callback to
mint we can only prove the preservation of the invariant Ginv() if it holds
before the call to mint. Of course if we have more information about an
external call, e.g., we know it does not call back, we can also take it into
account with our model: we can adjust externalCall to reflect this knowledge.

In our example, if we swap the lines 12 and 17 (Listing A.5), Dafny cannot
verify that GInv() is preserved by transfer. The reason is that the invariant
Ginv() does not hold before the external call.

To the best of our knowledge this solution is the first that does not require
any specific reasoning device or extension to prove properties of smart
contracts under adversarial conditions, but can be encoded directly in a
verification-friendly language.

#### Running Dafny and Reproducing the Verification Results.

The code used in this paper omits some functions and proofs hints (like sum)
and may not be directly verifiable with Dafny. The interested reader is
invited to check out the code in the repository
https://github.com/ConsenSys/dafny-sc-fmics to get the full version of our
contracts. The repository contains the code of the Token contract, a
simplified auction contract and instructions how to reproduce the Dafny
verification results.

The auction contract demonstrates that global invariants (GInv() in Token) are
not limited to specifying _state_ properties but can also capture two-state or
multi-state properties. This can be achieved by adding ghost history variables
using sequences. This type of specifications is expressive enough to encode
some standard temporal logic properties on sequences of states of a contract,
e.g., “Once the variable ended is set to true, it remains true for ever” in
the simplified auction contract.

In our experiments, Dafny can handle complex specifications and the contracts
we have verified are checked with Dafny within seconds on a standard laptop
(MacBook Pro). The performance does not seem to be an issue at that stage, and
if it would become an issue, there are several avenues to mitigate it: Dafny
supports modular verification, so we can break down our code into smaller
methods; Dafny has built-in strategies to manipulate the verification
conditions and break them into simpler ones that can be checked independently.

##  4 Conclusion

We have proposed a methodology to model and reason about (Ethereum) smart
contracts using the verification-friendly language Dafny. The main features of
our approach are: $i)$ we encode the specifications and implementations of
contracts directly in Dafny with no need for any language extensions; $ii)$ we
take into account the possibility of _failures_ and (arbitrary number of)
_external calls_ ; $iii)$ we specify the main properties of a contract using
contract _global invariants_ and prove these properties in a modular manner by
a conservative abstraction of external calls with no need to know the code of
externally called contracts.

To the best of our knowledge, our abstract model of the effect of external
calls is new and the associated proof technique (mutually recursive method
calls) is readily supported by Dafny which makes it easy to implement.

We have tested our methodology on several contracts (e.g., Token, Simple
Auction, Bank) and we believe that this technique can be used to verify larger
contracts. Indeed, we can take advantage of the modular proof approach (based
on pre- and post-conditions) supported by Dafny to design scalable proofs.

Our current work aims to automate the methodology we have presented by
automatically generating the different versions of a given contract (closed,
revert, external calls) from a simple source contract.

The approach we have presented is general and not exclusive to Dafny, and our
methodology can be implemented within other verification-friendly languages
like Why3 [20], Whiley [25], or proof assistants like Isabelle/HOL [21] or Coq
[24].

## References

  * [1] Ahrendt, W., Bubel, R.: Functional verification of smart contracts via strong data integrity. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications, ISoLA 2020\. Part III. LNCS, vol. 12478, pp. 9–24. Springer (2020). https://doi.org/10.1007/978-3-030-61467-6_2
  * [2] Alt, L., Reitwießner, C.: SMT-based verification of solidity smart contracts. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, ISoLA 2018. Part IV. LNCS, vol. 11247, pp. 376–388. Springer (2018). https://doi.org/10.1007/978-3-030-03427-6_28
  * [3] Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in Isabelle/HOL. In: Andronick, J., Felty, A.P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018. pp. 66–77. ACM (2018). https://doi.org/10.1145/3167084
  * [4] Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Béguelin, S.Z.: Formal verification of smart contracts. In: PLAS@CCS 2016. pp. 91–96. ACM (2016). https://doi.org/10.1145/2993600.2993611
  * [5] Bräm, C., Eilers, M., Müller, P., Sierra, R., Summers, A.J.: Rich specifications for ethereum smart contract verification. Proc. ACM Program. Lang. 5(OOPSLA), 1–30 (2021). https://doi.org/10.1145/3485523
  * [6] Britten, D., Sjöberg, V., Reeves, S.: Using coq to enforce the checks-effects-interactions pattern in DeepSea smart contracts. In: Bernardo, B., Marmsoler, D. (eds.) 3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021. OASIcs, vol. 95, pp. 3:1–3:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/OASIcs.FMBC.2021.3
  * [7] Cassez, F.: Verification of the incremental merkle tree algorithm with Dafny. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) Formal Methods - 24th International Symposium, FM 2021, November 20-26, 2021, Proceedings. LNCS, vol. 13047, pp. 445–462. Springer (2021). https://doi.org/10.1007/978-3-030-90870-6_24
  * [8] Choo, L.: Crypto is crumbling, and DeFi hacks are getting worse, https://www.protocol.com/fintech/defi-hacks-web3
  * [9] ConsenSys Diligence: Mythx, https://mythx.io/
  * [10] Dharanikota, S., Mukherjee, S., Bhardwaj, C., Rastogi, A., Lal, A.: Celestial: A smart contracts verification framework. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, pp. 133–142. IEEE (2021). https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_22
  * [11] Ethereum Foundation: Solidity documentation (2022), https://docs.soliditylang.org/en/v0.8.14/
  * [12] Fe Team: Fe: an emerging smart contract language for the Ethereum blockchain (2022), https://github.com/ethereum/fe
  * [13] Güçlütürk, O.G.: The DAO Hack Explained: Unfortunate Take-off of Smart Contracts (2018), https://ogucluturk.medium.com/the-dao-hack-explained-unfortunate-take-off-of-smart-contracts-2bd8c8db3562
  * [14] Hajdu, Á., Jovanovic, D.: solc-verify: A modular verifier for Solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments, VSTTE 2019\. LNCS, vol. 12031, pp. 161–179. Springer (2019). https://doi.org/10.1007/978-3-030-41600-3_11
  * [15] Hajdu, Á., Jovanovic, D., Ciocarlie, G.F.: Formal specification and verification of Solidity contracts with events (short paper). In: Bernardo, B., Marmsoler, D. (eds.) 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020. OASIcs, vol. 84, pp. 2:1–2:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/OASIcs.FMBC.2020.2
  * [16] da Horta, L.P.A., Reis, J.S., de Sousa, S.M., Pereira, M.: A tool for proving Michelson smart contracts in WHY3. In: IEEE International Conference on Blockchain, Blockchain 2020. Rhodes, Greece, pp. 409–414. IEEE (2020). https://doi.org/10.1109/Blockchain50366.2020.00059
  * [17] Leino, K.R.M.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94–97 (2017). https://doi.org/10.1109/MS.2017.4121212
  * [18] Marescotti, M., Otoni, R., Alt, L., Eugster, P., Hyvärinen, A.E.J., Sharygina, N.: Accurate smart contract verification through direct modelling. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications, ISoLA 2020. LNCS, vol. 12478, pp. 178–194. Springer (2020). https://doi.org/10.1007/978-3-030-61467-6_12
  * [19] Marmsoler, D., Brucker, A.D.: A denotational semantics of Solidity in Isabelle/HOL. In: Calinescu, R., Pasareanu, C.S. (eds.) 19th International Conference on Software Engineering and Formal Methods, SEFM 2021. LNCS, vol. 13085, pp. 403–422. Springer (2021). https://doi.org/10.1007/978-3-030-92124-8_23
  * [20] Nehaï, Z., Bobot, F.: Deductive proof of industrial smart contracts using WHY3. In: Formal Methods. FM 2019. Porto, Portugal, Part I. LNCS, vol. 12232, pp. 299–311. Springer (2019). https://doi.org/10.1007/978-3-030-54994-7_22
  * [21] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)
  * [22] Park, D., Zhang, Y.: Formal verification of the incremental merkle tree algorithm (2020), https://github.com/runtimeverification/verified-smart-contracts/blob/master/deposit/formal-incremental-merkle-tree-algorithm.pdf
  * [23] Park, D., Zhang, Y., Rosu, G.: End-to-end formal verification of Ethereum 2.0 deposit smart contract. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification, CAV 2020, Los Angeles, CA, USA, Part I. LNCS, vol. 12224, pp. 151–164. Springer (2020). https://doi.org/10.1007/978-3-030-53288-8_8
  * [24] Paulin-Mohring, C.: Introduction to the Coq proof-assistant for practical software verification. In: Meyer, B., Nordio, M. (eds.) Tools for Practical Software Verification, LASER, International Summer School 2011. LNCS, vol. 7682, pp. 45–95. Springer (2011). https://doi.org/10.1007/978-3-642-35746-6_3,
  * [25] Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with Whiley. In: Engineering Trustworthy Software Systems, SETSS 2018. LNCS, vol. 11430, pp. 1–37. Springer (2018). https://doi.org/10.1007/978-3-030-17601-3_1
  * [26] Schiffl, J., Ahrendt, W., Beckert, B., Bubel, R.: Formal analysis of smart contracts: Applying the key system. In: Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, LNCS, vol. 12345, pp. 204–218. Springer (2020). https://doi.org/10.1007/978-3-030-64354-6_8
  * [27] Vyper Team: Documentation (2020), https://vyper.readthedocs.io/en/stable/
  * [28] Wesley, S., Christakis, M., Navas, J.A., Trefler, R.J., Wüstholz, V., Gurfinkel, A.: Verifying Solidity smart contracts via communication abstraction in SmartAce. In: Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 13182, pp. 425–449. Springer (2022). https://doi.org/10.1007/978-3-030-94583-1_21
  * [29] Wood, D.: Ethereum: a secure decentralised generalised transaction ledger (2022), https://ethereum.github.io/yellowpaper/paper.pdf, berlin version d77a387 - 2022-04-26
  * [30] Wüstholz, V., Christakis, M.: Harvey: A Greybox Fuzzer for Smart Contracts, pp. 1398–1409. Association for Computing Machinery, New York, NY, USA (2020), https://doi.org/10.1145/3368089.3417064
  * [31] Zakrzewski, J.: Towards verification of Ethereum smart contracts: A formalization of core of Solidity. In: Verified Software. Theories, Tools, and Experiments, VSTTE 2018, Oxford, UK, July 18-19, 2018. LNCS, vol. 11294, pp. 229–247. Springer (2018). https://doi.org/10.1007/978-3-030-03592-1_13


# Energy Efficiency of Quantum Statevector Simulation at Scale

Jakub Adamski<EMAIL_ADDRESS>0009-0000-5221-2070 EPCC, The University
of EdinburghEdinburghUK ,  James Peter Richings<EMAIL_ADDRESS>0000-0003-0895-4063 EPCC, The University of EdinburghEdinburghUK and  Oliver
Thomson Brown<EMAIL_ADDRESS>0000-0002-5193-8635 EPCC, The University
of EdinburghEdinburghUK

(2023)

###### Abstract.

Classical simulations are essential for the development of quantum computing,
and their exponential scaling can easily fill any modern supercomputer. In
this paper we consider the performance and energy consumption of large Quantum
Fourier Transform (QFT) simulations run on ARCHER2, the UK’s National
Supercomputing Service, with QuEST toolkit. We take into account CPU clock
frequency and node memory size, and use cache-blocking to rearrange the
circuit, which minimises communications. We find that using 2.00 GHz instead
of 2.25 GHz can save as much as 25% of energy at 5% increase in runtime.
Higher node memory also has the potential to be more efficient, and cost the
user fewer CUs, but at higher runtime penalty. Finally, we present a cache-
blocking QFT circuit, which halves the required communication. All our
optimisations combined result in 40% faster simulations and 35% energy savings
in 44 qubit simulations on 4,096 ARCHER2 nodes.

©Adamski, Richings, Brown 2023. This is the author’s version of the work. It
is posted here for your personal use. Not for redistribution. The definitive
version was published in Workshops of The International Conference on High
Performance Computing, Network, Storage, and Analysis (SC-W 2023),
https://doi.org/10.1145/3624062.3624270.

††copyright: none††journalyear: 2023††ccs: Hardware Impact on the
environment††ccs: Applied computing Physics††ccs: Theory of computation
Quantum computation theory††ccs: Computing methodologies Parallel computing
methodologies

##  1\. Introduction

Quantum computing has become a major area of research in recent years. In
2019, Google published a paper, in which they claimed to have successfully
performed the classically intractable task of random circuit sampling (Arute
et al., 2019), leading to an explosion of public interest and investment in
quantum computers. The technology is still in its infancy and noise is still a
major challenge for quantum hardware, so classical simulation plays an
important role in algorithm development and testing. It is straightforward to
fill any known or planned supercomputer with exact simulations of fewer than
50 qubits. Given the rapidly growing interest in these unprecedentedly large
simulations, we believe it is important to consider their sustainability.
ARCHER2 has been used to simulate 44-qubit systems using 4,096 nodes with 1 PB
of memory111A feat in part inspired by a recent AWS HPC blog post where the
authors also ran a 44 qubit simulation using QuEST:
https://aws.amazon.com/blogs/hpc/simulating-44-qubit-quantum-circuits-using-
aws-parallelcluster/. – a number far below the size of the recently announced
433-qubit ‘Osprey’ quantum processor from
IBM222https://newsroom.ibm.com/2022-11-09-IBM-Unveils-400-Qubit-Plus-Quantum-
Processor-and-Next-Generation-IBM-Quantum-System-Two.. This application domain
is growing in popularity and often requires use of most of the available
resources on a given target hardware, entailing high energy consumption.
Focusing on its efficiency therefore plays a crucial role in HPC
sustainability.

Most frequently, classical simulations are implemented by the Schrödinger’s
algorithm, which is a naïve but exact approach to simulating quantum circuits.
The principle is to keep the whole statevector in memory, and evolve it by
applying gates (a matrix-vector product) from the simulated circuit. This
requires keeping track of all $2^{n}$ complex amplitudes, for $n$ qubits, and
modifying them with each iteration. The maximum number of qubits in the
register is bound by the total memory available on the target hardware. At the
same time, the runtime of a circuit simulation scales linearly with the number
of gates in the circuit, for a fixed size quantum register.

The main advantage of the statevector approach is that once a circuit is
simulated, all amplitudes are available, which enables any required
measurements to be made without the need to rerun the simulation. In contrast,
many alternative approaches, like the Feynman path algorithm (Aaronson and
Chen, 2017), or tensor network contraction (Pan and Zhang, 2022), are
restricted to a limited number of amplitudes in the output state in order to
limit the memory usage. The trade-off is that those methods typically require
repeated runs to perform all the desired measurements. This is also true of
real quantum hardware, where the output of an individual run is always a
classical bit string.

##  2\. Methodology

###  2.1. QuEST Software

QuEST (Jones et al., 2019) is a statevector simulator implemented in C and
parallelised with MPI+OpenMP, which acts as described in section 1. In order
to evolve the statevector, each amplitude needs to be updated for every
applied gate.

We can distinguish three kinds of quantum operators:

  * •

Fully local gates – each amplitude can be updated without accessing other
amplitudes. Mathematically, these are diagonal matrices.

  * •

Local memory gates – each update is a linear combination of amplitudes on the
same process. As matrices, those gates are block-diagonal, with blocks size
less-or-equal to the number of amplitudes per process.

  * •

Distributed gates – new amplitudes depend on amplitudes from other processes.

As long as the update dependencies are located on the same node, no message
passing is required, and the gates can be applied relatively quickly. When the
operators become distributed, MPI takes up a large portion of the runtime.
Hence, distributed gates are much more expensive to execute.

QuEST requires the statevector to be split evenly across $2^{n}$ processes.
This ensures pairwise communication for any given gate. It also means that the
entire local statevector needs to be exchanged – 64 GB per process on ARCHER2
assuming one MPI process per node. This was the case in all experiments
presented here. Due to limitations of some implementations of MPI, individual
messages cannot be larger than 2 GB, so the communication cannot be done in a
single message. Instead, 32 messages are exchanged per distributed gate, and
QuEST implements the communications as a sequence of blocking MPI_Sendrecv.

###  2.2. Potential Optimisations

We have identified three different strategies that help perform statevector
simulations more efficiently.

  1. (1)

Changing the clock frequency of the CPU.  ARCHER2 allows users to set the CPU
frequency of computing nodes to reduce energy consumption. The default
currently is 2.00 GHz (medium), but users have the ability to change this to
either 1.50 GHz (low), or 2.25 GHz (high) with a SLURM environment
parameter333https://docs.archer2.ac.uk/user-guide/energy/#controlling-cpu-
frequency..

  2. (2)

Using nodes with larger memory size.  There are two node types available on
ARCHER2 – standard (256 GB), and high memory nodes (512 GB). We can use fewer
high-mem nodes for a given size state vector simulation.

  3. (3)

Transpiling the circuit to reduce communication via cache-blocking.  Cache-
blocking is a technique that can improve memory locality of the circuit. When
a gate acts on lower index qubits, the dependencies between statevector
elements are located closer together. It is possible to lower a target qubit
index by swapping it with another qubit. Each distributed SWAP gate requires
communication, but it can be compensated if the target is frequently acted on.
Although not implemented in QuEST, cache-blocking is already a part of some
frameworks, such as Qiskit, where it serves as a means of distribution to
multiple processes (Doi and Horii, 2020), and cuQuantum for multi-GPU support
(Faj et al., 2023). However, it is the first time this optimisation is used at
such a scale and for energy reasons.

###  2.3. Circuits

(a) Standard.

(b) Cache-blocked.

Figure 1. Standard and cache-blocked QFT circuit.

The main circuit used in this paper is the Quantum Fourier Transform (QFT),
shown on fig. 1(a). It is a common subroutine of larger quantum algorithms,
like Quantum Phase Estimation.

The QFT is straightforward to cache-block without adding new gates, as it
already features SWAP gates at the end. By shifting them to the left, we can
guarantee that all Hadamard gates are applied to local qubits. Gates to the
right of the swaps need to be vertically flipped. As a result, the only
communication remains in the distributed SWAP gates. An example is shown in
fig. 1(b), where the last two Hadamard gates were made local.

To test the effects of communication, two other benchmarking circuits were
designed – the Hadamard gate benchmark and the SWAP gate benchmark. Their
structure is simple, consisting of $k$ gates applied sequentially to the same
target qubits. Despite lack of practical use, they give insight into
properties of statevector simulations. Importantly, a Hadamard benchmark on
the last qubit of the system should be the worst-case simulation scenario,
since all gates in the circuit are guaranteed to be distributed (provided the
simulation spans multiple nodes).

###  2.4. Energy Measurements and Profiling

The energy consumption of statevector simulations can be retrieved by querying
SLURM on ARCHER2, which uses power counters on the nodes to determine energy
usage. However, this is missing the energy used by the network, which we
estimated with the following formula:
$E_{net}=n_{s}\cdot\bar{P}_{s}\cdot\Delta t$. The value $n_{s}$ represents the
number of switches in the utilised network – 1 switch per 8 nodes on ARCHER2.
The typical average power of a switch under load on ARCHER2 $\bar{P}_{s}$ is
equal to 235 W. Finally, $\Delta t$ is the total runtime of the circuit. The
estimated switch energy and the energy extracted from SLURM are added together
to calculate the total energy consumed by the jobs being studied. We have
omitted other sources of energy consumption during the job, as we do not have
values for other rack level overheads nor do we include energy consumed in
cooling the system.

##  3\. Results

We ran a QFT circuit at register sizes from 33 to 44 qubits, using the minimum
possible number of nodes to fit the statevector, as well as the Hadamard and
SWAP circuits to calculate the cost of distributed gates444Resources used are
available at https://github.com/jjacobx/arb23..

###  3.1. Clock Frequency and Node Memory

Figure 2. Runtimes of the QFT circuit simulations with different register
size. Standard nodes have 256 GB, highmem nodes have 512 GB.

To benchmark the most efficient combination of the CPU frequency and available
memory, we ran the QFT circuit. Results are shown in fig. 2. Additional
buffers are required in the MPI implementation, doubling the overall memory
requirement. As a result, 33 qubits will fit on a standard node, but 4 nodes
are required for a 34 qubit simulation. The 33 qubit standard node results,
and slower of the two 34 qubit high memory node results are single node runs.

QFT runtimes scale linearly, due to the number of distributed gates rising
linearly. The actual number of gates grows quadratically. High memory nodes
are slower, but less than twice as slow as the standard nodes. Higher memory
means twice as much data in the local memory needs to be recomputed at each
gate application. A maximum of 41 qubits could be simulated on 256 high memory
nodes, and 44 qubits on 4,096 standard nodes.

Figure 3. Comparison of the default medium frequency, standard nodes to other
setups.

Since the standard node medium frequency setup is currently the default on
ARCHER2, we plotted its fractional comparison to other setups on fig. 3, in
terms of runtime and energy consumption. By interpreting both plots together,
it is possible to assess which configuration is most optimal. The standard
high frequency setup is consistently 5% to 10% faster than the default, but it
uses around 25% more energy, up to 43 qubits, where the consumption
significantly decreases. Therefore, we conclude that the defaults are
appropriate for most simulations.

The use of high memory nodes drastically increases the runtime, however the CU
cost of high memory simulations is lower than for standard memory. High
frequency on high memory nodes required from 20% to over 40% more energy. We
found that the lowest frequency available on ARCHER2 (1.5 GHz) was not of
benefit in either case due to a large increase in runtime, and so these runs
are omitted from our figures.

###  3.2. Cache Blocking

The cache blocking approach was described in section 2.2. In addition to the
QFT, we ran the two other benchmarks from section 2.3, with 50 gates in each
circuit. During the investigation, we noted that QuEST uses a series of
blocking communications. We rewrote the message passing function to use non-
blocking communication, which allows multiple messages to be sent and received
in parallel when using an interconnect with high bandwidth. Each of our
experiments here includes results from both the default QuEST implementation
and our modified version.

Qubit Index | Blocking | Non-blocking
---|---|---
Time | Energy | Time | Energy
29 | 0.51 s | 15.3 kJ | 0.53 s | 15.0 kJ
30 | 0.59 s | 15.7 kJ | 0.74 s | 18.7 kJ
31 | 0.80 s | 20.8 kJ | 0.97 s | 24.2 kJ
32 | 9.63 s | 191 kJ | 8.82 s | 179 kJ
Table 1. Time/energy per gate in the Hadamard benchmark on qubits 29–32 using
blocking/non-blocking MPI.

Fifty Hadamard gates were applied to a specific qubit, from 0 to 37, on 64
nodes and per-gate values calculated. Table 1 presents the results on qubits
29–32. Up until qubit 29 the time per gate is roughly constant at 0.5 s, and
the energy is approximately 15 kJ. At qubits 30 and 31 both values slightly
increase, towards 1.0 s and 25 kJ due to data dependencies spreading to
multiple NUMA regions. At qubit 32 and above, the runtime drastically rises to
almost 10 s per gate for blocking communication, and 9 s for our non-blocking
version, similarly, the energy shoots up to 190 kJ and 180 kJ respectively.
The twenty-fold increase in runtime is caused by MPI, which now needs to
communicate all the local elements of the statevector to another process. It
is clear that non-blocking messages mitigate some of the communication costs.

Figure 4. Energy consumption of the SWAP benchmark.

Next, a similar benchmark with 50 SWAP gates was run. The SWAP gates require
two targets, and as long as one is in the distributed regime, the operation
entails communication. Since it is expensive to try all possible combinations
of targets, we instead selected 5 local targets $[0,4,8,12,16]$, and 3
distributed targets $[35,36,36]$. The energy results are shown on fig. 4.
Again, the non-blocking communication visibly improved the performance – with
blocking communication the time per gate ranges from 9.0 s to 9.75 s and the
energy consumption is from 180 kJ to 195 kJ; meanwhile, our non-blocking
implementation requires 8.25 s to 9.0 s per gate and 160 kJ to 180 kJ.

Figure 5. Profiles of the Hadamard and QFT benchmarks.

Lastly, we profiled the different QFT implementations and compared them to the
worst-case communication scenario (last qubit Hadamard benchmark). The built-
in QFT in QuEST implements the circuit shown in fig. 1(a), but the controlled
phase gates are applied more efficiently. The cache blocking circuit is as
fig. 1(b), but the swaps are done after the 30th Hadamard gate to prevent any
increase in gate execution time, and the controlled phase gates used the
optimised QuEST implementation.

The profiles of each run are presented on fig. 5. In the Hadamard benchmark
MPI completely dominates the runtime. The QFT gates are mostly local, so
communication only takes up to 43% of runtime, and the rest is split roughly
2:1 between memory access and computation. By applying our optimisation, we
managed to reduce communication to 25%.

###  3.3. Best QFT Performance

Our final experiments were runs designed to use a significant share of ARCHER2
(which has 5,860 nodes), with and without optimisations. We tested the QFT on
43 and 44 qubits, using 2,048 and 4,096 nodes respectively. The ‘Fast’ version
uses cache-blocking to move all the Hadamard gates out of the distributed
regime, and implements non-blocking communication for the SWAP gates. Results
are shown in table 2.

Experiment | Built-in | Fast | Built-in | Fast
---|---|---|---|---
Qubits | 43 | 43 | 44 | 44
Nodes | 2048 | 2048 | 4096 | 4096
Runtime | 417 s | 270 s | 476 s | 285 s
Energy | 294 MJ | 206 MJ | 664 MJ | 431 MJ
Table 2. Runtime and energy consumption of large QFT runs on ARCHER2. ‘Built-
in’ is using the standard QuEST QFT, ‘Fast’ is our modified version.

We achieved 35% and 40% improvements in runtime, along with 30% and 35%
reductions in energy for the 2,048-node and 4,096-node runs respectively. The
biggest energy improvement was 233 MJ, which is around 65 kWh saved in a
little more than 3 minutes.

##  4\. Conclusions and Future Work

We explored multiple ways to mitigate the energy consumption on ARCHER2 with
QuEST framework. First, we highlighted the importance of using moderate CPU
frequencies, which reduces the energy consumption with only a small runtime
penalty. We note that the benefits end at 2.00 GHz – any further decrease
worsens the runtime while keeping the energy usage fixed. Second, we
investigated whether high memory nodes are beneficial. Results were mixed,
although high memory nodes are more efficient for the CU budget, the energy
consumption is sometimes slightly higher and other times slightly lower than
for the standard nodes. In particular, due to memory bandwidth being a
limiting factor, we do not recommend specifying high-memory nodes over more
balanced nodes if selecting hardware for this application. Last, we explored
transpiling the simulated circuit to be cache-blocking, which can reduce the
number of distributed operations. The QFT is a perfect circuit for cache
blocking, as SWAP gates are already a part of it. We also found that
communication in QuEST could be improved on high-end networks using non-
blocking communication. Applying all these optimisations, we managed to
simulate 44 qubit QFT 40% faster, saving 35% energy. This work provides energy
benchmarks both for both classical simulation codes and real quantum hardware
to consider.

In future work we will further explore cache-blocking. If SWAP gates are the
only distributed operations, communication could potentially be halved, as
swapping only modifies half of the statevector. With this improvement, ARCHER2
could possibly simulate up to 45 qubits. It would also be useful to implement
a cache-blocking transpiler, for example as an LLVM optimisation pass using
the newly developed QIR (Lubinski et al., 2022). We believe it would be
beneficial to reimplement QuEST’s core data-structures using a complex data
type rather than separate real and imaginary arrays, in order to improve data
locality. Finally, we will explore the impact on performance and energy usage
of porting QuEST to multiple GPUs.

###### Acknowledgements.

This work used the ARCHER2 UK National Supercomputing Service
(https://www.archer2.ac.uk).

## References

  * (1)
  * Aaronson and Chen (2017) Scott Aaronson and Lijie Chen. 2017.  Complexity-Theoretic Foundations of Quantum Supremacy Experiments. In _Proceedings of the 32nd Computational Complexity Conference_ (Riga, Latvia) _(CCC ’17)_. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, DEU, Article 22, 67 pages.
  * Arute et al. (2019) Frank Arute et al. 2019\.  Quantum supremacy using a programmable superconducting processor.  _Nature_ 574, 7779 (01 Oct 2019), 505–510.  https://doi.org/10.1038/s41586-019-1666-5
  * Doi and Horii (2020) Jun Doi and Hiroshi Horii. 2020.  Cache Blocking Technique to Large Scale Quantum Computing Simulation on Supercomputers. In _2020 IEEE International Conference on Quantum Computing and Engineering (QCE)_. Institute of Electrical and Electronics Engineers Inc., Denver, CO, USA, 212–222.  https://doi.org/10.1109/QCE49297.2020.00035
  * Faj et al. (2023) Jennifer Faj, Ivy Peng, Jacob Wahlgren, and Stefano Markidis. 2023\.  Quantum Computer Simulations at Warp Speed: Assessing the Impact of GPU Acceleration.  arXiv:2307.14860 [cs.PF]
  * Jones et al. (2019) Tyson Jones, Anna Brown, Ian Bush, and Simon C. Benjamin. 2019\.  QuEST and High Performance Simulation of Quantum Computers.  _Scientific Reports_ 9 (12 2019), 10736.  Issue 1. https://doi.org/10.1038/s41598-019-47174-9
  * Lubinski et al. (2022) Thomas Lubinski, Cassandra Granade, Amos Anderson, Alan Geller, Martin Roetteler, Andrei Petrenko, and Bettina Heim. 2022.  Advancing hybrid quantum–classical computation with real-time execution.  _Frontiers in Physics_ 10 (2022).  https://doi.org/10.3389/fphy.2022.940293
  * Pan and Zhang (2022) Feng Pan and Pan Zhang. 2022.  Simulation of Quantum Circuits Using the Big-Batch Tensor Network Method.  _Physical Review Letters_ 128 (1 2022), 030501\.  Issue 3. https://doi.org/10.1103/PhysRevLett.128.030501


# Ruling out real-valued standard formalism of quantum theory

Ming-Cheng Chen1,2,∗, Can Wang1,2,∗, Feng-Ming Liu1,2,∗, Jian-Wen Wang1,2,
Chong Ying1,2, Zhong-Xia Shang1,2, Yu-Lin Wu1,2, Ming Gong1,2, Hui Deng1,2,
Fu-Tian Liang1,2, Qiang Zhang1,2, Cheng-Zhi Peng1,2, Xiao-Bo Zhu1,2, Adan
Cabello3,4, Chao-Yang Lu1,2,†, Jian-Wei Pan1,2 1 Hefei National Laboratory for
Physical Sciences at Microscale and Department of Modern Physics, University
of Science and Technology of China, Hefei, Anhui 230026, China  2 CAS Centre
for Excellence and Synergetic Innovation Centre in Quantum Information and
Quantum Physics, University of Science and Technology of China, Shanghai
201315, China  3 Departamento de Física Aplicada II, Universidad de Sevilla,
E-41012 Sevilla, Spain  4 Instituto Carlos Ide Fisica Teoricay Computacional,
Universidad de Sevilla, Spain

(September 2, 2024)

###### Abstract

Standard quantum theory was formulated with complex-valued Schrödinger
equations, wave functions, operators, and Hilbert spaces. Previous work
attempted to simulate quantum systems using only real numbers by exploiting an
enlarged Hilbert space. A fundamental question arises: are the complex numbers
really necessary in the standard formalism of quantum theory? To answer this
question, a quantum game has been developed to distinguish standard quantum
theory from its real-number analogue by revealing a contradiction in the
maximum game scores between a high-fidelity multi-qubit quantum experiment and
players using only real-number quantum theory. Here, using superconducting
qubits, we faithfully experimentally implement the quantum game based on
entanglement swapping with a state-of-the-art fidelity of 0.952(1), which
beats the real-number bound of 7.66 by 43 standard deviations. Our results
disprove the real-number formulation and establish the indispensable role of
complex numbers in the standard quantum theory.

Figure 1: A non-local game to disprove real-number model of quantum mechanics.
(a) A three-party Bell-CHSH-like game based on entanglement swapping. Two EPR
pairs are distributed between Alice and Bob, and between Bob and Charlie. The
measurement settings are labelled as $x$, $y$, and $z$, and the outcomes are
$a$, $b$, and $c$, respectively. Bob performs a complete Bell-state
measurement. Alice and Charlies perform single-qubit local measurements. (b)
The score of the non-local game divides the physics into three regimes:
classical, real-number quantum mechanics, and complex quantum mechanics, which
are experimental testable. The score $\Gamma$ is calculated from the weighted
sum of the conditional joint probability distribution.

Physicists use mathematics to describe nature. In classical physics, the real
number appears complete to describe the physical reality in all classical
phenomenon, whereas the complex number is only sometimes employed as a
convenient mathematical tool. In quantum mechanics, the complex number was
introduced as the first principle in Schrödinger’s equation and Heisenberg’s
commutation relation Schrödinger (1926); Dirac (1981). The complex-valued wave
function has been shown to represent the physical reality of quantum objects
under certain physically plausible assumptions Pusey  _et al._ (2012).
Experimentally, the real and imaginary parts of the wave function have been
directly measured Lundeen  _et al._ (2011). Today, quantum mechanics with
complex-valued wave functions seems the most successful theory to describe
nature.

On the other hand, starting with von Neumann in 1936, many works Birkhoff and
Von Neumann (1936); Stueckelberg (1959, 1960); Guenin and Stueckelberg (1961);
Soler (1995); Pál and Vértesi (2008); McKague  _et al._ (2009); Aleksandrova
_et al._ (2013); Dyson (1962) have shown possible to universally simulate
quantum systems using only real numbers by exploiting an enlarged Hilbert
space in various alternative formalisms of quantum theory. For example, by
adding an extra qubit $\left|\pm i\right\rangle=(\left|0\right\rangle\pm
i\left|1\right\rangle)/\sqrt{2}$, a single-quantum system with a complex
density matrix $\rho$ and Hermitian operator $H$ can be simulated through
$tr(\rho H)=tr(\tilde{\rho}\tilde{H})$, where $\tilde{\rho}$ and $\tilde{H}$
are real and of the form:

$\displaystyle\tilde{\rho}=(\rho\otimes\left|+i\right\rangle\left\langle+i\right|+{{\rho}^{*}}\otimes\left|-i\right\rangle\left\langle-i\right|)/2\;,$
$\displaystyle\tilde{H}=H\otimes\left|+i\right\rangle\left\langle+i\right|+{{H}^{*}}\otimes\left|-i\right\rangle\left\langle-i\right|\;.$

Therefore, it is interesting to ask a fundamental question why the complex
number is necessary in the standard formalism of quantum theory. The standard
quantum theory is established by the following four axioms Nielsen and Chuang
(2002):

  * (1)

A pure quantum system is described by a unit complex vector in Hilbert space.

  * (2)

The state space of a composite quantum system is the tensor product of the
state spaces of the component systems.

  * (3)

The dynamics of a closed quantum system is described by a unitary operator
acting on the state vector.

  * (4)

A physical observable is described by a Hermitian operator and the measurement
outcome obeys the Born rule.

In this work, we intend to investigate the real-number formalism of standard
quantum theory, which satisfies the formalism in the above four axioms but
replaces the complex vectors and operators in the Hilbert space by
corresponding real vectors and operators, respectively. In this formalism, the
dimension of real Hilbert space is not restricted to be the same as the
complex Hilbert space. A distinguishing feature of the standard quantum theory
from other quantum theories is at the second axiom, where the Hilbert space of
composite quantum systems has a tensor-product structure.

Recently, Renou et al. developed an elegant scheme to provide an observable
effect in quantum experiments to distinguish between the two formalisms Renou
_et al._ (2021). The scheme is a Bell-like Bell (1964); Clauser  _et al._
(1969); Gisin (2009); Acín  _et al._ (2016); Bowles  _et al._ (2018) three-
party game based on deterministic entanglement swapping Zukowski  _et al._
(1993). The new theory predicts that the players obeying real-number formalism
of standard quantum theory cannot obtain the maximal score that the standard
complex-valued quantum theory allows, thus being falsified. An assumption used
in the proposal Renou  _et al._ (2021) is that the composite quantum state
produced by two independent sources is the tensor product of the two
independent quantum states, which has been ensured by the second axiom of
standard quantum theory. Very recently, it is shown that the second axiom can
be deduced from the first and fourth axioms, and is not independent Carcassi
_et al._ (2021). Specially, the tensor product structure of composite Hilbert
space can be induced by experimentally accessible observables Zanardi  _et
al._ (2004).

Figure 1a shows an illustration of the three-party quantum game for Alice,
Bob, and Charlie. First, two pairs of Einstein-Podolsky-Rosen (EPR) entangled
qubits Einstein  _et al._ (1935) are distributed between Alice and Bob, and
between Bob and Charlie, respectively. Bob then performs a joint Bell-state
measurement (BSM) on his two received qubits, which randomly projects them
into one of the four Bell states:

$\displaystyle\left|{{\phi}^{+}}\right\rangle\text{=(}\left|0\right\rangle\left|0\right\rangle+\left|1\right\rangle\left|1\right\rangle)/\sqrt{2},$
$\displaystyle\left|{{\psi}^{+}}\right\rangle\text{=(}\left|0\right\rangle\left|1\right\rangle+\left|1\right\rangle\left|0\right\rangle)/\sqrt{2},$
$\displaystyle\left|{{\phi}^{-}}\right\rangle\text{=(}\left|0\right\rangle\left|0\right\rangle-\left|1\right\rangle\left|1\right\rangle)/\sqrt{2},$
$\displaystyle\left|{{\psi}^{-}}\right\rangle\text{=(}\left|0\right\rangle\left|1\right\rangle-\left|1\right\rangle\left|0\right\rangle)/\sqrt{2}.$

The four results are correspondingly registered as $b\in\\{00,01,10,11\\}$.
Alice performs a single-qubit local measurement on her received qubit in the
eigenstate bases of an operator ${{A}_{x}}$ ($x\in\\{1,2,3\\}$) which yields
an outcome $a\in\\{0,1\\}$. Similarly, Charlie measures his qubit using
operator ${{C}_{z}}$ ($z\in\\{1,2,3,4,5,6\\}$) and obtain his outcome
$c\in\\{0,1\\}$. The score $\Gamma$ of the game is defined as the weighted sum
of the conditional joint probability distribution $P(abc|xz)$, given by

$\displaystyle\Gamma=\sum\limits_{abc,xz}{{{w}_{abc,xz}}P(abc|xz)},$

where ${{w}_{abc,xz}}\in\\{-1,+1\\}$ are the weights sup ,
$abc\in{{\\{0,1\\}}^{\otimes 4}}$ are the bit strings of measurement results,
and $xz\in\\{11,12,21,22,13,14,33,34,25,26,35,36\\}$ are 12 combinations of
local single-qubit measurement settings $x$ and $z$.

In the standard complex-valued quantum theory, we set Alice’s operator as
${{A}_{x}}\in\\{Z,X,Y\\}$, where $Z$, $X$, $Y$ are the standard Pauli
matrices, and Charlie’s operator as ${{C}_{z}}\in\\{Z\pm X,Z\pm Y,X\pm
Y\\}/\sqrt{2}$, where the score of the game reaches its maximum of $6\sqrt{2}$
($\approx$8.49). However, if one assumes the players can only use real-number
quantum resources (real-number states and real-number operations), the
numerically found optimal score Renou  _et al._ (2021) has an upper bound of
7.66, which sits between the classical limit of 6 and the quantum limit of
$6\sqrt{2}$, as shown in Fig. 1b. This contradiction opens a way to a direct
experimental test to distinguish between the complex-number and real-number
representations of standard quantum theory.

Figure 2: Experimental implementation. (a) The quantum circuit used to perform
the quantum game. The EPR pairs and BSM are realized by a two-qubit iSWAP
operation with additional single-qubit gates. (b) Optical image of the
superconducting quantum processor. The qubits (Q1-Q4) are placed in a linear
array and have direct nearest-neighbour couplings. Each qubit has a XY driving
and a Z tunning line and has an individual readout resonator (R1-R4) for
measurement. (c) The experimental control pulses. Single qubit is rotated by
Rabi resonance and two qubits are entangled by tunning the qubits into
resonant spin exchange. Two EPR pulse sequences are used to prepare the two
pairs of EPR entangled states. And the BSM pulse sequence is used to implement
the joint Bell-state measurement. (d) The magnitude of density matrix of the
product state of the two EPR pairs after the EPR pulses. The state fidelity is
97.5%. (e) The magnitude of density matrix of the four-qubit entangled state
after the BSM pulses. The state fidelity is 94.6%. (f) The entangled states
generated between Alice and Charlie conditional on the BSM outcomes. All are
above 92.7% threshold fidelity, and the average is 95.2%. Figure 3:
Experimental results. (a) The conditional joint probability distribution
matrices $P(abc|xz)$ from the quantum game (left) and the theoretical
prediction from an ideal complex-number quantum theory (right). The row index
represents the input measurement setting $\\{xz\\}$ and the column index is
the output measured strings $\\{abc\\}$. (b) The obtained game score of the
quantum experiment is 8.09(1), which is calculated from the experimentally
measured conditional joint probability distribution matrices and is 43
standard deviations above the upper bound of the score (7.66) from ideal real-
number quantum theory. The error bar on the experimental score presents one
standard deviation. The score ($6\sqrt{2}$) from ideal complex-number quantum
theory and score (6) from ideal classical hidden-variable theory are also
shown.

A generic quantum circuit for the experimental test is shown in Fig. 2a which
involves three deterministic entangling gates for preparing two maximum
entangled EPR pairs (1-2 and 3-4) and implementing the BSM between qubit 2 and
3. Very high quantum state and gate fidelities are required to surpass the
real-number players Renou  _et al._ (2021). We design and fabricate a
superconducting quantum processor (see Fig. 2b for its optical image) to
implement the quantum game. To keep Alice’s and Charlie’s qubits (1 and 4)
isolated from each other, we use I-shape transmon qubit design Barends  _et
al._ (2013) to increase the spacing of the qubits for reducing the non-
neighbor coupling and with large frequency detuning, the maximum population
exchange is smaller than ${{10}^{-9}}$ sup . The qubits are arranged in a
linear array Barends  _et al._ (2014) and each has individual control and
readout Wallraff  _et al._ (2004); Jeffrey  _et al._ (2014). The qubits work
at the transition frequency ${f}_{01}\\!\sim\\!5\text{ GHz}$ and are
capacitively coupled to their nearest neighbors with $g/2\pi\\!\sim\\!5\text{
MHz}$.

Single qubit is controlled by microwave pulses on the Rabi driving (XY) line
and fast flux-bias current on the frequency tuning (Z) line. Each qubit is
dispersively coupled to a readout resonator (R1-R4) and is readout through a
single coplanar waveguide. At the idle frequency, the qubits’ average lifetime
${{T}_{1}}$ is measured to be 34.8 $\upmu$s and the average coherence time
$T_{2}^{*}$ is 8.0 $\upmu$s. The qubits are initialized by idling 200 $\upmu$s
to decay into the ground states. The average fidelity of single-qubit gates
using 23 ns driving pulses is measured to be 99.88%. The average error in the
readout of the 16 computational bases after correcting the local bit-flip
error is 0.34%.

To implement the quantum circuit in Fig. 2(a), we design the control pulse
sequences as shown in Fig. 2(c). The entangling interactions are in the form
of iSWAP gates where the qubits fully exchange their populations as
$\left|01\right\rangle\to i\left|10\right\rangle,\left|10\right\rangle\to
i\left|01\right\rangle$ in $\sim$50 ns by tuning two nearest-neighbor qubits
into resonance Barends  _et al._ (2019); Sung  _et al._ (2021). The quantum
process fidelity of the iSWAP gate is measured to be 96.7% with state
preparation and measurement (SPAM) errors.

To characterize our experimental process, we make tomographic measurements of
the quantum entangled states created after each step. First, after the first
two EPR pulses (see Fig. 2c, at the point of $\sim$120 ns), we measure and
reconstruct the density matrix of the product state of the two EPR pairs as
shown in Fig. 2d. The experimental data agree well with the ideal case with
fidelity of 0.975(1). Next, after the third entangling pulse (at the point of
$\sim$230 ns in Fig. 2c), the four qubits become a fully entangled state. The
measured density matrix in Fig. 2e shows a fidelity of 0.946(1) compared to
the perfect state. Finally, projective measurements on the qubit 2 and 3 are
performed, which swap the entanglement onto the independent and non-
interacting qubit 1 and 4. Conditioned on random outcomes of the BSM, the
qubits 1 and 4 are projected into one of the four Bell states correspondingly,
whose quantum state fidelities are measured and plotted in Fig. 2e. The
obtained average fidelity is 0.952(1), well above the threshold of Renou  _et
al._ (2021) $\sim$0.927.

Having verified the high quantum operation and state fidelities, we proceed to
test the quantum game and measure the conditional joint probability
distributions $P(abc|xz)$. Alice and Charlie’s qubits are first unitarily
transformed using appropriate single-qubit gates sup  and then measured in the
computational bases. There are 12 different combinations of measurement
settings and 16 possible measured bit strings. The main experimental results
are plotted as a $12\times 16$ probability distribution matrix in Fig. 3(a)
together with the ideal values. Summing over the obtained probability
$P(abc|xz)$ with their corresponding weight sup , our quantum experiment gives
a score of 8.09(1). As shown in Fig. 4b, the result violates the upper bound
set by real-number quantum theory by 43 standard deviations, which provides
strong evidence to disprove the real-valued standard formalism of quantum
theory. Our implementation uses deterministic and high-fidelity quantum logic
gates Riebe  _et al._ (2008); Ning  _et al._ (2019) and single-shot
measurement with unity detection efficiency.

∗M. -C. Chen, C. Wang, and F. -M. Liu contributed equally to this work.

<EMAIL_ADDRESS>
## References

  * Schrödinger (1926) E. Schrödinger, Physical review 28, 1049 (1926).
  * Dirac (1981) P. A. M. Dirac,  _The principles of quantum mechanics_ , 27 (Oxford university press, 1981).
  * Pusey  _et al._ (2012) M. F. Pusey, J. Barrett, and T. Rudolph, Nature Physics 8, 475 (2012).
  * Lundeen  _et al._ (2011) J. S. Lundeen, B. Sutherland, A. Patel, C. Stewart, and C. Bamber, Nature 474, 188 (2011).
  * Birkhoff and Von Neumann (1936) G. Birkhoff and J. Von Neumann, Annals of mathematics , 823 (1936).
  * Stueckelberg (1959) E. C. Stueckelberg,  _Field quantization and time reversal in real Hilbert space_ , Tech. Rep. (European Organization for Nuclear Research, Geneva, 1959).
  * Stueckelberg (1960) E. C. Stueckelberg, Helv. Phys. Acta 33, 458 (1960).
  * Guenin and Stueckelberg (1961) M. Guenin and E. Stueckelberg, Helv. Phys. Acta 34, 621 (1961).
  * Soler (1995) M. P. Soler, Communications in Algebra 23, 219 (1995).
  * Pál and Vértesi (2008) K. F. Pál and T. Vértesi, Physical Review A 77, 042105 (2008).
  * McKague  _et al._ (2009) M. McKague, M. Mosca, and N. Gisin, Physical review letters 102, 020505 (2009).
  * Aleksandrova  _et al._ (2013) A. Aleksandrova, V. Borish, and W. K. Wootters, Physical Review A 87, 052106 (2013).
  * Dyson (1962) F. J. Dyson, Journal of Mathematical Physics 3, 1199 (1962).
  * Nielsen and Chuang (2002) M. A. Nielsen and I. Chuang, “Quantum computation and quantum information,” (2002).
  * Renou  _et al._ (2021) M.-O. Renou, D. Trillo, M. Weilenmann, L. P. Thinh, A. Tavakoli, N. Gisin, A. Acin, and M. Navascues, arXiv preprint arXiv:2101.10873 (2021).
  * Bell (1964) J. S. Bell, Physics Physique Fizika 1, 195 (1964).
  * Clauser  _et al._ (1969) J. F. Clauser, M. A. Horne, A. Shimony, and R. A. Holt, Physical review letters 23, 880 (1969).
  * Gisin (2009) N. Gisin, in  _Quantum Reality, relativistic causality, and closing the epistemic circle_ (Springer, 2009) pp. 125–138.
  * Acín  _et al._ (2016) A. Acín, S. Pironio, T. Vértesi, and P. Wittek, Physical Review A 93, 040102 (2016).
  * Bowles  _et al._ (2018) J. Bowles, I. Šupić, D. Cavalcanti, and A. Acín, Physical Review A 98, 042336 (2018).
  * Zukowski  _et al._ (1993) M. Zukowski, A. Zeilinger, M. A. Horne, and A. K. Ekert, Physical Review Letters 71 (1993).
  * Carcassi  _et al._ (2021) G. Carcassi, L. Maccone, and C. A. Aidala, Physical Review Letters 126, 110402 (2021).
  * Zanardi  _et al._ (2004) P. Zanardi, D. A. Lidar, and S. Lloyd, Physical review letters 92, 060402 (2004).
  * Einstein  _et al._ (1935) A. Einstein, B. Podolsky, and N. Rosen, Physical review 47, 777 (1935).
  * (25) See Supplemental Material for the operation of quantum game, the device information and the quantum control of the device.
  * Barends  _et al._ (2013) R. Barends, J. Kelly, A. Megrant, D. Sank, E. Jeffrey, Y. Chen, Y. Yin, B. Chiaro, J. Mutus, C. Neill, _et al._ , Physical review letters 111, 080502 (2013).
  * Barends  _et al._ (2014) R. Barends, J. Kelly, A. Megrant, A. Veitia, D. Sank, E. Jeffrey, T. C. White, J. Mutus, A. G. Fowler, B. Campbell, _et al._ , Nature 508, 500 (2014).
  * Wallraff  _et al._ (2004) A. Wallraff, D. I. Schuster, A. Blais, L. Frunzio, R.-S. Huang, J. Majer, S. Kumar, S. M. Girvin, and R. J. Schoelkopf, Nature 431, 162 (2004).
  * Jeffrey  _et al._ (2014) E. Jeffrey, D. Sank, J. Mutus, T. White, J. Kelly, R. Barends, Y. Chen, Z. Chen, B. Chiaro, A. Dunsworth, _et al._ , Physical review letters 112, 190504 (2014).
  * Barends  _et al._ (2019) R. Barends, C. Quintana, A. Petukhov, Y. Chen, D. Kafri, K. Kechedzhi, R. Collins, O. Naaman, S. Boixo, F. Arute, _et al._ , Physical review letters 123, 210501 (2019).
  * Sung  _et al._ (2021) Y. Sung, L. Ding, J. Braumüller, A. Vepsäläinen, B. Kannan, M. Kjaergaard, A. Greene, G. O. Samach, C. McNally, D. Kim, _et al._ , Physical Review X 11, 021058 (2021).
  * Riebe  _et al._ (2008) M. Riebe, T. Monz, K. Kim, A. Villar, P. Schindler, M. Chwalla, M. Hennrich, and R. Blatt, Nature Physics 4, 839 (2008).
  * Ning  _et al._ (2019) W. Ning, X.-J. Huang, P.-R. Han, H. Li, H. Deng, Z.-B. Yang, Z.-R. Zhong, Y. Xia, K. Xu, D. Zheng, _et al._ , Physical review letters 123, 060502 (2019).