|
|
|---|
|
|
|
|---|
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 they will do in same-committees, then they will choose the same leader. Given this common leader, each validator uses the certificates they receive in the immediately following odd round to carry out an election of that chosen leader: each following odd-round certificate that references the leader certificate counts as a `yes' vote, while each following odd-round certificate that does not reference the leader certificate counts as a `no' vote. If a validator has the leader certificate and has enough `yes' votes, that certificate becomes an anchor (see anchors). The validator commits that anchor, and potentially other preceding anchors, by generating blocks from them; but 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 `yes' and `no' votes.