|
|
|---|
|
|
|
|---|
Transitions for certificate acceptance.
Here we define the system state changes caused by
When the network contains a certificate message addresses to a correct validator, that validator can accept the certificate, i.e. add it to its DAG, provided that it already has, in its DAG, all the previous certificates referenced by the certificate, in order to keep the DAG backward-closed, which is an invariant, as proved elsewhere. Additionally, and critically, the validator needs to check that the signers of the certificate (i.e. author and endorsers) form a quorum in the active committee of the certificate's round.
The accepting validator does not need to perform other checks on the proposal contained in the certificate, which in our model only involves the checks on the authors of the previous certificates. This is because, as proved elsewhere, by checking the quorum of signaures, this validator may rely on at least one correct validator to have performed those checks. Note that the validator accepting a certificate is never the author (because the author immediately adds it to the DAG) and may or may not be an endorser.
Note that a certificate may be accepted by any validator in the system, not only validators in the committee. This is part of our way of modeling syncing, explained in system-states.
In an implementation, the validator would receive the message, removing it from the network, prior to checking the various condition. If the signature quorum check fails, the validator would discard the message; in our model, the message just sits in the network forever (we could easily add an event to remove that message from the network). If not all the previous referenced certificates are present in the DAG, the validator would buffer the certificate, adding it to the DAG if and when all the previous certificates are there; in our model, the message sits in the network until then, so in a way our network models not just the actual network, but also some validator buffers (we could easily extend our model with explicit buffers, but it makes no real difference).