The Giskard consensus protocol is used to validate transactions and computations in the PlatON network. This project provides a model of Giskard in Coq, and formally proves several key safety properties of the protocol.
- License: University of Illinois/NCSA Open Source License
- Compatible Coq versions: 8.10 or later
- Coq namespace:
Giskard
We recommend installing Coq 8.16 via OPAM:
opam install coq.8.16.0When Coq is installed, use the following commands to obtain and build the project:
git clone https://github.com/runtimeverification/giskard-verification.git
cd giskard-verification
make # or make -j <number-of-cores-on-your-machine>This will build all model definitions and check all the proofs.
An overview of the Giskard protocol is provided as part of the PlatON Consensus Solution documentation. The Coq formalization is based on a more abstract specification of the protocol.
The Coq protocol model aims to capture safety properties of Giskard, and thus omits many implementation-level details such as on verifiable random functions. For details on the model and the safety proofs, see the report:
Verifying Safety of the Giskard Consensus Protocol in Coq
All Coq code is in the theories directory and is organized as follows:
lib.v: supplementary general tactics and resultsstructures.v: definitions of Giskard datatypes and axiomslocal.v: local state operations, properties, and transitionsglobal.v: global state operations, transitions, and propertiesprepare.v: safety property one, prepare stage height injectivityprecommit.v: safety property two, precommit stage height injectivitycommit.v: safety property three, commit stage height injectivity
HTML documentation can be generated using coqdoc by running the following
command in the repository root:
make coqdoc
Then, a good entry point for your browser is docs/coqdoc/toc.html.