diff --git a/specs/fault-proof/stage-one/anchor-state-registry.md b/specs/fault-proof/stage-one/anchor-state-registry.md new file mode 100644 index 000000000..86b8eb307 --- /dev/null +++ b/specs/fault-proof/stage-one/anchor-state-registry.md @@ -0,0 +1,448 @@ +# Anchor State Registry + + + +**Table of Contents** + +- [Overview](#overview) + - [Perspective](#perspective) +- [Definitions](#definitions) + - [Dispute game](#dispute-game) + - [Maybe valid game](#maybe-valid-game) + - [Finalized game](#finalized-game) + - [Dispute game finality delay](#dispute-game-finality-delay) + - [Valid game](#valid-game) + - [Blacklisted game](#blacklisted-game) + - [Invalid game](#invalid-game) + - [Retired game](#retired-game) + - [Game retirement timestamp](#game-retirement-timestamp) + - [Anchor state](#anchor-state) + - [Anchor game](#anchor-game) + - [Withdrawal](#withdrawal) + - [Authorized input](#authorized-input) +- [Assumptions](#assumptions) + - [aFDG-001: Fault dispute games correctly report certain properties](#afdg-001-fault-dispute-games-correctly-report-certain-properties) + - [Mitigations](#mitigations) + - [aFDG-002: Fault dispute games with correct claims resolve correctly at some regular rate](#afdg-002-fault-dispute-games-with-correct-claims-resolve-correctly-at-some-regular-rate) + - [Mitigations](#mitigations-1) + - [aFDG-003: Fault dispute games are properly incentivized to resolve correctly](#afdg-003-fault-dispute-games-are-properly-incentivized-to-resolve-correctly) + - [Mitigations](#mitigations-2) + - [aDGF-001: Dispute game factory correctly identifies the games it created](#adgf-001-dispute-game-factory-correctly-identifies-the-games-it-created) + - [Mitigations](#mitigations-3) + - [aDGF-002: Games created by the DisputeGameFactory will be monitored](#adgf-002-games-created-by-the-disputegamefactory-will-be-monitored) + - [Mitigations](#mitigations-4) + - [aASR-001: Incorrectly resolving games will be invalidated within the dispute game finality delay period](#aasr-001-incorrectly-resolving-games-will-be-invalidated-within-the-dispute-game-finality-delay-period) + - [Mitigations](#mitigations-5) + - [aASR-002: The AnchorStateRegistry will be correctly initialized at deployment](#aasr-002-the-anchorstateregistry-will-be-correctly-initialized-at-deployment) + - [Mitigations](#mitigations-6) + - [aSC-001: SuperchainConfig correctly reports its guardian address](#asc-001-superchainconfig-correctly-reports-its-guardian-address) + - [Mitigations](#mitigations-7) +- [System Invariants](#system-invariants) + - [iSYS-001: Invalid withdrawals can never be finalized](#isys-001-invalid-withdrawals-can-never-be-finalized) + - [Impact](#impact) + - [Dependencies](#dependencies) + - [iSYS-002: Valid withdrawals can be finalized within some bounded amount of time](#isys-002-valid-withdrawals-can-be-finalized-within-some-bounded-amount-of-time) + - [Impact](#impact-1) + - [Dependencies](#dependencies-1) +- [Component Invariants](#component-invariants) + - [iASR-001: Only "truly" **valid games** will be represented as **valid games**](#iasr-001-only-truly-valid-games-will-be-represented-as-valid-games) + - [Impact](#impact-2) + - [Dependencies](#dependencies-2) + - [iASR-002: The anchor state is recent, within some bounded time period](#iasr-002-the-anchor-state-is-recent-within-some-bounded-time-period) + - [Impact](#impact-3) + - [Dependencies](#dependencies-3) + - [iASR-003: The anchor state is a correct L2 state root](#iasr-003-the-anchor-state-is-a-correct-l2-state-root) + - [Impact](#impact-4) + - [Dependencies](#dependencies-4) +- [Function-Level Invariants](#function-level-invariants) +- [Implementation Spec](#implementation-spec) + - [`constructor`](#constructor) + - [`initialize`](#initialize) + - [`getRecentValidState`](#getrecentvalidstate) + - [`updateAnchorState`](#updateanchorstate) + - [`getAnchorState`](#getanchorstate) + - [`registerAnchorGameCandidate`](#registeranchorgamecandidate) + - [`tryUpdateAnchorState`](#tryupdateanchorstate) + - [`isGameBlacklisted`](#isgameblacklisted) + - [`isGameRetired`](#isgameretired) + - [`isGameMaybeValid`](#isgamemaybevalid) + - [`isGameFinalized`](#isgamefinalized) + - [`isGameValid`](#isgamevalid) + - [`setRespectedGameType`](#setrespectedgametype) + - [`retireAllExistingGames`](#retireallexistinggames) + - [`setGameBlacklisted`](#setgameblacklisted) + - [`getGameFinalityDelay`](#getgamefinalitydelay) + + + +## Overview + +### Perspective + +The whole point of the fault proof system is to create correctly resolving games whose claims we can depend on to +finalize withdrawals (or other L2-to-L1 dependents). Indeed, everything about the system, from the contract mechanics to +bond incentives, is engineered to provide complete confidence that the outcome of a resolved game is correct. Yet, there +are corner cases where the resolved game rebukes its platonic, game-theoretic ideal, resolving incorrectly. The anchor +state registry appreciates this and affords games and their dependents probabalistic validity by enforcing a game +finality delay, and adding additional dependencies like blacklisting and game retirement. These concessions improve the +confidence in resolved games, and calcify the assumptions upon which withdrawals and other dependents rest. + +## Definitions + +### Dispute game + +> See [Fault Dispute Game](fault-dispute-game.md) + +A dispute game is a contract that resolves an L2 state claim. + +### Maybe valid game + +A **maybe valid game** is a dispute game that correctly resolved in favor of the defender. However, the system concedes +a possibility that it's not correct, and so it's not yet ready to be used as a **valid game** by dependents. A maybe +valid game meets the following conditions: + +- Game was created by the dispute game factory. +- Game is not **blacklisted**. +- Game was created while it was the respected game type. +- Game status is not `CHALLENGER_WINS`. +- Game `createdAt` timestamp is less than the **game retirement timestamp**. + +### Finalized game + +A finalized dispute game is a game that has been resolved in favor of either the challenger or defender. Furthermore, it +has passed the **dispute game finality delay** and can be used by dependents. A finalized game meets the following +conditions: + +- Game status is `CHALLENGER_WINS` or `DEFENDER_WINS`. +- Game `resolvedAt` timestamp is not zero. +- Game `resolvedAt` timestamp is more than `dispute game finality delay` seconds ago. + +### Dispute game finality delay + +> Also known as "air gap." + +The dispute game finality delay is the period of time between a dispute game resolving and a dispute game becoming +finalized. It's set via **authorized input**. + +### Valid game + +A game is a **valid game** if it, among other qualifications, has resolved in favor of the defender and has also matured +past the finality delay. In other words, it meets the conditions of both a **maybe valid game** and a **finalized +game**. + +### Blacklisted game + +A **blacklisted game** is a game that has been set as blacklisted via **authorized action**. It must not be considered +valid, and must not be used for finalizing withdrawals or any other dependent L2-to-L1 action. + +### Invalid game + +An **invalid game** is a game whose claim was false, or does not meet some other **maybe valid game** condition. + +### Retired game + +A **retired game** is a game whose `createdAt` timestamp is older than the **game retirement timestamp**. A game that +gets retired is no longer considered valid. + +### Game retirement timestamp + +The game retirement timestamp determines **retired games** and can only be adjusted via **authorized input**. + +### Anchor state + +> See [Fault Dispute Game -> Anchor State](fault-dispute-game.md#anchor-state). + +An anchor state is the state root from a correct L2 claim that is used as a starting point for new dispute games. + +### Anchor game + +The **anchor game** is the game whose state root is used as the **anchor state**. In the overwhelming majority of cases, +it is a **valid game**, and in any case, its claim is correct. + +### Withdrawal + +> See [Withdrawals](../../protocol/withdrawals.md). + +A withdrawal is a cross-chain transaction initiated on L2, and finalized on L1. + +### Authorized input + +An authorized input is an input for which there is social consensus, i.e. coming from governance. + +## Assumptions + +> **NOTE:** Assumptions are utilized by specific invariants and do not apply globally. Invariants typically only rely on +> a subset of the following assumptions. Different invariants may rely on different assumptions. Refer to individual +> invariants for their dependencies. + +### aFDG-001: Fault dispute games correctly report certain properties + +We assume that a fault dispute game will correctly report the following properties: + +- its game type. +- whether its game type was the respected game type when created (also assumes this is set once and never changes). +- the l2BlockNumber of its root claim. +- its `createdAt` timestamp. +- its `resolvedAt` timestamp. + +#### Mitigations + +- Existing audit on `FaultDisputeGame`. Note: Existing audit does not yet cover the second property above (that a game + correctly reports whether its game type was the respected game type when created). +- Integration testing. + +### aFDG-002: Fault dispute games with correct claims resolve correctly at some regular rate + +We assume that fault dispute games will regularly resolve in favor of the defender correctly. While the system can +handle games that resolve in favor of the challenger, as well as incorrect resolutions, there must be other games that +resolve correctly to maintain the system's integrity. + +#### Mitigations + +- Existing incentives in fault proof system design. + +### aFDG-003: Fault dispute games are properly incentivized to resolve correctly + +We assume that fault dispute games are properly incentivized to resolve correctly, implying that participants are +incentivized to play the game correctly to its correct conclusion. + +#### Mitigations + +- Existing incentives in fault proof system design. + +### aDGF-001: Dispute game factory correctly identifies the games it created + +We assume that `DisputeGameFactory` will correctly identify whether it created a game (i.e. whether the game is +"factory-registered"). + +#### Mitigations + +- Existing audit on the `DisputeGameFactory`. +- Integration testing. + +### aDGF-002: Games created by the DisputeGameFactory will be monitored + +We assume that games created by the `DisputeGameFactory` will be monitored for incorrect resolution. + +#### Mitigations + +- Stakeholder incentives. + +### aASR-001: Incorrectly resolving games will be invalidated within the dispute game finality delay period + +We assume that games that resolve incorrectly will be blacklisted or retired via **authorized action** within the dispute game +finality delay period. This further depends on +[aDGF-002](#adgf-002-games-created-by-the-disputegamefactory-will-be-monitored). + +#### Mitigations + +- Stakeholder incentives / processes. +- Incident response plan. + +### aASR-002: The AnchorStateRegistry will be correctly initialized at deployment + +We assume that the AnchorStateRegistry will be correctly initialized at deployment, including: + +- Address of initial anchor game. +- Address of `DisputeGameFactory`. +- An appropriate `DISPUTE_GAME_FINALITY_DELAY`. +- Address of `SuperchainConfig`. + +#### Mitigations + +- Verify the configured values in the deployment script. + +### aSC-001: SuperchainConfig correctly reports its guardian address + +We assume the SuperchainConfig contract correctly returns its guardian address. + +#### Mitigations + +- Existing audit on the `SuperchainConfig`. +- Integration testing. + +## System Invariants + +### iSYS-001: Invalid withdrawals can never be finalized + +#### Impact + +**Severity: Critical** + +If this invariant is broken, the system can finalize an invalid withdrawal, causing a loss of funds and a loss of +confidence. + +#### Dependencies + +- [aASR-001](#aasr-001-incorrectly-resolving-games-will-be-invalidated-within-the-dispute-game-finality-delay-period) +- [aASR-002](#aasr-002-the-anchorstateregistry-will-be-correctly-initialized-at-deployment) +- [aSC-001](#asc-001-superchainconfig-correctly-reports-its-guardian-address) +- [aFDG-001](#afdg-001-fault-dispute-games-correctly-report-certain-properties) +- [aFDG-002](#afdg-002-fault-dispute-games-with-correct-claims-resolve-correctly-at-some-regular-rate) +- [aDGF-001](#adgf-001-dispute-game-factory-correctly-identifies-the-games-it-created) +- [aDGF-002](#adgf-002-games-created-by-the-disputegamefactory-will-be-monitored) + +### iSYS-002: Valid withdrawals can be finalized within some bounded amount of time + +#### Impact + +**Severity: Critical** + +If this invariant is broken, withdrawals can be frozen for a long period of time, causing a critical liveness failure. + +#### Dependencies + +- [aFDG-001](#afdg-001-fault-dispute-games-correctly-report-certain-properties) +- [aDGF-001](#adgf-001-dispute-game-factory-correctly-identifies-the-games-it-created) +- [aDGF-002](#adgf-002-games-created-by-the-disputegamefactory-will-be-monitored) +- [aASR-001](#aasr-001-incorrectly-resolving-games-will-be-invalidated-within-the-dispute-game-finality-delay-period) +- [aASR-002](#aasr-002-the-anchorstateregistry-will-be-correctly-initialized-at-deployment) +- [aSC-001](#asc-001-superchainconfig-correctly-reports-its-guardian-address) + +## Component Invariants + +### iASR-001: Only "truly" **valid games** will be represented as **valid games** + +When asked for a **valid game** by its dependents, the AnchorStateRegistry will only serve **valid games** representing +correct L2 state claims. + +#### Impact + +**Severity: Critical** + +If this invariant is broken, the L1 will have an inaccurate view of L2 state. The `OptimismPortal` can be tricked into +finalizing withdrawals based on incorrect state roots, causing loss of funds. Other dependents will also be affected. + +#### Dependencies + +- [aFDG-001](#afdg-001-fault-dispute-games-correctly-report-certain-properties) +- [aDGF-002](#adgf-002-games-created-by-the-disputegamefactory-will-be-monitored) +- [aASR-001](#aasr-001-incorrectly-resolving-games-will-be-invalidated-within-the-dispute-game-finality-delay-period) +- [aASR-002](#aasr-002-the-anchorstateregistry-will-be-correctly-initialized-at-deployment) +- [aSC-001](#asc-001-superchainconfig-correctly-reports-its-guardian-address) + +### iASR-002: The anchor state is recent, within some bounded time period + +When asked for the **anchor state** by fault dispute games, the contract will only serve an **anchor state** whose L2 +block timestamp is recent, within some bounded period of time. + +#### Impact + +**Severity: High** + +If this invariant is broken, proposer software can break (run out of memory), leading to dispute game liveness issues +and incorrect game resolution. + +#### Dependencies + +- [aASR-002](#aasr-002-the-anchorstateregistry-will-be-correctly-initialized-at-deployment) +- [aFDG-002](#afdg-002-fault-dispute-games-with-correct-claims-resolve-correctly-at-some-regular-rate) + +### iASR-003: The anchor state is a correct L2 state root + +When asked for the **anchor state** by fault dispute games, the contract will serve an **anchor state** that's correct, +i.e. in agreement with a flawless L2 state oracle. + +#### Impact + +**Severity: High** + +If this invariant is broken, dispute games can be created with incorrect starting points, leading to games that can be +used to prove false claims. This would lead to an operational failure, requiring incident response. If incident response +doesn't occur, this could lead to loss of funds. + +#### Dependencies + +- TODO + +## Function-Level Invariants + +## Implementation Spec + +### `constructor` + +The constructor must disable the initializer on the implementation contract. + +### `initialize` + +- Initial anchor state must be an **authorized input**. +- Dispute game factory must be an **authorized input**. +- `dispute game finality delay` must be an **authorized input**. +- Superchain config must be an **authorized input**. + +### `getRecentValidState` + +Returns the state of the **anchor game**. Reverts if the **anchor game** has been **retired**. + +### `updateAnchorState` + +- Game must be a **valid game**. +- Game's block number must be higher than current **anchor state**'s block number. +- This function is the ONLY way to update the **anchor state** (after initialization). + +### `getAnchorState` + +Returns the **anchor state** of the **anchor game**. + +- Must revert if the **anchor game** is a **blacklisted game**. +- Must maintain the property that the timestamp of the game is not too old. + - TODO: How old is too old? + +### `registerAnchorGameCandidate` + +Register a **maybe valid game** as a candidate for **anchor game**. + +- Callable only by a **maybe valid game**. +- Calling game must only register itself (and not some other game). + - TODO: determine any invariants around registry ordering. + +### `tryUpdateAnchorState` + +Try to update the **anchor state** using registry of **maybe valid games**. + +- Callable by anyone. +- Find the most recent (comparing on l2BlockNumber) valid game you can find in the register within a fixed amount of + gas. + - Fixed gas amount ensures that this function does not get more expensive to call as time goes on. +- Use this as input to `updateAnchorGame`. + +### `isGameBlacklisted` + +Returns whether the game is a **blacklisted game**. + +### `isGameRetired` + +Returns whether the game is a **retired game**. + +### `isGameMaybeValid` + +Returns whether the game is a **maybe valid game**. + +### `isGameFinalized` + +Returns whether the game is a **finalized game**. + +### `isGameValid` + +Returns whether the game is a **valid game**. + +### `setRespectedGameType` + +- Must be **authorized** by guardian role. + +### `retireAllExistingGames` + +Retires all currently deployed games. + +- Must set the **game retirement timestamp** to the current block timestamp. +- Must be **authorized** by guardian role. + +### `setGameBlacklisted` + +Blacklists a game. + +- Must be **authorized** by guardian role. + +### `getGameFinalityDelay` + +Returns **authorized** finality delay duration in seconds. No external dependents; public getter for convenience. diff --git a/specs/fault-proof/stage-one/dispute-game-interface.md b/specs/fault-proof/stage-one/dispute-game-interface.md index e4dcaa650..d7ecb6718 100644 --- a/specs/fault-proof/stage-one/dispute-game-interface.md +++ b/specs/fault-proof/stage-one/dispute-game-interface.md @@ -305,5 +305,9 @@ interface IDisputeGame is IInitializable { /// @return rootClaim_ The root claim of the DisputeGame. /// @return extraData_ Any extra data supplied to the dispute game contract by the creator. function gameData() external view returns (GameType gameType_, Claim rootClaim_, bytes memory extraData_); + + /// @notice Returns whether this game's game type was the `respectedGameType` when created. + /// @return isRespectedGameType_ Whether this game's game type was the `respectedGameType` when created. + function wasRespectedGameTypeWhenCreated() external view returns (bool wasRespectedGameType_); } ``` diff --git a/specs/fault-proof/stage-one/fault-dispute-game.md b/specs/fault-proof/stage-one/fault-dispute-game.md index dd50424ef..f30b86392 100644 --- a/specs/fault-proof/stage-one/fault-dispute-game.md +++ b/specs/fault-proof/stage-one/fault-dispute-game.md @@ -11,7 +11,6 @@ - [Execution Trace](#execution-trace) - [Claims](#claims) - [Anchor State](#anchor-state) - - [Anchor State Registry](#anchor-state-registry) - [DAG](#dag) - [Subgame](#subgame) - [Game Tree](#game-tree) @@ -92,20 +91,7 @@ claims, committing to different output roots and FPVM states in the FDG. An anchor state, or anchor output root, is a previous output root that is assumed to be valid. An FDG is always initialized with an anchor state and execution is carried out between this anchor state and the [claimed output root](#claims). FDG contracts pull their anchor state from the -[Anchor State Registry](#anchor-state-registry) contract. The initial anchor state for a FDG is the -genesis state of the L2. - -Clients must currently gather L1 data for the window between the anchor state and the claimed -state. In order to reduce this L1 data requirement, [claims](#claims) about the state of the L2 -become new anchor states when dispute games resolve in their favor. FDG contracts set their anchor -states at initialization time so that these updates do not impact active games. - -### Anchor State Registry - -The Anchor State Registry is a registry that maps FDG types to their current [anchor states](#anchor-state). -The Anchor State Registry is specific to Fault Dispute Game contracts and may not be applicable to -other types of dispute game contracts that do not have the same concept of state that progresses -over time. +[Anchor State Registry](anchor-state-registry.md) contract. ### DAG diff --git a/specs/fault-proof/stage-one/optimism-portal.md b/specs/fault-proof/stage-one/optimism-portal.md new file mode 100644 index 000000000..d3236d8b9 --- /dev/null +++ b/specs/fault-proof/stage-one/optimism-portal.md @@ -0,0 +1,168 @@ +# Optimism Portal + + + +**Table of Contents** + + - [Overview](#overview) + - [Perspective](#perspective) + - [Definitions](#definitions) + - [Authorized input](#authorized-input) + - [Proven withdrawal](#proven-withdrawal) + - [Finalized withdrawal](#finalized-withdrawal) + - [Proof maturity delay](#proof-maturity-delay) + - [Assumptions](#assumptions) + - [aASR-001: AnchorStateRegistry correctly distinguishes maybe valid games](#aasr-001-anchorstateregistry-correctly-distinguishes-maybe-valid-games) + - [Impact](#impact) + - [Mitigations](#mitigations) + - [aASR-002: AnchorStateRegistry correctly distinguishes valid games](#aasr-002-anchorstateregistry-correctly-distinguishes-valid-games) + - [Impact](#impact-1) + - [Mitigations](#mitigations-1) + - [aSC-001: SuperchainConfig correctly reports system pause status](#asc-001-superchainconfig-correctly-reports-system-pause-status) + - [Impact](#impact-2) + - [Mitigations](#mitigations-2) + - [Top-Level Invariants](#top-level-invariants) +- [Function-Level Invariants](#function-level-invariants) + - [`initialize`](#initialize) + - [`proveWithdrawalTransaction`](#provewithdrawaltransaction) + - [`finalizeWithdrawalTransaction`](#finalizewithdrawaltransaction) + + + +## Overview + +### Perspective + +The whole point of the fault proof system is to create correctly resolving games whose claims we can depend on to +finalize withdrawals (or other L2-to-L1 dependents). This contract is responsible for moderating L2-to-L1 +[withdrawals](../../protocol/withdrawals.md). Because of the probabilistic validity of games as discussed in +[AnchorStateRegistry](./anchor-state-registry.md), we can't immediately finalize withdrawals. Instead, we must wait for +both a [dispute game finality delay](./anchor-state-registry.md#dispute-game-finality-delay) and a **proof maturity +delay** to pass before we can finalize a withdrawal. Meanwhile, our assumptions about the fault proof system do work +such that by the time the withdrawal is finalized, we're confident the withdrawal is correct. + +## Definitions + +### Authorized input + +An input for which there is social consensus, i.e. coming from governance. + +### Proven withdrawal + +A **proven withdrawal** is a withdrawal that is maybe valid, because it's been proven using a **maybe valid game**. +However, because we don't have full confidence in the game's validity, we can't yet finalize the withdrawal. + +### Finalized withdrawal + +A **finalized withdrawal** is a withdrawal transaction that has been proven against a game that we now know is +**valid**, and has waited the **proof maturity delay**. + +### Proof maturity delay + +The **proof maturity delay** is time that must elapse between a withdrawal being proven and it being finalized. + +## Assumptions + +### aASR-001: AnchorStateRegistry correctly distinguishes maybe valid games + +We assume that the AnchorStateRegistry correctly reports whether a game is a [**maybe valid +game**](./anchor-state-registry.md#maybe-valid-game). + +#### Impact + +**Severity: Medium** + +If a game is reported as maybe valid when it is not, an attacker can prove a withdrawal that is invalid. If +[aASR-002](#aasr-002-anchorstateregistry-correctly-distinguishes-valid-games) holds, this may not result in severe +consequences, but would negatively impact system hygiene. + +#### Mitigations + +- Pending audit of `AnchorStateRegistry` +- Integration testing + +### aASR-002: AnchorStateRegistry correctly distinguishes valid games + +We assume that the AnchorStateRegistry correctly reports whether a game is a [**valid +game**](./anchor-state-registry.md#valid-game). + +#### Impact + +**Severity: Critical** + +If a game is reported as valid when it is not, we may finalize a withdrawal that is invalid. This would result to a loss +of funds and a loss of confidence in the system. + +#### Mitigations + +- Pending audit of `AnchorStateRegistry` +- Integration testing + +### aSC-001: SuperchainConfig correctly reports system pause status + +We assume SuperchainConfig correctly returns system pause status. + +#### Impact + +**Severity: Critical** + +If SuperchainConfig incorrectly reports system pause status, we may prove / finalize a withdrawal when the system is +paused. This would create bad system hygiene, and could lead to a loss of funds or a loss of confidence in the system. + +#### Mitigations + +- Existing audit of `SuperchainConfig` + +## Top-Level Invariants + +- A withdrawal transaction must be **proven** against a game that is **maybe valid**. +- A withdrawal transaction may only be **finalized** against a game that is **valid**. + - Implicit in this is that a withdrawal transaction may only be **finalized** after the **proof maturity delay** has + passed. +- A withdrawal transaction may only be **finalized** if it has already been **proven**. +- A withdrawal transaction must be used only once to **finalize** a withdrawal. +- A withdrawal transaction that is **finalized** must attempt execution. + +# Function-Level Invariants + +## `initialize` + +- Proof maturity delay seconds must be an **authorized input**. +- Anchor state registry must be an **authorized input**. +- Dispute game factory must be an **authorized input**. +- Superchain config must be an **authorized input**. +- System config must be an **authorized input**. + +## `proveWithdrawalTransaction` + +Proves a withdrawal transaction. + +- Withdrawal game must be a [**maybe valid game**](./anchor-state-registry.md#maybe-valid-game). +- Withdrawal transaction's target must not be the `OptimismPortal` address. +- Withdrawal game's root claim must be equal to the hashed `outputRootProof` input. +- Must verify that the hash of this withdrawal is stored in the `L2toL1MessagePasser` contract on L2. +- A withdrawal cannot be reproved by the same proof submitter unless both of the following are true: + - the dispute game previously used to prove the withdrawal is now an [**invalid + game**](./anchor-state-registry.md#invalid-game). + - the withdrawal was never finalized. +- System must not be paused. + +## `finalizeWithdrawalTransaction` + +Finalizes a withdrawal transaction that has already been proven. + +- Withdrawal transaction must have already been proven. +- The proof maturity delay duration must have elapsed between the time the withdrawal was proven and this call for its + finalization. +- The time the withdrawal was proven must be greater or equal to the time at which the withdrawal's game was created. +- Withdrawal transaction must not have been finalized before. +- The game upon which the withdrawal proof is based must be a [**valid game**](./anchor-state-registry.md#valid-game). +- Function must revert when system is paused. +- If the gas-paying token is not ether: + - Withdrawal transaction's target must not be the OP token address. + - If the withdrawal transaction transfers value: + - The call to `transfer` must revert on fail. + - The input amount must equal the balance delta of this contract after transfer. +- System must not be paused. +- If these invariants are met, function must attempt execution of the withdrawal transaction. +- If the transaction wasn't successful and the `tx.origin` is the `ESTIMATION_ADDRESS`, revert with `GasEstimation()`.