# New inboxes

## Specification of an infinite inbox with SOL/EOL

Given $\mathbb{M}$ a set that aims to represent messages, we define $\mathbb{M}^{\dagger}$ as:

$$\mathbb{M}^{\dagger} = \mathbb{M} \sqcup \mathrm{SOL} \sqcup \mathrm{EOL}$$

where $\sqcup$ represents the disjoint union.

An inbox is defined as a function $\mathcal{I} : \mathbb{N} \times \mathbb{N} -> \mathbb{M}^{\dagger}$ such that:

- $\mathcal{I}(l,i) = \mathrm{EOL} \Leftrightarrow \forall j, j< i, \exists m', \mathcal{I}(l,j) = m'$
- $\mathcal{I}(l,0) = \mathrm{SOL}$

with $l$ a block level, and $i$ is the message position.

Consequently, a function $\mathrm{size_{\mathcal{I}} : \mathbb{N} \to \mathbb{N}}$ can be defined such that

$$\mathrm{size_{\mathcal{I}}}(l) = i \text{ such that } \mathcal{I}(l,i) = \mathrm{EOL}$$

If the inbox can be inferred from the context, we will just note $\mathrm{size}(l)$.

We also define the set $\mathrm{Dom}(\mathcal{I}) = \{(l,i) \mid \exists m \in \mathbb{M}^{\dagger}, \mathcal{I}(l,i) = m\}$.

For the refutation game, we need to prove that the successor of a message is part of the inbox. A naive definition for the successor could be the function $\mathcal{S} : \mathbb{N} \times \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ such that

- $\mathcal{S}(l,i) = (l,i+1) \Leftrightarrow
i < \mathrm{size}_{\mathcal{I}}(l)$
- $\mathcal{S}(l,i) = (l+1,0) \Leftrightarrow i = \mathrm{size}_{\mathcal{I}}(l)$

Note that there is a nice property with this definition which is:

- $(l,i) \in \mathrm{Dom}(\mathcal{I}) \Leftrightarrow \mathcal{S}(l,i) \in \mathrm{Dom}(\mathcal{I})$ $(1)$

The specification of the refutation game for the inbox is given $(l,i)$, to write to functions $\mathrm{prove}$ and $\mathrm{verify}$ such that:

- $\mathrm{prove}(l,i) = (m,p)$ where $m \in \mathcal{M}^{\dagger}$
- $\mathrm{verify}((l,i),p) = m$

such that:

$$\forall l, \forall i, \forall m, \forall p, \mathrm{prove}(\mathcal{S}(l,i))=(m,p) \Leftrightarrow \mathrm{verify}(\mathcal{S}(l,i),p) = m$$

This has the consequence that $\mathrm{prove}$ and $\mathrm{verify}$ functions are properly defined only on $\mathrm{Dom}(\mathcal{I})$

As a consequence, and because of $(1)$, this property is the same as:

$$\forall l, \forall i, \forall m, \forall p, \mathrm{prove}(l,i)=(m,p) \Leftrightarrow \mathrm{verify}((l,i),p) = m$$

It is not reasonable in practice to work with infinite inboxes. Instead, an inbox is always finite with an upper bound. Moreover, the starting point of an inbox is not always the level $0$.

## Finite inboxes

Because a commitment will commit only a finite number of level and that the data-structure associated

A finite inbox can be represented as a $3-$uples: $(\mathcal{I},l_s,l_e)$ such that:

- $\mathcal{I}$ is an infinite inbox
- $\forall l, \forall i, l < l_s \Rightarrow \mathcal{I}(l,i) = \bot$ (it is undefined)
- $\mathcal{I}(l_s,1) = \mathrm{EOL}$
- $\forall l, l > l_e \Rightarrow \mathcal{I}(l,0) = \mathrm{SOL}$

Consequently, we can define the domain of a finite inbox as
$$\mathrm{Dom_f}(\mathcal{I,l_s,l_e})= \mathrm{Dom(\mathcal{I}) \cap \{(l,i)} \mid l > l_s \land l \leq l_e\}$$

The function $\mathcal{S}$ is not longer stable over the domain $\mathrm{Dom_f}$. This is one difficulty we identified in the current implementation.

A second issue is the base case. In this formalisation, we requires the first level of a finite inbox to be empty. This trick allows to simplify cases, in particular to get rid off the $\mathrm{Initial}$ constructor. In the context of SCORU, this means that the input state after initialisation will be $\mathrm{First\_after}(l_s,0)$.

To recover the property that proving and verify a message in the inbox is the same as proving and verify the successor of a message in the inbox, we can just extend the domain of the finite inbox:

$$\mathrm{Dom_f^+}(\mathcal{I,l_s,l_e})= \mathrm{Dom_f(\mathcal{I},l_s,l_e)}\cup \{(l_e+1,0)\}$$

Consequently $\mathcal{S} : \mathrm{Dom_f(\mathcal{I},l_s,l_e)} \to \mathrm{Dom_f^+(\mathcal{I},l_s,l_e)}$, and we will define $\mathrm{prove}$ and $\mathrm{verify}$ on $\mathrm{Dom_f^+}(\mathcal{I},l_s,l_e)$.

:::info
In practice, $l_s$ will be the level for which the rollup was originated, while $l_e$ will be the commitment level.
:::

## How to integrate those ideas into the current code

### Get rid of `Initial` constructor

As mentioned above, it seems that the particular case for `Initial` could be removed by forcing the inbox of the original level to be empty and containing the single but implicit message $\mathrm{EOL}$. Considering that such inbox exists or not, this will be already the case. We could also ensure that from the level of activation of SCORU, there is a new inbox that will be populated by SOL/EOL messages.

This design forbids rollup originations at level $0$.

### Inbox proof

A major change in this design, is that it will be the responsibility of the rollup node to compute the successor of a pair $(l,i)$. The code producing the proof does not need to find the next message. Looking for the successor becoming trivial with SOL/EOL.

For example, assume the level $5$ contains $3$ messages and the level $6$ contains $1$ message. Right now, calling the function $\mathrm{prove}$ with parameters $(5,10)$ is equivalent to calling it with parameters $(6,0)$. In the formalism proposed here, calling this function with $(5,0)$ will simply produce an error.

### How to prove $\mathrm{SOL}$

Assume we want to prove that the next message at level $l+1$ is $\mathrm{SOL}$, then we only need to prove that the message at level $l$ for some position $i$ is $\mathrm{EOL}$.

The proof of such message does not need to be *implicit* because if we have only one inbox, this message will be added by the protocol during the block finalisation.

### How to prove $\mathrm{EOL}$

Proving $\mathrm{EOL}$ is the message as proving any other message of the inbox.

### Cutting the inbox

Cutting the inbox is not needed anymore:
- There is no message for level $l\leq l_s$
- There is no message for level $l > l_e$

By definition, the next message after $\mathrm{EOL}$ at level $l_e$ is $\mathrm{SOL}$ at level $l_e+1$.