|
|
|---|
|
|
|
|---|
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 committees evolves. The agreement on the blockchains of the validators also provides an agreement on how the committee evolves, as proved in same-committees.
In our model a committee consists of a non-empty set of validator addresses. We introduce a fixtype to wrap that, to enforce non-emptiness, and also for greater abstraction and extensibility.
Membership in a committee is simply set membership, but we introduce a slightly more abstract operation for that, also for future 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 might affect the correctness properties, so we will need to be careful about the choice.
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, and that is what most directly may affect the correctness properties.
Here we define both notions, of bonded and active committee. We might need to revise them slightly as we investigate the correctness properties.
Committees are not explicit components of the system states, but they are in a way derived components of validator states.