Formal verification of More Viable Plasma

This is based on the specification document of OmiseGo team with my comments and a few modifications to render tex of scrapbox.

Formalization of Definitions

Transactions

$ TX is the transaction space, where each transaction has $ inputs and $ outputs. For simplicity, each input and output is an integer that represents the position of that input or output in the Plasma chain.

$ TX ((I_1, I_2, ..., I_n), (O_1, O_2, ..., O_m))

For every transaction $ t in $ TX we define the “inputs” and “outputs” functions:

$ I(t) = (I_1, I_2, ..., I_n)

$ O(t) = (O_1, O_2, ..., O_m)

Chain

A Plasma chain is composed of transactions. For each Plasma chain $ T, we define a mapping between each transaction position and the corresponding transaction at that position.

$ T_n: \lbrack1, n\rbrack \rightarrow TX

We also define a shortcut to point to a specific transaction in the chain.

$ t_i = T_n(i)

Competing Transaction, Competitors

Two transactions are competing if they have at least one input in common.

$ competing(t, t') = I(t) \cap I(t') \neg \varnothing

$ competing(t, t') = I(t) \cap I(t') \neq \varnothing

The set of competitors to a transaction is therefore every other transaction competing with the transaction in question.

$ competitors(t) = { t_{i} : i \in (0, n \rbrack, competing(t_{i}, t) }

Canonical Transaction

A transaction is called “canonical” if it’s oldest of all its competitors. We define a function $ first that determines which of a set $ T of transactions is the oldest transaction.

$ first(T) = t \in T : \forall t' \in T, t \neq t', \min(O(t)) < \min(O(t'))

The set of canonical transactions is any transaction which is the first of all its competitors.

$ canonical(t) = (first(competitors(t)) \stackrel{?}{=} t)

For convenience, we define $ reality as the set of all canonical transactions for a given chain.

$ reality(T_{n}) = { canonical(t_{i}) : i \in [1, n\rbrack }

Unspent, Double Spent

We define two helper functions $ unspent and $ double\_spent. $ unspent takes a set of transactions and returns the list of transaction 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.

$ txo(t) = O(t) \cup I(t)

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

$ TXO(T_{n}) = \bigcup_{i = 1}^{n} txo(t_{i})

Now we can define $ unspent and $ double\_spent:

$ unspent(T) = { o \in TXO(T) : \forall t \in T, o \notin I(t) }

$ double\_spent(T) = { o \in TXO(T) : \exists t,t' \in T, t \neq t', o \in I(t) \wedge o \in I(t') }

nrryuya.icon > $ unspent/$ double\_spentreturns the outputs that haven't spent / have spent more than once. $ competitors(t)returns the transactions that have at least one input in common.

Requirements

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}:

$ \forall o \in E(T_{n}) : o \notin I(t_{n+1}) \rightarrow o \in E(T_{n+1})

Liveness

The liveness rule states 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 ensures that 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.

$ \forall o \in E(T_{n}), o \in I(t_{n+1}) \rightarrow o \in E(T_{n+1}) \oplus O(t_{n+1}) \subseteq E(T_{n+1})

nrryuya.icon > This spec is modified later.

Basic Exit Protocol

Formalization

$ E(T_{n}) = unspent(reality(T_{n})) \setminus double\_spent(T_{n})

nrryuya.icon > Why explicitly remove double spent TXOs?

Priority

Exits are ordered by a given priority number. An exit with a lower priority number will process before an exit with a higher priority number. We define the priority of an exit from a transaction$ t, $ p(t), as:

$ p(t) = \max(I(t))

Proof of Requirements

Safety

Our safety property says:

$ \forall o \in E(T_{n}), o \notin I(t_{n+1}) \rightarrow o \in E(T_{n+1})

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 \notin 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:

$ \forall o \in E(T_{n}), o \in I(t_{n+1}) \rightarrow o \in E(T_{n+1}) \oplus O(t_{n+1}) \subseteq E(T_{n+1})

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:

$ \forall o \in E(T_{n}), o \in I(t_{n+1}) \rightarrow o \in E(T_{n+1}) \oplus O(t_{n+1}) \subseteq E(T_{n+1}) \oplus o \in double\_spent(T_{n+1})

Proof strategy

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:

(i)$ o \in E(T_{n+1}) \rightarrow O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \notin double\_spent(T_{n+1})

and

(ii)$ O(t_{n+1}) \subseteq E(T_{n+1}) \rightarrow o \notin E(T_{n+1}) \wedge o \notin double\_spent(T_{n+1})

and

(iii)$ o \in double\_spent(T_{n+1}) \rightarrow O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \notin E(T_{n+1})

nrryuya.icon > First, we prove that three formula (name them as $ A, B, C) are not consistent by proving (i), (ii), (iii). After that, we just need to at least one of $ A, B, C must be true, i.e. $ A \lor B \lor C. We prove it by proof of contradiction.

Proof of inconsistency

(i) Let's show the first. nrryuya.icon > $ A \rightarrow \neg{B} \land \neg{C}

$ 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.

nrryuya.icon > By the difinition, $ o \in E(T_{n+1}) \rightarrow unspent(reality(T_{n+1})) \rightarrow \forall t \in reality(T_{n+1}), o \notin I(t). Therefore, if we assume that $ t_{n+1}is canonical, i.e. $ t_{n+1} \in reality(T_{n+1}), then $ o \notin I(t_{n+1})is deduced and it's contradictory to $ o \in I(t_{n+1}).

$ 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}) \rightarrow o \notin 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}) \rightarrow o \notin double\_spent(T_{n+1}).

(ii) Next, we'll show the second statement. nrryuya.icon > $ B \rightarrow \neg{A} \land \neg{C}

$ 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 \notin E(T_{n+1}). If $ t is canonical then there cannot exist another earlier spend of the input, so $ o \notin double\_spent(T_{n+1}).

(iii) Now the third statement. nrryuya.icon > $ C \rightarrow \neg{A} \land \neg{B}

$ 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 \notin E(T_{n+1}) because of our $ \setminus double\_spent(T_{n}) clause.

Proof of at least one of three formula is true

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

$ O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \land o \notin E(T_{n+1}) \land o \notin double\_spent(T_{n+1})

nrryuya.icon > Assumed $ \neg{A} \land \neg{B} \land \neg{C} to prove $ A \lor B \lor C

nrryuya.icon > We prove this is contradictory under the assumption $ \forall o \in E(T_{n}), o \in I(t_{n+1})

We've already shown that:

$ o \in E(T_{n+1}) \rightarrow O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \land o \notin double\_spent(T_{n+1})

nrryuya.icon > $ B \rightarrow \neg{A} \land \neg{C} proved in (ii)

We can negate this statement to find:

$ o \notin E(T_{n+1}) \land (O(t_{n+1}) \subseteq E(T_{n+1}) \vee o \in double\_spent(T_{n+1}))

nrryuya.icon > $ \neg{B} \land A \lor C

nrryuya.icon > Tips: $ (X \rightarrow Y) \rightarrow (\neg{Y} \rightarrow \neg{X}) \rightarrow Y \lor \neg{X}

However, we assumed that:

$ O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \notin double\_spent(T_{n+1})

nrryuya.icon > $ \neg{A} \land \neg{C}

Therefore we've shown the statement by contradiction.

Exit Ordering

Let $ t_{v} be some valid transaction and $ t_{iv} be the first invalid, but still exitable and canonical, transaction in the chain. $ t_{iv} must either be a deposit transaction or spend some input that didn’t exist when $ t_{v} was created, otherwise $ t_{iv} would be valid. Therefore:

$ \max(I(t_{v})) < \max(I(t_{iv}))

nrryuya.icon > This is just because $ t_{iv}is assumed to spend some input that didn’t exist when $ t_{v} was created. This is related to the assumption that users of Plasma chain need to exit when they find $ t_{iv}.

and therefore by our definition of $ p(t):

$ p(t_{v}) < p(t_{iv})

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

$ (O(t_{iv}) \cap I(t') \neq \varnothing) \vee (\exists t : stems\_from(t_{iv}, t) \wedge stems\_from(t, t'))

nrryuya.icon > Omitted definition of $ stems\_from:

$ stems\_from(t_j, t_k) = (O(t_j) \cap I(t_k) \neq \emptyset) \lor (\exists{t} : stems\_from(t_j, t) \land stems\_from(t, t_k))

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

$ p(t') = \max(I(t')) \geq \max(I(t') \cap O(t_{iv})) \geq \min(O(t_{iv})) > \max(I(t_{iv})) = p(t_{iv})

Otherwise, there's a chain of transactions from $ p_{iv} to $ p' for which the first is true, and therefore the inequality holds by transitivity. Therefore, all exiting outputs created by valid transactions will exit before any output created by an invalid transaction.

Notes

This work:

models transactions and defines "exitable" TXOs

proves safety and liveness properties about exitable TXOs

Assumptions

Plasma chain exists and includes transactions so that it can be treated as the set of transactions

Data availability

Not exitable TXOs are prevented from exitting by the "challenge"

"TXOs in $ TXO(T_n) but not in $ E(T_n) are challengable"

Enhancement

Definition of$ t_{iv}which is invalid and non-challengable tx.

exitted tx (this still exists in$ E(T_n)) (the exit of this tx is prevented easiliy by Plasma contract in Plasma Cash)

out of nowhere tx