SuperchainWETH: add sendETH and relayETH invariants (#471)

* SuperchainWETH: update to include sendETH and relayETH

* Add TODO

specs/interop/superchain-weth.md

@@ -14,6 +14,8 @@
     - [`withdraw`](#withdraw)
     - [`crosschainBurn`](#crosschainburn)
     - [`crosschainMint`](#crosschainmint)
+    - [`sendETH`](#sendeth)
+    - [`relayETH`](#relayeth)
 - [ETHLiquidity](#ethliquidity)
   - [Invariants](#invariants-1)
     - [Global Invariants](#global-invariants)
@@ -22,11 +24,20 @@
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
-Superchain WETH is a version of the standard WETH contract that allows ETH to be interoperable across the Superchain.
-Superchain WETH treats ETH as an ERC-20 token for interoperability and avoids native ETH support.
-Superchain WETH integrates with the [SuperchainTokenBridge](./predeploys.md#superchainerc20bridge) as its entrypoint
-for interopable actions.
-Superchain WETH also introduces a liquidity contract used to provide liquidity for native ETH across chains.
+Superchain WETH is an enhanced version of the standard WETH contract, enabling ETH interoperability across the
+Superchain. The Superchain WETH contract serves two primary functions:
+
+1. **Native ETH Transfers**: It provides the `sendETH` and `relayETH` functions to transfer **native ETH** directly
+between interoperable chains that both use ETH as their native token. If the destination chain does not use ETH as
+its native asset, the transferred ETH is converted into the **SuperchainWETH** ERC20 token on the destination chain
+instead.
+2. **ERC20 Token**: It extends the **ERC20** contract, allowing ETH to be wrapped into the **SuperchainWETH** ERC20
+token. This wrapped token can be transferred across interoperable chains via the
+[SuperchainTokenBridge](./predeploys.md#superchainerc20bridge), serving as the entry point for ERC20 token
+interoperability.
+
+Superchain WETH integrates with the `ETHLiquidity` contract to manage native ETH liquidity across chains, ensuring
+seamless cross-chain transfers of ETH in both its native and ERC20 forms.
 
 ## Motivation and Constraints
 
@@ -57,7 +68,7 @@ but does not preclude a protocol-layer solution as long as we minimize implement
 | `ETHLiquidity` Address   | `0x4200000000000000000000000000000000000025` |
 
 ## SuperchainWETH
-
+<!-- TODO (https://github.com/ethereum-optimism/specs/issues/479) re-write invariants to use imperative form -->
 ### Invariants
 
 #### `deposit`
@@ -72,11 +83,11 @@ but does not preclude a protocol-layer solution as long as we minimize implement
 
 - Reverts if called by any address other than the `SuperchainTokenBridge`.
 - Reverts if attempting to send more than the sender's available balance.
-- Reduce's the sender's balance by the sent amount.
+- Reduces the sender's balance by the sent amount.
 - Emits a transfer event from sender to null address for the sent amount.
 - Burns liquidity by sending the sent amount of ETH into the `ETHLiquidity` contract if native token is ETH.
   - Must not revert.
-- Emits a `CrosschainBurnt` event.
+- Emits a `CrosschainBurn` event.
 
 #### `crosschainMint`
 
@@ -85,7 +96,26 @@ but does not preclude a protocol-layer solution as long as we minimize implement
   - Must not revert.
 - Increases the recipient's balance by the sent amount.
 - Emits a transfer event from null address to recipient for the sent amount.
-- Emits a `CrosschainMinted` event.
+- Emits a `CrosschainMint` event.
+
+#### `sendETH`
+
+- Reverts if the `msg.sender`'s balance is less than the `msg.value` being sent.
+- Reverts if the `to` address is the zero address.
+- Reverts if the native token on the source chain is not ETH.
+- Transfers `msg.value` of ETH from the `msg.sender` to the `ETHLiquidity` contract.
+- Sends a cross-chain message to the destination chain to call `relayETH`.
+- Emits a `SendETH` event with details about the sender, recipient, amount, and destination chain.
+
+#### `relayETH`
+
+- Reverts if called by any address other than the `L2ToL2CrossDomainMessenger`.
+- Reverts if the cross-domain sender is not `SuperchainWETH` on the source chain.
+- If the destination chain uses ETH as its native token:
+  - Transfers the relayed ETH to the recipient.
+- If the destination chain uses a custom gas token:
+  - Mints **SuperchainWETH** ERC-20 tokens to the recipient.
+- Emits a `RelayETH` event with details about the sender, recipient, amount, and source chain.
 
 ## ETHLiquidity