Awesome

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.

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:

<img src="resources/pdf-icon.png" alt="PDF" width="20" /> 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.