Merge pull request #7385 from ethereum-optimism/cl/fdg-spec-update

Update `FaultDisputeGame` resolution spec

specs/fault-dispute-game.md

@@ -246,12 +246,122 @@ A move against a particular claim is no longer possible once the parent of the d
 
 ### Resolution
 
-Resolving the FDG determines which team won.
-This is done by examining the left-most, uncontested (or undisputed) claim.
-If the depth of this claim is odd then Challengers win, otherwise Defenders win.
-Resolution is only possible once the Clock of the left-most, uncontested claim has expired.
-
-Given these rules, players are motivated to move quickly to challenge dishonest claims.
+Resolving the FDG determines which team won the game. To do this, we use the internal sub game structure.
+Each claim within the game is the root of its own sub game. These subgames are modeled as nested DAGs, each with a max
+depth of 1. In order for a claim to be considered countered, only one of its children must be uncountered. Subgames
+can also not be resolved until all of their children, which are subgames themselves, have been resolved and
+the potential opponent's chess clock has run out. Because each claim is the root of its own sub-game,
+truth percolates upwards towards the root claim by resolving each individual sub-game bottom-up.
+
+In a game like the one below, we can resolve up from the deepest subgames. Here, we'd resolve `b0`
+to uncountered and `a0` to countered by walking up from their deepest children, and now that all children of the
+root game are resolved, we can resolve the root to countered due to `b0` remaining uncountered.
+
+<!--
+digraph G {
+    rankdir=LR
+    newrank=true
+  node [shape=plaintext]
+  subgraph cluster_01 {
+    label = "Legend";
+    key [label=<<table border="0" cellpadding="2" cellspacing="0" cellborder="0">
+      <tr><td align="right" port="i1">bisection</td></tr>
+      <tr><td align="right" port="i2">resolution</td></tr>
+      </table>>]
+    key2 [label=<<table border="0" cellpadding="" cellspacing="0" cellborder="0">
+      <tr><td port="i1">&nbsp;</td></tr>
+      <tr><td port="i2">&nbsp;</td></tr>
+      </table>>]
+    key:i1:e -> key2:i1:w [color=green]
+    key:i2:e -> key2:i2:w [color=coral1, style=dotted]
+  }
+
+  subgraph cluster_0 {
+    color=cornflowerblue;
+    node [style=filled];
+    a0 -> a1 [color=green];
+    a1 -> a0 [color=coral1, style=dotted];
+    subgraph cluster_0_0 {
+        label = "subgame #5";
+        color=purple;
+
+        a1 -> a2 [color=green];
+        a2 -> a1 [color=coral1, style=dotted];
+
+        subgraph cluster_0_1 {
+            label = "subgame #6";
+            color=magenta;
+
+            a2 -> a3 [color=green];
+            a3 -> a2 [color=coral1, style=dotted];
+            a2 -> a4 [color=green];
+            a4 -> a2 [color=coral1, style=dotted];
+
+            subgraph cluster_0_2 {
+                label = "subgame #7";
+                color=lightpink;
+
+                a3
+            }
+
+            subgraph cluster_0_3 {
+                label = "subgame #8";
+                color=lightpink;
+
+                a4 -> a5 [color=green];
+                a5 -> a4 [color=coral1, style=dotted];
+
+                subgraph cluster_0_4 {
+                    label = "subgame #9";
+                    color=palegreen;
+
+                    a5
+                }
+            }
+        }
+    }
+    label = "subgame #4";
+  }
+
+  subgraph cluster_1 {
+    node [style=filled];
+
+    label = "subgame #1";
+    color=cornflowerblue
+
+    b0 -> b1 [color=green];
+    b1 -> b0 [color=coral1, style=dotted];
+    subgraph cluster_1_0 {
+        label = "subgame #2";
+        color=purple;
+
+        b1 -> b2 [color=green];
+        b2 -> b1 [color=coral1, style=dotted];
+
+        subgraph cluster_1_1 {
+            label = "subgame #3";
+            edge [style=invis]
+            color=magenta;
+
+            b2
+        }
+    }
+  }
+
+  Root -> a0 [color=green];
+  Root -> b0 [color=green];
+  a0 -> Root [color=coral1, style=dotted];
+  b0 -> Root [color=coral1, style=dotted];
+
+  Root [shape=Mdiamond];
+}
+-->
+<!-- markdownlint-disable no-inline-html -->
+<p align="center">
+<img src="https://github.com/ethereum-optimism/optimism/assets/8406232/9b20ba8d-0b64-47b3-9962-5533f7eb4ef7" width=60%>
+</p>
+
+Given these rules, players are motivated to move quickly to challenge all dishonest claims.
 Each move bisects the execution trace and eventually, `MAX_GAME_DEPTH` is reached where disputes
 can be settled conclusively. Dishonest players are disincentivized to participate, via backwards induction,
 as an invalid claim won't remain uncontested. Further incentives can be added to the game by requiring