Correctness
Correctness proofs of our model of
AleoBFT with static committees.
We introduce some additional operations used
to formulate and prove the correctness of the protocol.
We prove a number of properties of both these additional operations
and of the operations used in the definition of
the labeled state transition system.
Many of these properties are in invariants of the system.
We start with simple ones,
and culminate into high-level properties of interest of the protocol.
The invariants are mostly state invariants,
i.e. predicates that hold in the initial state
and are preserved by every transition.
There are also some transition invariants,
i.e. predicates that hold of
each pair of old and new states linked by a transition.
Subtopics
- Invariant-unequivocal-certificates
- Invariant that certificates have unique author and round.
- Invariant-same-certificates
- Invariant that correct validators have the same set of certificates,
if messages in the network are taken into account.
- Invariant-committed-redundant
- Invariant that the set of committed certificates is redundant.
- Invariant-signers-have-author-round
- Invariant that the signers of every certificate
have a a record of the certificate's author and round.
- Property-paths-to-voted-anchor
- Property that if an anchor in a DAG has enough votes
then all the certificates in the DAG
that are at least two rounds after the anchor
have some path to the anchor.
- Properties-dags
- Some properties of the operations on DAGs.
- Invariant-no-self-endorsed
- Invariant that the recorded author-round pairs
of endorsed certificates are from other validators.
- Properties-certificate-retrieval
- Some properties of the certificate retrieval operations,
when applied to unequivocal sets of certificates.
- Invariant-last-anchor-voters
- Invariant that the last committed anchor
has a certain number of voters in the subsequent round.
- Invariant-blockchain-redundant
- Invariant that the blockchain is redundant.
- Invariant-previous-are-quorum
- Invariant that the previous certificates of every certificate
form a quorum if the round is not 1, and there are none in round 1.
- Invariant-no-self-buffer
- Invariant that the certificates in the buffer
are from different validators.
- Invariant-anchors-not-forking
- Invariant that committed anchors do not fork.
- Invariant-signers-are-validators
- Invariant that the signers of every certificate
are validators in the system.
- Invariant-previous-in-dag
- Invariant that the previous certificates
referenced by a certificate in a DAG
are also in the DAG.
- Invariant-last-before-current
- Invariant that the current round is always ahead of
the last committed round.
- Invariant-last-anchor-present
- Invariant that the last committed round, if non-zero,
has an anchor certificate.
- Properties-anchors-extension
- Properties about extending anchor sequences.
- Invariant-unequivocal-dag
- Invariant that the certificates in each DAG
have a unique combination of author and round.
- Property-paths-to-other-voted-anchor
- Property that if an anchor in a DAG has enough votes
then all the certificates in any other DAG
that are at leaast two rounds after the anchor
have some path to the anchor, which is also in the other DAG.
- Invariant-no-self-messages
- Invariant that messages are never self-addressed.
- Invariant-paths-to-other-last-anchor
- Invariant that all the certificate in a DAG
at least two rounds after the last committed anchor
of a possibly different DAG
have paths to that anchor in the first DAG.
- Invariant-addresses
- Invariant that validator addresses do not change.
- Invariant-last-is-even
- Invariant that the last committed round is always even.
- Invariant-signers-are-quorum
- Invariant that the signers of every certificate form a quorum.
- Invariant-messages-to-correct
- Invariant that messages are sent only to correct validators.
- Properties-blockchain
- Some properties of the operations on blockchains.
- Invariant-paths-to-last-anchor
- Invariant that all the certificates in a DAG
at least two rounds after the last committed anchor
have paths to that anchor.
- Invariant-unequivocal-dags
- Invariant that the certificates in two DAGs
have a unique combination of author and round.
- Invariant-blockchain-not-forking
- Invariant that blockchains do not fork.
- Operations-additional
- Additional operations on system states and their components.
- Invariant-quorum
- Invariant that the quorum number does not change.
- Invariant-dag-previous-are-quorum
- Invariant that
the previous certificates of every certificate in every DAG
form a quorum if the round is not 1, and there are none in round 1.
- Properties-anchors
- Some properties of operations on anchors.
- Property-committed-anchors-of-next-event
- How committed-anchors changes under each event.
- Property-last-anchor-of-next-event
- How last-anchor changes under each event.
- Invariant-max-faulty
- Invariant that the maximum tolerated number of faulty validators
does not change.
- Invariant-certificate-retrieval
- Invariant that the retrieval operations on existing certificates
do not change results as states change.
- Invariant-dag-authors-are-validators
- Invariant that all the authors of certificates in each DAG
are validators in the system.
- Invariant-causal-histories
- Invariant that the causal histories of existing certificates
do not change as states change.
