Backward-closure
Invariant that DAGs are backward-closed.
A validator's DAG is extended via two kinds of events,
namely create and accept.
A create event may only occur if
the certificate's author has all the previous certificates in its DAG.
An accept event may only occur if
the DAG has all the previous certificates as well.
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-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
- Backward-closed-p-when-reachable
- The invariant holds in every reachable state.
- Backward-closed-p-of-events-next
- Preservation of the invariant by multiple transitions.
