Authors: Ben Jones, Kelvin Fichter

And a very special thank you to vi, Li Xuanji, David Knott, Eva Beylin, Vitalik Buterin, and Kasima Tharnpipitchai for invaluable contributions to putting this together.

## TL;DR

We propose an alternative to confirmation signatures and (semi) formalize the properties of any valid Plasma MVP exit game. Our game provides significantly improved UX at the cost of a two-period challenge-response scheme in the worst case.

## Background

### Exit Priority

The original Plasma MVP specification requires that exits be processed in priority order. Each exit references an unspent transaction output, and priority is determined by the age of the transaction output. This is generally necessary so that valid exits can be processed before exits stemming from invalid â€śout of nowhereâ€ť transactions. More information about exit priority can be found at the OmiseGO research repository here.

This post introduces a new way to calculate exit priority, which we call â€śyoungest-inputâ€ť priority. Instead of ordering exits by the age of the *output*, we now order exits by the age of the *youngest input*. This has the effect that exits of outputs, even if theyâ€™re included in withheld blocks after â€śout of nowhereâ€ť transactions, will be correctly processed as long as they only stem from valid inputs.

### Exit Game

Plasma MVP also introduces an exit game, whereby some outputs are deemed â€śexitableâ€ť. This game correctly incentivizes parties to challenge a â€śnon-exitableâ€ť output. For example, spent outputs are considered â€śnon-exitable.â€ť The game requires the exitor to place a bond, such that anyone who knows the output to be spent is sufficiently incentivized to reveal the transaction and take the bond.

The basic exit game has one challenge condition - outputs must not be spent. This condition is enough to make the exit game complete because of a construction of confirmation signatures. Basically, both parties to a transaction must â€śsign offâ€ť on a transactionâ€™s inclusion in the chain. Honest clients wonâ€™t sign off on withheld (and therefore possibly invalid) transactions, so honest clients wonâ€™t accept funds that might be stolen by the operator (discussed more below).

### In-flight Transactions

Without confirmation signatures, the above exit game is exploitable by the operator in two ways:

- The operator may include, but withhold, a transaction, and later grief the sender(s) by challenging exits from the transactionâ€™s inputs.
- More importantly, the operator may include a transaction after some invalid â€śout of nowhereâ€ť transaction that creates money for the operator. Standard exit priority dictates that the operatorâ€™s outputs will be processed before the valid outputs, thereby stealing money.

Our new exit game solves these problems without confirmation signatures.

## Youngest-Input Priority

This proposal replaces output-age priority with something we call â€śyoungest-inputâ€ť priority. Basically, the exit priority of an output is now the age of its youngest input. We claim that this construction is safe (honest clients cannot have money stolen) as long as clients donâ€™t spend any outputs included after any invalid or witheld transaction.

We show that if there exists an â€śout of nowhereâ€ť input, then any transactions stemming from that input would have an even higher queue number than the â€śout of nowhereâ€ť itself. Therefore, valid outputs will be processed first.

### Safety Proof

We begin with definitions to be used throughout this post.

TX is the transaction space, of the form (`inputs`

, `outputs`

), where `inputs`

and `outputs`

are sets of integers representing position in the Plasma chain:

For all t \in TX, we define the â€śinputsâ€ť function I(t)=(I_{1}, I_{2}, \ldots, I_{n}) and the â€śoutputsâ€ť function O(t)=(O_{1}, O_{2}, \ldots, O_{n}).

Transactions have older inputs than outputs, more formally:

We also define the mapping T_{n} which maps a Plasma chainâ€™s first n transaction indices to its first n transactions.

As a shortcut,

We define the priority number (â€ślower exits firstâ€ť, â€ślower is betterâ€ť) of a transaction, p(t), as:

We say that a transaction t_{k} stems from a transaction t_{j} (an output from t_{j} eventually chains into an input of t_{k}) if the following holds:

A transaction t_{i} with n inputs is considered an â€śout of nowhereâ€ť transaction if any input â€śpoints to itselfâ€ť:

This is how deposits are structured, so itâ€™s like a deposit that never happened - creating money â€śout of nowhereâ€ť.

Let t_{v} be some transaction and t_{nw} be an out of nowhere transaction such that, from our previous definition:

and therefore by our definition of p(t):

So p(t_{v}) will exit before p(t_{nw}). We now need to show that for any t' that stems from t_{nw}, p(t_{v}) < p(t') as well. Because t' stems from t_{nw}, we know that:

