MoreVPの擬似的な形式手法による表現

#1

omisego/elixir-omg/blob/master/docs/morevp.md がTeX表記をアレな感じにしていたので整形して貼っておく

ちなみに https://github.com/github/markup/issues/897#issuecomment-326506820 によると、githubは全然TeX表記に対応しないっぽい

Appendix

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: [1, n] \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’) \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], 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] } Unspent, Double Spent We define two helper functions unspent and doublespent. unspent takes a set of transactions and returns the list of transaction outputs that haven’t been spent. doublespent 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 doublespent: unspent(T) = { o \in TXO(T) : \forall t \in T, o \not\in I(t) } doublespent(T) = { o \in TXO(T) : \exists t,t' \in T, t \neq t', o \in I(t) \wedge o \in I(t') } 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 \not\in I(t_{n+1}) \implies 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}) \implies o \in E(T_{n+1}) \oplus O(t_{n+1}) \subseteq E(T_{n+1}) Basic Exit Protocol Formalization E(T_{n}) = unspent(reality(T_{n})) \setminus doublespent(T_{n}) 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 \not\in I(t_{n+1}) \implies 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 doublespent(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: \forall o \in E(T_{n}), o \in I(t_{n+1}) \implies 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 doublespent(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}) \implies o \in E(T_{n+1}) \oplus O(t_{n+1}) \subseteq E(T_{n+1}) \oplus o \in doublespent(T_{n+1}) 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: o \in E(T_{n+1}) \implies O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \not\in doublespent(T_{n+1}) and O(t_{n+1}) \subseteq E(T_{n+1}) \implies o \not\in E(T_{n+1}) \wedge o \not\in doublespent(T_{n+1}) and o \in doublespent(T_{n+1}) \implies O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \not\in E(T_{n+1}) 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 doublespent(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 doublespent(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 doublespent(T_{n+1}). Now the third statement. o \in doublespent(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 doublespent(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: O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \not\in E(T_{n+1}) \wedge o \not\in doublespent(T_{n+1}) We’ve already shown that: o \in E(T_{n+1}) \implies O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \not\in doublespent(T_{n+1}) We can negate this statement to find: o \not\in E(T_{n+1}) \wedge (O(t_{n+1}) \subseteq E(T_{n+1}) \vee o \in doublespent(T_{n+1})) However, we assumed that:$

O(t_{n+1}) \cap E(T_{n+1}) = \varnothing \wedge o \not\in doublespent(T_{n+1})

\$

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

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'))

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.