Correctness
Correctness proofs of the AleoBFT labeled state transition system.
We formulate and prove a number of properties of the protocol,
culminating in the main property that we are interested in,
namely the non-forking of blockchains.
We formulate the correctness properties of AleoBFT
mainly as state invariants, which we show
to hold in the initial states
to be preserved by state transitions,
and to hold in every state reachable from an initial state.
Subtopics
- Unequivocal-dags-def-and-init
- Invariant that DAGs are unequivocal:
definition and establishment.
- Same-committees-def-and-implied
- Invariant that correct validators calculate the same committees:
definition, and proof that it is implied by other invariants.
- Dag-omni-paths
- Property that certain certificates in DAGs
are reachable from all the certificates in later rounds,
also in different DAGs.
- Signer-records
- Invariant that each correct signer of each certificate
has a record of the certificate.
- Unequivocal-dags-next
- Invariant that DAGs are unequivocal:
preservation.
- Quorum-intersection
- Quorum intersection.
- Dag-previous-quorum-def-and-init-and-next
- Invariant that each certificate in a DAG
has references to previous certificates
that form a non-zero quorum in the committee for the previous round,
unless the round is 1,
in which case there are no references to previous certificates:
definition, establishment, and preservation.
- Unequivocal-signed-certificates
- Invariant that
the certificates signed by a correct validator are unequivocal.
- Signed-previous-quorum
- Invariant that each certificate signed by a correct validator
has references to previous certificates
that form a non-zero quorum in the committee for the previous round,
as calculated by that signing validator,
unless the round is 1,
in which case there are no references to previous certificates.
- Nonforking-anchors-def-and-init-and-next
- Invariant that committed anchors do not fork:
definition, establishment, and preservation.
- Successor-predecessor-intersection
- Intersection of successors and predecessors.
- Fault-tolerance
- Fault tolerance.
- Last-anchor-voters-def-and-init-and-next
- Invariant that the last committed anchor
has at least a certain stake of successors:
definition, establishment, and preservation.
- Signer-quorum
- Invariant that each certificate in the DAG of a validator
has signers that form a quorum in the committee.
- Committed-redundant-def-and-init-and-next
- Invariant that the set of committed certificates is redundant:
definition, establishment, and preservation.
- Nonforking-blockchains-def-and-init
- Invariant that blockchains do not fork:
definition and establishment.
- Blockchain-redundant-def-and-init-and-next
- Invariant that the blockchain is redundant:
definition, establishment, and preservation.
- No-self-endorsed
- Invariant that the recorded author-round pairs
of endorsed certificates are from other validators.
- Last-anchor-present
- Invariant that the last committed round, if non-zero,
has an anchor certificate.
- Anchors-extension
- Extension of anchor sequences.
- Nonforking-blockchains-next
- Invariant that blockchains do not fork:
preservation.
- Backward-closure
- Invariant that DAGs are backward-closed.
- Last-blockchain-round
- Invariant that the last round in the blockchain of a validator
is the last committed round of the validator.
- Dag-certificate-next
- Invariant that retrieving an existing certificate from a DAG
always returns the same result under all transitions.
- Omni-paths-def-and-implied
- Invariant that the last committed anchor in a validator
is also present and reachable from later certificates
in any validator:
definition, and proof that it is implied by other invariants.
- Ordered-blockchain
- Invariant that blocks in validators' blockchains
have strictly increasing, even round numbers.
- Simultaneous-induction
- Proof by simultaneous induction for certain invariants.
- System-certificates
- Certificates in the system.
- Last-anchor-def-and-init
- Last anchor committed by a validator:
definition and initial result.
- Last-anchor-next
- Last anchor committed by a validator:
how events change the result.
- Dag-previous-quorum
- Invariant that each certificate in a DAG
has references to previous certificates
that form a non-zero quorum in the committee for the previous round,
unless the round is 1,
in which case there are no references to previous certificates:
proof that it holds in every reachable state.
- Signed-certificates
- Certificates signed by validators.
- Committed-anchor-sequences
- Sequences of anchors committed by validators.
- Omni-paths
- Invariant that the last committed anchor in a validator
is also present and reachable from later certificates
in any validator:
proof that it holds in every reachable state.
- Last-anchor-voters
- Invariant that the last committed anchor
has at least a certain number of successors:
proof that it holds in every reachable state.
- Unequivocal-dags
- Invariant that DAGs are unequivocal:
proof that it holds in every reachable state.
- Nonforking-blockchains
- Invariant that blockchains do not fork:
proof that it holds in every reachable state.
- Nonforking-anchors
- Invariant that committed anchors do not fork:
proof that it holds in every reachable state.
- Committed-redundant
- Invariant that the set of committed certificates is redundant:
proof that it holds in every reachable state.
- Same-committees
- Invariant that correct validators calculate the same committees:
proof that it holds in every reachable state.
- Blockchain-redundant
- Invariant that the blockchain is redundant:
proof that it holds in every reachable state.
