The leader schedule of an honest chain

The represented chain grows by one block per active slot. A different data type would represent a leader schedule in which leaders do not necessarily extend the block from the previous active slot.

INVARIANT: at least one active slot

The argument of uniformTheHonestChain and the output of checkHonestRecipe

• base the type-level name of the top-level timeline
• hon the type-level name of the honest chain's slot interval

TODO: Rename to CheckedHonestSchemaSpec

The argument of checkHonestRecipe'

Checks whether the given HonestRecipe determines a valid input to uniformTheHonestChain

A ChainSchema that satisfies checkHonestChain

This generator proceeds in three stages to create a random schema that satisfies the requirement of at least k+1 blocks in every s slots.

• It begins by drawing a sample of length Len from the Bernoulli process induced by the active slot coefficient Asc, just like in Praos. (IE Len many i.i.d. samples from Uniform(asc)).
• It then visits the first window in that sampled vector. If it has less than k+1 active slots, the generator randomly toggles empty slots to be active until the window contains exactly k+1 active slots.
• It then visits the rest of the windows in oldest-to-youngest order. Each window must contain at least k active slots when visited, since it shares all but its youngest slot with the previous window, which was already visited. In particular, when the window contains only k active slots, that youngest slot must be empty, and so the generator will toggle it, thereby re-establishing the required density.

NOTE: This process may add more active slots to the initial sampled vector than strictly necessary---ensuring the minimum number of toggles would be an integer programming optimization problem as far as we can tell. We have settled for this relatively simple algorithm that approaches the minimal number of toggled slots (TODO calculate how tight the bounds are).

NOTE: When visting windows after the first, only the youngest slot can be toggled. If we activated any other slot in the sliding window, then older windows, which already have at least k+1 active slots, would unnecessarily end up with even more active slots.

NOTE: The larger Asc is, the more active slots there will be when sampling from the Bernoulli process. When Asc is much larger than (k+1)/s the sample will require toggling very few additional slots.

NOTE: When no Asc value is provided, we start with a vector with no active slots, and the second phase causes the first window to end up with k+1 active slots in a pattern that is then repeated exactly for the rest of the chain. For instance,

k=2, s=6

000000000000000000000000 -- stage 1
1 11                     -- stage 2
      1 11  1 11  1 11   -- stage 3
101100101100101100101100 -- final

k=2, s=6

000000000000000000000000 -- stage 1
   111                   -- stage 2
         111   111   111 -- stage 3
000111000111000111000111 -- final

NOTE: When Asc is close to 0, the sample will have a few active slots. In the relatively common case where none of those initially active slots are in the same window, the final schema will be periodic between the active slots from the sample, but the patterns in those intervals may vary. For instance,

k=2, s=6

000000000000010000000000000000001000000000000000000 -- stage 1
1 1 1                                               -- stage 2
      1 1 1 1   1 11  1 11  1 11    111   111   111 -- stage 3
101010101010110010110010110010111000111000111000111 -- final

TODO sample from a disjunction of generators that explore interesting boundary conditions. i.e. different windows could use different strategies to fill each of the windows. For instance, we could arrange for some windows to start with empty slots and be dense at the end.

A stability window

Check the Extended Praos Chain Growth assumption

Definition of window and anchored window. A window is a contiguous sequence of slots. A window anchored at a block starts with the slot immediately after that block.

Definition of Extended Praos Chain Growth Assumption. We assume the honest chain contains at least k+1 blocks in every window that contains s slots.

Definition of Stability Window. The s parameter from the Praos Chain Growth property. (At the time of writing, this is 2k during Byron and 3k/f after Byron on Cardano mainnet.)