Signed-previous-quorum
Invariant that each certificate signed by a correct validator
has references to previous certificates
that form a non-zero quorum in the committee for the previous round,
as calculated by that signing validator,
unless the round is 1,
in which case there are no references to previous certificates.
This invariant is expressed on
the set of certificates signed by a correct validator,
as returned by signed-certs.
The invariant is satisfied by every certificate in that set,
with respect to (the state of) the signing validator.
When a new certificate is created via a create event,
that event's preconditions require that the certificate includes
a non-zero quorum of references to certificates in the previous round,
unless the certificate round is 1,
in which case there must be no references.
As proved in signed-certs-of-next,
the only kind of events that changes signed-certs is create.
All the other kinds of events leave the set unchanged,
and thus the invariant is preserved.
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.
The names do not mention the `non-zero' requirement either,
but the quorum aspect is the main one here.
Subtopics
- Signed-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-signed-previous-quorum-p
- Check if either a certificate has round 1
and it has no references to previous certificates,
or the round is not 1 and
the certificate's references to previous certificates
are in the committee for the round just before the certificate round
and form a non-zero quorum in that committee,
where the committee is calculated by a validator
(represented by its state).
- Signed-previous-quorum-p
- Definition of the invariant:
for each certificate signed by each correct 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 non-zero quorum in the committee of
the preceding round of the certificate.
- Signed-previous-quorum-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
- Signed-previous-quorum-p-of-events-next
- Preservation of the invariant by multiple transitions.
- Signed-previous-quorum-p-when-reachable
- The invariant holds in every reachable state.
