Previous-quorum
Invariant that each certificate accepted by a validator
has references to previous certificates
that form a quorum in the committee,
unless the round is 1,
in which case there are no references to previous certificates.
When a new certificate is created via a create-certificate event,
that event's preconditions require that the certificate includes
a quorum of references to certificates in the previous round,
unless the certificate round is 1,
in which case there must be no references.
When a certificate is received via a receive-certificate event,
that event's preconditions impose a similar requirement.
Thus, all the certificates accepted by a validator
satisfy that requirement.
Recall that a store-certificate event
does not change the set of accepted certificates;
it just moves a certificate between buffer and DAG.
The names for this invariant,
i.e. this XDOC topic as well as the function and theorem names,
just mention `quorum' for brevity,
even though that does not apply to round 1.
But rounds greater than 1 are the ``normal'' case,
while round 1 is a special case.
Subtopics
- Previous-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-previous-quorum-p
- Check if either a certificate has round 1
or its references to previous certificates
are in the committee for the certificate's round
and form a quorum in that committee,
where the committee is calculated by a validator
(represented by its state).
- Previous-quorum-p
- Definition of the invariant:
for each certificate accepted by a validator,
either the certificate's round is 1
and the certificate has no references to previous certificates,
or the certificate's round is not 1
and the references to previous certificates
form a quorum in the committee of
the preceding round of the certificate.
- Previous-quorum-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- Previous-quorum-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
