|
|
|---|
|
|
|
|---|
Transitions for certificate receipt.
Here we define the system state transitions
caused by
As defined in system-states, the network contains a set of messages, each of which consists of a certificate and a recipient address. The receipt of a certificate is modeled by removing the message from the network and adding the certificate to the validator's buffer.
As also mentioned in create-endorser-possiblep,
nothing prevents a
A message may be received by any validator in the system, not only validators in the current committee. The rationale for this modeling approach is explained in create-next.
The reason for putting the certificate into the buffer,
and not into the DAG, is to ensure that DAGs are backward-closed.
A certificate is moved from the buffer to the DAG
only after all the predecessor certificates referenced by the certificate
are already in the DAG.
An AleoBFT implementation would normally actively request
those certificates from other validators.
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.
The move of certificates from buffers to DAGs
is modeled via
Certificate receipt 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 receipt involves just one validator.