record_attested_shards ctxt attestation shards records that the list of shards shards were attested (declared available by some attestor). The function assumes that a shard belongs to the interval 0; number_of_shards - 1. Otherwise, for each shard outside this interval, it is a no-op.

register_slot_header ctxt slot_header returns a new context where the new candidate slot have been taken into account. Returns Some (ctxt,updated) where updated=true if the candidate is registered. Some (ctxt,false) if another candidate was already registered previously. Returns an error if the slot is invalid.

candidates ctxt returns the current list of slot for which there is at least one candidate.

is_slot_index_attested ctxt slot_index returns true if the slot_index is declared available by the protocol. false otherwise. If the index is out of the interval 0;number_of_slots - 1, returns false.

shards_of_attestor ctxt ~attestor returns the shard assignment of the DAL committee of the current level for attestor. This function never returns an empty list.

The DAL committee is a subset of the Tenderbake committee. A shard from 0;number_of_shards is associated to a public key hash. For efficiency reasons, the committee is both: a mapping from public key hashes to shards and a mapping from shards to public key hashes. The DAL committee ensures the shards associated to the same public key hash are contiguous. The list of shards is represented as two natural numbers (initial, power) which encodes the list of shards: initial; initial + 1; ... ; initial + power - 1.

This data-type ensures the following invariants:

• \forall pkh shard, find pkh_to_shards pkh = Some (start,n) -> \forall i, i \in start; start + n - 1 -> find shard_to_pkh i = Some pkh

• forall pkh shard, find shard_to_pkh shard = Some pkh -> \exists (start,n), find pkh_to_shards pkh = Some (start,n) /\ start <= shard <= start + n - 1

• Given an attestor, all its shard assignments are contiguous

compute_committee ctxt pkh_from_tenderbake_slot computes the DAL committee using the pkh_from_tenderbake_slot function. This functions takes into account the fact that the DAL committee and the Tenderbake committee may have different sizes. If the DAL committee is smaller, then we simply take a projection of the Tenderbake committee for the first n slots. If the DAL committee is larger, shards are computed modulo the Tenderbake committee. Slots assignments are reordered for a given a public key hash to ensure all the slots (or shards in the context of DAL) shards are contiguous (see committee).

init_committee ctxt committee returns a context where the committee is cached. The committee is expected to be the one for the current level.