Accepted-certificate-committee
Invariant that validators know
the active committees at the rounds of their accepted certificates.
When a new certificate is created via create-certificate,
the author must know the active committee at the certificate's round,
which it uses to check quorum conditions.
When a certificate is received via receive-certificate,
the receiver must know the active committee at the certificate's round,
which it uses to check quorum conditions.
The above events are the only ones that extend
the set of certificates accepted by a validator.
Thus, it is the case that the active committee
at the round of each certificate accepted by a validator
is known to (i.e. calculable by) the validator.
Subtopics
- Accepted-certificate-committee-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Accepted-certificate-committee-p
- Definition of the invariant:
for every certificate accepted by a validator,
the validator can calculate the active committee
at the round of the certificate.
- Accepted-certificate-committee-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- Accepted-certificate-committee-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
