|
|
|---|
|
|
|
|---|
Initial states of the AleoBFT labeled state transition system.
There are multiple possible initial states of the system, corresponding to different choices of (the addresses of) the correct validators in the system, and of the genesis committee. Recall that faulty validators are not modeled explicitly in the system state, except for the presence, in some components of the system state, of some addresses of faulty validators (e.g. the authors of some certificates).
As explained in committees, the genesis committee is modeled via a constrained nullary function, namely genesis-committee.
We could have similarly introduced a constrained nullary function that returns the set of addresses of the correct validators, which are also arbitrary, but fixed during the execution of the protocol. Then we could have formalized system states a little differently, using just a map from validator addresses to validator states, and constraining the keys of the map to be the set of correct validator addresses returned by the nullary function. But we prefer the current formulation, without the two nullary function, and with a system state containing an unconstrained map from addresses to validator states, because this is more natural for a future version of the model in which, instead of having a fixed collection of all possible (correct) validators, we actually have validators coming into and going out of existence, i.e. being added to and removed from the map in the system state.
There is a unique possible initial state of an individual (correct) validator, which we therefore formalize via a defined nullary function that returns that initial state.
We introduce a predicate that characterizes all the possible initial states of the system.
We also introduce a function that, given a sets of addresses for correct validators, constructs the initial system state with those validators. This is not necessary to define the labeled transition system, for which the predicate described in the previous paragraph suffices. However, this function may be useful to simulate the system: given the inputs to this functions and a list of events, we can calculate the initial state and the successive states that the system goes through by way of those events.