|
|
|---|
|
|
|
|---|
Invariant that validator addresses do not change.
The sets of the addresses of all validators, all correct validators, and all faulty validators do not change in the course of the protocol. That is, the identities of validators, and their correct vs. faulty status, remain constant during the protocol, although their internal states may obviously change.
These are transition invariants, i.e. they relate the old and new states of transitions.
The proofs are straightforward,
based on how transitions are defined.
Transitions only change validator states (the values of the map),
but never the validator addresses (the keys of the map).
Furthermore, they never change validator states into