Properties-dags
Some properties of the operations on DAGs.
Some of these come in two forms,
analogous to the ones described in properties-certificate-retrieval:
one form about the consistency of the growing DAG of a single validator,
and one form about the consistency across DAGs of different validators.
In fact, the proofs of these theorems about DAGs
make use of those theorems about certificate retrieval.
Besides the ones mentioned just above,
there are also other properties proved here,
which do not come in pairs like that.
Subtopics
- Certificate-causal-history-of-unequivocal-dag-superset
- The causal history of a certificate
in a backward-closed subset of an unequivocal DAG
is the same in the superset.
- Previous-certificates-of-unequivocal-dags
- The predecessor certificates of a common certificate
of two backward-closed unequivocal and mutually unequivocal DAGs
are the same in the two DAGs.
- Previous-certificates-of-unequivocal-dag-superset
- The predecessor cerfificates of a certificate
in a backward-closed subset of a DAG of unequivocal certificates
are the same in the superset.
- Path-to-author+round-of-unequivocal-dag-superset
- The paths from a certificate
in a backward-closed subset of a DAG of unequivocal certificates
are the same in the superset.
- 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
- 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,
assuming the DAG is unequivocal.
- Certificate-causal-history-of-unequivocal-dags
- The causal histories of a common certificate
of two backward-closed unequivocal and mutually unequivocal DAGs
are the same in the two DAGs.
- Path-to-author+round-of-unequivocal-dags
- The paths from a common certificate
of two backward-closed unequivocal and mutually unequivocal DAGs
are the same in the two DAGs.
- 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.
- Certificate-with-author+round-when-path-to-author+round
- If there is a path from a certificate in an unequivocal DAG
then retrieving a certificate with that author and round
results in a certificate.
- Dag-previous-in-dag-p-of-intersect
- Intersecting two unequivocal backward-closed DAGs
yields a backward-closed DAG.
- Cardinality-of-outgoing-quorum
- In a backward-closed unequivocal DAG
whose certificates have a given number of precedessors,
the number of outgoing certificates is equal to that number.
- 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-outgoing
- There is a path from a certificate
to each of its outgoing certificates.
- Path-from-incoming
- There is a path to a certificate
from each of its incoming certificates.
- Cardinality-of-incoming-to-tally-leader-votes
- Relation between the number of incoming certificates
and the number of `yes' votes to the certificate.
