Dag-committees
Invariant that every author of every certificate in every DAG
is a member of the active committee for that round,
which the validator can calculate.
When a new certificate is created via create,
the author must know the active committee at the certificate's round,
which it uses to check quorum conditions;
these conditions include the fact that
the author is a member of that committee.
When a certificate is stored via store,
the validator must know the active committee at the certificate's round,
which it uses to check quorum conditions;
these conditions include the fact that
the author of the certificate is a member of that committee.
The above events are the only ones that extend DAGs.
Thus, it is the case that the active committee
at the round of each certificate in the DAG of a validator
is known to (i.e. calculable by) the validator,
and that the author of that certificate is in that committee.
Subtopics
- Dag-committees-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Dag-committees-p
- Definition of the invariant:
for every certificate in the DAG of a validator,
the validator can calculate the active committee
at the round of the certificate,
and the certificate's author is a member of the that committee.
- Dag-committees-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- Dag-committees-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
