|
|
|---|
|
|
|
|---|
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 a map from validator addresses to validator states (see validators-state), and a set of messages that models the state of the network (see message for a rationale of this model of the network). As explained in validators-state, we only capture the state of correct validators.
As explained in system-states, the validators are all the possible ones, in the genesis committe as well as any future committee. 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 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.