|
|
|---|
|
|
|
|---|
Transitions of the AleoBFT labeled state transition system.
We define predicates that say which events are possible in which states, and functions that say, for such combinations of events and states, which new states the events lead to. In other words, we define the transitions of the state transition system that models AleoBFT.
Both the predicates and the functions are mostly executable; they only use a few constrained functions. This means that, given an initial state and a list of events, it is possible to simulate the execution of the system in ACL2 by running each event in turn, starting with the initial state; all of this, assuming executable attachments for the constrained functions. The execution is not necessarily fast, because the definition of the labeled state transition system prioritizes clarity over efficiency.