|
|
|---|
|
|
|
|---|
Fixtype of messages.
This is a product type introduced by fty::defprod.
We model a message as consisting of a certificate and a destination address. Note that the certificate includes the author's address, which is the sender's address. This fulfills the authentication assumption of network communication.
As formalized in the state transitions, when a validator broadcasts a certificate, messages with that certificate and different destinations are added to our model of the network. As separate events, messages are removed from the network and delivered to the destination validators, one at a time.