Correctness proof for the Hashgraph Consensus algorithm, formalized in Coq.
A formalization of The Swirlds Hashgraph Consensus Algorithm: Fair,
Fast, Byzantine Fault Tolerance, by Leemon Baird. Formalized in Coq
by Karl Crary, using some insights arising from an earlier,
partial formalization by Gregory Malecha and Ryan Wisnesky.
Build Instructions
The development is self-contained and should build without
modification using Coq version 8.8.0. Just run make.
Theorems
All theorems, lemmas, definitions, and axioms are listed in the codoq index.
Libraries (in dependency order)
- Order.v: The consensus order. Events from honest peers eventually appear in the order. Once an event is placed in the order, its predecessors are determined permanently.
- Received.v: Unique famous witnesses and round received. The round received is defined, immutable, and eventually computable by every peer.
- Famous.v: Famous witnesses exist, and no late-arriving event can be famous.
- Consensus.v: Consensus is eventually achieved on the fame of every witness.
- Decision.v: Decisions. Decisions are consistent and propagate everywhere.
- Vote.v: Voting. Votes are consistent.
- Progress.v: The algorithm continues to advance in round.
- Round.v: Rounds created and witnesses.
- Sees.v: Sees and strongly-sees. The strongly seeing lemma.
- HashgraphFacts.v: Basic facts regarding hashgraphs.
- Hashgraph.v: The types and axioms that underlie the Hashgraph algorithm.
- Median.v: The definition of median, and lemmas regarding it.
- Majority.v: Majorities and supermajorities of finite sets.
- Calculate.v: Useful arithmetic facts.
- Cardinality.v: Cardinality of finite sets.
- Decide.v: Definitions and lemmas regarding decidability.
- Relation.v: Definitions and lemmas regarding relations.
- Tact.v: Tactics used by the development.