		Search-engine friendly clone of the ACL2 documentation.

Transitions

Transitions-create

Transitions for certificate creation.

Here we define the system state transitions caused by create 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 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 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-signer-possiblep: Check if a certificate creation event is possible, from the point of view of a correct signer.
Create-next: New system state resulting from a create event.
Create-endorsers-next: Update, in a system state, to a certificate's endorsers' states resulting from a create event.
Create-endorsers-possiblep: Check if a certificate creation event is possible, from the point of view of all the certificate's endorsers.
Create-author-possiblep: Check if a certificate creation event is possible, from the point of view of a correct author.
Create-possiblep: Check if a certificate creation event is possible.
Create-endorser-possiblep: Check if a certificate creation event is possible, from the point of view of a correct endorser.
Create-endorser-next: New correct endorser state resulting from a create event.
Create-author-next: New correct author state resulting from a create event.