|
|
|---|
|
|
|
|---|
Invariant that correct validators have the same associated certificates.
The notion of associated certificates is formalized in associated-certificates. Each validator has certificates in its DAG and buffer, but there may be also messages in the network addresses to the validator, which can therefore be eventually received by the validator: all of these certificates are (actually or potentially) associated to the validator.
An invariant of the protocol is that validators always have the same set of associated certificates. Their DAGs and buffers may have (together) different certificates, but there will be messages in transit that ``fill the gap''. This is a consequence of our reliable broadcast model, in which a certificate's author broadcasts the certificate to all correct validators, except possibly itself if correct (because in that case the certificate is immediately added to the DAG). DAGs and buffers may also individually differ across validators, but their union, together with the messages in the network, are always the same.
Initially there are no certificates,
so every validator has the empty set associated to it.
The only kind of event that changes the set is