Successor-predecessor-intersection
Intersection of successors and predecessors.
This is the second key intersection argument
for the correctness of AleoBFT,
besides quorum intersection. However, this second argument is very different:
it has nothing to do with correct and faulty validators;
it only has to do with paths in DAGs.
When an anchor A at a round r
has enough votes (i.e. successors) at round r+1,
then if there is a certificate C at round r+2
then there must be a certificate B at round r+1
that is both a successor (i.e. voter) of A
and a predecessor of C.
This actually also applies across differnt DAGs:
A is in DAG 1,
C is in DAG 2,
and B is in both DAG 1 and DAG 2.
The case in which DAGs 1 and 2 are the same is a special case.
Here we prove the non-emptiness of the intersection,
and we introduce a function to pick
a common certificate from the intersection.
This is then used in further proofs.
Here we talk about successors and predecessors,
not specifically voters and anchors,
because the argument is more general.
Subtopics
- Pick-successor/predecessor
- Pick a certificate in the successor-predecessor intersection.
- Cardinality-of-successors+predecessors-bound
- Bound on the cardinality of successors and predecessors.
- Pick-successor/predecessor-properties
- Key properties of pick-successor/predecessor.
- Cardinality-of-successors+predecessors
- Relation between the number of successor and predecessor certificates
and the number of their authors.
- Cardinality-of-successor-predecessor-intersection
- Abstract form of the intersection theorem.
- Successor-predecessor-intersection-not-empty
- The intersection of successors and predecessors is not empty.
- Successors+predecessors-same-round
- Successors and predecessors have all the same round.
