Dag-previous-quorum-def-and-init-and-next
Invariant that each certificate in a DAG
has references to previous certificates
that form a non-zero quorum in the committee for the previous round,
unless the round is 1,
in which case there are no references to previous certificates:
definition, establishment, and preservation.
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.
When a certificate is stored into the DAG via an accept event,
the validator checks that the certificate is signed by a quorum.
Under fault tolerance assumptions,
that quorum must contain at least one correct validator,
which must have signed the certificate only if
the references to previous certificates
form a non-zero quorum
(in the previous committee of the certiicate's round).
Under the invariant that validators agree on committees
(see same-committees-def-and-implied),
the correct signer and the storing validator
agree on the committee, and thus on the stake requirement.
Thus, all the certificates in a validator's DAG satisfy the invariant.
The other events do not modify DAGs.
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.
Here we define the invariant,
we prove that it holds in all initial states,
and we prove that it is preserved by all transitions.
Elsewhere we prove that
the invariant holds in every reachable state.
Subtopics
- Dag-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-dag-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).
- Dag-previous-quorum-p
- Definition of the invariant:
for each certificate in the DAG of each 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.
- Dag-previous-quorum-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
