Last-anchor-present
Invariant that the last committed round, if non-zero,
has an anchor certificate.
Initially the last committed round is 0, so the invariant trivially holds.
The only kind of event that modifies the last committed round
is commit, which is conditioned under the fact that
there is a certificate anchor for the new last committed round;
see commit-possiblep.
The other events do not change the last committed round,
and certificates are never removed from the DAG,
so if there was an anchor at the last committed round before the event,
there is still one after the event.
Subtopics
- Last-anchor-present-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Last-anchor-present-p
- Definition of the invariant:
for each correct validator,
if the last committed round is not 0,
there is an anchor at that round.
- Last-anchor-present-p-when-init
- Establishment of the invariant:
the invariant holds in any initial state.
- Last-anchor-present-p-of-events-next
- Preservation of the invariant by multiple transitions.
- Last-anchor-present-p-when-reachable
- The invariant holds in every reachable state.