If the first is true, then we can show p(t_{nw}) < p(t'):

Otherwise, thereâ€™s a chain of transactions from p_{nw} to p' for which the first is true, and therefore the inequality holds by transitivity.

So basically, anyone following the protocol can exit before anything that stems from an â€śout of nowhereâ€ť transaction.

## Required Exit Game Properties

Our exit game defines a set of â€śexitable outputsâ€ť given a transaction t. For example, spent outputs are not exitable in our rules. We formally define the properties that this game must satisfy. We call these properties â€śsafetyâ€ť and â€ślivenessâ€ť, because theyâ€™re largely analogous.

### Safety

The safety rule, in English, says â€śif an output was exitable at some time and is not spent in a later transaction, then it must still be exitableâ€ť. If we didnâ€™t have this condition, then it might be possible for a user to receive money but not be able to spend or exit from it later.

Formally, if we say that E(T_{n}) represents the set of exitable outputs for some Plasma chain and T_{n+1} is T_{n} plus some new transaction t_{n+1}:

### Liveness

The liveness rule basically says that â€śif an output was exitable at some time and *is* spent later, then immediately after that spend, either itâ€™s still exitable or all of the spendâ€™s outputs are exitable, but not bothâ€ť.

The second part probably makes sense - if something is spent, then all the resulting outputs should be exitable. The first case is special - if the spend is *invalid*, then the outputs should not be exitable and the input should still be exitable. So a short way to describe â€ślivenessâ€ť is that all â€ścanonicalâ€ť transactions should impact the set of exitable transactions.

We define â€ścanonicalâ€ť later.

Formally:

## Proof

### Exit Game Requirements

We need to formally show our exit game produces the exitable outputs E. To help us along the way, we make a few useful definitions.

#### Spends

We call two transactions â€ścompetingâ€ť if they contain any of the same inputs. The list of â€ścompetitorsâ€ť to a transaction is formally defined as follows:

Note that a transaction is a competitor to itself.

#### Canonical Transactions

We call a transaction â€ścanonicalâ€ť if itâ€™s the first included of any of its competitors.

We define a function that determines which of a set T of transactions came â€śfirstâ€ť:

Then we can define a function that takes a transaction and returns whether itâ€™s the â€ścanonicalâ€ť spend in its set of competitors.

Finally, we say that â€śrealityâ€ť is the set of canonical transactions for a given Plasma chain.

#### Unspent, Double Spent

We define two helper functions â€śunspentâ€ť and â€śdouble spentâ€ť. unspent takes a set of transactions and returns the list of outputs that havenâ€™t been spent. double\_spent takes a list of transactions and returns any outputs that have been used as inputs to more than one transaction.

First, we define a function txo that takes a transaction and returns a list of its inputs and outputs.

Next, we define a function TXO that lists all inputs and outputs for an entire set of transactions:

Now we can define unspent:

And finally, double\_spent:

#### Requirements

Combining all of these things, we define our function for exitable outputs given a set of transactions, E, as:

Basically, the set of exitable outputs are the outputs that are part of a canonical transaction, are unspent, and were not spent in two or more non-canonical transactions. This last part effectively punishes users for double spending.

### Satisfies Properties

This next section demonstrates that the function described above satisfies the desired properties of safety and liveness.

#### Safety

Our safety property says:

So to prove this for our E(T_{n}), letâ€™s take some o \in E(T_{n}). From our definition, o must be in unspent(reality(T_{n})), and must not be in double\_spent(T_{n}).

o \not\in I(t_{n+1}) means that o will still be in reality, because only a transaction spending o can impact its inclusion in reality. Also, o canâ€™t be spent (or double spent) if it wasnâ€™t used as an input. So our function is safe!

#### Liveness

Our liveness property states:

However, *we do have a case for which liveness does not hold* - namely that if the second transaction is a non-canonical double spend, then both the input and all of the outputs will not be exitable. This is a result of the \setminus double\_spent(T_{n}) clause. We think this is fine, because it means that only double spent inputs are at risk of being â€ślostâ€ť.

The updated property is therefore:

This is more annoying to prove, because we need to show each implication holds separately, but not together. Basically, given \forall o \in E(T_{n}), o \in I(t_{n+1}), we need:

and

and

Letâ€™s show the first. o \in I(t_{n+1}) means o was spent in t_{n+1}. However, o \in E(T_{n+1}) means that itâ€™s unspent in any canonical transaction. Therefore, t_{n+1} cannot be a canonical transaction. O(t_{n+1}) \cap E(T_{n+1}) is empty if t_{n+1} is not canonical, so weâ€™ve shown the half. Our specification states that o \in double\_spent(T_{n+1}) \implies o \not\in E(T_{n+1}), so we can show the second half by looking at the contrapositive of that statement o \in E(T_{n+1}) \implies o \not\in double\_spent(T_{n+1}).

Next, weâ€™ll show the second statement. O(t_{n+1}) \subseteq E(T_{n+1}) implies that t_{n+1} is canonical. If t_{n+1} is canonical, and o is an input to t_{n+1}, then o is no longer unspent, and therefore o \not\in E(T_{n+1}). If t is canonical then there cannot exist another earlier spend of the input, so o \not\in double\_spent(T_{n+1}).

Now the third statement. o \in double\_spent(T_{n+1}) means t is necessarily not canonical, so we have O(t_{n+1}) \cap E(T_{n+1}) = \varnothing. It also means that o \not\in E(T_{n+1}) because of our \setminus double\_spent(T_{n}) clause.

Finally, weâ€™ll show that at least one of these must be true. Letâ€™s do a proof by contradiction. Assume the following:

Weâ€™ve already shown that:

We can negate this statement to find:

However, we assumed that:

Therefore weâ€™ve shown the statement by contradiction.

Note that this means we should be careful to ensure that users donâ€™t double spend. Imagine the following scenario:

- Alice (UTXO1) and Bob (UTXO2) sign a transaction spending to Carol (TX1)
- Bob (UTXO2) signs a transaction spending to Dan (TX2). This transaction is included first.
- Alice (UTXO1) sees Bobâ€™s transaction and signs a separate transaction spending to Carol (TX3).
- The operator then includes TX1 and TX3. The chain is now byzantine and UTXO1 is also locked.

We can mitigate the above example by including timeouts on transactions. TX1 could have an n-block timeout, after which itâ€™s treated like a totally invalid transaction that canâ€™t be used to exit, challenge, or spend.

## In-flight Exit Game

We have to construct a game which, given a transaction, returns any exitable inputs or outputs.

### Construction

In the non-byzantine case, we can always use the standard exit game. However, in the event of invalid transactions or witheld blocks, we need to constuct a

â€śspecial exitâ€ť.

Our exit game involves two periods, triggered by a user who posts a bond alongside a transaction t. Note that *any user* (even someone who isnâ€™t a party to the transaction) can start the exit process, but the parties *must* piggyback onto the transaction separately if they want to join this exit. The first period consists of the following:

- Honest owners of inputs or outputs to t â€śpiggybackâ€ť on this exit and post a bond. Users who do not piggyback will not be able to exit.
- Any user may present any competitor to t.

Users who present a competitor (2.) must place a bond. Any other user may present an earlier competitor, claim the bond, and place a new bond. This construction ensures that the last presented competitor is also the earliest competitor.

If no competitors to t are brought to light, then the outputs can be challenged by an included spend. Any unchallenged outputs are exited. The bonds of all inputs and honest outputs are returned.

Otherwise, if competitors were presented, period 2 serves to determine whether t is canonical. Any user may present:

- t, included in the chain before all competitors presented in period 1.
- Spends of any â€śpiggybackedâ€ť inputs or outputs (except t itself).
- That some input was not created by a canonical transaction. This means revealing both the transaction that created the input, as well as some competitor to that transaction such that the competitor came first.

Challenges of type (2.) block any spent inputs or outputs to t from exiting. Challenges of type (3.) block any non-canonical inputs from exiting.

At the end of the game, only correctly exitable transactions will still be in the queue.

### Justification

This construction essentially allows any input or output to exit if it satisfies the following conditions:

- An earlier spend of one of its inputs does not exist.
- A spend of it does not exist.
- It has not been double spent (though note that if it has, the unspent outputs of the first canonical spend, if such a spend exists, are exitable separately).

(1.) is satisfied for t by the challenge-response game between periods 1 and 2, and for each of t's inputs by a type (3.) challenge in period 2.

Both (2.) and (3.) are satisfied by any type (2.) challenge in period 2.

In other words, the game determines if:

- canonical(t)
- o \in unspent(T_{n})
- o \not\in double\_spent(T_{n})

If all of these are true, then:

Otherwise, o \not\in E(T_{n}), which is the desired result.

## Notes

Hereâ€™s a picture that attempts to illustrate the exit game:

If someone spots a mistake that causes this whole construction to be hopelessly broken, please let us know!