|
|
|---|
|
|
|
|---|
Invariant that blockchains do not fork: preservation.
As discussed in nonforking-blockchains-def-and-init, the preservation of blockchain non-forking is proved separately from its definition and establishment proof, as done for certificate non-equivocation (see unequivocal-accepted-certificates-def-and-init and unequivocal-accepted-certificates-next), due to the need for simultaneous induction. Although it would be possible to prove the non-forking of blockchains from other invariants, particularly the non-forking of anchors, some of these invariants depend on blockchain non-forking, so this would not work for a proof by induction. Instead, as also done for anchors non-forking (see nonforking-anchors), we need to prove the preservation of blockchain non-forking from old state to new state.
In nonforking-blockchains we prove that the invariant holds in every reachable state.