No-self-buffer
Invariant that buffers of correct validators
never contain messages authored by themselves.
This is a consequence of the invariant no-self-messages.
A validator's buffer contains certificates
obtained from messages in the network,
which are never self-addresses as proved in that invariant.
Thus, any message in the buffer or a validator
is not self-authored, i.e. it is authored by another validator.
Initially all buffers are empty, so this invariant holds.
Subtopics
- No-self-buffer-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- No-self-buffer-p
- Definition of the invariant:
every certificaates in the buffer of a correct validator
is not authored by that validator.
- No-self-buffer-p-always
- The invariant holds in every state
reachable from an initial state via a sequence of events.
- No-self-buffer-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
