|
|
|---|
|
|
|
|---|
Invariant that correct validators own the same certificates.
The notion of `owned certificates' is formalized in owned-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) owned by the validator.
An important invariant of the protocol is that validators always have the same set of owned 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).
Initially there are no certificates,
so every validator owns the empty set.
The only kind of event that changes the set is