Transitions-create-certificate
Transitions for certificate creation.
Here we define the system state transitions
caused by create-certificate events.
In AleoBFT, certificates are created through an exchange of messages
involving proposals, signatures, and certificates,
following the Narwhal protocol, which AleoBFT is based on.
Currently we model certificate creation as an atomic event,
which abstracts the aforementioned message exchange process.
Our create-certificate event ``instantly'' creates a certificates,
and broadcasts it to the other validators.
This can be thought of as modeling the final act of
the aforementioned message exchange,
namely the creation and broadcasting of the certificates
after proposals and signatures have been exchanged,
with the exchange of proposals and signatures
not being explicitly modeled.
Modeling certificate creation as an atomic event
on the one hand simplifies things,
because there are fewer events and messages to consider,
but on the other hand makes the definition of
the certificate creation transitions slightlly more complicated,
because we need to model things related to
not only the actual certificate creation,
but also the (implicit) exchange of proposals and signatures.
This modeling of certificate creation is not ideal, but adequate for now.
We plan to develop, in the future, a model of AleoBFT that explicates
the exchange of proposals, signatures, and certificates.
Because of this atomic modeling of certificate creation,
a certificate creation transition involves multiple validators,
namely author and endorsers;
it also involves the network component of the system state.
In contrast, all other events involve just one validator.
Subtopics
- Create-certificate-signer-possiblep
- Check if a certificate creation event is possible,
from the point of view of a correct signer.
- Create-certificate-next
- New system state resulting from a create-certificate event.
- Create-certificate-endorsers-next
- Update, in a system state, to a certificate's endorsers' states
resulting from a create-certificate event.
- Create-certificate-endorsers-possiblep
- Check if a certificate creation event is possible,
from the point of view of all the certificate's endorsers.
- Create-certificate-author-possiblep
- Check if a certificate creation event is possible,
from the point of view of a correct author.
- Create-certificate-endorser-possiblep
- Check if a certificate creation event is possible,
from the point of view of a correct endorser.
- Create-certificate-possiblep
- Check if a certificate creation event is possible.
- Create-certificate-endorser-next
- New correct endorser state
resulting from a create-certificate event.
- Create-certificate-author-next
- New correct author state
resulting from a create-certificate event.
