Signer-records
Invariant that each correct signer of each certificate
has a record of the certificate.
A signer of a certificate is either the author or an endorser.
The author adds the certificate to its DAG as it creates the certificate,
as defined in the transitions for create,
so it has a record of the certificate.
As also defined in the transitions for create,
an endorser adds the certificate's author and round
to the set of endorsed pairs,
which also constitutes a record of the certificate.
Certificate creation also broadcasts the certificate to endorsers
(as well as to other correct validators, except the author),
so an endorser may receive the whole certificate at some point,
via an accept event,
which removes the author-round pair from the endorsed set,
but which adds the whole certificate to the DAG,
so the validator still has a record of the certificate.
Certificates are never removed by other events.
Thus, both in the case of the author and in the case of an endorser,
the signer in question always has a record of the certificate,
in its own validator state, in two possible forms:
in the DAG (the whole certificate),
or in the set of endorsed pairs (just author and round).
It may be tempting to formalize the notion of
`a signer having a record of a certificate'
as the disjunction of
(i) the certificate is in the DAG of the signer, or
(ii) the author and round of the certificate form a pair
in the set of endorsed pairs of the signer.
However, this would not be quite preserved by accept events.
The validator receiving a certificate C
and storing it in the DAG
could already have a record of a certificate C0,
different from C but with the same author and round,
i.e. C.author = C0.author and C.round = C0.round.
This cannot happen because of non-equivocation,
but this property is not yet available
at this point of this formal development,
and in fact we need to use the notion of signer records
to prove non-equivocation, so we cannot assume it here.
The problem is that, upon storing a received C into the DAG,
if the record of C0 is in the set of endorsed pairs,
and not in the DAG,
the pair of the common author and round is removed from the set,
and thus the validator no longer has a record of C0
in the sense defined by the tempting definition above,
although it now has a record of C.
So we need to weaken the notion of
`a signer having a record of a certificate C'
to the disjunction of
(i) the DAG of the signer has some certificate C'
(the same as C or not)
with the author and round of C,
(ii) the author and round of C form a pair
in the set of endorsed pairs of the signer.
That is, the notion is only about the author and signer,
not the whole certificate.
This is the formulation we define and prove here.
Subtopics
- Signer-records-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Signer-record-p
- Check if (the state of) a signer has
a record of a certificate author and round.
- Signer-records-p
- Definition of the invariant:
for every certificate signed by a correct validator,
the validator has a record of that certificate.
- Signer-records-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
- Signer-records-p-when-reachable
- The invariant holds in every reachable state.
- Signer-records-p-of-events-next
- Preservation of the invariant by multiple transitions.
