Ordered-blockchain
Invariant that blocks in validators' blockchains
have strictly increasing, even round numbers.
Blocks are committed in even rounds,
so all the block round numbers are even.
Furthermore, blocks are committed as rounds increase,
so blocks have strictly increasing round numbers in the blockchain.
Subtopics
- Ordered-blockchain-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Ordered-blockchain-p
- Definition of the invariant:
the blockchain of every correct validator has
strictly increasing, even round numbers.
- Ordered-blockchain-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
- Ordered-blockchain-p-of-events-next
- Preservation of the invariant by multiple transitions.
- Ordered-blockchain-p-when-reachable
- The invariant holds in every reachable state.
