Signer-quorum
Invariant that each certificate accepted by a validator
has signers that form a quorum in the committee.
The set of certificates accepted by a validator
is defined in accepted-certificates as
the certificates in the DAG or buffer of the validator.
It is the case that, for each such certificate,
the signers form a quorum in the committee for the certificate round
(which the validator can calculate,
as proved in accepted-certificate-committee);
we prove this invariant here.
There are two possible ways in which a validator accepts a new certificate.
One is when the validator authors the certificate,
and adds it to the DAG (besides broadcasting it to other validators).
For correct validators
(which are the ones we are interested here,
since the notion of accepted certificates is only defined for them),
a create-certificate event is only possible if
the signers form a quorum in the committee calculated by the author,
which maintains the invariant.
The other way in which a validator accepts a new certificate
is by receiving it from the network,
but in this case a receive-certificate event is possible
only if the receiving validator
can calculate the committee for the certificate round
and the signers of the certificate form a quorum in that committee;
that again maintains the invariant.
Subtopics
- Signer-quorum-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Validator-signer-quorum-p
- Check if the signers of a certificate
are a subset of the committee for a certificate's round
and form a quorum in that committee,
where the committee is calculated by a validator
(represented by its state).
- Signer-quorum-p
- Definition of the invariant:
the signers of every accepted certificate of every correct validator
form a quorum in the committee for the certificate's round,
calculated by the validator from its own blockchain.
- Signer-quorum-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- Signer-quorum-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
