|
|
|---|
|
|
|
|---|
Fixtype of system states.
This is a product type introduced by fty::defprod.
This fixtype captures the state of the whole system of validators, i.e. the state of the whole protocol. It consists of the state of the validators and the state of the network.
The state of the validators is captured by a map from addresses to validator states. This map captures the state of all the correct validators in the system, which, as explained in system-states, is a potentially large set of all the possible ones that could be in a committee at some point in time. 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 again these are all possible validators, not just a committee.
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, or even to include them explicitly in the state. This is why the map is only for the correct validators in the system; the faulty ones are implicit, and not explicitly part of the state. In the definition of the system transitions, we model the behavior of faulty validators in terms of nondeterministic generation of messages for other (correct) validators: this modeling approach does not require the explicit presence, in the system state, of the faulty validators. It also does not matter which messages are received by faulty validators, who can behave arbitrarily regardless of what they receive or not.
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 a correct implementation of AleoBFT or not; it is a separate problem whether the implementation is correct with respect to the specification of AleoBFT.
The network is modeled as a set of messages in transit.
As explained in system-states, the validators are all the possible ones, in the genesis committe as well as any future committee; more precisely, only the correct ones in all these committees, since the faulty ones are not explicitly represented. Note that the system state does not have any information about the current committee, because that is a notion that every validator computes on its own, based on their view of the blockchain.
The only shared state among validators is the network, which is shared in a very restricted way (as formalized by the state transitions), in terms of message sending and receiving. The rest of the system state is strictly partitioned among the validators, which communicate exclusively through network messages.