|
|
|---|
|
|
|
|---|
Transitions for round advancement.
Here we define the system state transitions
caused by
A round advancement event involves just one correct validator.
This is not the only event that advances the round:
see transitions-store,
where the round may advance to catch up a validator to others.
However,
Our current modeling of certificate creation as an atomic event interferes with properly modeling certain aspects of round advancement. For instance, it would be reasonable to allow a validator to advance round after it has created a proposal but before it creates the ceritifcate, if we had a more detailed model with explicit proposals and signatures; after the round has advanced, it would be possible for the validator to receive enough signatures and to create a certificate, which would be for the round of the proposal, and not the current round (which has advanced). Alternatively, we could relax the requirement that certificate creation must happen for the current round (in create-possiblep). But for now we do not worry about these aspects, because they do not affect the properties that we are proving in the short term, mainly blockchain non-forking. The exact details of round advancement need further study.
A round advancement event does not involve the network.