|
|
|---|
|
|
|
|---|
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 ``nearly'' executable. There are three constrained functions whose details are not needed for the proofs: genesis-committee, leader-at-round, and lookback. These functions would need to have executable attachments for the transition predicates and functions to be executable in the theorem prover. Once this is done, given an initial state and a list of events, it will be possible to simulate the execution of the system in ACL2 by running each event in turn, starting with the initial state. The execution will not necessarily be fast, because the definition of the labeled state transition system prioritizes clarity over efficiency.