|
|
|---|
|
|
|
|---|
Invariant that DAGs are unequivocal: definition and establishment.
In the model of AleoBFT with static committees,
certificates are unequivocal across the whole system,
i.e. all the certificates in the system have
unique combinations of author and round.
With dynamic committees (with or without stake),
this property must be weakened slightly in order to be proved.
The reason is that, in our model, the system always includes
all possible validators that may form committees.
Consider, for simplicity, the first few rounds, and the genesis committee.
Even with the fault tolerance assumptions
formalized in fault-tolerance,
there may well be a set of faulty validators,
outside the genesis committee,
who sign a new certificate that has
the same author and round as an existing certificate,
the latter having been properly created by the genesis committee.
This event is perfectly possible
according to our model of
The non-equivocation of the DAG of a single validator, as expressed by certificate-set-unequivocalp applied to the DAG of the validator, could be proved from some already proved invariants. However, we need the more general non-equivocation of DAGs across multiple validators, namely that if two validators have two certificates (one each) in their DAGs with the same author and round, then they are equal certificates. The latter property is expressed by certificate-sets-unequivocalp applied to the DAGs of the two validators. The property for two validator subsumes the property for one validator, by choosing the two validators to be equal. So there is no point in proving non-equivocation for a single validator, which involves some work, and instead we prove non-equivocation for multiple validators, which we need anyhow, and then we obtain non-equivocation for single validator as a very simple consequence.
However, proving DAG non-equivocation for multiple validators relies on another invariant, namely that blockchains do not fork, which is defined in nonforking-blockchains-def-and-init. The reason is that we need the fact that different validators agree on the active committees at certain rounds; since the active committee is calculated from the blockchain, we need the fact that blockchains do not fork, so that the validators calculate the same committee (for their common blockchain prefixes). In turn, the non-forking of blockchains relies on the non-equivocation of DAG certificates. So the preservation of the two invariants must be proved at the same time by induction, because we need a sufficiently strong induction hypothesis, with both invariants available in the old state, from which we can prove that both invariants also hold on the new state.
Here we define the invariant about unequivocal DAGs (for multiple validators, as explained above), and we also prove that it holds in the initial states. In nonforking-blockchains-def-and-init we do the same for the invariant about non-forking blockchains, i.e. we define it and prove it holds in the initial states. Elsewhere we prove that each invariant holds in the new state if both hold in the old state, and finally we put everything together in an induction proof for both invariants (along with other invariants that are all inter-dependent).