meta.yml

---
fullname: Giskard Verification
shortname: giskard-verification
opam_name: coq-giskard
organization: runtimeverification
community: false
action: true
dune: true

synopsis: >-
  Verified model of the Giskard consensus protocol in Coq

description: |-
  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.

authors:
- name: Elaine Li
- name: Karl Palmskog
- name: Mircea Sebe

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: University of Illinois/NCSA Open Source License
  identifier: NCSA
  file: LICENSE.md

supported_coq_versions:
  text: 8.10 or later
  opam: '{>= "8.10"}'

tested_coq_opam_versions:
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'
- version: '8.11'
- version: '8.10'

namespace: Giskard

keywords:
- name: Giskard
- name: consensus
- name: blockchain

categories:
- name: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems

build: |-
  ## Building instructions

  We recommend installing Coq 8.16 via [OPAM](http://opam.ocaml.org/doc/Install.html):
  ```shell
  opam install coq.8.16.0
  ```
  When Coq is installed, use the following commands to obtain and build the project:
  ```shell
  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.

documentation: |-
  ## Protocol

  An overview of the Giskard protocol is provided as part of the
  [PlatON Consensus Solution documentation](https://devdocs.platon.network/docs/en/PlatON_Solution/).
  The Coq formalization is based on a more abstract [specification](https://arxiv.org/abs/2010.02124)
  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](https://github.com/runtimeverification/giskard-verification/blob/master/report/report.pdf)*

  ## 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`.
---