		Search-engine friendly clone of the ACL2 documentation.

Transitions

Transitions-accept

Transitions for certificate acceptance.

Here we define the system state transitions caused by accept events.

As defined in system-states, the network contains a set of messages, each of which consists of a certificate and a recipient address; these messages are added to the network via create events. The receipt of a certificate is modeled by removing the message from the network and adding the certificate to the validator's DAG, under suitable conditions; if these conditions are not satisfied, the message is not delivered, and stays in the network, from where it may or may not be eventually delivered, should all the conditions become true. This is why this kind of event is called accept and not receive: it involves the validator accepting, not just receiving, the certificate. This means that, in our model, the network may actually model also certain ``incoming message buffers'' of validators: in an implementation, messages are delivered to validators, and the validators may delay them, or reject them outright; in our model, these situations correspond to the messages staying in the network component of the system state.

A message may be accepted by any validator in the system, not only validators in the current committee. The rationale for this modeling approach is explained in create-next.

In order for the certificate to be accepted, all the previous certificates referenced by the certificate must be already in the DAG. This serves to preserve the backward closure of DAGs. Even though this condition may not be fulfilled at some point, it may be fulfilled in the future, after more certificates have been accepted by the validator; at that point, the certificate in question may be accepted. An AleoBFT implementation would normally actively request the missing predecessor certificates from other validators, but we keep our model simpler by not explicitly modeling that, but instead letting those certificates arrive non-deterministically, in line with our eventually reliable network model.

As also mentioned in create-endorser-possiblep, nothing prevents a create event from modeling the creation of an equivocal certificate, signed by only faulty validators. Thus, in order for the certificate to be accepted, the signers of the certificate must form a quorum in the active committee of the certificate's round. If this condition is not fulfilled at some point, it will never be fulfilled in the future, because it depends only on the certificate itself. Thus, the message will sit in the network forever. We could extend our model with events to discard that message, but that is not necessary for proving the current properties of interest.

If the certificate is accepted, and if the validator had endorsed the certificate, the author-round pair of the certificate is removed from the set of endorsed author-round pairs; see transitions-create about these pairs. This is because now the validator has the full certificate.

Certificate acceptance and certificate creation are the only events that involve the network component of the system state. All the other events involve just one validator. As explained in transitions-create, certificate creation involves multiple validators; in constract, certificate acceptance involves just one validator.

Subtopics

Accept-possiblep: Check if a certificate acceptance event is possible.
Accept-next: New system state resulting from an accept event.