		Search-engine friendly clone of the ACL2 documentation.

Correctness

Backward-closure

Invariant that DAGs are backward-closed.

A validator's DAG is extended via two kinds of events, namely create-certificate and store-certificate.

The first kind of event may only occur if the certificate's author has all the previous certificates in its DAG.

The second kind of event may only occur if the DAG has all the previous certificates. 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.