Dag-omni-paths
Property that certain certificates in DAGs
are reachable from all certificates in later rounds,
also in separate DAGs.
This is a core property of AleoBFT.
Take an anchor A (or any certificate, for that matter) in a DAG,
with at least f+1 votes
(where f is introduced in max-faulty-for-total),
i.e. at least f+1 successors in the round just after A.
Then if there is a(ny) certificate C two rounds after A,
it must have n-f predecessors in the round just before,
which is the round just after A.
Since there can be at most n certificates in that round
(the one just after A and just before C),
the intersection argument in successor-predecessor-intersection
shows that there must be a certificate B between A and C.
That is, there is a path from C to A.
The above holds for every C two rounds after A.
Any certificate D in the round after C
must have predecessors in the previous round,
which, as argued, all have paths to A,
and therefore every D has a path to A as well.
Thus, every certificate at least two rounds after A
has a path to A.
The above has been explained for one DAG,
because it is easier to understand,
but it also holds across two DAGs of possibly different validators.
Given a certificate (anchor) A in DAG 1 at round r,
with at least f+1 voters for A in DAG 1 at round r+1,
and n-f predecessors in DAG 2 at round r+1,
every certificate C in DAG 2 at round r+2 or later
has a path to A, which must be also in DAG 2.
The reason is that there must be a certificate B
that is both in the f+1 or more voters in DAG 1
and in the n-f certificates in DAG 2.
In DAG 1, it has an edge to A.
Because of the backward closure of DAG 2,
A must be in DAG 2 too, with an edge to it from B.
Since B is a predecessor of C,
there is a path from C to A.
This holds for every C in DAG 2 in round r+2,
so every D in DAG 2 at round r+3
has a predecessor C with a path to A
and so D has a path to A too.
And so on for the rest of the rounds of DAG2.
Here we formulate and prove this core property, for two DAGs.
We do not need to talk about anchors specifically,
because A can be any certificate, not necessarily at an even round,
so long as it has at least f+1 successors.
Subtopics
- Dag-omni-paths-round-p-of-next-round
- Preservation of dag-omni-paths-round-p
from one round to the next.
- Dag-omni-paths-p
- Check if all the certificates
that are at least two rounds after a given certificate
have a path to that certificate.
- Dag-omni-paths-round-p
- Check if all the certificates at a certain round
that is at least two rounds after a given certificate
have a path to that certificate.
- Path-from-common-to-cert1-in-dag2
- There is a path in dag2
from the common certificate in the intersection
to cert1 in dag1,
which is also in dag2.
- Dag-omni-paths-rounds-p
- Check if dag-omni-paths-rounds-p holds for all rounds
that are at least two rounds after the given certificate.
- Dag-omni-paths-round-p-base-case
- Base case of our proof by induction.
- Path-from-cert2-to-cert1-in-dag2
- There is a path in dag2 from cert2 to cert1.
- Dag-omni-paths-round-p-step-case
- Step case of our proof by induction.
- Dag-omni-paths-round-p-of-round-delta
- Induction proof.
- Dag-omni-paths-p-holds
- Proof that dag-omni-paths-p holds.
- Dag-omni-paths-round-p-holds
- Proof that dag-omni-paths-round-p holds
for every round r \geq a+2.
