Dag-omni-paths
Property that certain certificates in DAGs
are reachable from all the certificates in later rounds,
also in different DAGs.
This is a core property of AleoBFT.
Take an anchor A (or any certificate, for that matter) in a DAG,
with more than f voting stake
(where f is introduced in max-faulty-for-total),
i.e. where the total stake of successors in the round just after A
is more than f.
Then if there is a(ny) certificate C two rounds after A,
its predecessors in the round just before,
which is the same as the round just after A,
must have at least n-f total stake.
Since there can be at most n total stake in that round
(the same round that is both 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, through B.
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 more than f voting stake for A in DAG 1 at round r+1,
and at least n-f predecessor stake 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 successors of A in DAG 1
and in the predecessors of C 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,
not necessarily a leader certificate
so long as it has more than f successors' stake.
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.
