Fixtype of states of a collection of validators.
This map captures the state of all the validators in the system, which in this model form a fixed committee. The (unchanging) addresses are captured in the keys of the map, while the changeable states are the values of the map. The set of keys of this map does not change, because the committee is fixed.
Since faulty validators may do almost arbitrary things
(short of breaking cryptography,
along with other well-defined and well-motivated restrictions),
there is no need to actually model their internal states.
So we use
A basic assumption in our model is that a validator is either always correct or not. If not, it is considered faulty, no matter how small its deviation from correct behavior. In practice, this corresponds to a validator either running snarkOS or not; whether snarkOS correctly implements AleoBFT is a separate problem.