|
|
|---|
|
|
|
|---|
Invariant that retrieving an existing certificate from a DAG always returns the same result under all transitions.
This is a transition invariant, instead of a state invariant. It says that if a certificate with a given author and round can be retrieved from the DAG of a correct validator, then it can be still retrieved, yielding the same result, as the validator changes state via events. That is, certificate retrieval is ``stable'' under state changes.
A critical assumption is that certificates are unequivocal. This transition invariant is based on properties of retrieval operations on unequivocal DAGs, which here we lift to (validators in) the system.