Last-blockchain-round
Invariant that the last round in the blockchain of a validator
is the last committed round of the validator.
The last component of a validator state stores the last committed round number,
or 0 if no block has been committed yet.
Initially, there are no blocks and last is 0.
When new blocks are committed,
which only happens with commit-anchors events,
last gets updated with the round number of
the last (i.e. newest) block added to the blockchain.
Subtopics
- Last-blockchain-round-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Last-blockchain-round-p
- Definition of the invariant:
for each correct validator in the system,
the last committed round is 0 if the blockchain is empty,
or the round of the newest block in the blockchain otherwise.
- Last-blockchain-round-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- Last-blockchain-round-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
