Signer-quorum
Invariant that each certificate in the DAG of a validator
has signers that form a quorum in the committee.
For each such certificate in the DAG of a validator,
the signers form a quorum in the committee for the certificate round
(which the validator can calculate, as proved in dag-committees);
we prove this invariant here.
There are two possible ways in which a validator's DAG is extended.
One is when the validator authors the certificate,
and adds it to the DAG (besides broadcasting it to other validators).
A create event is only possible if
the signers form a quorum in the committee calculated by the author,
which therefore maintains the invariant.
The other way in which a DAG is extended is when
a validator moves it to the DAG from the buffer;
in this case, a store event is possible
only if the 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 certificate
in the DAG 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.
