Backward-closure
Invariant that DAGs are backward-closed.
A validator's DAG is extended via two kinds of events,
namely create and store.
A create event may only occur if
the certificate's author has all the previous certificates in its DAG.
A store event may only occur if
the DAG has all the previous certificates as well.
Under that condition, the certificate is moved from the buffer to the DAG.
In fact, the purpose of the buffer is to wait
until all the previous certificates are in the DAG,
since they may be coming out of order with respect to round numbers.
This means that DAGs are always backward-closed:
there are no dangling edges.
Recall that edges always point backwards
(from a round to the round just before it),
which justifies the `backward' in `backward-closed'.
Subtopics
- Backward-closed-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Backward-closed-p
- Definition of the invariant:
the DAG of each correct validator is backward-closed.
- Backward-closed-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- Backward-closed-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
