Transitions
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.
The functions from old system states to new system states
include -val companion functions
that map old validator states to new validator states.
This factoring facilitates formal proofs of invariants,
so that validator-level invariants,
which are part of system-level invariants,
can be proved for the -val function,
making system-level invariant proofs more compositional.
Subtopics
- Events-possiblep
- Check if a sequence of events is possible.
- Events-next
- New state resulting from a sequence of events.
- Event-next
- New state resulting from an event.
- Event-possiblep
- Check if an event is possible.
- Transitions-create-certificate
- Transitions for certificate creation.
- Transitions-store-certificate
- Transitions for certificate storage.
- Transitions-receive-certificate
- Transitions for certificate receival.
- Transitions-timer-expires
- Transitions for timer expiration.
- Transitions-commit-anchors
- Transitions for anchor commitment.
- Transitions-advance-round
- Transitions for round advancement.
