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 voting stake from the 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.
- Pick-successor/predecessor-properties
- Key properties of pick-successor/predecessor.
- Not-empty-successor-predecessor-author-intersection
- Non-empty intersection of successor and predecessor authors.
- Not-empty-successor-predecessor-intersection
- Non-empty intersection of successors and predecessors
- Successors+predecessors-same-round
- Successors and predecessors have all the same round.
