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 the certificates book.
By `DAG-specific' we mean those operations 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 the certificates book 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.
- 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-cardinality-p
- Check if the number of precedessor certificates
of each certificate in a DAG
is 0 if the certificate's round is 1
or the quorum of the active committee at the previous round
if the certificate's round is not 1.
- Dag-rounds-in-committees-p
- Check if the (one or more) authors of
the certificates in each round of a DAG
are members of the active committee at that round.
- Path-to-previous
- In an unequivocal DAG,
there is always a path between a certificate
and each of its predecessors.
- 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-committees-p
- Check if the active committee
at the round of every certificate in a DAG
can be calculated from a given blockchain.
- Dag-closedp
- Check if a DAG is backward-closed.
- Path-to-author+round-transitive
- Transitivity of DAG paths.
- Path-to-author+round-to-certificate-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.
