|
|
|---|
|
|
|
|---|
Leader elections.
Each even round has a deterministically chosen leader among the validators that form the active committee at that round. If all validators agree on the committee at that round, which we prove elsewhere, then they choose the same leader. Given this common leader, each validator uses the certificates at the immediately following odd round to carry out an election of that chosen leader: each certificate that references the leader certificate adds its stake to the `yes' vote, while each certificate that references a different certificate adds its stake to the `no' vote. Thus these `yes' and `no' votes are amounts of stake. If the validator has enough `yes' vote stake, which implies that it must have the leader certificate itself, which is called an `anchor', then the validator commits that anchor, and potentially other precededing anchors, generating blocks from them; this is formalized elsewhere.
Here we formalize the choice of the leader, via a constrained function on committees and round numbers. We also formalize the counting of the voting stake.