|
|
|---|
|
|
|
|---|
Invariant that correct validators calculate the same committees: definition, and proof that it is implied by other invariants.
In the definition of the labeled state transition systems, each validator calculates the (active) committee at each round using its own copy of the blockchain. If blockchains do not fork, then any two correct validators that can both calculate an active committee at a round, will in fact compute the same active committee at that round.
Here we formulate this invariant, and we prove that it is a consequence of the invariant that blockchains do not non fork. We also need the already proved invariant that rounds in blockchains are even and strictly increasing.
If the blockchains of two validators do not fork, either the two blockchains are equal or one extends the other: see nonforking-blockchains-p and lists-noforkp. If the two blockchains are equal, clearly the same committees are calculated from them. If one is an extension of the other, they will still agree on the committees that they both calculate, because those are based only on the the blocks that are common to the two blockchains. The longer blockchain can calculate more committees (at later rounds), but the invariant that we prove here only concerns the committees that both blockchains can calculate.
Our proof fleshes out the details of the argument sketched above, which require some care. The interesting case for the proof is that of a longer blockchain that extends a shorter blockchain, since the case of two equal blockchains is easy. The calculation of the two committees can be rephrased in terms of a trimming operation applied to the blockchains. We define the trimming operation to remove the blocks that are not needed to calculate the (bonded) committee at a given round. Our rephrased calculations of the two committees trims the blockchains not quite at the round for the committee, but at the even round after the last round of the shorter blockchain, which is also the smallest round of the blocks that extend the shorter blockchain to become the longer blockchain (this may be clearer looking at the actual formulas). We show that trimming the shorter blockchain does not change it, and that trimming the longer blockchain yields exactly the shorter blockchain. Thus the two calculations have been reduced to be on equal blockchains, and therefore they must return the same committees. This is all for bonded committees, but the same easily follows for active committees, which are defined in terms of bonded committees.
Here we define the invariant, and we prove that is is implied by other invariants. Elsewhere we prove that this invariant holds in every reachable state.