|
|
|---|
|
|
|
|---|
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 and faulty validators in the system, and of the genesis committee.
As explained in committees, the genesis committee is modeled via a constrained nullary function.
We could have similarly introduced two constrained nullary functions that return the set of addresses of the correct validators and the set of addresses of the faulty 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 functions, and with a system state containing a map from addresses to optional 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 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 this initial state.
We introduce a predicate that characterizes all the possible initial states of the system. This predicate refers to the nullary function for the genesis committee, to ensure that the commitee is part of the validators.
We also introduce a function that, given two sets of disjoint addresses, one for correct validators and one for faulty ones, 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.