specs: cleanup interop derivation

Cleanup the interop derivation specs a bit now that we understand
what we are building more. This still needs more cleanup and is missing
both:

- #489
- #495

specs/interop/derivation.md

@@ -16,6 +16,22 @@
 
 ## Overview
 
+New derivation rules are added to guaranteee integrity of cross chain messages.
+The fork choice rule is updated to fork out unsafe blocks that contain invalid
+executing messages.
+
+### Invariants
+
+- An executing message MUST have a corresponding initiating message
+- The initiating message referenced in an executing message MUST come from a chain in its dependency set
+- A block MUST be considered invalid if it is built with any invalid executing messages
+
+L2 blocks that produce invalid executing messages MUST not be allowed to be considered safe.
+They MAY optimistically exist as unsafe blocks for some period of time. An L2 block that is invalidated
+because it includes invalid executing messages MUST be replaced by a deposits only block at the same
+block height. This guarantees progression of the chain, ensuring that an infinite loop of processing
+the same block in the proof system is not possible.
+
 ### Deposit Context
 
 Derivation is extended to create **deposit contexts**, which signifies the execution of a depositing transaction.
@@ -88,8 +104,22 @@ and `l2EpochStartBlockNum` is the L2 block number of the first L2 block in the e
 
 ### Gas Considerations
 
-There must be sufficient gas available in the block to destroy deposit context.
-There's no guarantee on the minimum gas available for the second L1 attributes transaction as the block
-may be filled by the other deposit transactions. As a consequence, a deposit context may spill into multiple blocks.
+There must be sufficient gas available in the block to destroy deposit context. Depending on the
+chain configuration, there is no guarantee that the amount of guaranteed gas plus the amount used
+by the system transactions is less than the L2 block gas limit. It is important that the chain operator
+maintains a ~9 million gas buffer between the guaranteed gas limit and the L2 gas limit.
+
+### Depositing an Executing Message
+
+Deposit transactions (force inclusion transactions) give censorship resistance to layer two networks.
+It is possible to deposit an invalid executing message, forcing the sequencer to reorg. It would
+be fairly cheap to continuously deposit invalid executing messages through L1 and cause L2 liveness
+instability. A future upgrade will enable deposits to trigger executing messages.
+
+### Reliance on History
+
+When fully executing historical blocks, a dependency on historical receipts from remote chains is present.
+[EIP-4444][eip-4444] will eventually provide a solution for making historical receipts available without
+needing to execute increasingly long chain histories.
 
-This will be fixed in the future.
+[eip-4444]: https://eips.ethereum.org/EIPS/eip-4444

specs/interop/verifier.md

@@ -19,48 +19,16 @@
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
-## Derivation Pipeline
+## Driver
 
-The derivation pipeline enforces invariants on safe blocks that include executing messages.
-
-- The executing message MUST have a corresponding initiating message
-- The initiating message that corresponds to an executing message MUST come from a chain in its dependency set
-- A block MUST be considered invalid if it is built with any invalid executing messages
-
-Blocks that contain transactions that relay cross domain messages to the destination chain where the
-initiating transaction does not exist MUST be considered invalid and MUST not be allowed by the
-derivation pipeline to be considered safe.
-
-There is no concept of replay protection at the lowest level of abstractions within the protocol because
-there is no replay protection mechanism that fits well for all applications. Users MAY submit an
-arbitrary number of executing messages per initiating message. Applications MUST build their own replay
-protection mechanisms if they are interacting with the lowest level abstractions.
-
-Blocks that contain invalid executing messages are considered invalid by the protocol. The derivation
-pipeline will never promote them from being `unsafe`. A block that contains invalid executing messages
-MUST be replaced by a deposits only block at the same block number.
-
-### Depositing an Executing Message
-
-Deposit transactions (force inclusion transactions) give censorship resistance to layer two networks.
-The derivation pipeline must gracefully handle the case in which a user uses a deposit transaction to
-relay a cross chain message. To not couple preconfirmation security to consensus, deposit transactions
-that execute cross chain messages MUST have an initiating message that is considered [safe](#safety) by the remote
-chain's derivation pipeline. This relaxes a strict synchrony assumption on the sequencer
-that it MUST have all unsafe blocks of destination chains as fast as possible to ensure that it is building
-correct blocks.
-
-If a deposit transaction references an initiating transaction that is not yet safe or does not exist,
-it MUST be dropped by the derivation pipeline.
-
-This inclusion property prevents a class of attacks where the user can trick the derivation pipeline
-into reorganizing the sequencer.
+The driver is responsible for validating L2 blocks and promoting them from unsafe
+to safe. A series of invariants are enforced before promotion.
 
 ### Safety
 
-Safety is an abstraction that is useful for reasoning about security. It should be thought about
-as a spectrum from `unsafe` to `finalized`. Users can choose to operate on information based on its
-level of safety depending on their risk profile and personal preferences.
+Safety is an abstraction that is useful for reasoning about the security of L2 blocks.
+It is a spectrum from `unsafe` to `finalized`. Users can choose to operate on L2 data
+based on its level of safety taking into account their risk profile and personal preferences.
 
 The following labels are used to describe both inputs and outputs:
 
@@ -143,41 +111,3 @@ messages is verified instead of verifying possible executing messages before
 inclusion.
 
 ## Security Considerations
-
-### Forced Inclusion of Cross Chain Messages
-
-The design is particular to not introduce any sort of "forced inclusion" between L2s. This design space introduces
-risky synchrony assumptions and forces the introduction of a message queue to prevent denial of service attacks where
-all chains in the network decide to send cross chain messages to the same chain at the same time.
-
-"Forced inclusion" transactions are good for censorship resistance. In the worst case of censoring sequencers, it will
-take at most 2 sequencing windows for the cross chain message to be processed. The initiating transaction can be sent
-via a deposit which MUST be included in the source chain or the sequencer will be reorganized at the end of the
-sequencing window that includes the deposit transaction. If the executing transaction is censored, it will take
-another sequencing window of time to force the inclusion of the executing message per the
-[spec][depositing-an-executing-message].
-
-[depositing-an-executing-message]: #depositing-an-executing-message
-
-#### What if Safety isn't Enough?
-
-It is possible that small latency differences may impact the allowance of deposited executing messages
-if the rule is that the initiating message is safe. A more strict invariant may be introduced:
-
-```text
-identifier.timestamp + sequencer_window <= block.timestamp
-```
-
-This says that a sequencer window must elapse before the initiating message can be referenced
-in an executing message.
-
-### Reliance on History
-
-When fully executing historical blocks, a dependency on historical receipts from remote chains is present.
-[EIP-4444][eip-4444] will eventually provide a solution for making historical receipts available without
-needing to require increasingly large execution client databases.
-
-It is also possible to introduce a form of expiry on historical receipts by enforcing that the timestamp
-is recent enough in the `CrossL2Inbox`.
-
-[eip-4444]: https://eips.ethereum.org/EIPS/eip-4444