# TheDAOロールバックのセミフォーマルな検討
## 要旨
本稿では、2016年のThe DAO事件に続くイーサリアムのハードフォークが、操作順序の合意(AO³)形式フレームワークにおける「合意的書き換え」に該当するかを検証する。厳密な分析を通じて、The DAOフォークが部分的な合意を表し、それが持続的なシステム分岐をもたらしたことを明らかにする。これは、元のAO³モデルにおけるコンセンサスの二元的な概念に疑問を投げかけるものである。我々は、部分的コンセンサスに対応するためにフレームワークの拡張を提案し、分散システムガバナンスの理解に対するその含意を分析する。
**キーワード:** The DAO、イーサリアム、コンセンサス、ハードフォーク、AO³フレームワーク、分散システム
## 1. 導入
2016年のThe DAO事件は、ブロックチェーン史上最も重要なガバナンス決定の一つである。The DAOスマートコントラクトの脆弱性が悪用され、約360万ETHが流出し、イーサリアムコミュニティを分裂させる論争の的となったハードフォークへとつながった。本稿は、この出来事がAO³フレームワークで定義される「合意的書き換え」に該当するかを検証する。
我々の分析は、The DAOフォークが元のAO³モデルにおけるコンセンサスの二元的な概念に異議を唱えるものであり、部分的コンセンサスと持続的なシステム分岐に対応するための理論的拡張が必要であることを明らかにする。
## 2. AO³フレームワーク再訪
### 2.1 中核的定義
AO³フレームワークから、以下を想起する:
- **操作 (Operations)**: $O$ は全ての可能な操作の集合
- **ローカルヒストリ (Local History)**: $h_a^t \in O^*$ は時刻 $t$ におけるエージェント $a$ のビューを表す
- **書き換え (Rewriting)**: 関数 $\text{Rewrite}: O^* \times T_{\text{rw}} \rightarrow O^*$
### 2.2 コンセンサスの定義
元のフレームワークでは、コンセンサスを次のように定義する:
$$\exists h^* \in O^*, \exists t_0 \in \mathbb{N}, \forall a \in A, \forall t \geq t_0 : h^* \preceq h_a^t$$
この定義は、全てのージェントが共通のプレフィックスについて最終的に合意することを仮定している。
## 3. The DAO事件のモデリング
### 3.1 形式的表現
AO³フレームワーク内でThe DAO事件をモデル化しよう:
**定義 3.1** (The DAO操作). 以下を定義する:
- $o_{\text{drain}} \in O$: The DAOコントラクトから資金を流出させる操作
- $h_{\text{pre}} \in O^*$: $o_{\text{drain}}$ 以前のコンセンサスヒストリ
- $h_{\text{attack}} = h_{\text{pre}} \cdot o_{\text{drain}} \cdot h_{\text{post}}$: 流出を含むヒストリ
**定義 3.2** (フォークトリガー). 書き換えトリガー:
$$\tau_{\text{DAO}} \in T_{\text{rw}}$$はフォークを行う決定を表し、以下を満たす:$$\text{Rewrite}(h_{\text{attack}}, \tau_{\text{DAO}}) = h_{\text{pre}} \cdot h'_{\text{post}}$$
ここで、$h'_{\text{post}}$ は $o_{\text{drain}}$ とその結果を除外する。
### 3.2 エージェント集合の分割
**定義 3.3** (エージェント分割). The DAOフォークは以下の分割を生み出した:
$$A = A_{\text{ETH}} \cup A_{\text{ETC}}$$
ここで:
- $A_{\text{ETH}}$: 書き換えを受け入れたエージェント
- $A_{\text{ETC}}$: 書き換えを拒否したエージェント
であり、$A_{\text{ETH}} \cap A_{\text{ETC}} = \emptyset$ である。
## 4. コンセンサスの分析
### 4.1 フォーク前のコンセンサス
**命題 4.1**. フォークトリガー以前、システムはAO³コンセンサス定義を満たしていた:
$$\forall a \in A, \forall t < t_{\text{fork}}: h_{\text{attack}} \preceq h_a^t$$
*証明*. 歴史的証拠は、全てのイーサリアムノードがフォーク発表前にThe DAO流出トランザクションを含むブロックチェーンの状態について合意していたことを示している。□
### 4.2 フォーク後の分岐
**定理 4.1** (コンセンサス不成立). フォーク後、システムはもはやAO³コンセンサス定義を満たさなくなった。
*証明*. フォーク後、以下が成り立つ:
- $\forall a \in A_{\text{ETH}}, \forall t > t_{\text{fork}}: h_a^t = \text{Rewrite}(h_{\text{attack}}, \tau_{\text{DAO}}) \cdot h_{\text{ETH}}^t$
- $\forall a \in A_{\text{ETC}}, \forall t > t_{\text{fork}}: h_a^t = h_{\text{attack}} \cdot h_{\text{ETC}}^t$
$\text{Rewrite}(h_{\text{attack}}, \tau_{\text{DAO}}) \neq h_{\text{attack}}$ であるため、全ての $a \in A$ に対して $h^* \preceq h_a^t$ となるような共通プレフィックス $h^*$ は存在しない。□
### 4.3 部分的コンセンサス
**定義 4.1** (部分的コンセンサス). 我々は部分的コンセンサスを以下のように導入する:
$$\exists \mathcal{P} = \{A_1, ..., A_k\} \text{ partition of } A, \forall i \in [k], \exists h_i^* \in O^*:$$
$$\forall a \in A_i, \forall t \geq t_0: h_i^* \preceq h_a^t$$
**定理 4.2**. The DAOフォークは、以下を伴う2-部分的コンセンサスをもたらした:
- $h_{\text{ETH}}^* = \text{Rewrite}(h_{\text{attack}}, \tau_{\text{DAO}})$
- $h_{\text{ETC}}^* = h_{\text{attack}}$
## 5. 「合意的」書き換えの問題
### 5.1 合意の測定
**定義 5.1** (コンセンサス強度). 書き換えトリガー $\tau$ に対し、コンセンサス強度を以下のように定義する:
$$\rho(\tau) = \frac{|A_{\text{accept}}|}{|A|}$$
ここで、$A_{\text{accept}} = \{a \in A : a \text{ accepts } \tau\}$ である。
### 5.2 実証分析
The DAOフォークについて:
- **ハッシュレートの分割**: 当初は約85% ETH、約15% ETC
- **時価総額の分割**: 時間とともに変動したが、当初は同様の比率
- **ノード数**: 正確な測定は困難
**観察 5.1**. フォーク時のハッシュレート指標に基づくと、$\rho(\tau_{\text{DAO}}) \approx 0.85$ であった。
### 5.3 哲学的考察
**問い**: 85%の採用は「合意的」書き換えに十分か?
**議論1** (多数決的見解): $\rho(\tau) > 0.5$ であればコンセンサスを構成する。
**議論2** (全会一致的見解): 真のコンセンサスには $\rho(\tau) = 1.0$ が必要である。
**議論3** (安定性重視の見解): 受け入れた側のパーティションが安定し機能的であればコンセンサスは存在する。
## 6. 部分的コンセンサスのためのAO³拡張
### 6.1 提案された拡張
**定義 6.1** (しきい値付き合意的書き換え). あるしきい値 $\theta \in [0, 1]$ に対して、書き換えが $\theta$-合意的であるとは:
$$\rho(\tau) \geq \theta$$
を満たす場合である。
**定義 6.2** (分岐型書き換え). 書き換えトリガー $\tau$ が分岐型であるとは:
$$0 < \rho(\tau) < 1$$
を満たす場合である。
### 6.2 分岐後のシステム進化
**定理 6.1** (独立的進化). 分岐型書き換えの後、各パーティションは独立して進化する:
$$\forall t > t_{\text{fork}}: h_{a_1}^t \cap h_{a_2}^t = h^*_{\text{common}}$$
ここで、$a_1 \in A_1, a_2 \in A_2$ (異なるパーティションに属する)であり、$h^*_{\text{common}}$ は最後の共通プレフィックスである。
## 7. 含意と結論
### 7.1 The DAOフォークは「合意的」だったのか?
拡張AO³フレームワーク内では:
1. **元の二元的コンセンサス下では**: 否。システムは普遍的な合意を維持できなかった。
2. **$\theta$-合意的定義下では**:
- $\theta \leq 0.85$ ならば、然り
- $\theta > 0.85$ ならば、否
3. **部分的コンセンサス下では**: 然り。ただし、永続的なシステム分岐を伴う。
### 7.2 理論的含意
The DAO事件は以下を明らかにする:
1. **コンセンサスは実際には二元的ではない**。システムは様々な程度の合意を示すことができる。
2. **書き換えは一時的な不一致ではなく、安定した分岐を生み出し得る**。
3. **分岐後、「システム」の定義が曖昧になる**。
### 7.3 結論
The DAOフォークは、部分的合意を許容する緩和されたコンセンサス定義の下でのみ、合意的書き換えを表す。この事件は、分散システムにおけるコンセンサス現象の全スペクトルを捉えることができる、よりニュアンスに富んだ形式フレームワークの必要性を浮き彫りにする。我々が提案した拡張を含むAO³フレームワークは、そのような分析のための基盤を提供する。
## 参考文献
[1] Agreement on Operation Order (AO³): A Formal Framework for Distributed Consensus with Rewritability https://hackmd.io/@ecdysisxyzbot-ea-001/r1jNOpaRyg
[2] Ethereum Foundation. (2016). Hard Fork Completed. Ethereum Blog.
[3] Buterin, V. (2016). Thinking About Smart Contract Security. Ethereum Blog.
[4] DuPont, Q. (2017). Experiments in Algorithmic Governance: A History and Ethnography of "The DAO," a Failed Decentralized Autonomous Organization. In Bitcoin and Beyond (pp. 157-177).
[5] Mehar, M. I., et al. (2019). Understanding a Revolutionary and Flawed Grand Experiment in Blockchain: The DAO Attack. Journal of Cases on Information Technology, 21(1), 19-32.