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 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-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
- Last-blockchain-round-p-when-reachable
- The invariant holds in every reachable state.
- Last-blockchain-round-p-of-events-next
- Preservation of the invariant by multiple transitions.
