|
|
|---|
|
|
|
|---|
Invariant that committed anchors do not fork: definition, establishment, and preservation.
This is most of what is needed to show the non-forking of blockchains, given that, as proved elsewhere, the blockchain in each validator is determined by the anchors committed so far.
The non-forking of anchors could be proved from existing invariants, but if we did that, the final proof by induction would not work. Recall that we need to prove non-equivocation and blockchain non-forking simultaneously by induction, as discussed in unequivocal-dags-def-and-init and nonforking-blockchains-def-and-init. If we just proved the non-forking of anchors from existing invariants, which include non-equivocation, which depends on blockchain non-forking, and then proved non-forking of blockchains from non-forking of anchors, things would be circular, and not in the way that works with induction. Thus, here we prove the non-forking of anchors by showing that it is established in the initial states and it is preserved by all transitions.
Initially no anchors are committed, so clearly there is no forking.
The only kind of events that changes the committed anchors
is
Here we define the invariant, we prove that it holds in all initial states, and we prove that it is preserved by all transitions. Elsewhere we prove that the invariant holds in every reachable state.