feat: add shared lockbox invariants

specs/interop/dependency-set.md

@@ -6,6 +6,7 @@
 
 - [Chain ID](#chain-id)
 - [Updating the Dependency Set](#updating-the-dependency-set)
+  - [Invariants](#invariants)
 - [Security Considerations](#security-considerations)
   - [Layer 1 as Part of the Dependency Set](#layer-1-as-part-of-the-dependency-set)
 
@@ -47,17 +48,18 @@ It is a known issue that not all software in the Ethereum can handle 32 byte cha
 
 ## Updating the Dependency Set
 
-The `SystemConfig` is updated to manage a new role, `dependencyManager`.
-It can only updated by the `ProxyAdmin` during an contract upgrade.
-The sole holder of this role is the only address
-permissioned to update (remove/add to) the dependency set of that chain.
+The `SystemConfig` is updated to have the `SuperchainConfig` address and to manage the dependency set.
 
-The `SystemConfig` is also updated to manage the dependency set.
-The address with the `dependency manager` role can add or remove
-chains from the dependency set through the `SystemConfig`.
+The `SuperchainConfig` can add or remove chains from the dependency set through the `SystemConfig`.
 
 The `SystemConfig` MUST enforce that the maximum size of the dependency set is `type(uint8).max` or 255.
 
+### Invariants
+
+- Only the `SuperchainConfig` contract MUST be able to add a new dependency
+
+- Only the `SuperchainConfig` contract MUST be able to remove a dependency
+
 ## Security Considerations
 
 ### Layer 1 as Part of the Dependency Set

specs/interop/optimism-portal-interop.md

@@ -5,39 +5,43 @@
 **Table of Contents**
 
 - [Overview](#overview)
-  - [Interface and properties](#interface-and-properties)
   - [Integrating `SharedLockbox`](#integrating-sharedlockbox)
+  - [Invariants](#invariants)
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
 ## Overview
 
 The `OptimismPortal` contract is upgraded to integrate the `SharedLockbox` and start using the shared ETH liquidity.
-
-### Interface and properties
-
-The `OptimismPortal` contract will add the following storage layout and modified functions:
-
-**`SHARED_LOCKBOX`**
-
-- An immutable address pointing to the `SharedLockbox` contract.
-- This address MUST be immutable because all `OptimismPortals` will point to the same `SharedLockbox`,
-  and this address SHOULD not change.
+This liquidity consists of every ETH balance migrated from each `OptimismPortal`
+when joining the op-governed dependency set.
 
 ### Integrating `SharedLockbox`
 
-The integration with the `SharedLockbox` involves adding extra steps when executing deposit transactions
-or finalizing withdrawal transactions.
-These steps include locking and unlocking ETH without altering other aspects of the current `OptimismPortal` implementation.
+The integration with the `SharedLockbox` locking ETH when executing deposit transactions and unlocking ETH
+when finalizing withdrawal transactions, without altering other aspects of the current `OptimismPortal` implementation.
+
 To implement this solution, the following changes are needed:
 
 **`depositTransaction`**
 
 Calls `lockETH` on the `SharedLockbox` with the `msg.value`.
 
-- The function MUST call `lockETH` on the `SharedLockbox` if:
+- The function MUST call `lockETH` with `msg.value` on the `SharedLockbox` if:
   - The token is `ETHER`.
   - `msg.value` is greater than zero.
+  - `OptimismPortal` address is authorized to interact with the `SharedLockbox`.
+
+```mermaid
+sequenceDiagram
+    participant User
+    participant OptimismPortal
+    participant SharedLockbox
+
+    User->>OptimismPortal: depositTransaction(...)
+    OptimismPortal->>SharedLockbox: lockETH()
+    OptimismPortal->>OptimismPortal: emit TransactionDeposited()
+```
 
 **`finalizeWithdrawalTransactionExternalProof`**
 
@@ -46,4 +50,30 @@ Calls `unlockETH` on the `SharedLockbox` with the `tx.value`.
 - The function MUST call `unlockETH` on the `SharedLockbox` if:
   - The token is `ETHER`.
   - `tx.value` is greater than zero.
+  - `OptimismPortal` address is authorized to interact with the `SharedLockbox`.
 - The ETH is received by the `OptimismPortal` and then sent with the withdrawal transaction
+
+```mermaid
+sequenceDiagram
+    participant User
+    participant OptimismPortal
+    participant SharedLockbox
+
+    User->>OptimismPortal: finalizeWithdrawalTransactionExternalProof(...)
+    OptimismPortal->>SharedLockbox: unlockETH(uint256 value)
+    SharedLockbox->>OptimismPortal: donateETH()
+    OptimismPortal->>OptimismPortal: emit WithdrawalFinalized()
+```
+
+### Invariants
+
+- It MUST lock the ETH amount on the `SharedLockbox` when on a deposit transaction with value greater than zero
+
+- Only MUST lock ETH if the `OptimismPortal` is authorized to interact with the `SharedLockbox`.
+
+- It MUST unlock the ETH amount being withdrawn from the `SharedLockbox` if it is greater than zero
+
+- Only MUST unlock ETH if the `OptimismPortal` is authorized to interact with the `SharedLockbox`.
+
+- It MUST NOT hold any ETH balance from any deposit transaction
+  if the `OptimismPortal` is authorized to interact with the `SharedLockbox`.

specs/interop/shared-lockbox-upgrade.md

@@ -5,7 +5,7 @@
 **Table of Contents**
 
 - [Overview](#overview)
-  - [Add the chain to the op-governed dependency set](#add-the-chain-to-the-op-governed-dependency-set)
+  - [Add the chain to the op-governed dependency set in `SuperchainConfig`](#add-the-chain-to-the-op-governed-dependency-set-in-superchainconfig)
   - [Migrate ETH liquidity from `OptimismPortal` to `SharedLockbox`](#migrate-eth-liquidity-from-optimismportal-to-sharedlockbox)
     - [`LiquidityMigrator`](#liquiditymigrator)
   - [`OptimismPortal` code upgrade](#optimismportal-code-upgrade)
@@ -17,13 +17,12 @@
 
 ## Overview
 
-Based on the assumption that a chain joining the dependency set is an irreversible process,
-the on-chain chains list is simplified by assuming that joining the Shared Lockbox is
-equivalent to joining the op-governed dependency set.
+Based on the assumption that a chain joining the op-governed dependency set is an irreversible process,
+it is assumed that joining the Shared Lockbox is equivalent to it.
 
 The upgrade process consists of three main points:
 
-- Add the chain to the op-governed dependency set
+- Add the chain to the op-governed dependency set in `SuperchainConfig`
 - Move ETH liquidity from `OptimismPortal` to `SharedLockbox`
 - Upgrade the code of `OptimismPortal` to include the `SharedLockbox` integration
 
@@ -33,17 +32,17 @@ This process also requires that:
 - `SuperchainConfig` is upgraded to manage the dependency set
 - `SystemConfig` is upgraded to the interop contract version
 
-### Add the chain to the op-governed dependency set
+### Add the chain to the op-governed dependency set in `SuperchainConfig`
 
 The `SuperchainConfig` contract will be responsible for storing and managing the dependency set.
 Its `addChain` function will be used to add the chain to the dependency set and call the `SystemConfig` of each chain
 to keep them in sync.
 It will also allowlist the corresponding `OptimismPortal`, enabling it to lock and unlock ETH from the `SharedLockbox`.
-Once this process is complete, the system will be ready to process deposits and withdrawals.
+Once `addChain` is called, the system will be ready to process deposits and withdrawals.
 
 ### Migrate ETH liquidity from `OptimismPortal` to `SharedLockbox`
 
-The ETH will be transferred from the `OptimismPortal` to the `SharedLockbox` using an intermediate contract.
+The ETH will be transferred from the `OptimismPortal` to the `SharedLockbox` using the `LiquidityMigrator` contract.
 This contract functions similarly to upgrades using the `StorageSetter`, being updated immediately before to the real implementation.
 Its sole purpose is to transfer the ETH balance.
 This approach eliminates the need for adding code to move the liquidity to the lockbox that won't be used again.
@@ -60,21 +59,22 @@ This approach avoids adding extra code to the `initialize` function, which could
 
 Transfers the entire ETH balance from the `OptimismPortal` to the `SharedLockbox`.
 
-- It MUST transfer the whole ETH balance to the `SharedLockbox` when called.
-
 ```solidity
 function migrateETH() external;
 ```
 
+**Invariants**
+
+- It MUST migrate the whole `OptimismPortal` ETH balance to the `SharedLockbox`
+
+- It MUST emit `ETHMigrated` when migrating the balance
+
 ### `OptimismPortal` code upgrade
 
 The `OptimismPortal` will start locking and unlocking ETH through the `SharedLockbox`.
 It will continue to handle deposits and withdrawals but won't directly hold the ETH liquidity.
 To set this up, the upgrade function will be called via `ProxyAdmin` to implement the new code,
 which includes the necessary `SharedLockbox` integration.
-The `SharedLockbox` address will be set during the `initialize` function. After this step,
-the `OptimismPortal` will not be able to process deposits and withdrawals until the chain is registered
-in `SuperchainConfig`.
 
 ## Batch transaction process
 
@@ -109,6 +109,7 @@ sequenceDiagram
 
     %% Step 1: Add chain to SuperchainConfig
     L1PAO->>SuperchainConfig: addChain(chainId, SystemConfig address)
+    SuperchainConfig->>SharedLockbox: authorizePortal(OptimismPortal address)
 
     %% Step 2: Upgrade OptimismPortal to intermediate implementation that transfers ETH
     L1PAO->>ProxyAdmin: upgradeAndCall()

specs/interop/shared-lockbox.md

@@ -8,14 +8,17 @@
 - [Design](#design)
   - [Interface and properties](#interface-and-properties)
   - [Events](#events)
+- [Invariants](#invariants)
+  - [System level invariants](#system-level-invariants)
+  - [Contract level invariants](#contract-level-invariants)
 - [Reference implementation](#reference-implementation)
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
 ## Overview
 
 With interoperable ETH, withdrawals will fail if the referenced `OptimismPortal` lacks sufficient ETH.
-This is due to having the possibility to move ETH liquidity accross the different chains and it could happen
+This is due to having the possibility to move ETH liquidity across the different chains and it could happen
 that a chain ends up with more liquidity than its `OptimismPortal`.
 The `SharedLockbox` improves the Superchain's interoperable ETH withdrawal user experience and avoids this issue.
 To do so, it unifies ETH L1 liquidity in a single contract (`SharedLockbox`), enabling seamless withdrawals of ETH
@@ -28,8 +31,9 @@ It implements two main functions: `lockETH` for depositing ETH into the lockbox,
 and `unlockETH` for withdrawing ETH from the lockbox.
 These functions are called by the `OptimismPortal` contracts to manage the shared ETH liquidity
 when making deposits or finalizing withdrawals.
-These `OptimismPortal`s will be allowlisted by the `SuperchanConfig` using the `authorizePortal` function
+These `OptimismPortal`s will be allowlisted by the `SuperchainConfig` using the `authorizePortal` function
 when a chain is added.
+The `SharedLockbox` contract is proxied and managed by the L1 `ProxyAdmin`.
 
 ### Interface and properties
 
@@ -38,7 +42,8 @@ when a chain is added.
 Deposits and locks ETH into the lockbox's liquidity pool.
 
 - The function MUST accept ETH.
-- Only authorized `OptimismPortal` addresses SHOULD be allowed to interact.
+- Only authorized `OptimismPortal` addresses MUST be allowed to interact.
+- The function MUST NOT revert when called by an authorized `OptimismPortal`
 - The function MUST emit the `ETHLocked` event with the `portal` that called it and the `amount`.
 
 ```solidity
@@ -49,7 +54,8 @@ function lockETH() external payable;
 
 Withdraws a specified amount of ETH from the lockbox's liquidity pool.
 
-- Only authorized `OptimismPortal` addresses SHOULD be allowed to interact.
+- Only authorized `OptimismPortal` addresses MUST be allowed to interact.
+- The function MUST NOT revert when called by an authorized `OptimismPortal`
 - The function MUST emit the `ETHUnlocked` event with the `portal` that called it and the `amount`.
 
 ```solidity
@@ -60,7 +66,7 @@ function unlockETH(uint256 _value) external;
 
 Grants authorization to a specific `OptimismPortal` contract.
 
-- Only `SuperchainConfig` address SHOULD be allowed to interact.
+- Only `SuperchainConfig` address MUST be allowed to interact.
 - The function MUST add the specified address to the mapping of authorized portals.
 - The function MUST emit the [`PortalAuthorized`](#events) event when a portal is successfully added.
 
@@ -94,6 +100,42 @@ MUST be triggered when `authorizePortal` is called
 event PortalAuthorized(address indexed portal);
 ```
 
+## Invariants
+
+### System level invariants
+
+- The ETH held in the SharedLockbox MUST never be less than the amount deposited but not yet withdrawn by the `OptimismPortal`s
+
+- The ETH unlocked by any `OptimismPortal` MUST NOT exceed the available shared liquidity in the `SharedLockbox`.
+
+- The total withdrawable ETH amount present on all the dependency set’s chains MUST NEVER be more than the amount held
+  by the `SharedLockbox` of the cluster
+  > With "withdrawable amount", the ETH balance held on `ETHLiquidity` is excluded
+
+### Contract level invariants
+
+- It MUST allow only authorized portals to lock ETH
+
+- It MUST allow only authorized portals to unlock ETH
+
+- Only the `SuperchainConfig` contract MUST be able to authorize an `OptimismPortal`
+
+- It MUST be in paused state if the `SuperchainConfig` is paused
+
+- No Ether MUST flow out of the contract when in a paused state
+
+- No `OptimismPortal` can be authorized when in a paused state
+
+- It MUST NOT trigger a new deposit when ETH amount is being unlocked from the `SharedLockbox` by the `OptimismPortal`
+
+- It MUST emit:
+
+  - An `ETHLocked` event when locking ETH
+
+  - An `ETHUnlocked` event when unlocking ETH
+
+  - A `PortalAuthorized` event when authorizing a new portal
+
 ## Reference implementation
 
 An example implementation could look like this: