|
|
|---|
|
|
|
|---|
Committees.
Dynamic committees are one of the most distinctive features of AleoBFT. Starting with a genesis (i.e. initial) committee, validators join and leave the committe, by bonding and unbonding, which happens via transactions in the blockchain. Since every validator has its own view of the blockchain, it also has its own view of how the committee evolves. The agreement on the blockchains of the validators also provides an agreement on how the committee evolves, as proved elsewhere.
In our model a committee consists of a finite map from validator addresses to their bonded stake, the latter expressed as a positive integer whose exact units are irrelevant (cf. transaction). We introduce a fixtype to wrap the finite map, for greater abstraction and extensibility.
The genesis committee is arbitrary, but fixed for each execution of the protocol. Thus, we model the genesis committee via a constrained nullary function that returns the genesis committee. The genesis committee is globally known to all validators.
Each validator's view of the evolution of the committee is formalized via functions that operate on the blockchain, and that, starting with the genesis committee, calculate the committee at every block, by taking into considerations bonding and unbonding transactions. Blocks are produced at, and are associated with, (a subset of the) even rounds of the DAG. The notion of interest is that of the committee at a round, but this actually specializes into two notions, because of the committee lookback approach of AleoBFT.
One notion is that of the committee bonded at each round, i.e. the committee resulting from applying all the bonding and unbonding transactions up to that round to the genesis committee in order. There are actually two possible choices for defining this notion precisely, based on whether the committee bonded at an even round that has a block includes or excludes the transactions in that block. That is, do we consider the committee resulting at the end of that block to be the committee at that even round, or at the odd round that follows? The exact choice should not actually matter to correctness: so long as committees are used consistently, the two key intersection arguments for correctness, namely quorum intersection and successor-predecessor intersection, should work fine either way.
The other notion is that of the committee active at each round, i.e. the committee that is in charge of that round. This is the lookback committee: it is the bonded committee at a fixed number of previous rounds (``lookback''). The choice of when a bonded committee starts vs. ends discussed above affects the choice of when an active committee starts vs. ends.
Committees are not explicit components of the system states, but they are, in a way, derived components of validator states.