# Yet another implementation for EOL

The current implementation [6239](https://gitlab.com/tezos/tezos/-/merge_requests/6239) of EOL is not good because it adds a lot of code in the trusted code-base and is really hard to ensure the correctness.

This document aims to understand the current difficulties and also elaborates a high-level specification for the EOL feature that would lead to an easier implementation. This new specification should also simplifies other parts related to the inbox.

## The problem

### Context

Each rollup maintains an inbox. This inbox is implemented by the protocol via a `skip list` which is a sparse data-structure to represent `L2` messages posted onto the `L1`. (The protocol only keeps the head of this skip-list while the rollup node maintains the whole skip-list. This makes the skip-list off-chain.)

A cell of the skip list is a list of messages posted at some level (i.e. `L1` block) and some metadata. If there is no message for a particular level, there is no cell. Consequently, proving the absence of message at some level $l$ requires to prove the existence of messages at some levels $l_1$ and $l_2$ such that:

- $l_1 < l < l_2$ and
- $pred(cell(l_2)) = cell(l_1)$

The second condition expresses that the predecessor cell at level $l_2$ in the skip list is the cell at level $l_1$.

The EOL feature proposes the addition of a special message $\mathrm{EOL}$ (for `End Of Level`) such that at every level, there is an `implicit` message $\mathrm{EOL}$.

We want to stress that `implicit` is important. Indeed, every message in the inbox is added via an explicit `L1` operation. But this is not the case for `EOL`.

An "easy" solution would be to have the `L1` that adds the $\mathrm{EOL}$ message explicitely into each rollup inbox. This is not reasonable because the complexity of this operation depends on the number of rollups and cannot be charged in gas.

The refutation game must consequently be changed to take into account this message implicitely at the end of the inbox.

### Current solution

The handling of $\mathrm{EOL}$ implicitely in the current code requires to handle several corner cases. Without being exhaustive here, we aim to provide some examples:

- To handle $\mathrm{EOL}$ for a level without messages in the inbox, we must prove there is no message at this level, by providing two non-empty cells of the skip list
- This does not work if those messages are after the last cell of the skip list
- A corner case must be made for the initial message
- Producing a proof is not that easy because proving the EOL message requires to prove the previous message is the last message of the inbox

In the following, we aim to provide a specification that, hopefully, should lead to an easier implementation that will avoid those corner cases.

[^disjoint]: $\sqcup$ is a disjoint union