More Viable Plasma における safety と liveness
m0t0k1ch1.icon More Viable Plasma の提案の中から safety と liveness に関する部分をピックアップ
---.icon
Introduction
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.
exit ゲームは、トランザクション$ tについて「exit 可能な出力」のセットを定義する。例えば、我々のルールの下では、使用済みの出力は exit 可能ではない。ゲームが満たさなければならないこのような性質を形式的に定義する。これらの性質は safety と liveness に分けて考える。なぜなら、これらは非常に類似しているから。
m0t0k1ch1.icon safety と liveness は並行システムが満たすべき性質（ここはもうちょっと掘りたい）
---.icon
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.
「ある時点でおいて、出力が exit 可能かつ後のトランザクションで使用されていない場合、それは exit 可能でなければならない」というのが safety に関するルールである。この条件を満たせなかった場合、ユーザーはお金を受け取ることは可能だが、後でそれを使用したり exit したりすることはできなくなる。
Formally, if we say that$ E(T_n)represents the set of exitable outputs for some Plasma chain and$ T_{n + 1}is$ T_nplus some new transaction$ t_{n + 1}:
形式的に、ある Plasma チェーンにおいて、$ E(T_n)を exit 可能な出力のセットとし、$ T_{n + 1}を$ T_nに何らかの新しいトランザクション$ t_{n + 1}を付加したものとした場合、safety は以下で表現される。
$ \forall{o} \in E(T_n) : o \notin I(t_{n + 1}) \Rightarrow o \in E(T_{n + 1})
m0t0k1ch1.icon $ T_nは全トランザクションのインデックスと内容を紐づけているマップ
m0t0k1ch1.icon $ \forallは「任意の」
m0t0k1ch1.icon ある時点$ T_nにおいて exit 可能な任意の出力$ \forall{o} \in E(T_n)がトランザクション$ t_{n + 1}の入力として使用されなかった場合、その出力は$ T_{n + 1}でも exit 可能$ o \in E(T_{n + 1})である、ということ
---.icon
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”.
「ある時点において exit 可能だったある出力が使用された場合、その使用の後、その出力が引き続き exit 可能な状態もしくはその使用によって新しく生まれた全ての出力が exit 可能な状態のどちらかの状態に即座に遷移し、両方を満たすような状態にはならない」というのが基本的な liveness に関するルールである。
m0t0k1ch1.icon 使われてないのか使われたのかハッキリしなさい！中途半端はダメ！ということか
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.
2 つ目の状態はおそらく当然のことである。なぜなら、ある出力の使用によって新しく生まれた全ての出力は exit 可能であるべきだから。1 つ目の状態は特別である。なぜなら、使用が不正だった場合、その使用によって新しく生まれた出力は exit 可能であるべきではなく、使用された出力が exit 可能であるべきだから。よって、liveness を端的に表現すると、全ての「カノニカル」なトランザクションは exit 可能なトランザクションに影響を与えるべき、ということになる。
We define “canonical” later.
「カノニカル」は後で定義する。
Formally:
形式的には以下で表現される。
$ \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})
m0t0k1ch1.icon $ \oplusは直和集合（$ A \oplus Bは、$ A \cap Bが空集合であるということを暗黙的に表現している）、$ \subseteqは部分集合
m0t0k1ch1.icon ある時点$ T_nにおいて exit 可能な任意の出力$ \forall{o} \in E(T_n)がトランザクション$ t_{n + 1}の入力として使用された場合、その出力が$ T_{n + 1}において exit 可能な出力のセット$ E(T_{n + 1})に含まれるか、トランザクション$ t_{n + 1}の出力$ O(t_{n + 1})が$ T_{n + 1}において exit 可能な出力のセット$ E(T_{n + 1})の部分集合であるかのどちらかである（両方を満たすことはない）、ということ（だと思う）
m0t0k1ch1.icon $ \oplusの解釈が合ってるのか少し不安だが、前述のルールから考えるとこれで合ってる気はする
---.icon
m0t0k1ch1.icon memo
kfichter も冒頭で述べているように safety と liveness は類似した概念でややこしい。が、以下は決定的に違うので、これだけでも頭に入れておくとよいかも。
safety は$ \forall{o} \in E(T_n), o \notin I(t_{n + 1})のときに満たすべき性質
liveness は$ \forall{o} \in E(T_n), o \in I(t_{n + 1})のときに満たすべき性質