|
|
|---|
|
|
|
|---|
Invariant that blockchains do not fork: definition and establishment.
Each (correct) validator has its own view (i.e. copy) of the blockchain, but the protocol guarantees that these views are consistent: that is, the blockchains never fork. One may be a prefix of another at times, but they never evolve in different directions. This is the most important property of the protocol, namely that, being a consensus protocol for a blockchain, it does indeed reach consensus on the blockchains.
Blockchains clearly do not fork in the initial state, because all blockchains are empty in the iniital state.
The preservation of this invariant relies on another invariant, namely that DAGs are unequivocal across validators. This is defined in unequivocal-dags-def-and-init, where it is also explained how that and this invariant are inter-dependent and must be proved together in the induction.
Similarly to unequivocal-dags-def-and-init, here we define the invariant, and we also prove that it holds in the initial states.