Giskard Verification

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.

Meta

• License: University of Illinois/NCSA Open Source License
• Compatible Coq versions: 8.10 or later
• Coq namespace: Giskard

Building instructions

We recommend installing Coq 8.16 via OPAM:

opam install coq.8.16.0

When 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.

Protocol

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.

Coq model and proofs

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

File organization

All Coq code is in the theories directory and is organized as follows:

• lib.v: supplementary general tactics and results
• structures.v: definitions of Giskard datatypes and axioms
• local.v: local state operations, properties, and transitions
• global.v: global state operations, transitions, and properties
• prepare.v: safety property one, prepare stage height injectivity
• precommit.v: safety property two, precommit stage height injectivity
• commit.v: safety property three, commit stage height injectivity

Generating documentation

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.