No-self-messages
Invariant that messages are never self-addressed.
Messages come into existence only due to create-certificate events.
If the author is a correct validator,
the certificate is broadcast to all the other correct validators,
while it is immediately added to the author's DAG;
the validator does not send a message to itself.
If the author is a faulty validator,
the certificate is broadcast to all the correct validators,
and to no faulty validator;
thus in particular the validator does not send the message to itself.
Either way, messages are never self-addressed:
the destination always differ from the sender,
i.e. the certificate's author.
Subtopics
- No-self-messages-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Message-set-noselfp
- Check that all the messages in a set are not self-addressed.
- No-self-messages-p
- Definition of the invariant:
all the messages in the network are not self-addressed.
- Message-noselfp
- Check that a message is not self-addressed.
- No-self-messages-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- No-self-messages-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
