Last-anchor-voters-def-and-init-and-next
Invariant that the last committed anchor
has at least a certain stake of successors:
definition, establishment, and preservation.
When the last committed round is not 0,
there is always an anchor at that round:
see last-anchor-present.
Furthermore, that anchor always has successors
whose total stake is more than f,
where f is introduced in max-faulty-for-total.
This total stake provides the votes
that are in fact necessary to commit that anchor.
Initially the last committed round is 0,
so the invariant holds trivially.
The only kind of events that changes the last committed anchor
is commit, whose preconditions establish the invariant.
The only kinds of events that may change the successors
are create and accept,
which may add a certificate to the DAG:
the added certificate may or may not be a successor,
but if it is, it can only increase the voting stake, never decrease it.
Here we define the invariant,
we prove that it holds in all initial states,
and we prove that it is preserved by all transitions.
Elsewhere we prove that
the invariant holds in every reachable state.
Subtopics
- Last-anchor-voters-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Validator-last-anchor-voters-p
- Check if a validator state satisfies the invariant.
- Last-anchor-voters-p
- Definition of the invariant:
for each correct validator,
if the last committed round is not 0,
the last committed anchor has at least f+1 successors,
where f is the maximum number of faulty validators
in the committee active at
the round just after the last committed one.
- Last-anchor-voters-p-when-init
- Establishment of the invariant:
the invariant holds in any initial state.
