|
|
|---|
|
|
|
|---|
Invariant that the set of committed certificates is redundant: definition, establishment, and preservation.
The state of each validator includes the set of all the certificates committed so far; see validator-state. This is useful for defining the state transitions of the system, since the block for each committed anchor contains the transactions in the causal history of the anchor, except for the already committed anchors, whose set is in the state component being discussed here.
However, it turns out that that state component, the set of all committed certificates so far, is redundant, and can be calculated from the other state components. Specifically, it is always equal to the causal history of the last committed anchor, or to the empty set if there is no committed anchor. Here we prove this property, as a system invariant.
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.