Dags
DAGs.
As defined in validator-state,
we model a DAG as a set of certificates.
Here we introduce operations on DAGs (as certificate sets)
that are more DAG-specific than the operations on certificate sets
defined in certificates.
By `DAG-specific' we mean that take into account the edges of the DAG,
as opposed to treating the DAG as just a set of vertices
as the operations in certificates do.
The edges are represented as the previous component of certificates,
so they are part of the vertices, in terms of data structures.
Subtopics
- Path-to-author+round
- Retrieve the certificate with the given author and round
reachable from a given certificate through the DAG edges.
- Successors
- Set of the certificates in a DAG that
are successors of a certificate in a DAG.
- Certificate-causal-history
- Causal history of a certificate in a DAG.
- Dag-in-committees-p
- Check if the author of every certificate in a DAG
is a member of the committee active at the round of the certificate.
- Paths-in-unequivocal-closed-dags
- Some theorems about paths in unequivocal, backward-closed DAGs.
- Predecessors
- Set of the certificates in a DAG that
are precedessors of a certificate in a DAG.
- Unequivocal-previous-certificates
- Some theorems about
retrieving the previous certificates of a certificate
in unequivocal DAGs.
- Certificate-previous-in-dag-p
- Check if all the previous certificates
referenced by a given certificate
are in a given DAG.
- Certificates-dag-paths-p
- Check if a list of zero or more certificates
are all in a DAG and are connected by paths.
- Causal-histories-in-unequivocal-closed-dags
- Some theorems about causal histories in
unequivocal, backward-closed DAGs.
- Dag-predecessor-quorum-p
- Check if the total stake of the precedessor certificates
of each certificate in a DAG at a round later than 1 is non-zero and
at least the quorum of the active committee at the previous round.
- Path-to-previous
- In an unequivocal DAG,
there is always a path between a certificate
and each of its predecessors.
- Dag-has-committees-p
- Check if the active committee
at the round of every certificate in a DAG
can be calculated from a given blockchain.
- Path-to-author+round-set-to-path-to-author+round
- In an unequivocal DAG,
if a certificate has a path to an author and round,
then any set including the certificate
has a path to that author and round,
and it results in the same certificate.
- Dag-closedp
- Check if a DAG is backward-closed.
- Path-to-author+round-transitive
- Transitivity of DAG paths.
- Path-to-author+round-to-cert-with-author+round
- If a certificate in an unequivocal DAG
has a path to a certain author and round,
the path ends up at the certificate retrieved
via that author and round.
- In-of-certificate-causal-history
- Characterization of the members of a certificate's causal history.
- Path-to-predecessor
- There is a path from a certificate
to each of its predecessors.
- Path-from-successor
- In an unequivocal DAG,
there is a path to a certificate
from each of its successors.
- Certificate-causal-history-subset-when-path
- In an unequivocal DAG, if there is a path between two certificates,
the causal history of the destination of the path is a subset of
the causal history of the source of the path.
- Path-to-head-of-predecessors
- There is a path from a certificate to
the first of its predecessors,
assuming that it has predecessors.
- Dag-no-prodecessors-round-1-p
- Check if each certificate in round 1 of a DAG
has no predecessors.
