Module notifications 

What a notification tells a client, and what it does not.

A Notification tells a client that a chain has changed. From a correct validator it is sound — what it reports really happened — but from any validator it may simply never arrive, and it carries nothing that could be checked if it did.

The channel is lossy by model, not merely unreliable in practice, so nothing here may assume a notification arrives. That would be alarming if clients used notifications merely to go faster. They do not: a ChainListener acts on them, processing inboxes and following new chains, so an application’s own liveness can rest on one arriving.

What makes a lossy channel tolerable is that the dependence is self-repairing, in three ways that are independent of each other: a client subscribes to every validator, so one silence is covered by the rest; establishing a stream resynchronizes chain state, so a gap is closed rather than replayed; and handlers bring a chain up to date rather than applying the change they were told about, so any later notification does the work of every lost one. All three need the client to be connected to somebody.

Traits

LostNotificationsAreRepaired

Lemma (A lost notification is repaired). A client that misses a notification still reaches the state it would have reached, provided it remains connected to at least one correct validator that has the change. Three independent mechanisms do this, and none of them replays the lost message.

NotificationChannelIsLossy

Definition (The notification channel is lossy). The channel carrying Notifications from a validator to a client may drop any message, without notice to either side. Delivery is never retried, never acknowledged, and never durable.

NotificationImpliesPersistedChange

Lemma (A correct validator’s notification reports a change that is already persisted). If a client receives a Notification from a correct validator, the state change it names is in that validator’s storage. Nothing is claimed about a faulty validator’s notifications, which by CorrectValidator may report anything at all.

NotificationIsCertificateBacked

Lemma (A notification is backed by a certificate the validator can serve — except for a new round). For every notification a correct validator emits other than Reason::NewRound, that validator holds a quorum-signed certificate establishing what the notification reports, and will hand it to anyone who asks. A recipient can therefore not merely learn that something happened but verify it, and carry the evidence to other validators.