Initialization
Initial states of the AleoBFT labeled state transition system.
There are multiple possible initial states of the system.
We introduce operations to calculate the initial states
(from suitable inputs),
and predicates to characterize the possible initial states.
Subtopics
- System-init
- Initial system state.
- Validator-init
- Initial (correct) validator state.
- Validators-state-initp
- Check if the states of a collection of validators is initial.
- System-state-initp
- Check if a system state is initial.
- System-init-loop2
- System-init-loop1
