Invariant-unequivocal-certificates
Invariant that certificates have unique author and round.
This is a critical property of AleoBFT:
each certificate is uniquely identified by its author and round,
i.e. no two distinct certificates may have the same author and round.
Given the separately proved invariant that validators have the same certificates, it suffices to prove this property for
the set of certificates of a single validator,
since it is the same set for all validators.
The intuitive argument is that
each certificate is signed (authored and endorsed)
by a quorum of validators.
In order for two different certificates with the same author and round
to exist,
a quorum n - F of validators must have signed both.
But since there are only n validators,
the intersection of any two sets of n - F validators
has at least F + 1 validators,
and therefore there is at least one correct validator in that set.
But a correct validator would not have signed two different certificates
with the same author and round.
Turning the above intuitive argument into an ACL2 proof
takes a bit of work, explained below as we develop the proof.
New certificates are created only by create-certificate events,
so it suffices to prove that each such new certificate
must have different author or round from all the existing ones.
This involves showing that,
if the new certificate has the same author and round
as an existing certificate,
then the create-certificate is actually not possible,
because it requires some correct validator to
both have signed the old one,
and thus having a record of that author-round pair,
and have not signed the new one yet,
and thus not having a record of that same author-round pair,
which is an impossibility.
For the other kinds of events, the proof is easy,
because no new certificates are created.
Subtopics
- System-unequivocal-certificates-p-of-create-certificate-next
- Preservation of the invariant by create-certificate events.
- System-unequivocal-certificates-p
- Definition of the invariant:
if any two certificates have the same author and round,
they are the same certificate.
- System-unequivocal-certificates-p-of-event-next
- Preservation of the invariant by all events.
- System-unequivocal-certificates-p-of-store-certificate-next
- Preservation of the invariant by store-certificate events.
- System-unequivocal-certificates-p-of-receive-certificate-next
- Preservation of the invariant by receive-certificate events.
- System-unequivocal-certificates-p-of-timer-expires-next
- Preservation of the invariant by timer-expires events.
- System-unequivocal-certificates-p-of-commit-anchors-next
- Preservation of the invariant by commit-anchors events.
- System-unequivocal-certificates-p-of-advance-round-next
- Preservation of the invariant by advance-round events.
- System-unequivocal-certificates-p-when-system-state-initp
- Estalishment of the invariant:
the invariant holds on any initial system state.