# DAL (Refutation) Proofs in SCORU Refutation

## DAL slots headers and confirmation
- At any L1 level L,
- A list of data slots (up to 256 in mainnet) (encoded with redundancy) is made available on the DAL network;
- Commitments of those slots are sent to L1 as: `{id = {published_level=L; slot_index}; commitment}` via a `Dal_publish_slot_header` operation, where `commitment` is the KATE commitment of the slot's data;
- At level `L+endorsement_lag`, endorsers are supposed to confirm which shards they were able to download from the DAL network;
- Shards are pieces of a slot. The corresponding slot is confirmed on L1 if sufficiently many shards are declared to be available by endorser (so that the full slot could be reconstructed);
- The list of confirmed slots at a given level L (sorted by their indexes) is added into a `slots_history` skip list at block finalization (one slot per skip list cell).
## DAL parameters
We can distinguish
- The parameters used by L1/rollup,
- `endorsement_lag`: which specifies the number of needed blocks before checking if a slot of a published level `PL` is available (default value is `1`, so the check is done at `PL+1`);
- `number_of_slots`: default value for mainnet is `256`;
- `availability_threshold`: default value is `50` on mainnet;
- The crypto parameters: used when encoding slots with redundancy/erasure-code, to verify pages proofs, etc.
- `redundancy_factor`: default value is `16`;
- `page_size` in bytes: default value is `4096`;
- `slot_size` in butes: default value is `1 lsl 20`;
- `number_of_shards` : default value is `2048`.

Note that a `page` is the unit of data fed to a PVM. The number of pages can be computed as `page_size/slot_size`. Its default value on the mainnet is `256`.

## Rollup node, downloading data
One of the roles of the rollup node is to download DAL data from the (DAL) network and save them into its store. Currently (with rollups subscription to DAL slots), given a level `L + endorsement_lag` and its associated block hash `H`, the node will, for each slot `si` of level `L`:
- If the rollup is not subscribed to `si`, ignore it;
- If the rollup subscribed to `si`, then:
- If the slot availability is confirmed, download the slot's data and save the slot's pages under `H` as a primary key and the `(si, page's index)` pair as a secondary key, for each page;
- When the slot is not confirmed to be available, it's considered unavailable forever. In this case, we update the node's store as above. But, instead of saving the pages' content, we record `None` to indicate that the data are unavailable.

## DAL proofs, the basis

