Documentation

The active slot coefficient

INVARIANT: 0 < x < 1

It's as precise as Double, which likely suffices for all of our needs.

The Δ parameter of the Praos theorems and so also of the Praos Race Assumption

ASSUMPTION: If an honest block b is minted at the start of slot x, then every (healthy) honest node will have selected a chain no worse than b by the onset of slot x + Δ + 1.

NOTE: If Δ=0, then the best block minted in each slot is selected by every (healthy) honest node before the onset of the next slot.

NOTE: If the honest block k+1 after its intersection with an alternative chain was minted in slot x, then the alternative block k+1 after the intersection can be minted no sooner than slot x + Δ + 1. Thus x + Δ is the youngest slot in the Praos Race Window.

The k parameter of the Praos Common Prefix property

Also known as the SecurityParam.

The maximum length of any leader schedule

This can be interpreted as the end of time, the final moment simulated during a test.

The s parameter of the Praos Chain Growth property

Also known as the width of the stability window. In particular, we assume that an adversarial stake holder cannot drastically increase their rate of election until at least s many slots after the first block on an adversarial chain.

In other words: we're assuming that any serious attempt to corrupt the leader schedule would be isolated to a private adversarial chain.

PRECONDITION: the bits aren't all the same

The Asc that equals the fraction w / 2^widthW.

Interpret Asc as a Double