Basically, proofs are related to pages confirmation. Given a page, identified by its (full) ID `= {id = {published_level; slot_index}; page_index}`, we want to prove that: either the page is not confirmed (or doesn't exist), or that it's confirmed and its content corresponds to some data. In fact, two (honest) rollup nodes that don't agree on a DAL input page are in one of the two following situations:
- A node interpreted a content of a page (thinking it was confirmed), but the other node didn't (thinking it was not confirmed);
- The two nodes agree that the page is confirmed but interpret two different contents.

A dishonest node can either go further and tries to interpret pages whose levels, slot_indexes or pages_indexes are inconsistents (too big and/or in the future, etc.).

A proof is done w.r.t. a snapshotted version of the `slots_history` skip list on L1, that contains the history of confirmed slots (Actually, only the last cell is remembered, but with links to the previous cells). The snapshot is taken at the beginning of the refutation game. The two possible cases are represented by the following OCaml type in the implementation (see more details on the type's definition in src/proto_alpha/lib_protocol/dal_slot_repr.ml):

   type proof =
      | Page_confirmed of {
          target_cell : history;
          inc_proof : inclusion_proof;
          page_data : Page.content;
          page_proof : Page.proof;
        }  (** The case where the slot's page is confirmed/attested on L1. *)
      | Page_unconfirmed of {
          prev_cell : history;
          next_cell_opt : history option;
          next_inc_proof : inclusion_proof;
        }
          (** The case where the slot's page doesn't exist or is not
              confirmed on L1. *)

The type `history` represents the (cells of the) skip list. An `inclusion_proof` is a list `[c1; ...; cn]` of cells that encodes a minimal path from the cell `c1` to the cell `cn` in the skip list. `c1` is typically the snapshotted/reference cell introduced above.

In case of a page confirmation proof, `target_cell` is supposed to contain the (confirmed) slot to which the page identified by `ID` belongs. `Page.content` are bytes. `Page.proof` is a cryptographic proof that the page whose content is `page_data` is part of the slot stored in `target_cell` (at the given page index).

In the case of a page unconfirmation proof, we either have:
- `next_cell_opt` is of the form `Some next_cell`, and
- `prev_cell` and `next_cell` are two consecutive cells in the skip list
- `slot_ID_of_cell prev_cell < ID < slot_ID_of_cell next_cell`

In this case, if one pretends that a page whose ID is surrounded by two consecutive confirmed slots ID in the L1 skip list is confirmed, the unconfirmation proof above contradicts his/her claim. `prev_cell` above could be the genesis cell `zero`, for which no page can be confirmed.

The other case where `next_cell_opt` is `None` means that one is producing a page unconfirmation proof for a page whose slot is above the last confirmed slot in the snapshotted skip list. In this case, `prev_cell` is necessarily equal to the snapshotted skip list/cell.

Two functions, called `produce_proof` and `verify_proof`, are implemented in src/proto_alpha/lib_protocol/dal_slot_repr.ml to produce pages confirmation/unconfirmation proofs as explained above, and to verify proof validity, respectively.

## Extending PVM_sig to plug DAL in PVMs

Enabling DAL in SCORU PVMs is as simple as extending the kind of inputs that can be provided. We now have a `Dal_page of Dal_slot_repr.Page.content option` case to provide `Some data` or `None` for, respectively, confirmed or unconfirmed pages in `reveal_data` datatype.

type reveal_data =
  | Raw_data of string
  | Metadata of Sc_rollup_metadata_repr.t
  | Dal_page of Dal_slot_repr.Page.content option

type input = Inbox_message of inbox_message | Reveal of reveal_data

Also, we extend the `reveal` datatype with a `Request_dal_page of Dal_slot_repr.Page.t` case to allow PVMs requesting pages (that are fully identified by the publication level, their slot index, and their position in the slot).

type reveal =
  | Reveal_raw_data of Input_hash.t
  | Reveal_metadata
  | Request_dal_page of Dal_slot_repr.Page.t

type input_request =
  | No_input_required
  | Initial
  | First_after of Raw_level_repr.t * Z.t
  | Needs_reveal of reveal

## Extending Arith PVM
We can do better and simpler once EOL/SOL is merged. But, for the moment, the PVM Arith's syntax is extended to accept inbox messages of the form

dal:<level>:<slot_index>:<page_index>

The intended semantics of this directive is to request the DAL page `page_index` published at level `level` and belonging to slot `slot_index`.

Additional checks are performed on the arguments of this directive, which requires some of the DAL parameters. Currently, the following DAL parameters (those of `test` in default_parameters.ml) are hard-coded in the Arith PVM. But, there is an open issue to provide these parameters dynamically via rollups metadata:

    let endorsement_lag = 1l in
    let page_size = 4096 in
    let slot_size = 65536 in
    let number_of_slots = 16 in
    let number_of_pages = slot_size / page_size in

These parameters are used for the following checks:
- `0 <= slot_index < number_of_slots`;
- `0 <= page_index < number_of_pages`;
- `1 < current_PVM_level - level < endorsement_lag`.

The conditions on `slot_index` and `page_index` are straightforward. The `level` check will become much simpler with EOL. In the check above, we forbid pages of levels that are in the future or very old. `current_PVM_level` refers to the level in which the directive `dal:xx:yy:zz` is included in the rollup's inbox.

**NB.**
> Actually, `1 < current_PVM_level - level` should probably be `0 < current_PVM_level - level`. But the way data are currently fetched by the rollup node, and the way inbox messages are interpreted, combined with Tenderbake finality, causes the Dal test to fail if `0` is chosen as a lower bound. This needs to be investigated afterward.

If one of the conditions above is not met, the PVM stops evaluating the directive and moves to a state where it waits for the next inbox messages. In case the checks succeed, it requests the DAL page identified by `{id = {published_level=level; slot_index}; page_index}`.

On the rollup side, and when receiving a request to fetch the content of a page `{id = {published_level=level; slot_index}; page_index}`, the `interpreter` does the following:
- It computes the level at which the page is supposed to be confirmed (i.e., `CL = published_level + endorsement_lag`);
- It retrieves the hash `H` corresponding to level `CL`;
- It retrieves from the store the content of the DAL under the primary key `H` and secondary key `(slot_index, page_index)`. It is returned if an entry is found in the store (either `None` or `Some data`). Otherwise, it fails with `"The rollup node didn't fetch page %a (yet)."`. Indeed, the rollup node is supposed to have already updated the appropriate DAL entries in the store under the block hash `H` (since the PVM only accepts a `level` if `current_PVM_level - level`).

## Plugging DAL proofs in SCORU proofs

For the integration, we assume that the DAL parameters are fixed forever (a follow-up issue has been created to relax this assumption). The integration is immediate. It remains to add the `Dal_page` and `Request_dal_page` cases in the existing code and to call DAL functions `verify_proof` and `produce_proof` at the right places.

**But, However, But!!** there is an extra but important check (somehow similar to `cut_level` function of inbox proofs) that needs to be added. In fact, basic DAL `produce/verify` proofs functions are not aware of rollup origination level or refutation game's starting level or commitment's level.

**In summary,**
- we accept to produce or verify a DAL proof only if the page's ID is not too recent or too old.

**In more detail,**

- If a page's level is not after the origination level, we should not call DAL `produce/verify` proofs at all;
- Similarly, if the refutation game started for a `commitment` whose `commit_level`(aka. `inbox_level`, see src/proto_alpha/lib_protocol/sc_rollup_commitment_repr.mli for its definition) is `L`, we should only accept to `produce/verify` proofs for pages referring to a level smaller than `L-endorsement_lag`.

The boundaries are derived from/explained in the figure below. Before explaining it, let's assume the following scenario:

- A rollup is originated at level 8;
- We assume one commitment per level;
- A commitment after the interpretation of inbox+DAL messages of level 15 is posted at level 17. Field `commit_level` of refutation game's state is `inbox_level = commit_level = 16`;
- Another (different) commitment for level 15 is posted at level 20, and a refutation game is started. field `level_start` of refutation game's state is `20`. The snapshotted skip lists used for inbox and DAL during the game are those updated at level 19 at most.

On the figure, we have:

- The first column is the L1/inbox levels;
- The second column represents the publication of some DAL slot for at the indicated `published_level`;
- The third column shows when each published slot is expected to be confirmed (assuming `endorsement_lag = 3`);
- The last column shows which slots/levels are availabe for the refutation game.


The two boundaries are derived generalized as follows:
- We made the choice that, we only accept slots that are published after the rollup origination. Hense the lower condition to accept a slot/page in the refutation game (otherwise, we cut):

page_published_level > origination_level

- For the upper bound, it appears clear from the figure that we should not accept slots/pages confirmed after level 15. This corresponds to the check (otherwise, we cut):

page_published_level dal_endorsement_lag < commit_level